CategoryTheory.Limits.limit.w
theorem CategoryTheory.Limits.limit.w :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasLimit F] {j j' : J} (f : j ⟶ j'),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j) (F.map f) =
CategoryTheory.Limits.limit.π F j'
The theorem `CategoryTheory.Limits.limit.w` is a statement in category theory about limits in a category. Specifically, for any category `J`, any category `C`, any functor `F` from `J` to `C`, and any morphism `f` from `j` to `j'` in `J`, the composition of the projection from the limit of `F` to `F.obj j` and the image of `f` under `F` is equal to the projection from the limit of `F` to `F.obj j'`. In other words, this theorem states that in a category with limits, the limit behaves functorially with respect to morphisms in the indexing category: the diagram formed by the limit, the projections, and the map `F` commutes.
More concisely: For any functor F from a small category J to a category C and any morphism f in J, the diagram commutes for the limit of F, that is, the composition of the limit projection to F(j) and the image of f under F equals the limit projection to F(j').
|
CategoryTheory.Limits.HasLimit.mk
theorem CategoryTheory.Limits.HasLimit.mk :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C}, CategoryTheory.Limits.LimitCone F → CategoryTheory.Limits.HasLimit F
This theorem states that for any type `J` that forms a category, any type `C` that also forms a category, and any functor `F` from `J` to `C`, if there is a limit cone for `F`, then `F` has a limit. In category theory, a limit of a functor is a universal cone, and a limit cone is a particular cone which is a candidate for being a limit. This theorem provides a way to construct a limit for a functor given a limit cone.
More concisely: If `J` is a type forming a category, `C` is another category type, and `F : J → C` is a functor with a limit cone, then `F` has a limit.
|
CategoryTheory.Limits.limit.post_π
theorem CategoryTheory.Limits.limit.post_π :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor J C) {D : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} D]
[inst_3 : CategoryTheory.Limits.HasLimit F] (G : CategoryTheory.Functor C D)
[inst_4 : CategoryTheory.Limits.HasLimit (F.comp G)] (j : J),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.post F G)
(CategoryTheory.Limits.limit.π (F.comp G) j) =
G.map (CategoryTheory.Limits.limit.π F j)
This theorem, `CategoryTheory.Limits.limit.post_π`, is stating a property regarding the composition of morphisms within the context of category theory and more specifically, limit objects. For any types `J`, `C`, and `D` that form categories and any functors `F` from `J` to `C` and `G` from `C` to `D`, given that `F` has a limit and the composition of `F` and `G` also has a limit, for any object `j` in `J`, the composition of the morphism from the limit object of `F` postcomposed with `G` to the limit object of the composition of `F` and `G`, and the projection from the limit object of the composition of `F` and `G` to the image of `j` under the composition of `F` and `G`, is equal to the morphism induced by `G` on the projection from the limit object of `F` to the image of `j` under `F`. In simpler terms, this theorem is about how limits are preserved under functorial action.
More concisely: Given functors `F: J → C` and `G: C → D` with limit objects, if both `F` and the composition `G ∘ F` have limits, then for any object `j` in `J`, the morphism from the limit of `F` to the image of `j` under `G ∘ F` is equal to the composition of the morphism from the limit of `F` to the image of `j` under `F`, and the morphism from the limit of `G ∘ F` to its image under `G`.
|
CategoryTheory.Limits.hasColimitsOfShape_of_equivalence
theorem CategoryTheory.Limits.hasColimitsOfShape_of_equivalence :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{J' : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} J'],
(J ≌ J') →
∀ [inst : CategoryTheory.Limits.HasColimitsOfShape J C], CategoryTheory.Limits.HasColimitsOfShape J' C
This theorem states that if we have a category `C` that has colimits of shape `J`, and if `J` is equivalent to another category `J'`, then `C` also has colimits of shape `J'`. In other words, the existence of colimits in a category is preserved under equivalence of categories.
More concisely: If categories `C` and `D` are equivalent, then `C` has colimits of shape `J` if and only if `D` has colimits of shape `J`.
|
CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_hom
theorem CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_hom :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F]
[inst_3 : CategoryTheory.Limits.HasColimit G] (w : F ≅ G) (j : J),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j)
(CategoryTheory.Limits.HasColimit.isoOfNatIso w).hom =
CategoryTheory.CategoryStruct.comp (w.hom.app j) (CategoryTheory.Limits.colimit.ι G j)
This theorem, named `CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_hom`, states that for any two functors `F` and `G` from a category `J` to a category `C`, given that both functors have colimits and there exists a natural isomorphism `w` between `F` and `G`, the composition of the coprojection from a value of the functor `F` to the colimit object of `F` with the homomorphism of the iso associated with the natural isomorphism `w`, is equal to the composition of the application of the homomorphism of `w` to `j` with the coprojection from a value of the functor `G` to the colimit object of `G`, for any object `j` in `J`. This theorem expresses a key property of natural isomorphisms and colimits in category theory.
More concisely: For any functors F and G from a category J to C with colimits, and given a natural isomorphism w between F and G, the following diagram commutes:
F(j) ───────────────────────────── w\_j ────────────────────────────── G(j)
│ │ │
│ │ v v
│ COLIM F ───────────────────=─────────────────────────────── COLIM G
│ │ │
│ │ up_F(j) ───────────────── v ────────────────────────────── down_G(j)
|
CategoryTheory.Limits.limit.pre_π
theorem CategoryTheory.Limits.limit.pre_π :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} K] {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor J C) [inst_3 : CategoryTheory.Limits.HasLimit F] (E : CategoryTheory.Functor K J)
[inst_4 : CategoryTheory.Limits.HasLimit (E.comp F)] (k : K),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.pre F E)
(CategoryTheory.Limits.limit.π (E.comp F) k) =
CategoryTheory.Limits.limit.π F (E.obj k)
The theorem `CategoryTheory.Limits.limit.pre_π` states that for any categories J, K, and C, and any functors F: J → C, E: K → J, when F has a limit and the composition of E and F also has a limit, then for any object k of K, the composition of the limit precomposition of F by E and the projection from the limit of the composition of E and F to the value at k, is equal to the projection from the limit of F to the value of E at k.
In other words, this theorem is saying that the limit precomposition of a functor followed by the limit projection can be "interchanged" with the limit projection of the original functor applied to the object of the secondary category. This is a key property in the study of limits in category theory.
More concisely: Given functors F: J → C, E: K → J, if F has a limit and the composition E∘F has a limit, then for all objects k in K, the limit precomposition of F by E and the projection from the limit of E∘F to k are equal to the projection from the limit of F to E(k).
|
CategoryTheory.Limits.colimit.ι_desc_assoc
theorem CategoryTheory.Limits.colimit.ι_desc_assoc :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F]
(c : CategoryTheory.Limits.Cocone F) (j : J) {Z : C} (h : c.pt ⟶ Z),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.desc F c) h) =
CategoryTheory.CategoryStruct.comp (c.ι.app j) h
This theorem, named `CategoryTheory.Limits.colimit.ι_desc_assoc`, is a statement about morphisms in the category theory. Specifically, it says that for any type `J` with a category structure, a type `C` with a category structure, a functor `F` from `J` to `C` that has a colimit, a cocone `c` over that functor, an object `j` from `J`, and a morphism `h` from the cocone point to an object `Z`, the composition of the coprojection from a value of the functor to the colimit object (denoted `CategoryTheory.Limits.colimit.ι F j`) and the composition of the morphism from the colimit object to the cocone point of any other cocone (denoted `CategoryTheory.Limits.colimit.desc F c`) with `h` is the same as the composition of the natural transformation of the cocone at `j` and `h`. In mathematical terms, `(CategoryTheory.Limits.colimit.ι F j) ≫ ((CategoryTheory.Limits.colimit.desc F c) ≫ h) = (c.ι.app j) ≫ h`. The symbol `≫` stands for the composition of morphisms.
More concisely: For any functor with a colimit, the composition of the coprojection from the functor to the colimit object, the morphism from the colimit object to any cocone point, and a given morphism to the coconet point is equal to the composition of the natural transformation of the cocone at the source object and the given morphism.
|
CategoryTheory.Limits.colimit.pre_eq
theorem CategoryTheory.Limits.colimit.pre_eq :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} K] {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C} [inst_3 : CategoryTheory.Limits.HasColimit F] {E : CategoryTheory.Functor K J}
[inst_4 : CategoryTheory.Limits.HasColimit (E.comp F)] (s : CategoryTheory.Limits.ColimitCocone (E.comp F))
(t : CategoryTheory.Limits.ColimitCocone F),
CategoryTheory.Limits.colimit.pre F E =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.isoColimitCocone s).hom
(CategoryTheory.CategoryStruct.comp (s.isColimit.desc (CategoryTheory.Limits.Cocone.whisker E t.cocone))
(CategoryTheory.Limits.colimit.isoColimitCocone t).inv)
This theorem provides an equation which relates the pre-colimit of two functors `F` and `E` in a category to the composition of a few other morphisms in the category. More specifically, given categories `J`, `K` and `C`, and functors `F: J -> C` and `E: K -> J`, if we have colimit cocones for `E ⋙ F` and for `F`, the pre-colimit of `F` and `E` is equal to the composition of the homomorphism of the iso colimit cocone of `s` and the composition of the description of isColimit `s` whiskered with the cocone `t` and the inverse of the homomorphism of the iso colomit cocone of `t`. Here, `s` is a colimit cocone of the composition of `E` and `F` and `t` is a colimit cocone of the functor `F`. This theorem essentially relates pre-colimit to certain compositions of morphisms associated with colimit cocones.
More concisely: Given functors `F: J -> C` and `E: K -> J` with colimit cocones `s` for `E ⋙ F` and `t` for `F`, the pre-colimit of `F` and `E` equals the composition of the homomorphism of `s` with `(descIsColimit E) ∘ t` and the inverse of the homomorphism of `t`.
|
CategoryTheory.Limits.HasLimit.ofConesIso
theorem CategoryTheory.Limits.HasLimit.ofConesIso :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J K : Type u₁}
[inst_1 : CategoryTheory.Category.{v₁, u₁} J] [inst_2 : CategoryTheory.Category.{v₂, u₁} K]
(F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor K C),
(F.cones ≅ G.cones) → ∀ [inst_3 : CategoryTheory.Limits.HasLimit F], CategoryTheory.Limits.HasLimit G
The theorem `CategoryTheory.Limits.HasLimit.ofConesIso` states that in the context of category theory, if we have two functors `F` and `G` from different categories `J` and `K` to a same category `C`, and if `F` has a limit and the collection of cones of `F` is isomorphic to the collection of cones of `G`, then `G` also has a limit.
More concisely: If functors `F` from category `J` and `G` from category `K` to category `C` have isomorphic collections of cones over a limit cone in `C`, then `G` also has a limit.
|
CategoryTheory.Limits.limit.hom_ext
theorem CategoryTheory.Limits.limit.hom_ext :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F] {X : C}
{f f' : X ⟶ CategoryTheory.Limits.limit F},
(∀ (j : J),
CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.limit.π F j) =
CategoryTheory.CategoryStruct.comp f' (CategoryTheory.Limits.limit.π F j)) →
f = f'
The theorem `CategoryTheory.Limits.limit.hom_ext` states that for any category `J` with a functor `F` to another category `C` (where `C` is also a category) and any object `X` in `C`, if there exist two morphisms `f` and `f'` from `X` to the limit object of the functor `F`, then `f` equals `f'` if and only if, for every object `j` in `J`, the composition of `f` and the projection from the limit object to the image of `j` under `F` equals the composition of `f'` and the same projection. In other words, it shows the uniqueness of a morphism into the limit, up to precomposition with the morphisms from the limit cone.
More concisely: For any functor from a category to another category and an object in the target category, if there exist two morphisms from the object to the limit of the functor, then they are equal if and only if their compositions with the projections from the limit to the images of objects under the functor are equal.
|
CategoryTheory.Limits.HasColimitsOfShape.has_colimit
theorem CategoryTheory.Limits.HasColimitsOfShape.has_colimit :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
[self : CategoryTheory.Limits.HasColimitsOfShape J C] (F : CategoryTheory.Functor J C),
CategoryTheory.Limits.HasColimit F
The theorem `CategoryTheory.Limits.HasColimitsOfShape.has_colimit` states that for any category `J` and any category `C`, if `C` has all colimits of a shape given by `J`, then for any functor `F` from `J` to `C`, `F` has a colimit. In other words, if a category `C` has colimits of a certain shape (determined by `J`), then any mapping from `J` to `C` (described by the functor `F`) will also have a colimit. This theorem is a fundamental result in category theory, a branch of mathematics which studies abstract algebraic structures.
More concisely: Given any category `C` with all colimits of shape `J` and any functor `F` from `J` to `C`, `F` has a colimit.
|
CategoryTheory.Limits.hasColimit_of_equivalence_comp
theorem CategoryTheory.Limits.hasColimit_of_equivalence_comp :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} K] {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C} (e : K ≌ J) [inst_3 : CategoryTheory.Limits.HasColimit (e.functor.comp F)],
CategoryTheory.Limits.HasColimit F
This theorem states that given two categories `J` and `K`, and a functor `F` from `J` to another category `C`, if there exists a colimit for the composite functor `E ⋙ F` (where `E` is an equivalence functor from `K` to `J`), it implies the existence of a colimit for the functor `F` itself. Hence, we can construct a colimit of `F` given that `E` is an equivalence and `E ⋙ F` has a colimit.
More concisely: If `F: J -> C` is a functor, `E: K -> J` is an equivalence, and `E ⋙ F` has a colimit in `C`, then `F` has a colimit in `C`.
|
CategoryTheory.Limits.HasColimit.ofCoconesIso
theorem CategoryTheory.Limits.HasColimit.ofCoconesIso :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{K : Type u₁} [inst_2 : CategoryTheory.Category.{v₂, u₁} K] (F : CategoryTheory.Functor J C)
(G : CategoryTheory.Functor K C),
(F.cocones ≅ G.cocones) → ∀ [inst : CategoryTheory.Limits.HasColimit F], CategoryTheory.Limits.HasColimit G
This theorem states that if we have two functors `F` and `G` from categories `J` and `K` to a category `C`, and if the set of cocones for `F` is isomorphic to the set of cocones for `G`, then if `F` has a colimit, `G` must also have a colimit. This theorem is a part of category theory and is related to the concept of limits and colimits.
More concisely: If functors `F` from category `J` and `G` from category `K` to category `C` have isomorphic sets of cocones, then `F` having a colimit implies `G` also has a colimit.
|
CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv
theorem CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F]
{c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (j : J),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j)
(hc.coconePointUniqueUpToIso (CategoryTheory.Limits.colimit.isColimit F)).inv =
c.ι.app j
This is a theorem in the field of category theory, specifically dealing with limits and colimits in a category. The theorem states that for any category `J`, any category `C`, any functor `F` from `J` to `C`, and any `j` in `J`, if `c` is a cocone over `F` and `hc` proves that `c` is a colimit cocone, then the composition of the coprojection from the `j`-th object of `F` to the colimit of `F` with the inverse of the isomorphism from the vertex of `c` to the colimit of `F` is the same as the `j`-th component of `c`. In simpler terms, it essentially says that composing the morphism `colimit.ι F j` with a certain inverse isomorphism gives us the same result as directly applying the `j`-th component of `c`. This is a property that must hold for all such categories, functors, and cocones.
More concisely: For any category `J`, any category `C`, any functor `F` from `J` to `C`, and any cocone `c` over `F` with verified colimit property, the composition of `F j` with the inverse of the vertex-to-colimit isomorphism is equal to the `j`-th component of `c` for all objects `j` in `J`.
|
CategoryTheory.Limits.HasColimitsOfSize.has_colimits_of_shape
theorem CategoryTheory.Limits.HasColimitsOfSize.has_colimits_of_shape :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
[self : CategoryTheory.Limits.HasColimitsOfSize.{v₁, u₁, v, u} C] (J : Type u₁)
[inst_1 : CategoryTheory.Category.{v₁, u₁} J], CategoryTheory.Limits.HasColimitsOfShape J C
This theorem states that for any category `C` and any small category `J`, if `C` has colimits of certain size, then `C` has colimits of shape `J`. In other words, if a category 'C' has colimits of a certain size, it will also have colimits of any shape, specified by a small category 'J'. The size and shape here refer to the nature of the indexing category used to define the colimit. This is a property of category theory, a branch of mathematics which deals with abstract algebraic structures.
More concisely: If a category `C` has colimits of size `J` for every small category `J`, then `C` has colimits of shape `J`.
|
CategoryTheory.Limits.ι_colimMap
theorem CategoryTheory.Limits.ι_colimMap :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F]
[inst_3 : CategoryTheory.Limits.HasColimit G] (α : F ⟶ G) (j : J),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j) (CategoryTheory.Limits.colimMap α) =
CategoryTheory.CategoryStruct.comp (α.app j) (CategoryTheory.Limits.colimit.ι G j)
The theorem `CategoryTheory.Limits.ι_colimMap` states that for any category `J` and `C`, and functors `F` and `G` from `J` to `C`, if `F` and `G` both have colimits, given a natural transformation `α` from `F` to `G` and an object `j` in `J`, then the composition of the coprojection from `F` at `j` to the colimit of `F` with the map induced by `α` from the colimit of `F` to the colimit of `G` is equal to the composition of the component of `α` at `j` with the coprojection from `G` at `j` to the colimit of `G`. In simpler terms, this theorem is a statement of naturality of the colimit map with respect to the transformation `α`.
More concisely: For any categories J and C, functors F and G from J to C with colimits, and a natural transformation α from F to G, the diagram commuting from the coprojections from F and G to their respective colimits and the maps induced by α holds.
|
CategoryTheory.Limits.ι_colimMap_assoc
theorem CategoryTheory.Limits.ι_colimMap_assoc :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F]
[inst_3 : CategoryTheory.Limits.HasColimit G] (α : F ⟶ G) (j : J) {Z : C}
(h : CategoryTheory.Limits.colimit G ⟶ Z),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimMap α) h) =
CategoryTheory.CategoryStruct.comp (α.app j)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G j) h)
This theorem states that for any two functors `F` and `G` from a category `J` to a category `C`, if both functors have colimit, and if `α` is a natural transformation from `F` to `G`, then for any object `j` in `J` and any morphism `h` from the colimit of `G` to an object `Z` in `C`, the composition of the coprojection from `j` under `F` to the colimit of `F` with the composition of the mapping of the colimit under `α` and `h` is equal to the composition of the application of `α` at `j` with the composition of the coprojection from `j` under `G` to the colimit of `G` and `h`.
In simpler terms, it ensures that mapping the colimit respects the structure of the category, specifically related to the composition of morphisms, in the scenario when we are dealing with two functors and a natural transformation between them.
More concisely: For any functors F and G from a category J to a category C with colimits, and any natural transformation α from F to G, the diagram commutes:
colim(F)(j) ⟶ colim(F) ⟶ Z ⟶ colim(G)(j) ⟶ Z
where j is an object in J, h is a morphism from colim(G) to Z, and the arrows represent the coprojections, α, and h.
|
CategoryTheory.Limits.HasColimit.mk
theorem CategoryTheory.Limits.HasColimit.mk :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C}, CategoryTheory.Limits.ColimitCocone F → CategoryTheory.Limits.HasColimit F
The theorem `CategoryTheory.Limits.HasColimit.mk` states that for any category `J` and functor `F` from `J` to category `C`, if there exists a ColimitCocone for `F`, then `F` has a colimit in `C`. In other words, a functor is guaranteed to have a colimit if a ColimitCocone for this functor can be identified.
More concisely: If a functor from a small category to another category has a ColimitCocone, then the functor has a colimit.
|
CategoryTheory.Limits.limit.isoLimitCone_inv_π
theorem CategoryTheory.Limits.limit.isoLimitCone_inv_π :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F]
(t : CategoryTheory.Limits.LimitCone F) (j : J),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.isoLimitCone t).inv
(CategoryTheory.Limits.limit.π F j) =
t.cone.π.app j
The theorem `CategoryTheory.Limits.limit.isoLimitCone_inv_π` states that in a category `C` with a functor `F` from a category `J`, given `t` as a limit cone of `F` and `j` as an object from category `J`, the composition of the inverse of the isomorphism from limit to limit cone `t` and the projection from the limit to the functor value at `j` equals to the projection of the cone `t` at `j`. In simpler terms, it signifies the correspondence between the mappings from the limit object and the vertex of the limit cone in the context of category theory.
More concisely: In a category with a functor, the inverse of the limit cone isomorphism to a limit and the projection from the limit to the functor value at an object are equal.
|
CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom
theorem CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F]
(t : CategoryTheory.Limits.ColimitCocone F) (j : J),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j)
(CategoryTheory.Limits.colimit.isoColimitCocone t).hom =
t.cocone.ι.app j
This theorem states that in the category theory, given a category `J`, another category `C`, a functor `F` from `J` to `C` which has a colimit, a colimit cocone `t` of the functor `F`, and an object `j` in `J`, the composition of the coprojection from `j` through the functor `F` to the colimit of `F`, and the morphism from the colimit of `F` to the colimit cocone `t`, is equal to the coprojection from `j` to the colimit cocone `t`. This essentially captures one of the properties of colimits in category theory.
More concisely: Given a functor `F` from category `J` to `C` with a colimit `t` and an object `j` in `J`, the composition of `F(j) ↓ t` and `t ↑ colim(F)` equals `j ↓ t` in `C`, where `↓` and `↑` denote the coprojections of the cocone.
|
CategoryTheory.Limits.hasLimitsOfSizeOfUnivLE
theorem CategoryTheory.Limits.hasLimitsOfSizeOfUnivLE :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : UnivLE.{v₂, v₁}] [inst_2 : UnivLE.{u₂, u₁}]
[inst_3 : CategoryTheory.Limits.HasLimitsOfSize.{v₁, u₁, v, u} C],
CategoryTheory.Limits.HasLimitsOfSize.{v₂, u₂, v, u} C
This theorem states that in category theory, if a category (denoted by 'C') has limits of a certain size (specified by the universe levels 'v₁' and 'u₁'), then it also has limits of smaller size (specified by the universe levels 'v₂' and 'u₂'). Here, 'UnivLE.{v₂, v₁}' and 'UnivLE.{u₂, u₁}' are the conditions that the universe levels 'v₂' and 'u₂' are less than or equal to 'v₁' and 'u₁' respectively. This ultimately allows us to generalize certain statements about limits in categories to different size levels.
More concisely: If a category has limits of size 'v₁' and 'u₁', then it has limits of smaller sizes 'v₂' and 'u₂' where 'v₂' and 'u₂' are less than or equal to 'v₁' and 'u₁' respectively.
|
CategoryTheory.Limits.HasLimit.exists_limit
theorem CategoryTheory.Limits.HasLimit.exists_limit :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C} [self : CategoryTheory.Limits.HasLimit F],
Nonempty (CategoryTheory.Limits.LimitCone F)
This theorem, `CategoryTheory.Limits.HasLimit.exists_limit`, states that for every functor `F` from a category `J` to a category `C`, if `F` has a limit, then there exists a limit cone for `F`. In category theory, a limit of a functor is a universal morphism from the functor to a constant functor. A limit cone is a particular kind of universal cone used to define limits. A cone is a natural transformation from a constant functor to `F`. This theorem is essentially saying that if a functor has a limit, there is a way to build a cone with the limit as its apex and the functor as its base which is universal, i.e., any other cone with the same apex and base factors uniquely through it.
More concisely: If a functor from one category to another has a limit, then there exists a universal cone for that limit.
|
CategoryTheory.Limits.hasColimitsOfSizeShrink
theorem CategoryTheory.Limits.hasColimitsOfSizeShrink :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
[inst_1 : CategoryTheory.Limits.HasColimitsOfSize.{max v₁ v₂, max u₁ u₂, v, u} C],
CategoryTheory.Limits.HasColimitsOfSize.{v₁, u₁, v, u} C
The theorem `CategoryTheory.Limits.hasColimitsOfSizeShrink` in Lean asserts that, for any category `C` of type `u` and for any instance where `C` has colimits of a certain size (expressed as `HasColimitsOfSize` of maximum of `v₁` and `v₂` and maximum of `u₁` and `u₂`), it is also true that `C` has colimits of a smaller size (`HasColimitsOfSize` of `v₁` and `u₁`). In other words, it indicates the existence of smaller colimits in a category, given that larger colimits exist.
More concisely: If a category of a certain size has colimits, then it also has colimits of smaller size.
|
CategoryTheory.Limits.colimit.ι_pre
theorem CategoryTheory.Limits.colimit.ι_pre :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} K] {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor J C) [inst_3 : CategoryTheory.Limits.HasColimit F] (E : CategoryTheory.Functor K J)
[inst_4 : CategoryTheory.Limits.HasColimit (E.comp F)] (k : K),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (E.comp F) k)
(CategoryTheory.Limits.colimit.pre F E) =
CategoryTheory.Limits.colimit.ι F (E.obj k)
The theorem `CategoryTheory.Limits.colimit.ι_pre` states that for any categories `J`, `K`, and `C`, a functor `F` from `J` to `C`, a functor `E` from `K` to `J`, and an object `k` in `K`, the composition of the coprojection from the colimit of the composite functor `E` followed by `F` at `k` and the colimit precomposition `F` with `E` is equal to the coprojection from the colimit of `F` at `E.obj k`. This means that the diagram involving these coprojections and the colimit precomposition commutes. This is a fundamental property in the theory of colimits in category theory.
More concisely: For any functors F from J to C, E from K to J, object k in K, the diagram commutes between the coprojection from the colimit of F at E.obj k, the colimit precomposition F with E at k, and the coprojection from the colimit of the composite functor E then F.
|
CategoryTheory.Limits.colimit.hom_ext
theorem CategoryTheory.Limits.colimit.hom_ext :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F] {X : C}
{f f' : CategoryTheory.Limits.colimit F ⟶ X},
(∀ (j : J),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j) f =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j) f') →
f = f'
This theorem, `CategoryTheory.Limits.colimit.hom_ext`, states that, given any category `J` with objects of type `u₁`, any category `C` with objects of type `u`, and a functor `F` from `J` to `C` that has a colimit, for any object `X` in `C`, if we have two morphisms `f` and `f'` from the colimit of `F` to `X`, then `f` equals `f'` if and only if for every object `j` in `J`, the composition of the coprojection from `j` to the colimit object and `f` equals the composition of the coprojection from `j` to the colimit object and `f'`. In other words, two morphisms from the colimit to another object are the same if they agree after pre-composing with the coprojections from every object of the original category.
More concisely: Given a functor with a colimit from a category to another, two morphisms from the colimit to an object are equal if and only if they agree on precomposition with all coprojections from objects in the original category.
|
CategoryTheory.Limits.hasLimitsOfSizeShrink
theorem CategoryTheory.Limits.hasLimitsOfSizeShrink :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
[inst_1 : CategoryTheory.Limits.HasLimitsOfSize.{max v₁ v₂, max u₁ u₂, v, u} C],
CategoryTheory.Limits.HasLimitsOfSize.{v₁, u₁, v, u} C
The theorem `CategoryTheory.Limits.hasLimitsOfSizeShrink` in Lean 4 is stating that for any type `C` which is a category and has limits of a certain size (defined by `HasLimitsOfSize.{max v₁ v₂, max u₁ u₂, v, u} C`), we can obtain a category with limits of a smaller size (`HasLimitsOfSize.{v₁, u₁, v, u} C`). In other words, if a category has larger size limits, it can certainly handle smaller size limits.
More concisely: For any category `C` with limits of size `(max v₁ v₂, max u₁ u₂)`, it has limits of size `(v₁, u₁)`.
|
CategoryTheory.Limits.hasColimitOfIso
theorem CategoryTheory.Limits.hasColimitOfIso :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F],
(G ≅ F) → CategoryTheory.Limits.HasColimit G
This theorem states that if a functor `F` has a colimit in a category, then any functor `G` that is naturally isomorphic to `F` also has a colimit in that category. Here, `J` and `C` are types representing the categories, and `F` and `G` are functors from category `J` to category `C`. The theorem takes a proof that `F` has a colimit and a natural isomorphism between `F` and `G` to construct a proof that `G` also has a colimit.
More concisely: If functors `F` and `G` are naturally isomorphic and `F` has a colimit in a category `C`, then `G` also has a colimit in `C`.
|
CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv
theorem CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F]
(t : CategoryTheory.Limits.ColimitCocone F) (j : J),
CategoryTheory.CategoryStruct.comp (t.cocone.ι.app j) (CategoryTheory.Limits.colimit.isoColimitCocone t).inv =
CategoryTheory.Limits.colimit.ι F j
This theorem states that for any category `J` of type `u₁`, category `C` of type `u`, and functor `F` from `J` to `C` that has a colimit, given any `j` from `J` and a co-limit cocone `t` of `F`, the composition of the morphism from `j` to the cocone's apex with the inverse of the isomorphism from the colimit to the cocone's apex is the same as the co-projection from the object `j` under the functor `F` to the colimit of the functor `F`. This result is a key part of the universal property defining colimits in a category.
More concisely: For any functor F from category J to C with a colimit, the inverse of the unique isomorphism from F's colimit to the cocone's apex equals the co-projection of the object under F from J to the colimit.
|
CategoryTheory.Limits.HasLimitsOfSize.has_limits_of_shape
theorem CategoryTheory.Limits.HasLimitsOfSize.has_limits_of_shape :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
[self : CategoryTheory.Limits.HasLimitsOfSize.{v₁, u₁, v, u} C] (J : Type u₁)
[inst_1 : CategoryTheory.Category.{v₁, u₁} J], CategoryTheory.Limits.HasLimitsOfShape J C
This theorem states that for any category `C` and any small category `J`, if `C` has limits of a certain size (as defined by `HasLimitsOfSize`), then `C` has limits of shape `J`. In the language of category theory, a category `C` has limits of shape `J` if every functor from `J` to `C` has a limit in `C`.
More concisely: If `C` is a category with limits of size `s` and `J` is a small category, then `C` has limits of shape `J`.
|
CategoryTheory.Limits.colimit.ι_map
theorem CategoryTheory.Limits.colimit.ι_map :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J C]
{G : CategoryTheory.Functor J C} (α : F ⟶ G) (j : J),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j) (CategoryTheory.Limits.colim.map α) =
CategoryTheory.CategoryStruct.comp (α.app j) (CategoryTheory.Limits.colimit.ι G j)
This theorem, `CategoryTheory.Limits.colimit.ι_map`, states that for any category `J`, any category `C` that has colimits of shape `J`, any two functors `F` and `G` from `J` to `C`, and a natural transformation `α` from `F` to `G`, the composition of the coprojection from `F` to the colimit of `F` and the map induced by `α` on the colimits is equal to the composition of the component of `α` at `j` and the coprojection from `G` to the colimit of `G`. In other words, the diagram
```
F.obj j --> colimit F
| |
v v
G.obj j --> colimit G
```
commutes, where the horizontal arrows are the coprojections, the vertical arrow on the left is `α.app j`, the vertical arrow on the right is `CategoryTheory.Limits.colim.map α`, and the compositions of the arrows along the top and bottom are equal.
More concisely: For any category J, any category C with colimits of shape J, and any functors F and G from J to C with a natural transformation α from F to G, the diagram commutes, where the horizontal arrows are the coprojections and the vertical arrows are the maps induced by α and the coprojections to the colimits.
|
CategoryTheory.Limits.limit.lift_π
theorem CategoryTheory.Limits.limit.lift_π :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F] (c : CategoryTheory.Limits.Cone F)
(j : J),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.lift F c) (CategoryTheory.Limits.limit.π F j) =
c.π.app j
The theorem `CategoryTheory.Limits.limit.lift_π` asserts that for any category `J`, any category `C`, any functor `F` from `J` to `C` that has a limit, any cone `c` of `F`, and any object `j` of `J`, the composition of the morphism from the cone point of `c` to the limit object of `F` (given by `CategoryTheory.Limits.limit.lift F c`) and the projection from the limit object of `F` to the `j`th value of the functor `F` (given by `CategoryTheory.Limits.limit.π F j`) is the same as the `j`th component of the natural transformation from the vertex of the cone `c` to the functor `F` (given by `c.π.app j`).
In terms of category theory, this is a way of saying that the limit of a functor is a universal cone over that functor: any other cone factors uniquely through the limit cone.
More concisely: For any functor with a limit, the limit object and cone projection morphisms make the limit a universal cone over the functor, meaning the limit projection to any object in the base category is equal to the composition of the projection from the limit object to that object and the cone morphism from the vertex to the functor.
|
CategoryTheory.Limits.HasLimitsOfShape.has_limit
theorem CategoryTheory.Limits.HasLimitsOfShape.has_limit :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
[self : CategoryTheory.Limits.HasLimitsOfShape J C] (F : CategoryTheory.Functor J C),
CategoryTheory.Limits.HasLimit F
This theorem states that for any given functor `F` mapping from a category `J` to a category `C`, if the category `C` has limits of shape `J` (i.e., for every diagram in `J` there exists a limit in `C`), then the functor `F` has a limit. This is a fundamental property in category theory, connecting the concept of limits in a category to the structure of functors between categories.
More concisely: If category `C` has limits of shape `J`, then every functor `F` from category `J` to `C` has a limit.
|
CategoryTheory.Limits.limit.lift_π_assoc
theorem CategoryTheory.Limits.limit.lift_π_assoc :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F] (c : CategoryTheory.Limits.Cone F)
(j : J) {Z : C} (h : F.obj j ⟶ Z),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.lift F c)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j) h) =
CategoryTheory.CategoryStruct.comp (c.π.app j) h
The theorem `CategoryTheory.Limits.limit.lift_π_assoc` states that for any category `J`, any category `C`, any functor `F` from `J` to `C`, any cone `c` over `F`, any object `j` in `J`, and any morphism `h` from `F.obj j` to any object `Z` in `C`, the composition of the morphism `lift` from the cone point of `c` to the limit of `F` with the composition of the projection morphism from the limit of `F` to `F.obj j` and `h` is equal to the composition of the morphism from the cone point of `c` to `F.obj j` and `h`.
In simpler terms, it says that in a category with limits, composing the lift from a cone to the limit with a projection from the limit gives the same result as applying the morphism from the cone directly to the object.
More concisely: For any cone over a functor and any morphism, composing the lift from the cone point to the limit with the composition of the projection from the limit and the morphism is equal to the composition of the morphism with the lift from the cone point to the object in the domain of the functor.
|
CategoryTheory.Limits.HasColimit.exists_colimit
theorem CategoryTheory.Limits.HasColimit.exists_colimit :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C} [self : CategoryTheory.Limits.HasColimit F],
Nonempty (CategoryTheory.Limits.ColimitCocone F)
This theorem states that for any category `J` and any functor `F` from `J` to a category `C`, if `F` has a colimit, then there exists a colimit cocone for `F`. A colimit cocone is a cocone to `F` from some object such that every other cocone to `F` factors through it. This theorem is a fundamental result in category theory and is particularly useful when working with diagrams in a category.
More concisely: Given any category `J` and functor `F` from `J` to a category `C` with a colimit, there exists a unique colimit cocone to `F`.
|
CategoryTheory.Limits.hasLimitOfEquivalenceComp
theorem CategoryTheory.Limits.hasLimitOfEquivalenceComp :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} K] {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C} (e : K ≌ J) [inst_3 : CategoryTheory.Limits.HasLimit (e.functor.comp F)],
CategoryTheory.Limits.HasLimit F
This theorem states that given a category `J`, a category `K`, a category `C`, and a functor `F` from `J` to `C`, if the composition of the equivalence functor `E` from `K` to `J` with `F` has a limit, then `F` itself has a limit. In other words, if we have an equivalence between categories `K` and `J`, and a functor `F` that has a limit when composed with this equivalence, then the functor `F` independently also has a limit.
More concisely: If `F: J -> C` is a functor and there exists a limit for `FE: K -> C` with `E: K -> J` an equivalence of categories, then `F` has a limit in `C`.
|
CategoryTheory.Limits.limit.pre_eq
theorem CategoryTheory.Limits.limit.pre_eq :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} K] {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C} [inst_3 : CategoryTheory.Limits.HasLimit F] {E : CategoryTheory.Functor K J}
[inst_4 : CategoryTheory.Limits.HasLimit (E.comp F)] (s : CategoryTheory.Limits.LimitCone (E.comp F))
(t : CategoryTheory.Limits.LimitCone F),
CategoryTheory.Limits.limit.pre F E =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.isoLimitCone t).hom
(CategoryTheory.CategoryStruct.comp (s.isLimit.lift (CategoryTheory.Limits.Cone.whisker E t.cone))
(CategoryTheory.Limits.limit.isoLimitCone s).inv)
This theorem states that, for given categories `J`, `K` and `C`, and functors `F : J → C` and `E : K → J`, if we have limit cones available for both the composition of functors `E ⋙ F` and `F`, we can express the pre-limit of `F` with respect to `E` in terms of these limit cones. Specifically, the pre-limit of `F` with respect to `E` is the same as the composition of the morphism from the limit cone of `F` to `C` and the composition of the morphism obtained by lifting the whisker of `E` with the limit cone of `F` to the limit cone of `E ⋙ F` and the inverse morphism from the limit cone of `E ⋙ F` to `C`.
More concisely: Given functors `F : J -> C` and `E : K -> J`, if both `F` and `E ⋙ F` have limits and their limit cones are known, then the pre-limit of `F` with respect to `E` is equal to the composition of the morphisms from the limit cones of `F` and `E ⋙ F`, followed by the inverse of the morphism from the limit cone of `E ⋙ F` to the limit cone of `F`.
|
CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp
theorem CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F] {c : CategoryTheory.Limits.Cone F}
(hc : CategoryTheory.Limits.IsLimit c) (j : J),
CategoryTheory.CategoryStruct.comp (hc.conePointUniqueUpToIso (CategoryTheory.Limits.limit.isLimit F)).hom
(CategoryTheory.Limits.limit.π F j) =
c.π.app j
The theorem `CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp` asserts that in the context of a category with limits, for any functor `F` and any limit cone `c` of `F`, the composition of the morphism from the cone point of `c` to the limit of `F` and the projection from the limit of `F` to a value of the functor `F` is equal to the morphism from the cone point of `c` to a value of the functor. In particular, this expresses the universal property of the category-theoretic limit, which states that every cone to `F` factors uniquely through the limit cone.
More concisely: In a category with limits, for any functor and limit cone, the composition of the morphism from the cone point to the limit and the projection from the limit to a value of the functor is equal to the morphism from the cone point to that value of the functor.
|
CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom
theorem CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F]
{c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (j : J),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j)
((CategoryTheory.Limits.colimit.isColimit F).coconePointUniqueUpToIso hc).hom =
c.ι.app j
This theorem in category theory states that for any category `J`, any category `C`, any functor `F` from `J` to `C`, any colimit `F` in `C`, and any cocone `c` of `F` for which `c` is a colimit, then for any object `j` in `J`, the composition of the coprojection from `j` to the colimit of `F` and the morphism from the colimit of `F` to `c` that is unique up to isomorphism is the same as the morphism from `j` to `c`. In other words, it ensures that the diagram commutes in the category, which means that the path from `j` to `c` via `F` and the direct path from `j` to `c` are the same.
More concisely: Given any functor `F` from a category `J` to a category `C`, any colimit `colim F` and cocone `c` of `F` in `C`, if `c` is the colimit of `F` and `j` is an object in `J`, then the composition of the coprojection from `j` to `colim F` and the unique morphism from `colim F` to `c` is equal to the morphism from `j` to `c`.
|
CategoryTheory.Limits.hasColimitsOfSizeOfUnivLE
theorem CategoryTheory.Limits.hasColimitsOfSizeOfUnivLE :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : UnivLE.{v₂, v₁}] [inst_2 : UnivLE.{u₂, u₁}]
[inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{v₁, u₁, v, u} C],
CategoryTheory.Limits.HasColimitsOfSize.{v₂, u₂, v, u} C
This theorem states that, in the context of Category Theory, if a category has colimits of a certain size (defined by the universe levels `v₁` and `u₁`), then it also has colimits of any smaller size (defined by universe levels `v₂` and `u₂`). Here, "smaller size" is formalized by the condition `UnivLE.{v₂, v₁}` and `UnivLE.{u₂, u₁}`, meaning that the universe levels `v₂` and `u₂` are less than or equal to `v₁` and `u₁` respectively.
More concisely: If a category has colimits of size `v₁` and `u₁`, then it has colimits of any smaller size `v₂` and `u₂` with `v₂ <= v₁` and `u₂ <= u₁`.
|
CategoryTheory.Limits.colimit.ι_desc
theorem CategoryTheory.Limits.colimit.ι_desc :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F]
(c : CategoryTheory.Limits.Cocone F) (j : J),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j)
(CategoryTheory.Limits.colimit.desc F c) =
c.ι.app j
This theorem, `CategoryTheory.Limits.colimit.ι_desc`, states that for any category `J` and `C`, any functor `F` from `J` to `C`, and any cocone `c` of `F`, the composition of the coprojection from a value of the functor to the colimit object, `colimit.ι F j` and the morphism from the colimit object to the cone point of the cocone `c`, `colimit.desc F c`, is equal to the morphism from the object `j` in the category `J` to the apex of the cocone `c`. Formally, this is written as `(CategoryTheory.Limits.colimit.ι F j) ≫ (CategoryTheory.Limits.colimit.desc F c) = c.ι.app j`. This theorem is particularly useful when working with expressions that are right associated due to the `Category.assoc` simplification lemma, allowing us to define additional simplification lemmas with an arbitrary extra morphism using the `reassoc` tactic.
More concisely: The composition of the coprojection from a functor's value to the colimit object and the descrition morphism from the colimit object to the cone point equals the morphism from the original object to the cone point in a given cocone.
|
CategoryTheory.Limits.limit.lift_map
theorem CategoryTheory.Limits.limit.lift_map :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F]
[inst_3 : CategoryTheory.Limits.HasLimit G] (c : CategoryTheory.Limits.Cone F) (α : F ⟶ G),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.lift F c) (CategoryTheory.Limits.limMap α) =
CategoryTheory.Limits.limit.lift G ((CategoryTheory.Limits.Cones.postcompose α).obj c)
The theorem `CategoryTheory.Limits.limit.lift_map` states that for any category `J` and `C`, and any functors `F` and `G` from `J` to `C`, if `F` and `G` both have limits and `c` is a cone of `F`, and `α` is a natural transformation from `F` to `G`, then the composition of the morphism from the cone point of `c` to the limit of `F` and the morphism induced by `α` from the limit of `F` to the limit of `G`, is the same as the morphism from the cone point of the cone obtained by postcomposing `α` on `c` to the limit of `G`. In simpler terms, this theorem ensures a specific commutativity condition for the diagram involving the limit of two functors and a natural transformation between them.
More concisely: Given categories `J` and `C`, functors `F` and `G` from `J` to `C`, their respective limits, a cone `c` of `F`, and a natural transformation `α` from `F` to `G`, the diagram commutes, i.e., the morphism from the cone point of `c` to the limit of `F` followed by `α` equals `α` followed by the morphism from the limit of `F` to the limit of `G`.
|
CategoryTheory.Limits.limMap_π_assoc
theorem CategoryTheory.Limits.limMap_π_assoc :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F]
[inst_3 : CategoryTheory.Limits.HasLimit G] (α : F ⟶ G) (j : J) {Z : C} (h : G.obj j ⟶ Z),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limMap α)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π G j) h) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j)
(CategoryTheory.CategoryStruct.comp (α.app j) h)
The theorem `CategoryTheory.Limits.limMap_π_assoc` states that in the context of a category with objects of type `C` and another category with objects of type `J`, given two functors `F` and `G` from `J` to `C` (both of which are assumed to have limits), a natural transformation `α` from `F` to `G`, an object `j` of `J`, and a morphism `h` from `G.obj j` to an object `Z` in `C`, the composition of the limit mapping of `α` with the composition of the projection from the limit of `G` to `j` and `h` is equal to the composition of the projection from the limit of `F` to `j` with the composition of the `j` component of `α` and `h`. In mathematical terms, this theorem establishes the commutativity of the given diagram in the category `C`.
More concisely: In a category with limits, given functors F and G from J to C, a natural transformation α from F to G, an object j of J, and a morphism h from G(j) to Z in C, the diagram commutes: limit(F)→j→G(j)→Z = limit(F)→j→F(j)→Z → G(j)→Z.
|
CategoryTheory.Limits.limMap_π
theorem CategoryTheory.Limits.limMap_π :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F]
[inst_3 : CategoryTheory.Limits.HasLimit G] (α : F ⟶ G) (j : J),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limMap α) (CategoryTheory.Limits.limit.π G j) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j) (α.app j)
The theorem `CategoryTheory.Limits.limMap_π` states that for any two categories `J` and `C` and two functors `F` and `G` from `J` to `C`, if `F` and `G` have limits and there is a natural transformation `α` from `F` to `G`, then for any object `j` in `J`, the composition of the map from the limit of `F` to `G` with the projection from the limit of `G` to the object `j` is equal to the composition of the projection from the limit of `F` to the object `j` with the application of the natural transformation `α` to `j`. This is a statement about the commutativity of a certain diagram involving limits in a category, which is a fundamental concept in category theory.
More concisely: For any functors F and G from category J to category C with limiting cones, and a natural transformation α from F to G, the diagram commutes, that is, the projection of the limit of F to an object j in J through α is equal to the composition of the projection of the limit of F to j and α(j).
|
CategoryTheory.Limits.colimit.ι_post
theorem CategoryTheory.Limits.colimit.ι_post :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor J C) {D : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} D]
[inst_3 : CategoryTheory.Limits.HasColimit F] (G : CategoryTheory.Functor C D)
[inst_4 : CategoryTheory.Limits.HasColimit (F.comp G)] (j : J),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.comp G) j)
(CategoryTheory.Limits.colimit.post F G) =
G.map (CategoryTheory.Limits.colimit.ι F j)
The theorem `CategoryTheory.Limits.colimit.ι_post` states that for any object `J` in a category, a functor `F` from `J` to a category `C`, another functor `G` from `C` to a different category `D`, and given that the functors and categories satisfy certain conditions (being co-limits), the composition of the coprojection from a value of the composite functor `F` followed by `G` to the co-limit object of the composite functor and the post-composed co-limit of `F` with `G` is equal to the `G`-mapping of the coprojection from a value of the functor `F` to the co-limit object of `F`. In mathematical terms, this is expressing a property of the co-limit object in category theory, specifically the universality of the co-limit.
More concisely: For any functors F from J to C and G from C to D, where J is an object in a category and F and G have co-limits, the post-composition of the coprojection of F's co-limit with G and the coprojection of F's co-limit is equal to G's mapping of F's coprojection.
|
CategoryTheory.Limits.limit.conePointUniqueUpToIso_inv_comp
theorem CategoryTheory.Limits.limit.conePointUniqueUpToIso_inv_comp :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F] {c : CategoryTheory.Limits.Cone F}
(hc : CategoryTheory.Limits.IsLimit c) (j : J),
CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.limit.isLimit F).conePointUniqueUpToIso hc).inv
(CategoryTheory.Limits.limit.π F j) =
c.π.app j
The theorem `CategoryTheory.Limits.limit.conePointUniqueUpToIso_inv_comp` states that in category theory, for any category `J`, another category `C`, a functor `F` from `J` to `C`, given `F` has a limit and `c` is a limit cone of `F`, the composition of the inverse of the isomorphism between the limit cone and `c` and the projection from the limit object of `F` to a value `j` of `J` is equal to the morphism from `c` to `j`. This essentially captures the uniqueness property of limit cones in a category up to isomorphism.
More concisely: In category theory, given a limit cone `c` of a functor `F` from a category `J` to `C` with limit, the composition of the inverse of the limit cone's isomorphism with the projection from the limit object to an object `j` in `J` is equal to the morphism from `c` to `j`.
|
CategoryTheory.Limits.hasLimitOfIso
theorem CategoryTheory.Limits.hasLimitOfIso :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F],
(F ≅ G) → CategoryTheory.Limits.HasLimit G
This theorem states that in the context of category theory, if a functor `F` has a limit, then any functor `G` that is naturally isomorphic to `F` also has a limit. Here, `J` and `C` are the source and target categories, respectively, and the isomorphism between `F` and `G` is a natural isomorphism. So essentially, the limit property is preserved under natural isomorphism between functors.
More concisely: If functors `F : J -> C` and `G : J -> C` are naturally isomorphic and `F` has a limit, then `G` also has a limit with the same limit cone.
|
CategoryTheory.Limits.colimit.w
theorem CategoryTheory.Limits.colimit.w :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasColimit F] {j j' : J} (f : j ⟶ j'),
CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.Limits.colimit.ι F j') =
CategoryTheory.Limits.colimit.ι F j
This theorem, named `CategoryTheory.Limits.colimit.w`, is a fundamental property of colimits in category theory. It states that for any category `J`, any category `C`, any functor `F` from `J` to `C` that has a colimit, and any morphism `f` from an object `j` to an object `j'` in `J`, the composition of the image of `f` under `F` and the co-projection from the image of `j'` under `F` to the colimit of `F` is equal to the co-projection from the image of `j` under `F` to the colimit of `F`. In other words, the following diagram commutes in the category `C`:
```
F.obj j --(F.map f)--> F.obj j' --(colimit.ι F j')--> colimit F
| |
|------------------(colimit.ι F j)--------------|
```
More concisely: Given a category `C`, a functor `F` from a small category `J` to `C` with a colimit, and morphisms `f : j -> j'` in `J`, the diagram of `F` commutes at the colimit, i.e., `F.map f ∘ colimit.ι F j = colimit.ι F j'`.
|
CategoryTheory.Limits.hasLimitsOfShape_of_equivalence
theorem CategoryTheory.Limits.hasLimitsOfShape_of_equivalence :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{J' : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} J'],
(J ≌ J') → ∀ [inst : CategoryTheory.Limits.HasLimitsOfShape J C], CategoryTheory.Limits.HasLimitsOfShape J' C
The theorem `CategoryTheory.Limits.hasLimitsOfShape_of_equivalence` states in category theory that for any two categories `J` and `J'` that are equivalent, denoted as `J ≌ J'`, if `C` is a category that has limits of shape `J`, then `C` also has limits of shape `J'`. This essentially means that limits of a certain shape in a category can be 'transported' along an equivalence between categories.
More concisely: If categories `J` and `J'` are equivalent, then a category `C` with limits of shape `J` has limits of shape `J'`.
|
CategoryTheory.Limits.limit.isoLimitCone_hom_π
theorem CategoryTheory.Limits.limit.isoLimitCone_hom_π :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F]
(t : CategoryTheory.Limits.LimitCone F) (j : J),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.isoLimitCone t).hom (t.cone.π.app j) =
CategoryTheory.Limits.limit.π F j
The theorem `CategoryTheory.Limits.limit.isoLimitCone_hom_π` states that for any category `J` with a functor `F` from `J` to a category `C`, if `C` has a limit for functor `F` and `t` is a limit cone of the functor `F`, then composing the morphism from the limit of `F` to the limit cone `t` with the projection from the limit cone `t` to a value `j` in `J` is equal to the projection from the limit of `F` to the value `j` through the functor `F`.
In other words, this theorem guarantees the commutativity of a specific diagram in the category theory, which relates the limit of a functor, limit cones, and the values of the functor.
More concisely: For any limit cone `t` and limit `l` of a functor `F` from a category `J` to a category `C`, the composition of the morphism from `l` to `t` and the projection `t` to an object `j` in `J` equals the projection `l` to `j` through `F`.
|