CategoryTheory.Limits.CoconeMorphism.w
theorem CategoryTheory.Limits.CoconeMorphism.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}
{A B : CategoryTheory.Limits.Cocone F} (self : CategoryTheory.Limits.CoconeMorphism A B) (j : J),
CategoryTheory.CategoryStruct.comp (A.ι.app j) self.hom = B.ι.app j
This theorem states that for any category `J`, a category `C`, a functor `F` from `J` to `C`, and two cocones `A` and `B` over `F`, any cocone morphism `self` from `A` to `B` satisfies a commutative condition. More specifically, the composition of the application of the natural transformation `A.ι` at a specific object `j` in `J` and the morphism `self.hom`, is equal to the application of the natural transformation `B.ι` at the same object `j`. This is often referred to as the triangle formed by the two natural transformations and `hom` commuting.
More concisely: For any functor $F$ from category $J$ to category $C$, and any two cocones $A$ and $B$ over $F$ with a cocone morphism $self$ between them, the diagram commutes: $A.ι\_j \circ self.hom\_j = B.ι\_j$, for all objects $j$ in $J$.
|
CategoryTheory.Limits.Cocone.w
theorem CategoryTheory.Limits.Cocone.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}
(c : CategoryTheory.Limits.Cocone F) {j j' : J} (f : j ⟶ j'),
CategoryTheory.CategoryStruct.comp (F.map f) (c.ι.app j') = c.ι.app j
The theorem `CategoryTheory.Limits.Cocone.w` states that for any category `J` and another category `C` along with a functor `F` from `J` to `C` and a cocone `c` of `F`, for any two objects `j` and `j'` in `J` and a morphism `f` from `j` to `j'`, the composition of `F` mapping `f` and the application of `c.ι.app` to `j'` is equal to the application of `c.ι.app` to `j`. Essentially, this theorem asserts the commutativity of a diagram in the category theory context, specifically involving the cocone structure.
More concisely: For any functor F from category J to C and a cocone c over F, the composition of F(f) and c.ι.app for any morphism f in J is equal to c.ι.app applied to the source of f.
|
CategoryTheory.Limits.ConeMorphism.ext
theorem CategoryTheory.Limits.ConeMorphism.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}
{c c' : CategoryTheory.Limits.Cone F} (f g : c ⟶ c'), f.hom = g.hom → f = g
This theorem states that, in the context of category theory, given two cones `c` and `c'` over a functor `F` from a category `J` to a category `C`, if two morphisms `f` and `g` exist from `c` to `c'` such that their homomorphisms are equal, then `f` and `g` themselves must be equal. This is essentially a statement about the uniqueness of such morphisms in this context.
More concisely: In category theory, if two cones over a functor have equal homomorphisms, then their morphisms are equal.
|
CategoryTheory.Limits.coconeOfConeLeftOp_ι_app
theorem CategoryTheory.Limits.coconeOfConeLeftOp_ι_app :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃}
[inst_1 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ}
(c : CategoryTheory.Limits.Cone F.leftOp) (j : J),
(CategoryTheory.Limits.coconeOfConeLeftOp c).ι.app j = (c.π.app (Opposite.op j)).op
This theorem states that in category theory, for any category J (of objects `u₁` and morphisms `v₁`), any category C (of objects `u₃` and morphisms `v₃`), any contravariant functor F from J to the opposite category of C, any cone c on the opposite functor of F, and any object j in J, the application of the natural transformation `ι` of the cocone derived from c by `coconeOfConeLeftOp` to the object j is equal to the opposite of the application of the natural transformation `π` of the cone c to the opposite of the object j.
More concisely: For any contravariant functor F from category J to the opposite category of C, any cone c on the opposite functor of F, and any object j in J, the natural transformation from the cocone derived from c to j is equal to the opposite of the natural transformation from c to the opposite of j.
|
CategoryTheory.Limits.Cone.w
theorem CategoryTheory.Limits.Cone.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} (c : CategoryTheory.Limits.Cone F)
{j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (c.π.app j) (F.map f) = c.π.app j'
This theorem is a statement about categories, limits, cones, and functors in category theory. The theorem states that for any type `J` and type `C` (both categories), and a functor `F` from `J` to `C`, given a cone `c` over the functor `F`, for any two objects `j` and `j'` in `J` and a morphism `f` from `j` to `j'`, the composition of the morphism `c.π.app j` (the projection of the cone at `j`) and the functor's action on the morphism `f` (represented by `F.map f`) is equal to the projection of the cone at `j'` (represented by `c.π.app j'`). This is a fundamental property of cones in the context of category theory and it is often used to define the limiting property of cones.
More concisely: For any functor F from category J to C and cone c over F, the composition of the projection of the cone at object j in J and the functor's action on a morphism from j to j' equals the projection of the cone at j'.
|
CategoryTheory.Limits.Cocones.cocone_iso_of_hom_iso
theorem CategoryTheory.Limits.Cocones.cocone_iso_of_hom_iso :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃}
[inst_1 : CategoryTheory.Category.{v₃, u₃} C] {K : CategoryTheory.Functor J C}
{c d : CategoryTheory.Limits.Cocone K} (f : c ⟶ d) [i : CategoryTheory.IsIso f.hom], CategoryTheory.IsIso f
This theorem in Lean is about category theory, specifically about cocones and isomorphisms. It states that given a cocone morphism, where the object part of the morphism is an isomorphism, we can produce an isomorphism of cocones. In more detail, for any category `J`, another category `C`, and a functor `K` from `J` to `C`, if `c` and `d` are cocones over `K` and `f` is a morphism from `c` to `d` such that the object part of `f` is an isomorphism, then `f` itself is also an isomorphism.
More concisely: If in a category `C` through a functor `K: J -> C`, cocones `c` and `d` are given over `K`, and `f: c -> d` is a morphism with isomorphic object parts, then `f` is an isomorphism of cocones.
|
CategoryTheory.Limits.CoconeMorphism.ext
theorem CategoryTheory.Limits.CoconeMorphism.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}
{c c' : CategoryTheory.Limits.Cocone F} (f g : c ⟶ c'), f.hom = g.hom → f = g
This theorem states that in the context of category theory, given two categories `J` and `C`, and a functor `F` from `J` to `C`, if we have two cocones `c` and `c'` over `F`, and two morphisms `f` and `g` from `c` to `c'`, then if the morphism `f.hom` is equal to `g.hom`, it implies that `f` is equal to `g`. In simpler terms, it states that two cocone morphisms between the same pair of cocones are equal if their underlying morphisms are equal.
More concisely: In category theory, if two cocones over the same functor have equal morphisms between them, then the cocones are equal.
|
CategoryTheory.Limits.Cones.cone_iso_of_hom_iso
theorem CategoryTheory.Limits.Cones.cone_iso_of_hom_iso :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃}
[inst_1 : CategoryTheory.Category.{v₃, u₃} C] {K : CategoryTheory.Functor J C}
{c d : CategoryTheory.Limits.Cone K} (f : c ⟶ d) [i : CategoryTheory.IsIso f.hom], CategoryTheory.IsIso f
This theorem states that given a cone morphism, if the object part of this morphism is an isomorphism in a category, then the entire cone morphism is an isomorphism. Specifically, it applies to any category with objects of type `J` and `C`, a functor `K` from `J` to `C`, and two cones `c` and `d` over `K`. The morphism `f` is from `c` to `d`, and if `f.hom` (the object part of the morphism) is an isomorphism, then `f` is also an isomorphism.
More concisely: If the object part of a cone morphism is an isomorphism in a category, then the entire morphism is an isomorphism.
|
CategoryTheory.Limits.ConeMorphism.w
theorem CategoryTheory.Limits.ConeMorphism.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}
{A B : CategoryTheory.Limits.Cone F} (self : CategoryTheory.Limits.ConeMorphism A B) (j : J),
CategoryTheory.CategoryStruct.comp self.hom (B.π.app j) = A.π.app j
The theorem `CategoryTheory.Limits.ConeMorphism.w` states that for any category `J`, any category `C`, any functor `F` from `J` to `C`, any cones `A` and `B` over `F`, any cone morphism `self` from `A` to `B`, and any object `j` in `J`, the composition of the morphism `self.hom` with the application of the natural transformation `B.π` at `j` is equal to the application of the natural transformation `A.π` at `j`. In other words, it says that the triangle formed by the two natural transformations and `self.hom` commutes.
More concisely: For any category J, functor F from J to C, cones A and B over F, cone morphism self from A to B, and object j in J, we have A.π(j) ∘ self.hom = B.π(j).
|