CategoryTheory.Limits.prod.lift_fst_comp_snd_comp
theorem CategoryTheory.Limits.prod.lift_fst_comp_snd_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C}
[inst_1 : CategoryTheory.Limits.HasBinaryProduct W Y] [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Z]
(g : W ⟶ X) (g' : Y ⟶ Z),
CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst g)
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd g') =
CategoryTheory.Limits.prod.map g g'
This theorem states that in any category `C` with binary products, for any four objects `W`, `X`, `Y`, and `Z`, and any two morphisms `g : W ⟶ X` and `g' : Y ⟶ Z`, the composition of `g` with the projection to the first component and `g'` with the projection to the second component, when applied to the limit of the pair `(W, Y)`, is the same as the morphism induced by `g` and `g'` on the product of `W` and `Y`. This is essentially an application of the universal property of a product in category theory.
More concisely: In any category with binary products, the morphism from the product of two objects to the product of their images under two morphisms is equal to the composition of the morphisms with the projections to the first and second components.
|
CategoryTheory.Limits.coprod.inr_map
theorem CategoryTheory.Limits.coprod.inr_map :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C}
[inst_1 : CategoryTheory.Limits.HasBinaryCoproduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct Y Z]
(f : W ⟶ Y) (g : X ⟶ Z),
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.Limits.coprod.map f g) =
CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.coprod.inr
The theorem `CategoryTheory.Limits.coprod.inr_map` states that for any category `C` and any four objects `W`, `X`, `Y`, and `Z` in `C`, given that `W` and `X` form a binary coproduct, and `Y` and `Z` also form a binary coproduct, then for any morphisms `f` from `W` to `Y` and `g` from `X` to `Z`, the composition of the inclusion map from the second component of the coproduct (`coprod.inr`) and the coproduct map derived from `f` and `g` (`coprod.map f g`) is equal to the composition of `g` and `coprod.inr`. This principle reflects the commutativity of the diagram in the categorical sense.
More concisely: For any objects `W`, `X`, `Y`, and `Z` in a category `C` forming binary coproducts, and morphisms `f: W → Y` and `g: X → Z`, the diagram commutes: `coprod.inr ∘ coprod.map f g = g ∘ coprod.inr`.
|
CategoryTheory.Limits.braid_natural
theorem CategoryTheory.Limits.braid_natural :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
{W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f g)
(CategoryTheory.Limits.prod.braiding Y W).hom =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.braiding X Z).hom
(CategoryTheory.Limits.prod.map g f)
The theorem `CategoryTheory.Limits.braid_natural` states that for any category `C` equipped with binary products, and for any objects `W, X, Y, Z` in `C` and morphisms `f : X ⟶ Y` and `g : Z ⟶ W`, the braiding isomorphism, which swaps the order of the product, can be moved through a map. Concretely, first mapping `(f, g)` and then applying the braiding isomorphism is the same as first applying the braiding isomorphism and then mapping `(g, f)`. This is a statement about the commutativity in the category with respect to the braiding and mapping operations.
More concisely: For any category with binary products, given objects X, Y, Z and morphisms f : X ⟶ Y and g : Z ⟶ W, the braiding isomorphism commutes with the product of morphisms: (g, f) * braid = braid * (f, g).
|
CategoryTheory.Limits.prod.map_map
theorem CategoryTheory.Limits.prod.map_map :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A₁ A₂ A₃ B₁ B₂ B₃ : C}
[inst_1 : CategoryTheory.Limits.HasBinaryProduct A₁ B₁] [inst_2 : CategoryTheory.Limits.HasBinaryProduct A₂ B₂]
[inst_3 : CategoryTheory.Limits.HasBinaryProduct A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f g) (CategoryTheory.Limits.prod.map h k) =
CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.comp f h)
(CategoryTheory.CategoryStruct.comp g k)
The theorem `CategoryTheory.Limits.prod.map_map` states that for any category `C` and six objects `A₁, A₂, A₃, B₁, B₂, B₃` in this category, given that we have binary products `A₁ x B₁`, `A₂ x B₂`, and `A₃ x B₃` and morphisms `f : A₁ ⟶ A₂`, `g : B₁ ⟶ B₂`, `h : A₂ ⟶ A₃`, and `k : B₂ ⟶ B₃`, the composition of `prod.map f g` and `prod.map h k` is the same as `prod.map` of the compositions `f ≫ h` and `g ≫ k`. In other words, the process of mapping across a product commutes with the process of composition of morphisms.
More concisely: For any category C and morphisms f : A₁ ⟶ A₂, g : B₁ ⟶ B₂, h : A₂ ⟶ A₃, and k : B₂ ⟶ B₃, the diagram commutes:
prod.map f g ∘ prod.map h k = prod.map (f ∫ h) (g ∫ k)
Here, ∘ denotes composition of morphisms and ∫ denotes the product construction.
|
CategoryTheory.Limits.coprodComparison_inv_natural
theorem CategoryTheory.Limits.coprodComparison_inv_natural :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
(F : CategoryTheory.Functor C D) {A A' B B' : C} [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A B]
[inst_3 : CategoryTheory.Limits.HasBinaryCoproduct A' B']
[inst_4 : CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)]
[inst_5 : CategoryTheory.Limits.HasBinaryCoproduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B')
[inst_6 : CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)]
[inst_7 : CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A' B')],
CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A B))
(CategoryTheory.Limits.coprod.map (F.map f) (F.map g)) =
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.coprod.map f g))
(CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A' B'))
The theorem `CategoryTheory.Limits.coprodComparison_inv_natural` states that for any category `C` and `D`, and a functor `F` from `C` to `D`, if `A`, `A'`, `B`, `B'` are objects in `C` that have binary coproducts, and the binary coproducts of the images of these objects under `F` also exist, then for any morphisms `f : A ⟶ A'` and `g : B ⟶ B'`, if the coproduct comparison morphism is an isomorphism, then its inverse is natural. In other words, the inverse of the coproduct comparison morphism composed with the map of the coproducts is equal to the functor applied to the coproduct map, composed with the inverse of the comparison of the coproduct.
More concisely: If `F : C -> D` is a functor between categories `C` and `D` such that for any objects `A, A', B, B` with binary coproducts in `C` and their images `FA, FA', FB, FB` have binary coproducts in `D`, then the naturality of the inverse of the coproduct comparison morphisms for `F` holds.
|
CategoryTheory.Limits.coprod.inl_map_assoc
theorem CategoryTheory.Limits.coprod.inl_map_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C}
[inst_1 : CategoryTheory.Limits.HasBinaryCoproduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct Y Z]
(f : W ⟶ Y) (g : X ⟶ Z) {Z_1 : C} (h : Y ⨿ Z ⟶ Z_1),
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f g) h) =
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h)
The theorem `CategoryTheory.Limits.coprod.inl_map_assoc` states that for any category `C`, given objects `W`, `X`, `Y`, `Z` and `Z_1` in `C` and morphisms `f: W ⟶ Y`, `g: X ⟶ Z`, and `h: Y ⨿ Z ⟶ Z_1` where `⨿` denotes the coproduct and provided that the binary coproducts `W ⨿ X` and `Y ⨿ Z` exist, the composition of morphisms `CategoryTheory.Limits.coprod.inl` and `(CategoryTheory.Limits.coprod.map f g) ≫ h` is equal to the composition of `f` and `CategoryTheory.Limits.coprod.inl ≫ h`. In simpler terms, it asserts a specific associativity property of the morphism composition in the context of category theory, specifically involving the inclusion map from the first component of the coproduct and the map from the binary coproduct.
More concisely: For any objects `W`, `X`, `Y`, `Z`, and `Z_1` in a category `C` with binary coproducts `W ⨿ X` and `Y ⨿ Z`, and given morphisms `f: W ⟶ Y`, `g: X ⟶ Z`, and `h: Y ⨿ Z ⟶ Z_1`, the composition of `f`, `CategoryTheory.Limits.coprod.inl`, and `h` equals the composition of `CategoryTheory.Limits.coprod.inl`, `g`, and `h`.
|
CategoryTheory.Limits.prod.functor.proof_1
theorem CategoryTheory.Limits.prod.functor.proof_1 :
∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
(X Y : C), CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.pair X Y)
The theorem `CategoryTheory.Limits.prod.functor.proof_1` states that for any category `C` that has binary products, and for any two objects `X` and `Y` in `C`, there is a limit for the functor which maps a discrete category with two objects (a "walking pair") to `X` and `Y` in `C`. In essence, it asserts the existence of product objects for any pair of objects in a category with binary products.
More concisely: For any category with binary products, the product of two objects exists.
|
CategoryTheory.Limits.coprod.map_id_id
theorem CategoryTheory.Limits.coprod.map_id_id :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
[inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X Y],
CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) =
CategoryTheory.CategoryStruct.id (X ⨿ Y)
The theorem `CategoryTheory.Limits.coprod.map_id_id` states that for any category `C` and any two objects `X` and `Y` in `C` that have a binary coproduct, the mapping from the binary coproduct of `X` and `Y` to itself using the identity morphisms of `X` and `Y` is the same as the identity morphism of the binary coproduct of `X` and `Y`. In other words, in the category theory context, mapping a binary coproduct to itself with identity morphisms doesn't change the binary coproduct, which is a fundamental property of identity mappings.
More concisely: Given a category `C` and objects `X` and `Y` with a binary coproduct, the identity mappings of `X` and `Y` to their coproduct are equal to the coproduct of the identity mappings of `X` and `Y`.
|
CategoryTheory.Limits.prodComparison_fst
theorem CategoryTheory.Limits.prodComparison_fst :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
(F : CategoryTheory.Functor C D) (A B : C) [inst_2 : CategoryTheory.Limits.HasBinaryProduct A B]
[inst_3 : CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)],
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A B) CategoryTheory.Limits.prod.fst =
F.map CategoryTheory.Limits.prod.fst
This theorem, `CategoryTheory.Limits.prodComparison_fst`, states that for any two types `C` and `D`, that are categories, and a functor `F` from `C` to `D`, if `A` and `B` are objects in the category `C` and both binary products `A x B` in `C` and `F.obj A x F.obj B` in `D` exist, then the composition of the product comparison map `prodComparison F A B` and the projection to the first factor `prod.fst` in `D` is equal to the image under `F` of the projection to the first factor `prod.fst` in `C`. In simpler terms, this theorem asserts a key property about the functoriality of the product in the context of category theory: the mapping of the projection of the product under a functor coincides with the projection of the mapped product.
More concisely: Given any categories C and D, functor F from C to D, objects A and B in C with existing binary products, the diagram commutes: prodComparison F A B ∘ prod.fst (D) = F ∘ prod.fst (C).
|
CategoryTheory.Limits.coprod.desc_comp
theorem CategoryTheory.Limits.coprod.desc_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {V W X Y : C}
[inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X Y] (f : V ⟶ W) (g : X ⟶ V) (h : Y ⟶ V),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.desc g h) f =
CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp g f)
(CategoryTheory.CategoryStruct.comp h f)
The theorem `CategoryTheory.Limits.coprod.desc_comp` in Lean 4 states that for any category `C` and objects `V`, `W`, `X`, `Y` in `C`, if the binary coproduct of `X` and `Y` exists, then for any morphisms `f : V ⟶ W`, `g : X ⟶ V`, and `h : Y ⟶ V` in `C`, the composition of the morphism `f` with the morphism induced by `g` and `h` from the coproduct `X ⨿ Y` to `V` is equal to the morphism from `X ⨿ Y` to `W` induced by the compositions of `f` with `g` and `f` with `h` respectively. In mathematical notation, this is saying that `(coprod.desc g h) ≫ f = coprod.desc (g ≫ f) (h ≫ f)`.
More concisely: For any category `C`, objects `V`, `W`, `X`, `Y` in `C`, and morphisms `f : V ⟶ W`, `g : X ⟶ V`, `h : Y ⟶ V`, if the binary coproduct of `X` and `Y` exists, then `(coprod.desc g h) ≫ f = coprod.desc (g ≫ f) (h ≫ f)`.
|
CategoryTheory.Limits.prod.lift_fst
theorem CategoryTheory.Limits.prod.lift_fst :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C}
[inst_1 : CategoryTheory.Limits.HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift f g) CategoryTheory.Limits.prod.fst = f
The theorem `CategoryTheory.Limits.prod.lift_fst` states that for any category `C` and objects `W`, `X`, and `Y` in `C`, if `X` and `Y` have a binary product, then for any morphisms `f : W ⟶ X` and `g : W ⟶ Y`, the composition of the morphism induced by `f` and `g` using `prod.lift` and the projection to the first component of the product (`prod.fst`) equals `f`. In other words, it illustrates one of the universal properties of the product in a category, namely that the composed map `W ⟶ X ⨯ Y ⟶ X` is the same as the original map `W ⟶ X`.
More concisely: For any object `W` in a category `C` with products, and morphisms `f : W ⟶ X` and `g : W ⟶ Y` where `X` and `Y` have a binary product, `prod.lift(prod.fst ∘ g) = f` holds.
|
CategoryTheory.Limits.prod.symmetry
theorem CategoryTheory.Limits.prod.symmetry :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P Q : C)
[inst_1 : CategoryTheory.Limits.HasBinaryProduct P Q] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Q P],
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.braiding P Q).hom
(CategoryTheory.Limits.prod.braiding Q P).hom =
CategoryTheory.CategoryStruct.id (P ⨯ Q)
The theorem `CategoryTheory.Limits.prod.symmetry` states that in a category `C` with binary products, for any two objects `P` and `Q` in `C`, the composition of the braiding isomorphism from `P ⨯ Q` to `Q ⨯ P` and back to `P ⨯ Q` is the identity morphism on `P ⨯ Q`. Here, the braiding isomorphism is a categorical concept that describes the interchange of the factors in a binary product (i.e., switching the roles of `P` and `Q`).
More concisely: In a category with binary products, the braiding isomorphism from `P ⨯ Q` to `Q ⨯ P` and its inverse are equal to the identity morphism on `P ⨯ Q`.
|
CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inr
theorem CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inr :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C},
CategoryTheory.Limits.IsInitial X →
∀ (c : CategoryTheory.Limits.BinaryCofan X Y),
Nonempty (CategoryTheory.Limits.IsColimit c) ↔ CategoryTheory.IsIso c.inr
The theorem `CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inr` states that for any category `C` and any objects `X` and `Y` in `C`, if `X` is initial in the category `C`, then a binary cofan `c` on the objects `X` and `Y` is a colimit if and only if the second inclusion map (denoted by `CategoryTheory.Limits.BinaryCofan.inr c`) is an isomorphism in the category `C`. In other words, the existence of a colimit for the cofan is equivalent to the second inclusion map being an isomorphism, given that `X` is an initial object in the category.
More concisely: For any category C and objects X, Y in C, if X is initial and the second inclusion map in a binary cofan on X and Y is an isomorphism, then the cofan is a colimit.
|
CategoryTheory.Limits.prod.comp_lift
theorem CategoryTheory.Limits.prod.comp_lift :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {V W X Y : C}
[inst_1 : CategoryTheory.Limits.HasBinaryProduct X Y] (f : V ⟶ W) (g : W ⟶ X) (h : W ⟶ Y),
CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.prod.lift g h) =
CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp f g)
(CategoryTheory.CategoryStruct.comp f h)
This theorem, titled `CategoryTheory.Limits.prod.comp_lift`, states that for any category `C` and objects `V`, `W`, `X`, and `Y` in `C`, if `X` and `Y` have a binary product, then for any morphisms `f : V ⟶ W`, `g : W ⟶ X`, and `h : W ⟶ Y`, the composite of `f` with the morphism induced by `g` and `h` via the product lifting operation (`prod.lift g h : W ⟶ X ⨯ Y`) is equal to the morphism induced by the composites `f ≫ g : V ⟶ X` and `f ≫ h : V ⟶ Y`. In other words, lifting to the product and then composing with `f` is the same as first composing with `f` and then lifting to the product. The theorem thus expresses a kind of associativity property of the product lifting operation with respect to composition of morphisms in a category.
More concisely: For any category `C`, objects `V`, `W`, `X`, and `Y` with a binary product, and morphisms `f : V ⟶ W`, `g : W ⟶ X`, and `h : W ⟶ Y`, the composite `f ∘ prod.lift g h` is equal to `prod.lift (f ∘ g) (f ∘ h)`.
|
CategoryTheory.Limits.prod.hom_ext
theorem CategoryTheory.Limits.prod.hom_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C}
[inst_1 : CategoryTheory.Limits.HasBinaryProduct X Y] {f g : W ⟶ X ⨯ Y},
CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.prod.fst =
CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.prod.fst →
CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.prod.snd =
CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.prod.snd →
f = g
The theorem `CategoryTheory.Limits.prod.hom_ext` states that in a category `C` with a binary product of objects `X` and `Y`, for any two morphisms `f` and `g` from an object `W` to the binary product `X ⨯ Y`, if the composition of `f` with the projection to the first component of the product equals the composition of `g` with the same projection, and similarly for the second component, then `f` must be equal to `g`. In other words, a morphism to a binary product in a category is determined by its compositions with the projection morphisms.
More concisely: In a category with binary products, if two morphisms from an object to the product have the same compositions with both projection morphisms, then they are equal.
|
CategoryTheory.Limits.coprod.inl_map
theorem CategoryTheory.Limits.coprod.inl_map :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C}
[inst_1 : CategoryTheory.Limits.HasBinaryCoproduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct Y Z]
(f : W ⟶ Y) (g : X ⟶ Z),
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.Limits.coprod.map f g) =
CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.coprod.inl
The theorem `CategoryTheory.Limits.coprod.inl_map` states that in any category `C`, given two binary coproducts `W ⨿ X` and `Y ⨿ Z`, and morphisms `f : W ⟶ Y` and `g : X ⟶ Z`, the composition of the inclusion map from the first component of the coproduct (`coprod.inl`) with the map induced by `f` and `g` on the coproducts (`coprod.map f g`) is equal to the composition of `f` with the inclusion map from the first component of the coproduct. This is essentially a property that relates the inclusion of elements into the coproduct and the mapping of the coproducts under given morphisms.
More concisely: In any category, the composition of the inclusion map of the first component of a binary coproduct with the map induced by two morphisms between the coproducts is equal to the composition of those morphisms with the inclusion map of the first component.
|
CategoryTheory.Limits.coprodComparison_natural
theorem CategoryTheory.Limits.coprodComparison_natural :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
(F : CategoryTheory.Functor C D) {A A' B B' : C} [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A B]
[inst_3 : CategoryTheory.Limits.HasBinaryCoproduct A' B']
[inst_4 : CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)]
[inst_5 : CategoryTheory.Limits.HasBinaryCoproduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B'),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprodComparison F A B)
(F.map (CategoryTheory.Limits.coprod.map f g)) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (F.map f) (F.map g))
(CategoryTheory.Limits.coprodComparison F A' B')
This theorem, named `CategoryTheory.Limits.coprodComparison_natural`, states that for any two categories `C` and `D`, and a functor `F` from `C` to `D`, if `A`, `A'`, `B`, `B'` are objects in `C` that have binary coproducts, and the images of these objects under `F` also have binary coproducts, then the composition of the coproduct comparison of `A` and `B` under `F` with the functor's mapping of the coproduct map of morphisms `f` and `g` is equal to the composition of the coproduct map of the functor's mapping of `f` and `g` with the coproduct comparison of `A'` and `B'` under `F`. This demonstrates the naturality of the coproduct comparison morphism in both arguments.
More concisely: Given functors F from category C to category D and objects A, A', B, B' in C with binary coproducts, if the images of A, B under F have binary coproducts and the coproduct maps commute with F, then the coproduct comparison morphisms commute naturally with F.
|
CategoryTheory.Limits.coprod.inr_map_assoc
theorem CategoryTheory.Limits.coprod.inr_map_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C}
[inst_1 : CategoryTheory.Limits.HasBinaryCoproduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct Y Z]
(f : W ⟶ Y) (g : X ⟶ Z) {Z_1 : C} (h : Y ⨿ Z ⟶ Z_1),
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f g) h) =
CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr h)
The theorem `CategoryTheory.Limits.coprod.inr_map_assoc` states that in any category `C` with binary coproducts, for objects `W`, `X`, `Y`, `Z`, and `Z_1` in `C`, and morphisms `f : W ⟶ Y`, `g : X ⟶ Z`, and `h : Y ⨿ Z ⟶ Z_1`, the composition of the inclusion map from the second component of the coproduct (`coprod.inr`) with the composition of the coproduct map of `f` and `g` with `h` is equal to the composition of `g` with the composition of `coprod.inr` with `h`. In other words, the diagram commutes: if we first include `X` into `X ⨿ Y` using `coprod.inr`, then map `W ⟶ Y` and `X ⟶ Z` to `Y ⨿ Z`, and finally use `h` to map to `Z_1`, this is the same as first mapping `X` to `Z` using `g`, then including into `Y ⨿ Z`, and finally using `h` to map to `Z_1`.
More concisely: In any category with binary coproducts, the composition of `h` with `coprod.inr` and the coproduct map of `f` and `g`, is equal to the composition of `g` with `coprod.inr` and `h`.
|
CategoryTheory.Limits.prod.lift_snd
theorem CategoryTheory.Limits.prod.lift_snd :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C}
[inst_1 : CategoryTheory.Limits.HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift f g) CategoryTheory.Limits.prod.snd = g
The theorem `CategoryTheory.Limits.prod.lift_snd` states that for a category `C`, and objects `W`, `X`, and `Y` in `C`, if `X` and `Y` have a binary product, then for any two morphisms `f : W ⟶ X` and `g : W ⟶ Y`, the composition of the morphism induced by `prod.lift f g` and the projection to the second component of the product (`CategoryTheory.Limits.prod.snd`) is equal to `g`. In other words, given any two morphisms from `W` to `X` and `W` to `Y`, the diagram commutes, i.e., the path via the product and then projection to `Y` is the same as the direct path to `Y` via `g`.
More concisely: Given a category with binary products, for any two morphisms from a object W to X and Y, where X and Y have a product, the diagram commuting from the product and the projections holds, that is, `prod.snd (prod.lift f g) = g`.
|
CategoryTheory.Limits.coprod.inr_desc
theorem CategoryTheory.Limits.coprod.inr_desc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C}
[inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W),
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.Limits.coprod.desc f g) = g
The theorem `CategoryTheory.Limits.coprod.inr_desc` states that in any category `C` which has binary coproducts, for any three objects `X`, `Y`, and `W` in `C`, and for any two morphisms `f` from `X` to `W` and `g` from `Y` to `W`, the composition of the inclusion map from the second component of the coproduct (`CategoryTheory.Limits.coprod.inr`) and the morphism induced by `f` and `g` (`CategoryTheory.Limits.coprod.desc f g`) is equal to `g`. In other words, when we map `Y` into the coproduct `X ⨿ Y` and then map to `W` using the morphism defined by `f` and `g`, we get the same result as if we had directly used `g` to map `Y` to `W`.
More concisely: In any category with binary coproducts, for any objects X, Y, and W, and morphisms f : X -> W and g : Y -> W, the composition of the inclusion map of the second component of the coproduct (inr : Y -> X ⨿ Y) and the morphism induced by f and g (desc f g : Y -> W) equals g.
|
CategoryTheory.Limits.coprod.map_map
theorem CategoryTheory.Limits.coprod.map_map :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A₁ A₂ A₃ B₁ B₂ B₃ : C}
[inst_1 : CategoryTheory.Limits.HasBinaryCoproduct A₁ B₁]
[inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A₂ B₂]
[inst_3 : CategoryTheory.Limits.HasBinaryCoproduct A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f g) (CategoryTheory.Limits.coprod.map h k) =
CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.comp f h)
(CategoryTheory.CategoryStruct.comp g k)
This theorem belongs to the domain of category theory within mathematics. It states that given a category `C` with objects `A₁`, `A₂`, `A₃`, `B₁`, `B₂`, `B₃` and binary coproducts for pairs `(A₁, B₁)`, `(A₂, B₂)`, `(A₃, B₃)`, and given morphisms `f : A₁ ⟶ A₂`, `g : B₁ ⟶ B₂`, `h : A₂ ⟶ A₃`, and `k : B₂ ⟶ B₃`, the composition of coproduct maps `coprod.map f g` and `coprod.map h k` is the same as the coproduct map of composed morphisms `(f ≫ h)` and `(g ≫ k)`. In more informal language, it says that mapping over coproducts (a kind of "combined" object in category theory) can be "interchanged" with composition of morphisms (functions between objects).
More concisely: Given categories `C` with objects `A₁, A₂, A₃, B₁, B₂, B₃` and binary coproducts, for morphisms `f : A₁ ⟶ A₂`, `g : B₁ ⟶ B₂`, `h : A₂ ⟶ A₃`, and `k : B₂ ⟶ B₃`, the map `coprod.map f g ≫ coprod.map h k` is equal to `coprod.map (f ≫ h) (g ≫ k)`.
|
CategoryTheory.Limits.coprod.hom_ext
theorem CategoryTheory.Limits.coprod.hom_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C}
[inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X Y] {f g : X ⨿ Y ⟶ W},
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl f =
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl g →
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr f =
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr g →
f = g
The theorem `CategoryTheory.Limits.coprod.hom_ext` states that in a category `C` with binary coproduct of objects `X` and `Y`, for any two morphisms `f` and `g` from the coproduct `X ⨿ Y` to another object `W`, if the composition of `f` and the inclusion map from `X` to `X ⨿ Y` is equal to the composition of `g` and the same inclusion map, and similarly for the inclusion from `Y`, then `f` must be equal to `g`. This can be viewed as a uniqueness property of morphisms out of the binary coproduct.
More concisely: In a category with binary coproducts, if for morphisms `f` and `g` from `X ⨿ Y` to `W`, the composition of `f` with the inclusion of `X` is equal to the composition of `g` with the inclusion of `X`, and the same for the inclusion of `Y`, then `f` is equal to `g`.
|
CategoryTheory.Limits.prod.map_fst_assoc
theorem CategoryTheory.Limits.prod.map_fst_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C}
[inst_1 : CategoryTheory.Limits.HasBinaryProduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Y Z]
(f : W ⟶ Y) (g : X ⟶ Z) {Z_1 : C} (h : Y ⟶ Z_1),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f g)
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) =
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp f h)
This theorem is named `CategoryTheory.Limits.prod.map_fst_assoc` in the Lean 4 library of category theory, specifically in the part dealing with limits and products. It states that for any category `C`, and any four objects `W, X, Y, Z` in `C`, if `W` and `X` have a binary product, and `Y` and `Z` also have a binary product, and if `f` is a morphism from `W` to `Y`, `g` is a morphism from `X` to `Z`, and `h` is a morphism from `Y` to some object `Z_1`, then the composition of the product map of `f` and `g` with the composition of the projection to the first component and `h` is equal to the composition of the projection to the first component with the composition of `f` and `h`. This is a categorical property related to the interaction between products and morphism composition.
More concisely: Given any category `C` and morphisms `f: W × X → Y`, `g: X → Z`, and `h: Y → Z_1` in `C`, where `W × X` and `Y × Z` are binary products, the diagram commutes: `(π₁₁ × π₂)_*(f × g) = (π₁₁ *) (f * h)`, where `π₁₁` denotes the projection to the first component.
|
Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts._auxLemma.3
theorem Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts._auxLemma.3 :
∀ {α : Sort u_1} [inst : Subsingleton α] (x y : α), (x = y) = True
This theorem, `Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts._auxLemma.3`, states that for any type `α` that is a subsingleton (i.e., a type that has at most one element), any two elements `x` and `y` of type `α` are equal. This is expressed as `(x = y) = True`, where the equality is universally valid for all `x` and `y`. In other words, in a type where there can be at most one distinct value, any two values of that type must necessarily be equal.
More concisely: In a subsingleton type, any two elements are equal.
|
CategoryTheory.Limits.BinaryFan.IsLimit.hom_ext
theorem CategoryTheory.Limits.BinaryFan.IsLimit.hom_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y},
CategoryTheory.Limits.IsLimit s →
∀ {f g : W ⟶ s.pt},
CategoryTheory.CategoryStruct.comp f s.fst = CategoryTheory.CategoryStruct.comp g s.fst →
CategoryTheory.CategoryStruct.comp f s.snd = CategoryTheory.CategoryStruct.comp g s.snd → f = g
This theorem is about the uniqueness of morphisms to the apex of a limiting binary fan in a category. Specifically, given a category `C` and objects `W`, `X`, `Y` in `C`, if `s` is a limiting binary fan over objects `X` and `Y`, then for any two morphisms `f` and `g` from `W` to the apex of `s`, if the compositions of `f` and `g` with the first and second projections of the fan are equal, then `f` and `g` must be the same. This expresses the universal property of a limit in categorical terms.
More concisely: Given a limiting binary fan $s$ in a category $C$ over objects $X$, $Y$, and an object $W$, if for morphisms $f$ and $g$ from $W$ to the apex of $s$, we have $s.p_1 \circ f = s.p_1 \circ g$ and $s.p_2 \circ f = s.p_2 \circ g$, then $f = g$.
|
CategoryTheory.Limits.prod.map_snd
theorem CategoryTheory.Limits.prod.map_snd :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C}
[inst_1 : CategoryTheory.Limits.HasBinaryProduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Y Z]
(f : W ⟶ Y) (g : X ⟶ Z),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f g) CategoryTheory.Limits.prod.snd =
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd g
This theorem is a statement about the behavior of morphisms and binary products in a category. Specifically, it asserts that for any category `C` and given objects `W`, `X`, `Y`, and `Z` in `C`, if `W ⨯ X` and `Y ⨯ Z` are binary products in `C`, and `f` is a morphism from `W` to `Y` and `g` is a morphism from `X` to `Z`, then the composition of `f` and `g` followed by the projection map to the second component of the product is equal to the composition of the projection map to the second component of the product and `g`. In mathematical terms, this can be written as `(f ⨯ g) ∘ π₂ = π₂ ∘ g`, where `π₂` denotes the second projection map.
More concisely: Given any category `C`, morphisms `f: W → Y` and `g: X → Z`, and objects `W`, `X`, `Y`, and `Z` such that `W ⨯ X` and `Y ⨯ Z` are binary products, then `(f ⨯ g) ∘ π₂ = π₂ ∘ g`, where `π₂` denotes the second projection map.
|
CategoryTheory.Limits.coprod.inl_desc
theorem CategoryTheory.Limits.coprod.inl_desc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C}
[inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W),
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.Limits.coprod.desc f g) = f
The theorem `CategoryTheory.Limits.coprod.inl_desc` states that, in any category `C` with a binary coproduct of `X` and `Y`, for any two morphisms `f` from `X` to `W` and `g` from `Y` to `W`, the composition of the inclusion map from the first component of the coproduct (`CategoryTheory.Limits.coprod.inl`) and the morphism induced by `f` and `g` (`CategoryTheory.Limits.coprod.desc f g`) is equal to `f`. In other words, this shows that the coproduct behaves as expected when mapping from one of its components.
More concisely: In any category with binary coproducts, the inclusion map from the first component of the coproduct to the coproduct and the composition of the morphisms from each component to a third object are equal. That is, `inl ∘ f = f` in the coproduct `X + Y` for morphisms `f : X → W` and `inl : X → X + Y`.
|
CategoryTheory.Limits.hasBinaryCoproducts_of_hasColimit_pair
theorem CategoryTheory.Limits.hasBinaryCoproducts_of_hasColimit_pair :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
[inst_1 : ∀ {X Y : C}, CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.pair X Y)],
CategoryTheory.Limits.HasBinaryCoproducts C
The theorem `CategoryTheory.Limits.hasBinaryCoproducts_of_hasColimit_pair` states that in a category `C`, if for every pair of objects `X` and `Y`, there exists a colimit of the diagram given by `pair X Y` (that is, a functor from the discrete category on a two-object set to `C` that sends the two objects of the discrete category to `X` and `Y`), then the category `C` has binary coproducts. In other words, for every pair of objects in the category, there is an object which serves as the coproduct of the pair.
More concisely: If every pair of objects in a category has a colimit of the discrete diagram, then the category has binary coproducts.
|
CategoryTheory.Limits.prod.map_fst
theorem CategoryTheory.Limits.prod.map_fst :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C}
[inst_1 : CategoryTheory.Limits.HasBinaryProduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Y Z]
(f : W ⟶ Y) (g : X ⟶ Z),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f g) CategoryTheory.Limits.prod.fst =
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst f
The theorem `CategoryTheory.Limits.prod.map_fst` states that, for all categories `C` and objects `W`, `X`, `Y`, `Z` in the category, given that there are binary products `W ⨯ X` and `Y ⨯ Z` in the category and morphisms `f : W ⟶ Y` and `g : X ⟶ Z`, the composition of the product map `CategoryTheory.Limits.prod.map f g` with the projection to the first component of the product `CategoryTheory.Limits.prod.fst` is equal to the composition of `CategoryTheory.Limits.prod.fst` and `f`. In other words, the map resulting from first applying the product map and then projecting onto the first component is the same as the map resulting from first projecting onto the first component and then applying `f`. This theorem is a part of the properties of categorical limits, specifically binary products, in Category Theory.
More concisely: For all categories, objects, and morphisms, the composition of the product map with the first projection is equal to the first projection followed by the morphism.
|
CategoryTheory.Limits.prodComparison_snd
theorem CategoryTheory.Limits.prodComparison_snd :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
(F : CategoryTheory.Functor C D) (A B : C) [inst_2 : CategoryTheory.Limits.HasBinaryProduct A B]
[inst_3 : CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)],
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A B) CategoryTheory.Limits.prod.snd =
F.map CategoryTheory.Limits.prod.snd
This theorem, `CategoryTheory.Limits.prodComparison_snd`, states that for any categories `C` and `D`, and any functor `F` from `C` to `D`, and for any objects `A` and `B` of `C`, given that both `A` and `B` have binary products in `C` and their images under `F` have binary products in `D`, the composition of the product comparison morphism `CategoryTheory.Limits.prodComparison F A B` and the projection to the second factor `CategoryTheory.Limits.prod.snd` is equal to the image under `F` of the projection to the second factor. In other words, it shows that the functor `F` preserves the second projection of the binary product up to an isomorphism.
More concisely: For any functor F between categories with binary products, the diagram commutes up to isomorphism: F(π₂(A, B)) = π₂(F(A), F(B)).
|
CategoryTheory.Limits.prod.map_id_id
theorem CategoryTheory.Limits.prod.map_id_id :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
[inst_1 : CategoryTheory.Limits.HasBinaryProduct X Y],
CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) =
CategoryTheory.CategoryStruct.id (X ⨯ Y)
This theorem, `CategoryTheory.Limits.prod.map_id_id`, states that for any type `C` which is a category and any objects `X`, `Y` in `C` that have a binary product, the product map induced by the identity morphisms on `X` and `Y` is equal to the identity morphism on the binary product of `X` and `Y`. In other words, it asserts the identity law for the product functor in a category, saying that mapping the identity transformations of `X` and `Y` under the product map gives the identity transformation of the binary product `X ⨯ Y`.
More concisely: For any category `C` and objects `X` and `Y` with a product, the product map of the identity morphisms on `X` and `Y` is equal to the identity morphism on their product `X ⨯ Y`.
|
CategoryTheory.Limits.prodComparison_natural
theorem CategoryTheory.Limits.prodComparison_natural :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
(F : CategoryTheory.Functor C D) {A A' B B' : C} [inst_2 : CategoryTheory.Limits.HasBinaryProduct A B]
[inst_3 : CategoryTheory.Limits.HasBinaryProduct A' B']
[inst_4 : CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)]
[inst_5 : CategoryTheory.Limits.HasBinaryProduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B'),
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.prod.map f g))
(CategoryTheory.Limits.prodComparison F A' B') =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A B)
(CategoryTheory.Limits.prod.map (F.map f) (F.map g))
The theorem `CategoryTheory.Limits.prodComparison_natural` establishes the naturality of the `prodComparison` morphism in both arguments in the context of category theory. Specifically, given categories `C` and `D`, a functor `F` from `C` to `D`, and objects `A`, `A'`, `B`, `B'` in `C` that have binary products both in `C` and in the image of `F`, along with morphisms `f` from `A` to `A'` and `g` from `B` to `B'`, the theorem states that the composition of the functor's map applied to the product map of `f` and `g` followed by the product comparison of `F` on `A'` and `B'` equals the composition of the product comparison of `F` on `A` and `B` followed by the product map of the functor's map applied to `f` and `g`. This naturality property captures the notion that the diagram involving these morphisms and objects commutes.
More concisely: Given functors F from category C to D, and objects A, A', B, B' in C with binary products, morphisms f : A → A' and g : B → B' in C, the naturality of prodComparison morphism in prodComparison\_natural theorem asserts that F(π\_1(f, g)) = π'_1(F(f), F(g)) ∘ prodComparison(F(A), F(B)). Here, π\_1 denotes the first projection of the product, and π'_1 the first projection of the product in the image of F.
|
CategoryTheory.Limits.coprod.desc_inl_inr
theorem CategoryTheory.Limits.coprod.desc_inl_inr :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
[inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X Y],
CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr =
CategoryTheory.CategoryStruct.id (X ⨿ Y)
This theorem, `CategoryTheory.Limits.coprod.desc_inl_inr`, states that in any category `C` with a binary coproduct of two objects `X` and `Y`, the morphism described by the coproduct of the inclusion maps from `X` and `Y` is equal to the identity morphism on the coproduct `X ⨿ Y`. In other words, it formalizes the universal property of the coproduct in category theory: for every pair of morphisms from `X` and `Y` to the coproduct `X ⨿ Y` (given by `CategoryTheory.Limits.coprod.inl` and `CategoryTheory.Limits.coprod.inr`), there exists a unique morphism from the coproduct to itself (given by `CategoryTheory.Limits.coprod.desc`) which makes the corresponding diagram commute, and this morphism is the identity on `X ⨿ Y`.
More concisely: In any category with binary coproducts, the coproduct inclusions are equal to the coproduct description morphisms, which are the identity morphisms on the coproduct.
|
CategoryTheory.Limits.prod.lift_fst_snd
theorem CategoryTheory.Limits.prod.lift_fst_snd :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
[inst_1 : CategoryTheory.Limits.HasBinaryProduct X Y],
CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd =
CategoryTheory.CategoryStruct.id (X ⨯ Y)
This theorem states that in any category `C` that has a binary product of two objects `X` and `Y`, the morphism obtained by lifting the pair of projection morphisms `CategoryTheory.Limits.prod.fst` and `CategoryTheory.Limits.prod.snd` to a morphism from the product `X ⨯ Y` to itself is actually the identity morphism on `X ⨯ Y`. In simpler words, taking the projection from the product to its constituents and then lifting it back to the product gives you the identity operation. This is a fundamental property of products in category theory.
More concisely: In any category with binary products, the projection morphisms' lift to the product is equal to the identity morphism on the product.
|
CategoryTheory.Limits.prodComparison_inv_natural
theorem CategoryTheory.Limits.prodComparison_inv_natural :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
(F : CategoryTheory.Functor C D) {A A' B B' : C} [inst_2 : CategoryTheory.Limits.HasBinaryProduct A B]
[inst_3 : CategoryTheory.Limits.HasBinaryProduct A' B']
[inst_4 : CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)]
[inst_5 : CategoryTheory.Limits.HasBinaryProduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B')
[inst_6 : CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)]
[inst_7 : CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A' B')],
CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A B))
(F.map (CategoryTheory.Limits.prod.map f g)) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (F.map f) (F.map g))
(CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A' B'))
This theorem states that in the context of category theory, for any categories `C` and `D` and a functor `F` from `C` to `D`, given objects `A`, `A'`, `B`, `B'` in `C` which have binary products both in `C` and in the image under `F`, and morphisms `f` from `A` to `A'` and `g` from `B` to `B'`, if the product comparison morphisms for `(A, B)` and `(A', B')` are both isomorphisms, then the composition of the inverse of the product comparison morphism for `(A, B)` and the functor `F` applied to the product map `(f, g)` is equal to the composition of the product map `(F(f), F(g))` and the inverse of the product comparison morphism for `(A', B')`. This captures a sense of "naturality" of the inverse of the product comparison morphism.
More concisely: Given functors F from category C to D, objects A, A', B, B with binary products in C and their images under F, and isomorphic product comparison morphisms in C and D, the diagram commutes:
(A × B) → A ↓ḥ A' × B' → A'
| (f, g) | ↓ FC(f, g) | |FC(f, g) | ↓ ḥ'
| | ↓ i₁ | | | ↓ i₁'
| C(f, g) | → 1_C | | 1_D | → 1_D
| | ↓ i₂ | | | ↓ i₂'
| B | → 1_C | | B' | → 1_D
where i₁, i₂ are identity morphisms and i'_1, i'_2 are product comparison morphisms.
|
CategoryTheory.Limits.BinaryCofan.IsColimit.hom_ext
theorem CategoryTheory.Limits.BinaryCofan.IsColimit.hom_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C} {s : CategoryTheory.Limits.BinaryCofan X Y},
CategoryTheory.Limits.IsColimit s →
∀ {f g : s.pt ⟶ W},
CategoryTheory.CategoryStruct.comp s.inl f = CategoryTheory.CategoryStruct.comp s.inl g →
CategoryTheory.CategoryStruct.comp s.inr f = CategoryTheory.CategoryStruct.comp s.inr g → f = g
This theorem, `CategoryTheory.Limits.BinaryCofan.IsColimit.hom_ext`, states that in any category `C`, for any three objects `W`, `X`, `Y` and a binary cofan `s` of `X` and `Y`, if `s` is a colimit, then for any two morphisms `f` and `g` from the point of `s` to `W`, if the composition of `f` (respectively, `g`) and the first inclusion of `s` equals the composition of `g` (respectively, `f`) and the first inclusion of `s`, and the composition of `f` (respectively, `g`) and the second inclusion of `s` equals the composition of `g` (respectively, `f`) and the second inclusion of `s`, then `f` equals `g`.
In other words, the morphisms from the colimit of the binary cofan to any object are uniquely determined by their composition with the inclusions of the binary cofan.
More concisely: In any category with binary cocones, if a binary cocone is a colimit, then any two morphisms from the point to the domain of the cocone with equal compositions with both inclusions are equal.
|
CategoryTheory.Limits.prod.lift_map
theorem CategoryTheory.Limits.prod.lift_map :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {V W X Y Z : C}
[inst_1 : CategoryTheory.Limits.HasBinaryProduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Y Z]
(f : V ⟶ W) (g : V ⟶ X) (h : W ⟶ Y) (k : X ⟶ Z),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift f g) (CategoryTheory.Limits.prod.map h k) =
CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp f h)
(CategoryTheory.CategoryStruct.comp g k)
This theorem in category theory states that for any objects `V`, `W`, `X`, `Y`, `Z` in a category `C` that has binary products of `W` and `X` and `Y` and `Z`, and given any morphisms `f : V ⟶ W`, `g : V ⟶ X`, `h : W ⟶ Y`, `k : X ⟶ Z`, the composition of the lift of the product of `f` and `g` with the map of the product of `h` and `k` is equal to the lift of the product of the composition of `f` and `h` with the composition of `g` and `k`. In mathematical terms, this can be written as `(f x g) ∘ (h x k) = (f ∘ h) x (g ∘ k)`, where `∘` denotes composition of morphisms, `x` denotes the product of two morphisms, and `f x g` and `h x k` are the lifts of the product of the morphisms.
More concisely: For any objects `V`, `W`, `X`, `Y`, `Z` in a category with binary products, and morphisms `f : V ⟶ W`, `g : V ⟶ X`, `h : W ⟶ Y`, `k : X ⟶ Z`, the lifts of their products satisfy `(f x g) ∘ (h x k) = (f ∘ h) x (g ∘ k)`.
|
CategoryTheory.Limits.coprod.symmetry
theorem CategoryTheory.Limits.coprod.symmetry :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
(P Q : C),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.braiding P Q).hom
(CategoryTheory.Limits.coprod.braiding Q P).hom =
CategoryTheory.CategoryStruct.id (P ⨿ Q)
The theorem `CategoryTheory.Limits.coprod.symmetry` states that, for any category `C` that has binary coproducts, and for any two objects `P` and `Q` in `C`, the composition of the braiding morphism from `P` to `Q` and the braiding morphism from `Q` to `P` is equal to the identity morphism on the coproduct of `P` and `Q`. In other words, braiding `P` and `Q` and then braiding them back gives us the original coproduct, indicating that the braiding process is symmetric.
More concisely: For any category with binary coproducts, the braiding morphisms of two objects with respect to the coproduct are mutually inverse.
|
CategoryTheory.Limits.hasBinaryProducts_of_hasLimit_pair
theorem CategoryTheory.Limits.hasBinaryProducts_of_hasLimit_pair :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
[inst_1 : ∀ {X Y : C}, CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.pair X Y)],
CategoryTheory.Limits.HasBinaryProducts C
This theorem states that if a category `C` has all limits of diagrams `pair X Y` for all objects `X` and `Y` in `C`, then `C` has binary products. In other words, if for any two objects in the category, there exists a limit for the functor that maps the discrete category of a walking pair to `C` (with the two objects of the walking pair mapped to `X` and `Y`), then for any two objects in the category `C`, there exists a product of these two objects.
More concisely: If a category has all limits of binary diagrams, then it has binary products.
|
CategoryTheory.Limits.coprod.map_desc
theorem CategoryTheory.Limits.coprod.map_desc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S T U V W : C}
[inst_1 : CategoryTheory.Limits.HasBinaryCoproduct U W] [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct T V]
(f : U ⟶ S) (g : W ⟶ S) (h : T ⟶ U) (k : V ⟶ W),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map h k)
(CategoryTheory.Limits.coprod.desc f g) =
CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp h f)
(CategoryTheory.CategoryStruct.comp k g)
The theorem `CategoryTheory.Limits.coprod.map_desc` states that in a category `C` with binary coproducts, for objects `S`, `T`, `U`, `V`, and `W`, given two morphisms `f: U ⟶ S` and `g: W ⟶ S`, and two other morphisms `h: T ⟶ U` and `k: V ⟶ W`, the composition of `CategoryTheory.Limits.coprod.map h k` and `CategoryTheory.Limits.coprod.desc f g` is equal to `CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp h f) (CategoryTheory.CategoryStruct.comp k g)`. In other words, this expresses a commutative property regarding the composition of morphisms involving the coproduct.
More concisely: In a category with binary coproducts, the composition of morphisms `h` and `k` with `CategoryTheory.Limits.coprod.map` followed by `CategoryTheory.Limits.coprod.desc` is equal to `CategoryTheory.Limits.coprod.desc` of their composition.
|