CategoryTheory.Limits.Types.limit_ext
theorem CategoryTheory.Limits.Types.limit_ext :
∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
[inst_1 : CategoryTheory.Limits.HasLimit F] (x y : CategoryTheory.Limits.limit F),
(∀ (j : J), CategoryTheory.Limits.limit.π F j x = CategoryTheory.Limits.limit.π F j y) → x = y
The theorem `CategoryTheory.Limits.Types.limit_ext` states that for any category `J` and any functor `F` from `J` to the category of types, which has a limit, if `x` and `y` are objects in the limit of `F`, and for every object `j` in `J`, the projection from `x` to `F(j)` is the same as the projection from `y` to `F(j)`, then `x` and `y` must be equal. This theorem basically asserts the uniqueness property of limit objects in a category: any two limit objects that behave identically with respect to the morphisms defined by the functor must actually be the same object.
More concisely: In any category, if two objects in the limit of a functor have identical projections to the images of all objects in the category under the functor, then they are equal.
|
CategoryTheory.Limits.Types.jointly_surjective'
theorem CategoryTheory.Limits.Types.jointly_surjective' :
∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)}
[inst_1 : CategoryTheory.Limits.HasColimit F] (x : CategoryTheory.Limits.colimit F),
∃ j y, CategoryTheory.Limits.colimit.ι F j y = x
The theorem `CategoryTheory.Limits.Types.jointly_surjective'` states that for any category `J`, any functor `F` from `J` to the category of types, and any `x` in the colimit of `F` (provided this colimit exists), there exists an object `j` of `J` and an element `y` of the type `F` maps `j` to, such that the coprojection from `j` to the colimit of `F` applied to `y` gives `x`. In other words, every element in the colimit of a functor can be 'reached' by the coprojection from some object of the original category.
More concisely: For any category J, functor F from J to Type, and an element x in the colimit of F, there exists an object j in J and an element y in the image of F(j) such that the coprojection of j to the colimit of F maps y to x.
|
CategoryTheory.Limits.Types.Limit.π_mk
theorem CategoryTheory.Limits.Types.Limit.π_mk :
∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
[inst_1 : CategoryTheory.Limits.HasLimit F] (x : (j : J) → F.obj j)
(h : ∀ (j j' : J) (f : j ⟶ j'), F.map f (x j) = x j') (j : J),
CategoryTheory.Limits.limit.π F j (CategoryTheory.Limits.Types.Limit.mk F x h) = x j
This theorem, `CategoryTheory.Limits.Types.Limit.π_mk`, states that for any category `J` with objects of type `v` and morphisms of type `w`, and any functor `F` from `J` to the category of types, if `F` has a limit, then for any function `x` assigning to each object `j` of `J` an element of `F.obj j`, and for any proof `h` that `x` respects the morphisms of `J` (i.e., for all objects `j` and `j'` of `J` and any morphism `f` from `j` to `j'`, `F.map f` applied to `x j` equals `x j'`), if you take the limit of `F` and apply the projection to `j` to the limit object associated with `F`, `x`, and `h`, you get back `x j`. In other words, the projection function from the limit object of the functor to the value of the functor at a given point is equal to the function value at that point when the function is cohesive with the functor.
More concisely: Given a limit-preserving function `x` from objects of a category `J` to the values of a functor `F` from `J`, the projection of the limit object of `F` to `x j` equals `x j`, for any object `j` in `J`.
|
CategoryTheory.Limits.Types.Limit.map_π_apply'
theorem CategoryTheory.Limits.Types.Limit.map_π_apply' :
∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F G : CategoryTheory.Functor J (Type v)} (α : F ⟶ G)
(j : J) (x : CategoryTheory.Limits.limit F),
CategoryTheory.Limits.limit.π G j (CategoryTheory.Limits.limMap α x) =
α.app j (CategoryTheory.Limits.limit.π F j x)
This theorem states that for any categories `J` and `(Type v)`, and any two functors `F` and `G` from `J` to `(Type v)`, given a natural transformation `α` from `F` to `G`, and an object `j` in `J` and `x` in the limit object of the functor `F`, applying the limit projection (`CategoryTheory.Limits.limit.π`) of functor `G` at `j` to the limit map (`CategoryTheory.Limits.limMap`) of `α` at `x`, is the same as applying `α` at `j` to the limit projection of `F` at `j` applied to `x`.
In terms of category theory, this theorem confirms the expected behavior of limit projections and limit maps under natural transformations between functors, which is fundamental to the definition and properties of limit objects in a category.
More concisely: Given functors F and G from category J to Type v, a natural transformation α from F to G, an object j in J, and an object x in the limit of F, the limit projection of G at j applied to the limit map of α at x equals applying α at j to the limit projection of F at j applied to x.
|
CategoryTheory.Limits.Types.limitConeIsLimit.proof_1
theorem CategoryTheory.Limits.Types.limitConeIsLimit.proof_1 :
∀ {J : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} J] (F : CategoryTheory.Functor J TypeMax)
(s : CategoryTheory.Limits.Cone F) (v : s.pt) {j j' : J} (f : j ⟶ j'),
CategoryTheory.CategoryStruct.comp (s.π.app j) (F.map f) v = s.π.app j' v
The theorem `CategoryTheory.Limits.Types.limitConeIsLimit.proof_1` states that for any category `J` and any functor `F` from `J` to `TypeMax`, given a cone `s` of `F` and an element `v` of the vertex of the cone, if there is a morphism `f` from `j` to `j'` in `J`, then the composition of the morphism `s.π.app j` in the category of types with the mapping of `f` under `F` applied to `v`, is equal to the morphism `s.π.app j'` applied to `v`. In simpler terms, it validates the commutativity of the diagram involving the cone, the functor and the morphism in the category.
More concisely: For any cone `s` in a category `J` and functor `F` from `J` to `TypeMax`, if `v` is an element of the vertex of `s` and `f` is a morphism in `J`, then `F(f)(s.π.app j v) = s.π.app j' v` holds in the category of types.
|