§ Intuition for limits in category theory
§ A characterization of limits
The theorem that characterizes limits is this:
A category has Finite Limits iff it has all finite products and equalizers. limits have maps out of them.
§ Ravi Vakil's intuition for limits: Take sub things.
- An element of a limit gives one of each of its ingredients. For example,, since we can geta degree n polynomial for all n, from any power series by truncation.
- limits have maps out of them.
- RAPL: right adjoints preserve limits.
- Limits commute with limits.
- These are mentioned in "Algebraic geometry in the time of Covid: Pseudolecture 2"
- Also, recalling that kernels are limits allows one to remember that we havemaps that go out of a limit.
§ Limits are things you get maps out of.
- product has projections going out of it.
gcd is less than the things that build it:
gdb(a, b) -> a, b since
gcd(a, b) < a and
gcd(a, b) < b.
- single point set can be mapped out of.
type Limit f = forall a. f a
§ Limits in Haskell
data Limit (f :: * -> *) where
MkLimit :: (forall a. f a) -> Limit f
projectOut :: Limit f -> f a
projectOut (MkLimit fa) = fa
data Colimit (f:: * -> *) where
MkCoLimit :: f a -> Colimit f
projectIn :: f a -> Colimit f
projectIn = MkCoLimit