CategoryTheory.Limits.IsColimit.uniq_cocone_morphism
theorem CategoryTheory.Limits.IsColimit.uniq_cocone_morphism :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃}
[inst_1 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
{s t : CategoryTheory.Limits.Cocone F}, CategoryTheory.Limits.IsColimit t → ∀ {f f' : t ⟶ s}, f = f'
This theorem states that in the context of category theory, for any given category `J` and a functor `F` from `J` to another category `C`, if we have two cocones `s` and `t` over `F` with `t` being a colimit, then any two morphisms `f` and `f'` from `t` to `s` are equal. This theorem is asserting the uniqueness of such a morphism in a specific category-theoretic context, namely when the starting cocone is a colimit.
More concisely: In category theory, given a category `J`, a functor `F` from `J` to another category `C`, and a colimit cocone `t` over `F`, any two morphisms from `t` to a cocone `s` over `F` are equal.
|
CategoryTheory.Limits.IsColimit.hom_ext
theorem CategoryTheory.Limits.IsColimit.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}
{t : CategoryTheory.Limits.Cocone F},
CategoryTheory.Limits.IsColimit t →
∀ {W : C} {f f' : t.pt ⟶ W},
(∀ (j : J),
CategoryTheory.CategoryStruct.comp (t.ι.app j) f = CategoryTheory.CategoryStruct.comp (t.ι.app j) f') →
f = f'
This theorem, `CategoryTheory.Limits.IsColimit.hom_ext`, states that given any category `J`, any category `C`, and any functor `F` from `J` to `C`, if `t` is a cocone over `F` and is also a colimit, then for any object `W` in `C` and any two morphisms `f` and `f'` from the tip of the cocone `t` to `W`, if for every object `j` in `J` the composition of the morphism from `j` to the tip of the cocone with `f` equals the composition of the same morphism with `f'`, then `f` and `f'` must be equal.
In simpler terms, in the context of category theory, this theorem asserts that two morphisms from a colimit in a category to another object in the category are equal if they yield the same result when composed with each morphism from the indexing category to the colimit. This is a formal statement of the uniqueness property of colimits in a category.
More concisely: Given any category `C`, functor `F` from a small category `J` to `C`, and a colimit `t` of `F`, if for every morphism `j:` `J` → `t` and for all morphisms `f, f'` : `t` → `W` in `C`, `j∘f = j∘f'` implies `f = f'`, then `t` is the unique colimit of `F`.
|
CategoryTheory.Limits.IsColimit.hom_isIso
theorem CategoryTheory.Limits.IsColimit.hom_isIso :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃}
[inst_1 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
{s t : CategoryTheory.Limits.Cocone F},
CategoryTheory.Limits.IsColimit s → CategoryTheory.Limits.IsColimit t → ∀ (f : s ⟶ t), CategoryTheory.IsIso f
The theorem `CategoryTheory.Limits.IsColimit.hom_isIso` states that for any type `J` which forms a category, any type `C` which also forms a category, and any functor `F` from `J` to `C`, if we have two colimits `s` and `t` over `F`, then any cocone morphism `f` from `s` to `t` is an isomorphism, given that `s` and `t` are colimits. In other words, any morphism between colimit cocones in a category is an isomorphism. This reflects the important property in category theory that colimits are unique up to unique isomorphism.
More concisely: Given any functor from a small category to a category, any two colimits of the functor are isomorphic via the unique isomorphism between their colimit cocones.
|
CategoryTheory.Limits.IsColimit.fac_assoc
theorem CategoryTheory.Limits.IsColimit.fac_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}
{t : CategoryTheory.Limits.Cocone F} (self : CategoryTheory.Limits.IsColimit t)
(s : CategoryTheory.Limits.Cocone F) (j : J) {Z : C} (h : s.pt ⟶ Z),
CategoryTheory.CategoryStruct.comp (t.ι.app j) (CategoryTheory.CategoryStruct.comp (self.desc s) h) =
CategoryTheory.CategoryStruct.comp (s.ι.app j) h
The theorem `CategoryTheory.Limits.IsColimit.fac_assoc` states that for any type `J` that is a Category, a Category `C`, a functor `F` from `J` to `C`, a cocone `t` over `F`, and a proof `self` that `t` is a colimit, given another cocone `s` over `F`, an object `j` of `J`, and a morphism `h` from the apex of `s` to some other object `Z` in `C`, the composition of the morphism from `j` in the diagram of `t` and the composition of the unique morphism from `t` to `s` (given by `self.desc s`) with `h`, is equal to the composition of the morphism from `j` in the diagram of `s` with `h`. In other words, this theorem is expressing associativity in the triangle commutative diagram involving two cocones and a morphism in a category.
More concisely: Given a Category `J`, a Category `C`, a functor `F` from `J` to `C`, a colimit cocone `t` over `F` with proof `self` of colimiteness, and another cocone `s` over `F`, for any object `j` in `J` and morphism `h` from the apex of `s` to an object in `C`, the composition of the morphisms from `j` in the diagrams of `t` and `s`, followed by `h`, is equal to the composition of the morphisms from `j` in the diagrams of `s` and `t`, followed by `h`.
|
CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom_fac
theorem CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom_fac :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃}
[inst_1 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {X : C}
(h : (CategoryTheory.yoneda.obj X).comp CategoryTheory.uliftFunctor.{u₁, v₃} ≅ F.cones) {Y : C} (f : Y ⟶ X),
CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom h f =
(CategoryTheory.Limits.IsLimit.OfNatIso.limitCone h).extend f
This theorem states that for any category `J` of type `u₁` and category `C` of type `u₃`, and a functor `F` from `J` to `C`, if `F.cones` is represented by `X` in `C`, then the cone corresponding to a morphism `f` from some object `Y` in `C` to `X`, is the limit cone extended by `f`. In simpler terms, it says that if we have a mapping represented by `X` in the category `C`, a morphism that leads to `X` can be viewed as an extension of the limit cone.
More concisely: For any functor `F` from a category `J` to a category `C`, if `F.cones` is represented by an object `X` in `C` and `f` is a morphism from an object `Y` in `C` to `X`, then the cone on `f` is the limit cone of `F` extended by `f`.
|
CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp
theorem CategoryTheory.Limits.IsLimit.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}
{s t : CategoryTheory.Limits.Cone F} (P : CategoryTheory.Limits.IsLimit s) (Q : CategoryTheory.Limits.IsLimit t)
(j : J), CategoryTheory.CategoryStruct.comp (P.conePointUniqueUpToIso Q).inv (s.π.app j) = t.π.app j
This theorem states that for any category `J` and `C`, and any covariant functor `F` from `J` to `C`, if `s` and `t` are limits of the functor `F`, with `P` certifying that `s` is a limit and `Q` certifying that `t` is a limit, then for any object `j` in the category `J`, the composition of the inverse of the isomorphism from `s.pt` to `t.pt` and the morphism from the limit cone `s` to `j` equals the morphism from the limit cone `t` to `j`. In essence, this shows that the points (or apexes) of the limiting cones `s` and `t` are uniquely determined up to isomorphism.
More concisely: For any covariant functor F from category J to C, if objects s and t in C are limits of F with limit cones certified by P and Q respectively, then the inverse of the isomorphism from s.pt to t.pt equals the morphism from s to j composed with the morphism from j to t for any object j in J.
|
CategoryTheory.Limits.IsColimit.fac
theorem CategoryTheory.Limits.IsColimit.fac :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃}
[inst_1 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
{t : CategoryTheory.Limits.Cocone F} (self : CategoryTheory.Limits.IsColimit t)
(s : CategoryTheory.Limits.Cocone F) (j : J),
CategoryTheory.CategoryStruct.comp (t.ι.app j) (self.desc s) = s.ι.app j
The theorem `CategoryTheory.Limits.IsColimit.fac` states that for any category `J`, category `C`, functor `F` from `J` to `C`, cocone `t` on `F`, instance of `t` being a colimit, another cocone `s` on `F`, and an object `j` in `J`, the composition of the morphism `t.ι.app j` and the morphism `self.desc s` is equal to the morphism `s.ι.app j`. In other words, this theorem is establishing a condition for a diagram involving natural transformations to commute in the context of category theory. This makes `self.desc s` a sort of "universal" morphism from `t` to `s` in the category of cocones, which is characteristic of the notion of colimit in category theory.
More concisely: For any category `J`, functor `F` from `J` to `C`, cocone `t` and `s` on `F` with `t` being a colimit, the morphism `t.ι.app j ∘ s.π.app j = s.ι.app j` for all objects `j` in `J`.
|
CategoryTheory.Limits.IsLimit.uniq_cone_morphism
theorem CategoryTheory.Limits.IsLimit.uniq_cone_morphism :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃}
[inst_1 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
{s t : CategoryTheory.Limits.Cone F}, CategoryTheory.Limits.IsLimit t → ∀ {f f' : s ⟶ t}, f = f'
This theorem states that for any type `J` (viewed as a category under instance `inst`), any type `C` (viewed as a category under instance `inst_1`), any functor `F` from `J` to `C`, and any two cones `s` and `t` over `F`, if `t` is a limit cone, then any two morphisms `f` and `f'` from `s` to `t` must be identical. This is a restatement of the uniqueness property of limit cones in category theory: any two morphisms from a cone to a limit cone are necessarily the same.
More concisely: Given any functor F from category J to category C, any limit cone t over F, and any two morphisms f and f' from a cone s to t, if t is a limit cone, then f and f' are equal.
|
CategoryTheory.Limits.IsLimit.hom_isIso
theorem CategoryTheory.Limits.IsLimit.hom_isIso :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃}
[inst_1 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
{s t : CategoryTheory.Limits.Cone F},
CategoryTheory.Limits.IsLimit s → CategoryTheory.Limits.IsLimit t → ∀ (f : s ⟶ t), CategoryTheory.IsIso f
This theorem states that in the context of category theory, for any given category `J`, an arbitrary category `C`, and a functor `F` from `J` to `C`, if `s` and `t` are limit cones of `F`, then any cone morphism `f` from `s` to `t` is an isomorphism. An isomorphism, in this context, means that the morphism has an inverse morphism, so you can "undo" the mapping from `s` to `t`. Therefore, this theorem describes a fundamental property of limit cones in category theory.
More concisely: In category theory, if two objects in a category are limit cones of the same functor from another category, then any morphism between them is an isomorphism.
|
CategoryTheory.Limits.IsLimit.fac_assoc
theorem CategoryTheory.Limits.IsLimit.fac_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} {t : CategoryTheory.Limits.Cone F}
(self : CategoryTheory.Limits.IsLimit t) (s : CategoryTheory.Limits.Cone F) (j : J) {Z : C} (h : F.obj j ⟶ Z),
CategoryTheory.CategoryStruct.comp (self.lift s) (CategoryTheory.CategoryStruct.comp (t.π.app j) h) =
CategoryTheory.CategoryStruct.comp (s.π.app j) h
The theorem `CategoryTheory.Limits.IsLimit.fac_assoc` is a statement about category theory, specifically about the concept of a "limit" in a category. Given a category `J` and a functor `F` from `J` to a category `C`, and given a cone `t` over `F` and another cone `s` over `F`, if `t` is a limit cone, then for any object `j` in `J` and any morphism `h` from `F.obj j` to any object `Z` in `C`, the composition of the morphism `self.lift s` with the composition of the morphism `t.π.app j` and `h` is equal to the composition of the morphism `s.π.app j` and `h`. This theorem essentially formalizes the universal property of limits in a category in terms of morphism composition.
More concisely: Given a limit cone `t` and another cone `s` over a functor `F` from a category `J` to `C`, if `t` is a limit cone, then for any object `j` in `J` and any morphism `h` from `F j` to any object `Z` in `C`, the composition of `s.π.app j` with `h` is equal to the composition of `t.π.app j` with `h` and `self.lift s h`.
|
CategoryTheory.Limits.IsLimit.fac
theorem CategoryTheory.Limits.IsLimit.fac :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃}
[inst_1 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F}
(self : CategoryTheory.Limits.IsLimit t) (s : CategoryTheory.Limits.Cone F) (j : J),
CategoryTheory.CategoryStruct.comp (self.lift s) (t.π.app j) = s.π.app j
The theorem `CategoryTheory.Limits.IsLimit.fac` states that for any category `J`, category `C`, functor `F` from `J` to `C`, a cone `t` of the functor `F` which is a limit, another cone `s` of the functor `F`, and an object `j` in `J`, the composition of the lift morphism from `s` to `t` (given by the fact that `t` is a limit) with the morphism from `t` to `F j` (given by `t` being a cone) equals the morphism from `s` to `F j` (given by `s` being a cone). In mathematical terms, this means that the diagram formed by these morphisms commutes.
More concisely: For any limit cone `t` and cone `s` of a functor `F` from a category `J` to a category `C`, and for any object `j` in `J`, the diagram commutes, i.e., the composition of the lift morphism from `s` to `t` and the morphism from `t` to `F j` equals the morphism from `s` to `F j`.
|
CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom_fac
theorem CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom_fac :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃}
[inst_1 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {X : C}
(h : (CategoryTheory.coyoneda.obj (Opposite.op X)).comp CategoryTheory.uliftFunctor.{u₁, v₃} ≅ F.cocones) {Y : C}
(f : X ⟶ Y),
CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom h f =
(CategoryTheory.Limits.IsColimit.OfNatIso.colimitCocone h).extend f
The theorem `CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom_fac` states that, given a category `J`, a category `C`, and a functor `F` from `J` to `C`, if the functor `F.cocones` is corepresented by an object `X` in `C` (expressed as the natural isomorphism `h` between the composition of the co-Yoneda embedding on `X` and the ulift functor, and `F.cocones`), then for any object `Y` in `C` and any morphism `f` from `X` to `Y`, the cocone corresponding to the morphism `f` is equal to the extension of the colimit cocone (associated with the natural isomorphism `h`) by the morphism `f`. In simpler terms, the theorem explains how to construct the cocone associated with a given morphism under the assumption that `F.cocones` is corepresented by `X`.
More concisely: Given a functor `F: J -> C` with corepresented cocones by an object `X` in `C` via a natural isomorphism `h`, the cocone of any morphism `f: X -> Y` in `C` is equal to the extension of the colimit cocone of `F` by `f`.
|
CategoryTheory.Limits.IsLimit.OfNatIso.cone_fac
theorem CategoryTheory.Limits.IsLimit.OfNatIso.cone_fac :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃}
[inst_1 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {X : C}
(h : (CategoryTheory.yoneda.obj X).comp CategoryTheory.uliftFunctor.{u₁, v₃} ≅ F.cones)
(s : CategoryTheory.Limits.Cone F),
(CategoryTheory.Limits.IsLimit.OfNatIso.limitCone h).extend
(CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone h s) =
s
This theorem states that in the context of a category with objects of some type `J` and `C`, and a given functor `F` from `J` to `C`, if the cones over `F` are represented by an object `X` in `C`, then for any cone `s` over `F`, its extension by the morphism from the terminal object of the cone to `X` (given by the natural isomorphism between the functor `F.cones` and the composition of the Yoneda embedding and the ulift functor) is exactly `s` itself. Essentially, it says that any cone is the extension of the limit cone by the corresponding morphism.
More concisely: In a given category with objects of types `J` and `C` and a functor `F` from `J` to `C`, if an object `X` in `C` represents the cones over `F`, then for any cone `s` over `F`, its extension by the morphism from the terminal object of the cone to `X` is equal to `s` itself.
|
CategoryTheory.Limits.IsColimit.ι_map
theorem CategoryTheory.Limits.IsColimit.ι_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}
{c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (d : CategoryTheory.Limits.Cocone G)
(α : F ⟶ G) (j : J),
CategoryTheory.CategoryStruct.comp (c.ι.app j) (hc.map d α) =
CategoryTheory.CategoryStruct.comp (α.app j) (d.ι.app j)
The theorem `CategoryTheory.Limits.IsColimit.ι_map` states the following:
For any category `J` and any type `C` that is also a category, given two functors `F` and `G` from `J` to `C`, a cocone `c` over `F`, and a morphism `α` from `F` to `G`, if `c` is a co-limit of `F`, then the composition of the application of `c.ι` to `j` and the mapping of `hc` (which is the property that `c` is a co-limit) to `d` under `α` is equal to the composition of the application of `α` to `j` and the application of `d.ι` to `j`.
In other words, this theorem is about the commutativity of a certain diagram involving co-limits in a category. It says that two different ways of getting from one object to another in the category, using the structures of the co-limits and the given morphism, are actually the same.
More concisely: Given functors F and G from category J to C, a co-limit cocone c over F, and a morphism α from F to G, if c is the co-limit of F, then the diagram commutes, that is, c.ι ∘ j = α ∘ j ∘ d.ι for all objects j in J and d in the limit cone of G over j.
|
CategoryTheory.Limits.IsColimit.existsUnique
theorem CategoryTheory.Limits.IsColimit.existsUnique :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃}
[inst_1 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
{t : CategoryTheory.Limits.Cocone F},
CategoryTheory.Limits.IsColimit t →
∀ (s : CategoryTheory.Limits.Cocone F),
∃! d, ∀ (j : J), CategoryTheory.CategoryStruct.comp (t.ι.app j) d = s.ι.app j
This theorem states that for any category `J`, another category `C`, and a functor `F` from `J` to `C`, if `t` is a colimit cocone for `F`, then for any other cocone `s` for `F`, there exists a unique morphism `d` such that for all objects `j` in `J`, the composition of the `j`-th component of the natural transformation of `t` with `d` equals the `j`-th component of the natural transformation of `s`. This is essentially a restatement of the definition of a colimit cocone in category theory, expressed using the `∃!` (there exists exactly one) operator.
More concisely: Given any category `J`, functor `F` from `J` to `C`, and colimit cocone `t` and cocone `s` for `F`, there exists a unique morphism `d` such that for all `j` in `J`, `t.ι j ∘ d = s.ι j`.
|
CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom
theorem CategoryTheory.Limits.IsColimit.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}
{s t : CategoryTheory.Limits.Cocone F} (P : CategoryTheory.Limits.IsColimit s)
(Q : CategoryTheory.Limits.IsColimit t) (j : J),
CategoryTheory.CategoryStruct.comp (s.ι.app j) (P.coconePointUniqueUpToIso Q).hom = t.ι.app j
The theorem `CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom` states that for any category `J` and any category `C`, given a functor `F` from `J` to `C`, two cocones `s` and `t` over `F`, and assuming `P` is a colimit of `s` and `Q` is a colimit of `t`, then for any object `j` in `J`, the composition of the morphism from `j` to the vertex of `s` with the unique isomorphism from the vertex of `s` to the vertex of `t` is equal to the morphism from `j` to the vertex of `t`. In other words, it asserts the uniqueness of the morphism up to a specific isomorphism in the context of category theory, specifically dealing with colimits and cocones.
More concisely: Given any functor F from category J to C, if two cocones over F have equal colimits, then the unique isomorphism between their vertices maps each morphism from an object in J to the first vertex to the corresponding morphism to the second vertex.
|
CategoryTheory.Limits.IsLimit.map_π
theorem CategoryTheory.Limits.IsLimit.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}
(c : CategoryTheory.Limits.Cone F) {d : CategoryTheory.Limits.Cone G} (hd : CategoryTheory.Limits.IsLimit d)
(α : F ⟶ G) (j : J),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.IsLimit.map c hd α) (d.π.app j) =
CategoryTheory.CategoryStruct.comp (c.π.app j) (α.app j)
The theorem `CategoryTheory.Limits.IsLimit.map_π` states that for any two categories `J` and `C`, and any two functors `F` and `G` from `J` to `C`, given a cone `c` over the diagram formed by `F`, another cone `d` over the diagram formed by `G`, where `d` is a limit cone, and a natural transformation `α` from `F` to `G`, the composition of the map induced by `c`, `hd`, and `α` with the projection of `d` at `j` equals the composition of the projection of `c` at `j` with the application of `α` at `j`. This statement is about the compatibility of the mapping of limit cones with the projections of the cones.
More concisely: Given cones $c$ and $d$ over functors $F$ and $G$ from category $J$ to category $C$ with $d$ a limit cone, and a natural transformation $\alpha$ from $F$ to $G$, the maps induced by $c$, $d$, and $\alpha$ commute at each object $j$ in $J$: $(c\_j)^*\alpha\_j = d\_j\circ (F(j) \to G(j))_\alpha$.
|
CategoryTheory.Limits.IsLimit.uniq
theorem CategoryTheory.Limits.IsLimit.uniq :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃}
[inst_1 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F}
(self : CategoryTheory.Limits.IsLimit t) (s : CategoryTheory.Limits.Cone F) (m : s.pt ⟶ t.pt),
(∀ (j : J), CategoryTheory.CategoryStruct.comp m (t.π.app j) = s.π.app j) → m = self.lift s
This theorem, `CategoryTheory.Limits.IsLimit.uniq`, states that for any category `J`, category `C`, functor `F` from `J` to `C`, and a cone `t` of `F`, if `t` is a limit cone and `s` is any other cone of `F` with a morphism `m` from the apex of `s` to the apex of `t`, then `m` is equal to the lift of `s` through `t` (as given by the limit property of `t`) if and only if for every object `j` in `J`, the composition of `m` with the `j`-component of the natural transformation `t.π` is equal to the `j`-component of `s.π`. In less formal terms, this theorem is saying that there is a unique morphism from any other cone to the limit cone that makes the triangle commute for each object in the original category.
More concisely: Given a limit cone and any other cone in a functor from a category to another, with a morphism between their apexes, the morphism is the lift of the other cone through the limit cone if and only if the composition of the morphism with the natural transformation from the limit cone to the original category's object is equal to the natural transformation of the other cone for each object in the category.
|
CategoryTheory.Limits.IsLimit.hom_ext
theorem CategoryTheory.Limits.IsLimit.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} {t : CategoryTheory.Limits.Cone F},
CategoryTheory.Limits.IsLimit t →
∀ {W : C} {f f' : W ⟶ t.pt},
(∀ (j : J),
CategoryTheory.CategoryStruct.comp f (t.π.app j) = CategoryTheory.CategoryStruct.comp f' (t.π.app j)) →
f = f'
This theorem, `CategoryTheory.Limits.IsLimit.hom_ext`, states that in the category theory, given any category `J`, any category `C`, any functor `F` from `J` to `C`, and any cone `t` over `F`, if `t` is a limit cone, then for any object `W` in `C` and any two morphisms `f` and `f'` from `W` to the apex of the cone `t`, if for each object `j` in `J`, the composition of `f` with the morphism from the cone `t` to `j` is equal to the composition of `f'` with the same morphism, then `f` and `f'` are equal.
In other terms, two morphisms into a limit are the same if they yield the same result when composed with each cone morphism. This theorem is a fundamental property of limit cones in category theory.
More concisely: In any category, if a cone over a functor is a limit cone and two morphisms from an object to the apex of the cone have equal compositions with all cone morphisms, then they are equal.
|
CategoryTheory.Limits.IsColimit.ι_map_assoc
theorem CategoryTheory.Limits.IsColimit.ι_map_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}
{c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (d : CategoryTheory.Limits.Cocone G)
(α : F ⟶ G) (j : J) {Z : C} (h : d.pt ⟶ Z),
CategoryTheory.CategoryStruct.comp (c.ι.app j) (CategoryTheory.CategoryStruct.comp (hc.map d α) h) =
CategoryTheory.CategoryStruct.comp (α.app j) (CategoryTheory.CategoryStruct.comp (d.ι.app j) h)
This theorem is a part of category theory in mathematics and it states that for any category `J`, with an instance `inst` of CategoryTheory.Category, and any category `C` with an instance `inst_1` of CategoryTheory.Category, given two functors `F` and `G` from `J` to `C`, a cocone `c` of `F` and `d` of `G`, if `c` is a colimit (`hc` being a proof of this) and a natural transformation `α` from `F` to `G` exists, then for any object `j` of `J` and any morphism `h` from the tip of cocone `d` to an object `Z` in `C`, the composite of the morphism `c.ι.app j` with the composite of the map of the colimit `hc` via `α` to `d` and `h` is equal to the composite of the application of `α` at `j` with the composite of the morphism `d.ι.app j` and `h`. In other words, it's a statement about the commutativity of a certain diagram in the category `C`.
More concisely: Given functors F and G from category J to category C, a cocone (c, hc) of F and (d, hd) of G, a natural transformation α from F to G, and an object Z in C with a morphism h from d's tip to Z, if c is a colimit and α exists, then the composite of hc ∘ c.ι.app j with h is equal to α.app j ∘ hd.ι.app j for all objects j in J.
|
CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp
theorem CategoryTheory.Limits.IsLimit.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}
{s t : CategoryTheory.Limits.Cone F} (P : CategoryTheory.Limits.IsLimit s) (Q : CategoryTheory.Limits.IsLimit t)
(j : J), CategoryTheory.CategoryStruct.comp (P.conePointUniqueUpToIso Q).hom (t.π.app j) = s.π.app j
The theorem `CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp` states that for any category `J`, any category `C`, any functor `F` from `J` to `C`, and any two cones `s` and `t` over `F` for which `s` and `t` are limits, for any object `j` in `J`, the composition of the morphism from the isomorphism between the apexes of the cones `s` and `t` and the cone morphism from the apex of `t` to the object `F(j)` is equal to the cone morphism from the apex of `s` to `F(j)`. In other words, the isomorphism mapping the limit of `F` from `s` to `t` preserves the structure of the cones.
More concisely: For any functors F from J to C, and cones s and t over F that are limits, the isomorphism between their apexes induces equal composition with any morphism from the apex of t to an object F(j) in C, as compared to the morphism from the apex of s to F(j).
|
CategoryTheory.Limits.IsColimit.uniq
theorem CategoryTheory.Limits.IsColimit.uniq :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃}
[inst_1 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
{t : CategoryTheory.Limits.Cocone F} (self : CategoryTheory.Limits.IsColimit t)
(s : CategoryTheory.Limits.Cocone F) (m : t.pt ⟶ s.pt),
(∀ (j : J), CategoryTheory.CategoryStruct.comp (t.ι.app j) m = s.ι.app j) → m = self.desc s
The theorem `CategoryTheory.Limits.IsColimit.uniq` states that in the context of category theory, for any category `J`, any category `C`, a functor `F` from `J` to `C`, a cocone `t` of `F` that is a colimit, another cocone `s` of `F`, and a morphism `m` from the vertex of `t` to the vertex of `s`, if for each object `j` in `J`, the composition of the `j`-component of the natural transformation of `t` with `m` is equal to the `j`-component of the natural transformation of `s`, then `m` is uniquely determined to be the morphism from the vertex of `t` to the vertex of `s` described by the colimit property of `t` with respect to `s`. In other words, it states the uniqueness of the morphism from a colimit cocone to any other cocone, which is one half of the defining property of colimits in category theory.
More concisely: Given any category `J`, category `C`, functor `F` from `J` to `C`, a colimit cocone `t` of `F` and another cocone `s` of `F` with the same image under the natural transformations of `t` and `s`, the unique morphism from the vertex of `t` to the vertex of `s` is the one determined by the colimit property.
|
CategoryTheory.Limits.IsColimit.OfNatIso.cocone_fac
theorem CategoryTheory.Limits.IsColimit.OfNatIso.cocone_fac :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃}
[inst_1 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {X : C}
(h : (CategoryTheory.coyoneda.obj (Opposite.op X)).comp CategoryTheory.uliftFunctor.{u₁, v₃} ≅ F.cocones)
(s : CategoryTheory.Limits.Cocone F),
(CategoryTheory.Limits.IsColimit.OfNatIso.colimitCocone h).extend
(CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone h s) =
s
The theorem `CategoryTheory.Limits.IsColimit.OfNatIso.cocone_fac` states that, for any category `J`, any category `C`, any functor `F` from `J` to `C`, and any object `X` in `C`, if the cocones of `F` is corepresented by `X` (i.e., the embedding of `X` into the co-presheaves on `C` composed with the functor embedding `Type u₁` into `Type v₃` is isomorphic to the cocones of `F`), then for any given cocone `s` of `F`, the result of extending the colimit cocone (generated via the natural isomorphism) by the homomorphism constructed from cocone `s` via the natural isomorphism, is equal to `s` itself. This essentially means that any cocone is the extension of the colimit cocone by the corresponding morphism.
More concisely: Given a category `J`, a functor `F` from `J` to `C`, an object `X` in `C`, and a cocone `s` of `F`, if the cocone `s` is equal to the extension of the colimit cocone of `F` at `X`, then `s` is the colimit cocone itself.
|
CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv
theorem CategoryTheory.Limits.IsColimit.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}
{s t : CategoryTheory.Limits.Cocone F} (P : CategoryTheory.Limits.IsColimit s)
(Q : CategoryTheory.Limits.IsColimit t) (j : J),
CategoryTheory.CategoryStruct.comp (t.ι.app j) (P.coconePointUniqueUpToIso Q).inv = s.ι.app j
This theorem states that for any category `J` with objects of type `u₁` and morphisms of type `v₁`, and another category `C` with objects of type `u₃` and morphisms of type `v₃`, given a functor `F` from `J` to `C`, and two cocones `s` and `t` over `F`, if `P` is a colimit of `s` and `Q` is a colimit of `t`, then for any object `j` in `J`, the composition of the morphism from `j` to the vertex of `t` and the inverse of the unique isomorphism between the vertices of `s` and `t` (which is guaranteed to exist by the property of being a colimit) is equal to the morphism from `j` to the vertex of `s`. This theorem can be thought of as a way of comparing the structures of two colimits over the same diagram, and specifically, it's about how the morphisms into the colimit from the diagram are related to each other.
More concisely: Given functors between categories and two cocones over the same diagram, the inverse of the unique isomorphism between their vertices maps morphisms from any object in the base category to the morphism from that object to the other vertex. In other words, the composition of a morphism with the inverse of the isomorphism between the colimit vertices is equal to the morphism to the first colimit vertex.
|
CategoryTheory.Limits.IsLimit.existsUnique
theorem CategoryTheory.Limits.IsLimit.existsUnique :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃}
[inst_1 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F},
CategoryTheory.Limits.IsLimit t →
∀ (s : CategoryTheory.Limits.Cone F),
∃! l, ∀ (j : J), CategoryTheory.CategoryStruct.comp l (t.π.app j) = s.π.app j
This theorem states that, given a limit cone `t` for a functor `F` from a category `J` to a category `C`, for any other cone `s` over `F`, there exists a unique morphism `l` from `s` to `t` such that, for all objects `j` in `J`, the composition of `l` and the morphism from `t` to `F(j)` equals the morphism from `s` to `F(j)`. In other words, `l` makes the diagram commute for each `j`. This is essentially restating the definition of a limit cone in terms of the unique existence operator `∃!`.
More concisely: Given any functor `F` from a category `J` to `C` and limit cones `t` and `s` over `F`, there exists a unique morphism `l` from `s` to `t` making all diagram commutes: `l ∘ t(j) = s(j)` for all `j` in `J`.
|