CategoryTheory.Limits.HasBinaryBiproduct.mk
theorem CategoryTheory.Limits.HasBinaryBiproduct.mk :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{P Q : C}, CategoryTheory.Limits.BinaryBiproductData P Q → CategoryTheory.Limits.HasBinaryBiproduct P Q
This theorem states that in category theory, given a category `C` with zero morphisms, and two objects `P` and `Q` in `C`, if there exists a `BinaryBiproductData` for `P` and `Q`, then `P` and `Q` have a binary biproduct.
In simpler terms, it's saying that if we have some sort of structure (`BinaryBiproductData`) relating two objects in a category that has "zero" morphisms (mappings between objects), then those two objects have a binary biproduct. A binary biproduct is a specific type of "product" and "coproduct" pair in the category.
More concisely: In a category with zero morphisms, the existence of `BinaryBiproductData` for objects `P` and `Q` implies the existence of a binary biproduct for `P` and `Q`.
|
CategoryTheory.Limits.bicone_ι_π_ne
theorem CategoryTheory.Limits.bicone_ι_π_ne :
∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) {j j' : J},
j ≠ j' → CategoryTheory.CategoryStruct.comp (B.ι j) (B.π j') = 0
The theorem `CategoryTheory.Limits.bicone_ι_π_ne` states that for any given type `J`, type `C`, a category structure on `C`, a property that `C` has zero morphisms, a functor `F` from `J` to `C`, and a bicone `B` over `F`, if `j` and `j'` are two distinct objects of type `J`, then the composition of the morphism `B.ι j` and the morphism `B.π j'` is zero. In other words, in the category theory context, if two objects are distinct, the composition of their morphisms results in a zero morphism.
More concisely: For any category `C` with zero morphisms, functor `F` from a type `J` to `C`, and a bicone `B` over `F`, the composition of `B.ι j` and `B.π j'` is zero for distinct objects `j` and `j'` of `J`.
|
CategoryTheory.Limits.BinaryBicone.inl_fst
theorem CategoryTheory.Limits.BinaryBicone.inl_fst :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q),
CategoryTheory.CategoryStruct.comp self.inl self.fst = CategoryTheory.CategoryStruct.id P
The theorem `CategoryTheory.Limits.BinaryBicone.inl_fst` states that for any category `C` that has zero morphisms, and any pair of objects `P` and `Q` in `C`, if we have a binary bicone structure `self` on `P` and `Q`, then the composition of the morphisms `self.inl` and `self.fst` is equivalent to the identity morphism on `P`.
In more detail, a binary bicone structure for a pair of objects `P` and `Q` involves a cone point `X` and four morphisms: two from `X` to each of `P` and `Q`, and two from each of `P` and `Q` to `X`. The theorem is verifying one of the defining properties of this structure: namely, that composing the morphism from the cone point to `P` (`self.inl`) with the morphism from `P` to the cone point (`self.fst`) gives us the identity morphism on `P`. This means that if we start at `P`, go to `X`, and then go back to `P`, we end up exactly where we started.
More concisely: For any category with zero morphisms and given a binary bicone structure on objects P and Q, the composition of inl and fst morphisms is equal to the identity morphism on P.
|
CategoryTheory.Limits.biprod.inr_map
theorem CategoryTheory.Limits.biprod.inr_map :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{W X Y Z : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct W X]
[inst_3 : CategoryTheory.Limits.HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z),
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.Limits.biprod.map f g) =
CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.biprod.inr
The theorem `CategoryTheory.Limits.biprod.inr_map` states that for any category `C` that has zero morphisms, given four objects `W`, `X`, `Y`, `Z` in `C`, such that `C` has binary biproducts of `W` and `X`, and `Y` and `Z`, and two morphisms `f : W ⟶ Y` and `g : X ⟶ Z`, the composition of the inclusion into the second summand of a binary biproduct (`CategoryTheory.Limits.biprod.inr`) followed by the mapping of the binary biproduct via `f` and `g` is equal to the composition of `g` followed by the inclusion into the second summand of a binary biproduct. In other words, this theorem is about the commutativity of a certain diagram involving binary biproducts in a category.
More concisely: For any category with zero morphisms `C` having binary biproducts, the inclusion into the second summand of a binary biproduct of objects `W`, `X` followed by morphisms `f : W ⟶ Y` and `g : X ⟶ Z`, is equal to the morphism `g` followed by the inclusion into the second summand of the binary biproduct of objects `X`, `Z`.
|
CategoryTheory.Limits.biprod.associator_inv_natural
theorem CategoryTheory.Limits.biprod.associator_inv_natural :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {U V W X Y Z : C} (f : U ⟶ X) (g : V ⟶ Y) (h : W ⟶ Z),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f (CategoryTheory.Limits.biprod.map g h))
(CategoryTheory.Limits.biprod.associator X Y Z).inv =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.associator U V W).inv
(CategoryTheory.Limits.biprod.map (CategoryTheory.Limits.biprod.map f g) h)
The theorem `CategoryTheory.Limits.biprod.associator_inv_natural` states that for any category `C` with zero morphisms and binary biproducts, and any objects `U`, `V`, `W`, `X`, `Y`, `Z` in `C`, for any morphisms `f : U ⟶ X`, `g : V ⟶ Y`, `h : W ⟶ Z`, the following equality holds: if we first map `f` and `g h` via a biprod map, and then use the inverse of the associator on `X`, `Y`, `Z`, this is the same as if we first use the inverse of the associator on `U`, `V`, `W`, and then map the biprod of `f g` and `h`. In simpler terms, this theorem says that changing the order of operations, mapping via biprod and using the associator, doesn't affect the final result; the two processes are compatible with each other.
More concisely: For any category with zero morphisms and binary biproducts, the application of the inverse of the biproduct associator is commutative, i.e., `(∫(X, Y) (f ⊕ g) ⊣ h) = (f ⊕ (g ⊕ h)) ⊣ ∫(X, Z) (idX ⊣ invAssoc)`, where `invAssoc` is the inverse of the biproduct associator.
|
CategoryTheory.Limits.biprod.lift_snd
theorem CategoryTheory.Limits.biprod.lift_snd :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{W X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift f g) CategoryTheory.Limits.biprod.snd = g
The theorem `CategoryTheory.Limits.biprod.lift_snd` states that in any category `C` with zero morphisms, given three objects `W`, `X`, and `Y` such that `X` and `Y` have a binary biproduct, and given any two morphisms `f` from `W` to `X` and `g` from `W` to `Y`, the composition of the morphism constructed by the lift operation on `f` and `g` and the projection onto the second summand of the binary biproduct equals `g`. In more mathematical terms, this means that if we form a morphism from `W` to the biproduct `X ⊞ Y` using `f` and `g`, and then project onto `Y`, we get back the original morphism `g`.
More concisely: Given a category with zero morphisms `C` where `X` and `Y` have a binary biproduct, for any morphisms `f: W → X` and `g: W → Y`, we have `(π₂ ∘ lift₂ X Y f g) = g`, where `lift₂` is the lift operation on morphisms, `π₂` is the projection onto the second summand of the biproduct, and the domain of all morphisms is the object `W`.
|
CategoryTheory.Limits.biproduct.matrix_π
theorem CategoryTheory.Limits.biproduct.matrix_π :
∀ {J : Type} [inst : Finite J] {K : Type} [inst_1 : Finite K] {C : Type u}
[inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C} {g : K → C} (m : (j : J) → (k : K) → f j ⟶ g k)
(k : K),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix m)
(CategoryTheory.Limits.biproduct.π g k) =
CategoryTheory.Limits.biproduct.desc fun j => m j k
This theorem, `CategoryTheory.Limits.biproduct.matrix_π`, states that in a category `C` that has zero morphisms and finite biproducts, for any two functions `f : J → C` and `g : K → C` where `J` and `K` are finite types, and a family of morphisms `m : (j : J) → (k : K) → f j ⟶ g k`, the composition of the biproduct matrix of `m` and the projection onto a summand of `g` is equal to the biproduct descent of the function that maps each element of `J` to the morphism `m j k`.
In other words, this theorem is about the interaction of biproduct matrices and projections in a category with certain properties, namely having zero morphisms and finite biproducts.
More concisely: In a category with zero morphisms and finite biproducts, for any two functions and a family of morphisms between them, the composition of the biproduct matrix and the projection onto a summand equals the biproduct descent of the function mapping each element to the morphism.
|
CategoryTheory.Limits.BinaryBicone.inr_snd
theorem CategoryTheory.Limits.BinaryBicone.inr_snd :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q),
CategoryTheory.CategoryStruct.comp self.inr self.snd = CategoryTheory.CategoryStruct.id Q
This theorem describes a property of binary bicones in category theory. A binary bicone for a pair of objects `P` and `Q` in a category `C` is made up of a cone point `X`, maps from `X` to both `P` and `Q`, and maps from both `P` and `Q` to `X`. The theorem states that for any such binary bicone `self`, if we compose the morphism `self.inr` with `self.snd` (denoted by `self.inr ≫ self.snd`), we get the identity morphism on `Q` (denoted by `𝟙 Q`). This property must hold in any category `C` that has zero morphisms.
More concisely: In any category with zero morphisms, for any binary bicone between objects P and Q, the composition of its right injective arrow with its right arrow is the identity morphism on Q.
|
CategoryTheory.Limits.hasBinaryBiproducts_of_finite_biproducts
theorem CategoryTheory.Limits.hasBinaryBiproducts_of_finite_biproducts :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C], CategoryTheory.Limits.HasBinaryBiproducts C
This theorem states that in the context of category theory, if a category has finite biproducts, then it also has binary biproducts. However, this is not typically set as an instance because in most concrete categories, there will be an alternative construction that has preferable definitional properties. In more detail, for any category 'C' that is equipped with zero morphisms and finite biproducts, the theorem proves that 'C' also has binary biproducts.
More concisely: In a category with finite biproducts, binary biproducts exist.
|
CategoryTheory.Limits.biprod.inl_desc_assoc
theorem CategoryTheory.Limits.biprod.inl_desc_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{W X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) {Z : C} (h : W ⟶ Z),
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.desc f g) h) =
CategoryTheory.CategoryStruct.comp f h
This theorem states that, in any category `C` with zero morphisms and binary biproducts, for any objects `W`, `X`, `Y`, and `Z` in `C`, and for any morphisms `f : X ⟶ W`, `g : Y ⟶ W`, and `h : W ⟶ Z`, the composition of the inclusion of `X` into the first summand of the binary biproduct `X ⊞ Y` with the composition of the morphism described by `f` and `g` and `h` is the same as the composition of `f` and `h`. In more mathematical language, it states that `(inl ∘ (desc(f, g) ∘ h)) = (f ∘ h)`, where `inl` is the inclusion into the first summand of a binary biproduct, `desc` is a morphism described by `f` and `g`, and `∘` denotes the composition of morphisms.
More concisely: In any category with zero morphisms and binary biproducts, the inclusion of an object into the first summand of the biproduct and the composition of morphisms from it to the target object through a common intermediate object is equal to the direct composition of these morphisms.
|
CategoryTheory.Limits.biproduct.toSubtype_π
theorem CategoryTheory.Limits.biproduct.toSubtype_π :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
(p : J → Prop) [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] (j : Subtype p),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.toSubtype f p)
(CategoryTheory.Limits.biproduct.π (Subtype.restrict p f) j) =
CategoryTheory.Limits.biproduct.π f ↑j
This theorem, `CategoryTheory.Limits.biproduct.toSubtype_π`, asserts that in a category with zero morphisms and a biproduct, for a function `f` from a type `J` to a category `C`, and a proposition `p` on `J`, if we restrict `f` to the subtype of `J` where `p` holds, then the composition of the projection from the biproduct to the subtype with the projection from the biproduct to the element of the subtype, is equal to the projection from the biproduct to the preimage of the element. In mathematical terms, this means that if we have a biproduct (a "direct sum" or "coproduct" in algebra) of some objects in a category, and we consider a subset of these objects satisfying some property, then the projection map from the biproduct to an object in this subset is the same whether we consider the subset as part of the whole biproduct or as a separate biproduct of its own.
More concisely: Given a category with zero morphisms and a biproduct, for a function from a type to the category and a proposition on that type, the projection from the biproduct to the subtype of satisfying the proposition is equal to the composition of the projections from the biproduct to the subtype and to the element in the subtype.
|
CategoryTheory.Limits.biprod.inl_map_assoc
theorem CategoryTheory.Limits.biprod.inl_map_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{W X Y Z : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct W X]
[inst_3 : CategoryTheory.Limits.HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {Z_1 : C} (h : Y ⊞ Z ⟶ Z_1),
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f g) h) =
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl h)
The theorem `CategoryTheory.Limits.biprod.inl_map_assoc` states that in a category `C` with zero morphisms and binary biproducts, for any objects `W`, `X`, `Y`, `Z`, and `Z_1`, and any morphisms `f : W ⟶ Y`, `g : X ⟶ Z`, and `h : Y ⊞ Z ⟶ Z_1`, the composition of the inclusion morphism into the first summand of the binary biproduct and the composition of the map morphism and `h` is equivalent to the composition of `f` and the composition of the inclusion morphism and `h`. This theorem essentially establishes the associativity of these operations in the context of category theory.
More concisely: In a category with zero morphisms and binary biproducts, the composition of the inclusion morphism into the first summand and the composition of a map morphism and the inclusion morphism into the second summand is equal to the composition of the map morphism, the inclusion morphism into the second summand, and the given morphism.
|
CategoryTheory.isIso_left_of_isIso_biprod_map
theorem CategoryTheory.isIso_left_of_isIso_biprod_map :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z)
[inst_3 : CategoryTheory.IsIso (CategoryTheory.Limits.biprod.map f g)], CategoryTheory.IsIso f
This theorem states that in a category `C` with zero morphisms and binary biproducts, for any four objects `W, X, Y, Z` in `C` and morphisms `f : W ⟶ Y` and `g : X ⟶ Z`, if the biproduct map `(f 0)(0 g)` is an isomorphism (i.e., has an inverse), then `f` is also an isomorphism. This result is a property of categories with binary biproducts, which are a particular type of category in category theory, a branch of abstract mathematics.
More concisely: In a category with zero morphisms and binary biproducts, if the biproduct map of morphisms `f : W ⟶ Y` and `g : X ⟶ Z` is an isomorphism, then `f` is an isomorphism.
|
CategoryTheory.Limits.biprod.conePointUniqueUpToIso_hom
theorem CategoryTheory.Limits.biprod.conePointUniqueUpToIso_hom :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
(X Y : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] {b : CategoryTheory.Limits.BinaryBicone X Y}
(hb : b.IsBilimit),
(hb.isLimit.conePointUniqueUpToIso (CategoryTheory.Limits.BinaryBiproduct.isLimit X Y)).hom =
CategoryTheory.Limits.biprod.lift b.fst b.snd
The theorem `CategoryTheory.Limits.biprod.conePointUniqueUpToIso_hom` states that, in the context of a category `C` with zero morphisms, for any two objects `X` and `Y` in `C` where a binary biproduct exists, and given a binary bicone `b` of `X` and `Y` that is a bilimit, the morphism resulting from the uniqueness (up to isomorphism) of the limit cone's apex for this bicone and the predefined limit of the binary biproduct, is equal to the morphism obtained by lifting the two morphisms `fst` and `snd` of the binary bicone through the biproduct. In other terms, the unique morphism from the limit cone's apex to the biproduct coincides with the morphism constructed by lifting the two morphisms of the binary bicone.
More concisely: Given a category with zero morphisms, for any two objects with a binary biproduct and a bilimit binary bicone, the unique limit cone morphism to the biproduct equals the morphism obtained by lifting the bicone's components through the biproduct.
|
CategoryTheory.Limits.BinaryBicone.inr_snd_assoc
theorem CategoryTheory.Limits.BinaryBicone.inr_snd_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q) {Z : C} (h : Q ⟶ Z),
CategoryTheory.CategoryStruct.comp self.inr (CategoryTheory.CategoryStruct.comp self.snd h) = h
The theorem `CategoryTheory.Limits.BinaryBicone.inr_snd_assoc` states that for any category 'C' with zero morphisms, given binary bicone on objects 'P' and 'Q' of the category, and any morphism `h` from 'Q' to another object 'Z' in the category, the composition of the morphism `h` with the second morphism of the bicone followed by the 'inr' morphism of the bicone is equal to the morphism `h`. In the language of category theory, this theorem is about the associativity of composition of morphisms in the context of binary bicones.
More concisely: For any category with zero morphisms, given a binary bicone on objects P and Q, and a morphism h from Q to another object Z, the composition h ∘ bicone.2 ∘ inr = h.
|
CategoryTheory.Limits.biproduct.conePointUniqueUpToIso_inv
theorem CategoryTheory.Limits.biproduct.conePointUniqueUpToIso_inv :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
{b : CategoryTheory.Limits.Bicone f} (hb : b.IsBilimit),
(hb.isLimit.conePointUniqueUpToIso (CategoryTheory.Limits.biproduct.isLimit f)).inv =
CategoryTheory.Limits.biproduct.desc b.ι
The theorem `CategoryTheory.Limits.biproduct.conePointUniqueUpToIso_inv` states that for any type `J`, type `C` that is a category with zero morphisms, a functor `f : J → C` that has a biproduct, and a bicone `b` of the functor that is a bilimit, the inverse of the unique isomorphism from the limit cone of the biproduct to the cone of the bilimit is equal to the morphism described by `b.ι` in the biproduct. This theorem is an auxiliary lemma for the proof of `biproduct.uniqueUpToIso` which asserts the uniqueness (up to isomorphism) of the biproduct in a category.
More concisely: For a functor with a biproduct and a bilimit in a zero-morphism category J, the inverse of the isomorphism from the biproduct limit cone to the bilimit cone is equal to the morphism given by the biproduct's inclusion map.
|
CategoryTheory.Limits.biproduct.ι_π
theorem CategoryTheory.Limits.biproduct.ι_π :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : DecidableEq J] (f : J → C)
[inst_3 : CategoryTheory.Limits.HasBiproduct f] (j j' : J),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j)
(CategoryTheory.Limits.biproduct.π f j') =
if h : j = j' then CategoryTheory.eqToHom ⋯ else 0
This theorem, `CategoryTheory.Limits.biproduct.ι_π`, states that for any type `J`, type `C`, an instance of `CategoryTheory.Category` for `C`, an instance of `CategoryTheory.Limits.HasZeroMorphisms` for `C`, an instance of `DecidableEq` for `J`, a function `f` from `J` to `C`, and an instance of `CategoryTheory.Limits.HasBiproduct` for `f`, along with two elements `j` and `j'` of `J`, the composition of the inclusion into a summand of a biproduct of `f` at `j` and the projection onto a summand of a biproduct of `f` at `j'` equals the morphism from `j` to `j'` if `j` equals `j'`, otherwise it equals zero. It is important to note that due to the presence of an `if` in the statement of the theorem, a `DecidableEq` argument is included, meaning you may not be able to use simplification (`simp`) with this theorem unless you open the classical logic scope (`open scoped Classical`).
More concisely: For any functor `f` from a decidable category with biproducts `J` to a category `C`, and for any `j`, `j'` in `J`, the composition of the inclusion and projection morphisms of the biproduct of `f` at `j` and `j'` equals `f(j) = f(j')` if and only if `j = j'`, otherwise it is the zero morphism.
|
CategoryTheory.Limits.biproduct.ι_desc
theorem CategoryTheory.Limits.biproduct.ι_desc :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
{P : C} (p : (b : J) → f b ⟶ P) (j : J),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j)
(CategoryTheory.Limits.biproduct.desc p) =
p j
This theorem, `CategoryTheory.Limits.biproduct.ι_desc`, states that for any category `C` with zero morphisms and a given type `J`, if we have a function `f : J → C` forming a biproduct in `C`, and a morphism `p` from each component of `f` to an object `P` in `C`, then the composition of the inclusion from `f j` into the biproduct and the morphism from the biproduct to `P` given by `p` is equal to the morphism `p j` itself. In other words, this theorem states a universal property of biproducts in a category, providing a way to describe and work with such objects in a general and abstract manner.
More concisely: For any category with zero morphisms and a biproduct `(i, s, t, μ, λ)` over a type `J`, the following commutative square holds:
`di ⊎ f j ⥤ P ⊆ biproduct i j ⥤ P ≅ p j`
where `di` is the inclusion morphism of the biproduct component, `f j` is the morphism from the function `f : J → C` to the biproduct component, and `p j` is the given morphism from each component to an object `P` in the category.
|
CategoryTheory.Limits.biprod.inl_map
theorem CategoryTheory.Limits.biprod.inl_map :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{W X Y Z : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct W X]
[inst_3 : CategoryTheory.Limits.HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z),
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.Limits.biprod.map f g) =
CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.inl
This theorem states that in a category with zero morphisms and binary biproducts, for any four objects W, X, Y, Z, and given morphisms f from W to Y and g from X to Z, the composition of the morphism that includes W into the binary biproduct of W and X with the morphism that maps the binary biproduct of W and X to the binary biproduct of Y and Z using f and g, is equal to the composition of f with the morphism that includes Y into the binary biproduct of Y and Z. In other words, the diagram commutes when mapping from the binary biproducts.
More concisely: In a category with zero morphisms and binary biproducts, the diagram commutes when forming the binary biproduct of any three objects and composing with given morphisms between them.
|
CategoryTheory.Limits.biproduct.ι_toSubtype
theorem CategoryTheory.Limits.biproduct.ι_toSubtype :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
(p : J → Prop) [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] [inst_4 : DecidablePred p]
(j : J),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j)
(CategoryTheory.Limits.biproduct.toSubtype f p) =
if h : p j then CategoryTheory.Limits.biproduct.ι (Subtype.restrict p f) ⟨j, h⟩ else 0
This theorem, `CategoryTheory.Limits.biproduct.ι_toSubtype`, states that in the context of a category `C` with zero morphisms and a function `f` from type `J` to `C` that forms a biproduct, for a predicate `p` which also forms a biproduct when restricted by function `f`, and that is decidable, for any element `j` of type `J`, the composition of the inclusion morphism into a summand of biproduct `f` at `j` and the function `CategoryTheory.Limits.biproduct.toSubtype f p` is equal to the inclusion into the summand of the biproduct of the restricted function `Subtype.restrict p f` at subtype `{ val := j, property := h }` if `p j` holds, and is the zero morphism otherwise. This theorem essentially describes the relationship between the inclusion into a summand of a biproduct and the restriction of a function to a subtype in the context of category theory.
More concisely: For a decidable predicate `p` that forms a biproduct with a function `f` in a category `C` with zero morphisms, the inclusion into a summand of the biproduct of `f` at `j` is equal to the inclusion into the summand of the restricted function `Subtype.restrict p f` at `{ val := j, property := true }` if `p(j)` holds, and is the zero morphism otherwise.
|
CategoryTheory.Limits.biproduct.ι_desc_assoc
theorem CategoryTheory.Limits.biproduct.ι_desc_assoc :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
{P : C} (p : (b : J) → f b ⟶ P) (j : J) {Z : C} (h : P ⟶ Z),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.desc p) h) =
CategoryTheory.CategoryStruct.comp (p j) h
The theorem `CategoryTheory.Limits.biproduct.ι_desc_assoc` establishes a property of product structures in a category with zero morphisms. It says that for any type `J`, category `C` with zero morphisms, a function `f` from `J` to `C`, a biproduct of `f`, a morphism `p` from type `J` to `C`, and any objects `P`, `Z` in `C`, the composition of the inclusion into a summand of a biproduct `(CategoryTheory.Limits.biproduct.ι f j)` and the composition of the morphism that maps each factor to a fixed target object `(CategoryTheory.Limits.biproduct.desc p)` with a morphism `h`, is the same as the composition of the morphism `p` at `j` with the morphism `h`. In more mathematical terms, this theorem is stating the associativity condition `(ι j) ≫ ((desc p) ≫ h) = (p j) ≫ h` in the context of a category with a biproduct.
More concisely: In a category with zero morphisms, for any function `f` from a type `J` to `C`, biproduct `(ι f)`, morphism `p` from `J` to `C`, and object `Z` in `C`, the composition `(ι j) ≫ (desc p ≫ h)` equals `(p j) ≫ h` for all `j` in `J`.
|
CategoryTheory.Limits.BinaryBicone.inl_fst_assoc
theorem CategoryTheory.Limits.BinaryBicone.inl_fst_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q) {Z : C} (h : P ⟶ Z),
CategoryTheory.CategoryStruct.comp self.inl (CategoryTheory.CategoryStruct.comp self.fst h) = h
In the context of category theory, the theorem `CategoryTheory.Limits.BinaryBicone.inl_fst_assoc` states that for any type `C` that forms a category with zero morphisms, given objects `P` and `Q` in `C` forming a binary bicone, for any object `Z` in `C` and a morphism `h` from `P` to `Z`, the composition of the morphism `h` with the morphism `self.fst` after `self.inl` is equal to `h`. Here, `self.inl` is a morphism from some object to `P`, and `self.fst` is a morphism from `P` to another object. The composition of morphisms is performed using `CategoryTheory.CategoryStruct.comp` function.
More concisely: For any category with zero morphisms `C`, given a binary bicone `(P, Q, self)` and any morphism `h : P → Z` in `C`, we have `h ∘ self.inl ∘ self.fst = h`.
|
CategoryTheory.Limits.biprod.inr_map_assoc
theorem CategoryTheory.Limits.biprod.inr_map_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{W X Y Z : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct W X]
[inst_3 : CategoryTheory.Limits.HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {Z_1 : C} (h : Y ⊞ Z ⟶ Z_1),
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f g) h) =
CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr h)
The theorem `CategoryTheory.Limits.biprod.inr_map_assoc` states that for any category `C` that has zero morphisms, and for any four objects `W, X, Y, Z` in this category `C` with binary biproducts `W ⊞ X` and `Y ⊞ Z`, given morphisms `f : W ⟶ Y`, `g : X ⟶ Z`, and another morphism `h : Y ⊞ Z ⟶ Z_1`, the composition of the inclusion into the second summand `biprod.inr` followed by the composition of the map `biprod.map f g` with `h` is equal to the composition of `g` with the composition of `biprod.inr` and `h`. In more intuitive terms, this theorem expresses a commutative property of certain mappings associated with binary biproducts in a category.
More concisely: For any morphisms `f : W ⟶ Y`, `g : X ⟶ Z`, and `h : Y ⊞ Z ⟶ Z_1` in a category `C` with zero morphisms and binary biproducts, `h ∘ biprod.map f g ∘ biprod.inr = g ∘ h ∘ biprod.inr` for objects `W, X, Y, Z` in `C`.
|
CategoryTheory.Limits.HasFiniteBiproducts.out
theorem CategoryTheory.Limits.HasFiniteBiproducts.out :
∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
[self : CategoryTheory.Limits.HasFiniteBiproducts C] (n : ℕ),
CategoryTheory.Limits.HasBiproductsOfShape (Fin n) C
The theorem `CategoryTheory.Limits.HasFiniteBiproducts.out` states that for any category `C` that has zero morphisms and a choice of biproduct for every family of objects in `C` indexed by a finite type (the condition `HasFiniteBiproducts C`), there exist biproducts of shape `Fin n` for all natural numbers `n`. In other words, in such a category `C`, we can find a biproduct for every family of `n` objects, where `n` is a natural number. This is a statement about the existence of certain limit and colimit structures (biproducts) in the category.
More concisely: In a category with zero morphisms and a finite biproduct for every finite family of objects, there exists a biproduct for every finite indexed family of objects.
|
CategoryTheory.Limits.biproduct.conePointUniqueUpToIso_hom
theorem CategoryTheory.Limits.biproduct.conePointUniqueUpToIso_hom :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
{b : CategoryTheory.Limits.Bicone f} (hb : b.IsBilimit),
(hb.isLimit.conePointUniqueUpToIso (CategoryTheory.Limits.biproduct.isLimit f)).hom =
CategoryTheory.Limits.biproduct.lift b.π
This theorem, `CategoryTheory.Limits.biproduct.conePointUniqueUpToIso_hom`, states that for any type `J`, a category `C` with zero morphisms, and a function `f : J → C` that has a biproduct, given a bicone `b` of `f` that is a bilimit, the homomorphism component of the isomorphism that makes the limit of the cone unique with respect to the bicone `b` is equal to the lift of the projection morphisms of the bicone. Essentially, this establishes the uniqueness (up to isomorphism) of a specific limit structure (the biproduct) in category theory.
More concisely: Given a category with zero morphisms `C`, a function `f : J → C` with a biproduct, and a bilimit bicone `b` of `f`, the isomorphism that makes the limit of the cone unique is equal to the homomorphism component of the bicone's projection morphisms' lift.
|
CategoryTheory.isIso_right_of_isIso_biprod_map
theorem CategoryTheory.isIso_right_of_isIso_biprod_map :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z)
[inst_3 : CategoryTheory.IsIso (CategoryTheory.Limits.biprod.map f g)], CategoryTheory.IsIso g
In the context of category theory, this theorem states that if the biproduct map, which consists of two morphisms `f: W ⟶ Y` and `g: X ⟶ Z` in a category `C`, is an isomorphism (meaning it is invertible), then the morphism `g` is also an isomorphism. Here, `C` is a category with zero morphisms and binary biproducts.
More concisely: If the biproduct map `(f, g) : X ⊕ W ⟶ Y ⊗ Z` is an isomorphism in a category `C` with zero morphisms and binary biproducts, then `g : X ⟶ Z` is an isomorphism.
|
CategoryTheory.Limits.biprod.inr_desc
theorem CategoryTheory.Limits.biprod.inr_desc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{W X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W),
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.Limits.biprod.desc f g) = g
The theorem `CategoryTheory.Limits.biprod.inr_desc` states that in any category `C` with zero morphisms and binary biproducts, for any three objects `W`, `X`, and `Y` in `C`, and given any two morphisms `f : X ⟶ W` and `g : Y ⟶ W`, the composition of the morphism `CategoryTheory.Limits.biprod.inr` (which is the inclusion into the second summand of a binary biproduct) with the morphism `CategoryTheory.Limits.biprod.desc f g` is equal to the morphism `g`. Essentially, it asserts a fundamental property of the construction of binary biproducts in a category.
More concisely: In a category with zero morphisms and binary biproducts, the inclusion morphism into the second summand of a binary biproduct, composed with the description morphism of two given morphisms to the same object, equals one of those morphisms.
|
CategoryTheory.Limits.bicone_ι_π_self
theorem CategoryTheory.Limits.bicone_ι_π_self :
∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : J),
CategoryTheory.CategoryStruct.comp (B.ι j) (B.π j) = CategoryTheory.CategoryStruct.id (F j)
This theorem states that for any type `J`, type `C` which forms a category, where `C` also has zero morphisms, and a function `F` that maps `J` to `C`; given a `bicone` `B` on `F` and any object `j` from `J`, the composition of the morphisms `B.ι j` and `B.π j` (in that order) is the identity morphism on the object `F j`. In other words, the composition of these two morphisms makes no change to the object `F j` in the category `C`. This theorem is a standard result in category theory, specifically within the context of limits and bicones.
More concisely: For any type `J`, type `C` forming a category with zero morphisms, and a function `F : J �� /******/ C` with a bicone `B` on `F`, the composition of `B.π j` and `B.ι j` is the identity morphism on `F j` for any object `j : J`.
|
CategoryTheory.Limits.biprod.isoProd_inv
theorem CategoryTheory.Limits.biprod.isoProd_inv :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
(CategoryTheory.Limits.biprod.isoProd X Y).inv =
CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd
This theorem states that for any category `C` that has zero morphisms and any two objects `X` and `Y` in `C` with a binary biproduct, the inverse of the isomorphism from the binary biproduct to the product of `X` and `Y` is given by the lift of the product's first and second projection maps. In other words, this isomorphism from the binary biproduct to the product can be inverted by taking a lift of the projection maps to the individual components of the product.
More concisely: For any category with zero morphisms and objects `X` and `Y` having a binary biproduct, the inverse of the isomorphism from the binary biproduct to their product is given by the lifts of their projection maps.
|
CategoryTheory.Limits.biprod.hom_ext
theorem CategoryTheory.Limits.biprod.hom_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y Z : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] (f g : Z ⟶ X ⊞ Y),
CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst =
CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.biprod.fst →
CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.snd =
CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.biprod.snd →
f = g
The theorem `CategoryTheory.Limits.biprod.hom_ext` states that in a category `C` which has zero morphisms and a binary biproduct of objects `X` and `Y`, for any two morphisms `f` and `g` from an object `Z` to the biproduct `X ⊞ Y`, if the composition of `f` and the projection onto the first summand of the biproduct is equal to the composition of `g` and the same projection, and the composition of `f` and the projection onto the second summand of the biproduct is equal to the composition of `g` and the same projection, then `f` and `g` must be the same morphism. In essence, it provides a uniqueness criterion for morphisms to a biproduct in terms of the compositions with the biproduct projections.
More concisely: In a category with zero morphisms and binary biproducts, if two morphisms from an object to a biproduct have equal compositions with both projections, they are equal.
|
CategoryTheory.Limits.biproduct.ι_fromSubtype_assoc
theorem CategoryTheory.Limits.biproduct.ι_fromSubtype_assoc :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
(p : J → Prop) [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] (j : Subtype p) {Z : C}
(h : ⨁ f ⟶ Z),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (Subtype.restrict p f) j)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.fromSubtype f p) h) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f ↑j) h
This theorem states that, for any types `J` and `C`, given a category structure on `C`, the presence of zero morphisms in `C`, a function `f` from `J` to `C`, and the existence of a biproduct for the function `f`, along with a property `p` on `J`, and the existence of a biproduct for the restricted function `f` to the subtype `p`, for any subtype `j` of `p` and any object `Z` of `C`, and a morphism `h` from the biproduct of `f` to `Z`, composing the inclusion morphism from `j` into the biproduct of the restricted function `f` to the subtype `p` with the composition of the morphism from the biproduct of the subtype `p` to the biproduct of `f` and the morphism `h`, is equal to the composition of the inclusion morphism from `j` into the biproduct of `f` and the morphism `h`. In simpler terms, this theorem asserts a certain commutativity property in the context of category theory and its notion of biproducts.
More concisely: For any type `J`, category `C` with zero morphisms, function `f` from `J` to `C`, and biproduct `B` of `f`, given property `p` on `J`, subtype `j` of `p`, object `Z` of `C`, and morphism `h` from `B` to `Z`, the compositions of the inclusion morphism from `j` into `B` with the morphism from `B` to `Z` and the inclusion morphism from `j` into the biproduct of `f` to `p` with `h` are equal.
|
CategoryTheory.Limits.biprod.hom_ext'
theorem CategoryTheory.Limits.biprod.hom_ext' :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y Z : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] (f g : X ⊞ Y ⟶ Z),
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl f =
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl g →
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr f =
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr g →
f = g
The theorem `CategoryTheory.Limits.biprod.hom_ext'` states that in a category `C` equipped with a binary biproduct structure and zero morphisms, for any three objects `X`, `Y`, and `Z` and any two morphisms `f, g : X ⊞ Y ⟶ Z`, if we have that the composition of `f` (or `g`) with the inclusion from `X` into the first summand (denoted `CategoryTheory.Limits.biprod.inl`) is equal, and similarly for `Y` into the second summand (denoted `CategoryTheory.Limits.biprod.inr`), then `f` must be equal to `g`. In mathematical terms, it states that if `(inl ≫ f) = (inl ≫ g)` and `(inr ≫ f) = (inr ≫ g)` then `f = g`. This is a statement about the uniqueness of morphisms in the context of biproducts in a category.
More concisely: In a category with binary biproducts and zero morphisms, if the inclusions of the summands make the same compositions with two morphisms from the biproduct to another object, then those morphisms are equal.
|
CategoryTheory.Limits.biproduct.fromSubtype_π
theorem CategoryTheory.Limits.biproduct.fromSubtype_π :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
(p : J → Prop) [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] [inst_4 : DecidablePred p]
(j : J),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.fromSubtype f p)
(CategoryTheory.Limits.biproduct.π f j) =
if h : p j then CategoryTheory.Limits.biproduct.π (Subtype.restrict p f) ⟨j, h⟩ else 0
This theorem from the Category Theory in Lean 4 is regarding the composition of morphisms in the context of biproducts. Given the parameters J and C which represent types, a function `f` from J to C, and a decidable predicate `p` on J, if we have a biproduct of `f` and also a biproduct of the function `f` restricted to the subtype defined by `p`, then the composition of the morphism `CategoryTheory.Limits.biproduct.fromSubtype f p` with the projection `CategoryTheory.Limits.biproduct.π f j` is equal to either the projection `CategoryTheory.Limits.biproduct.π (Subtype.restrict p f) { val := j, property := h }` if the predicate `p` holds true for `j` (denoted as `h : p j`) or `0` otherwise. This is essentially stating the relationship between the biproducts of a function and its restriction to a subtype, in terms of their projections.
More concisely: Given a biproduct of a function `f` and its restriction `Subtype.restrict p f` over a decidable predicate `p` on the domain J, the composition of the morphism from the biproduct of `f` to `f`'s biproduct projection and the biproduct projection of `f`'s restriction is equal to the biproduct projection of `f`'s restriction if `p` holds for the index, and 0 otherwise.
|
CategoryTheory.Limits.HasBinaryBiproduct.exists_binary_biproduct
theorem CategoryTheory.Limits.HasBinaryBiproduct.exists_binary_biproduct :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{P Q : C} [self : CategoryTheory.Limits.HasBinaryBiproduct P Q],
Nonempty (CategoryTheory.Limits.BinaryBiproductData P Q)
This theorem, `CategoryTheory.Limits.HasBinaryBiproduct.exists_binary_biproduct`, states that for any category `C` with zero morphisms and any two objects `P` and `Q` in `C`, if `C` has a binary biproduct for `P` and `Q`, then there exists a binary biproduct data for `P` and `Q`. In other words, there exists a bicone which is both a limit and a colimit of the diagram formed by the pair `P` and `Q`.
More concisely: For any category with zero morphisms `C`, given objects `P` and `Q`, if `C` has a binary biproduct for `P` and `Q`, then there exists a binary biproduct data (i.e., a limit and colimit cone) for `P` and `Q`.
|
CategoryTheory.Limits.BinaryBicone.inr_fst
theorem CategoryTheory.Limits.BinaryBicone.inr_fst :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q),
CategoryTheory.CategoryStruct.comp self.inr self.fst = 0
The theorem `CategoryTheory.Limits.BinaryBicone.inr_fst` states that in the context of a category `C`, which has zero morphisms, for any two objects `P` and `Q` in `C`, given a binary bicone structure `self` for the pair `P` and `Q`, the composition of the morphism `inr` (from `P` or `Q` to the apex `X` of the bicone) and the morphism `fst` (from `X` to `P`) is a zero morphism. In other words, this theorem asserts one of the key properties of a binary bicone: any path from `Q` to `P` via `X` is nullified.
More concisely: Given a binary bicone `self` in a zero-morphism category `C` with objects `P` and `Q` and the morphisms `inr: P ⟶ X` and `fst: X ⟶ P`, the composition `inr ∘ fst` is the zero morphism from `P` to `P`.
|
CategoryTheory.Limits.HasBiproduct.mk
theorem CategoryTheory.Limits.HasBiproduct.mk :
∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C},
CategoryTheory.Limits.LimitBicone F → CategoryTheory.Limits.HasBiproduct F
This theorem states that for any category `C` with zero morphisms and any indexed family of objects `F` in `C`, if a limit bicone exists for `F`, then `F` has a biproduct. In other words, it assures us the existence of a biproduct (a concept in category theory combining both a product and a coproduct) for every object in the category `C` whenever a limit bicone (a certain structure involving limits in category theory) exists for `F`.
More concisely: If a category with zero morphisms has an indexed family of objects with a limit bicone, then each object in the family has a biproduct.
|
CategoryTheory.Limits.BinaryBicone.inl_snd_assoc
theorem CategoryTheory.Limits.BinaryBicone.inl_snd_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q) {Z : C} (h : Q ⟶ Z),
CategoryTheory.CategoryStruct.comp self.inl (CategoryTheory.CategoryStruct.comp self.snd h) =
CategoryTheory.CategoryStruct.comp 0 h
This theorem, `CategoryTheory.Limits.BinaryBicone.inl_snd_assoc`, states that for any category `C` with zero morphisms, given objects `P`, `Q`, and `Z` in `C`, and a binary bicone `self` with `P` and `Q` as its apexes, the composition of the morphism `self.inl` with the composition of the morphism `self.snd` and some morphism `h` from `Q` to `Z` is equal to the composition of the zero morphism and `h`. In other words, it expresses a certain associativity property in the context of a binary bicone structure in category theory.
More concisely: For any category with zero morphisms, the composition of a binary bicone's left injection with the composition of its right projection and a morphism is equal to the composition of the zero morphism and that morphism.
|
CategoryTheory.Limits.biproduct.hom_ext'
theorem CategoryTheory.Limits.biproduct.hom_ext' :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
{Z : C} (g h : ⨁ f ⟶ Z),
(∀ (j : J),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) g =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) h) →
g = h
This theorem, `CategoryTheory.Limits.biproduct.hom_ext'`, states that for any type `J` and category `C` that has zero morphisms, given a function `f` from `J` to `C` which has a biproduct, and any object `Z` in `C`, for two morphisms `g` and `h` from the biproduct of `f` to `Z`, if for every `j` in `J`, the composition of the inclusion of `f j` into the biproduct with `g` is equal to the composition of the inclusion of `f j` into the biproduct with `h`, then `g` and `h` are equal. In other words, it's a uniqueness property for morphisms originating from the biproduct: if two such morphisms coincide on each inclusion from the constituents of the biproduct, they are the same morphism.
More concisely: Given a function `f` from a type `J` to a zero-object category `C` with a biproduct, if for all `j` in `J` and morphisms `g` and `h` from the biproduct of `f` to an object `Z` in `C`, the composition of the inclusion of `f j` with `g` equals the composition of the inclusion of `f j` with `h`, then `g` and `h` are equal.
|
CategoryTheory.Limits.biprod.inl_desc
theorem CategoryTheory.Limits.biprod.inl_desc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{W X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W),
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.Limits.biprod.desc f g) = f
The theorem `CategoryTheory.Limits.biprod.inl_desc` states that for any category `C` with zero morphisms, and any objects `W`, `X`, `Y` in `C` that form a binary biproduct, the composition of the inclusion into the first summand of the binary biproduct (`CategoryTheory.Limits.biprod.inl`) with the morphism (`CategoryTheory.Limits.biprod.desc`) that describes the biproduct in terms of maps `f : X ⟶ W` and `g : Y ⟶ W`, will always equal `f`. In other words, if you first include `X` into the biproduct and then apply the biproduct description, you get back the original morphism `f`. This theorem captures a fundamental property of binary biproducts in category theory.
More concisely: For any category with zero morphisms and objects forming a binary biproduct, the inclusion into the first summand and the biproduct description morphism commute, i.e., `inl (desc X Y W f g) = f`.
|
CategoryTheory.Limits.BinaryBicone.inr_fst_assoc
theorem CategoryTheory.Limits.BinaryBicone.inr_fst_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q) {Z : C} (h : P ⟶ Z),
CategoryTheory.CategoryStruct.comp self.inr (CategoryTheory.CategoryStruct.comp self.fst h) =
CategoryTheory.CategoryStruct.comp 0 h
This theorem, named `CategoryTheory.Limits.BinaryBicone.inr_fst_assoc`, is a statement about category theory, specifically about binary bicones and zero morphisms. In a category `C` that has zero morphisms, for any objects `P`, `Q`, and `Z` in `C` and any morphism `h` from `P` to `Z`, the composition of the morphism `inr` of a binary bicone `self` of `P` and `Q` with the composition of the morphism `fst` of `self` and `h` is the same as the composition of the zero morphism and `h`. In more mathematical terms, if we write composition as `≫`, we have `(self.inr ≫ (self.fst ≫ h)) = (0 ≫ h)`.
More concisely: In a category with zero morphisms, for any object $P$, any object $Q$, any object $Z$, any morphism $h$ from $P$ to $Z$, and any binary bicone $self$ from $P$ to $Q$, we have $(self.inr ≫ (self.fst ≫ h)) = (0 ≫ h)$.
|
CategoryTheory.Limits.biproduct.map_π
theorem CategoryTheory.Limits.biproduct.map_π :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
[inst_3 : CategoryTheory.Limits.HasBiproduct g] (p : (j : J) → f j ⟶ g j) (j : J),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.map p)
(CategoryTheory.Limits.biproduct.π g j) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j) (p j)
The theorem `CategoryTheory.Limits.biproduct.map_π` states that for any category `C`, which possesses zero morphisms and for any pair of functions `f` and `g` from `J` to `C`, such that `C` has biproducts of both `f` and `g`, and for any function `p` from elements of `J` to morphisms from `f j` to `g j` for each `j` in `J`, the composition of the map from the biproduct of `f` to the biproduct of `g` induced by `p` and the projection onto the `j`-th summand of the biproduct of `g` is equal to the composition of the projection onto the `j`-th summand of the biproduct of `f` and the `j`-th component of `p`. In mathematical terms, this says that the diagram involving the biproducts and the maps `p` commutes.
More concisely: For any category with zero morphisms having biproducts of `f` and `g` from `J`, and a function `p` from `J` to morphisms from `f j` to `g j`, the diagram commuting between the projections and `p` components of the biproducts of `f` and `g` holds.
|
CategoryTheory.Limits.biprod.lift_fst
theorem CategoryTheory.Limits.biprod.lift_fst :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{W X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift f g) CategoryTheory.Limits.biprod.fst = f
This theorem states that for any category `C` with zero morphisms, and any objects `W`, `X`, `Y` in `C` where `X` and `Y` form a binary biproduct, the composition of the lift morphism from `W` to the biproduct `X ⊞ Y` with the projection onto the first summand `X` of the biproduct is equal to the original morphism `f : W ⟶ X`. In essence, the theorem is a statement about morphism composition in categories involving binary biproducts.
More concisely: For any category with zero morphisms and any objects forming a binary biproduct, the lift morphism from one object to the biproduct and the projection onto the first summand compose to give the original morphism.
|
CategoryTheory.Limits.biproduct.map_π_assoc
theorem CategoryTheory.Limits.biproduct.map_π_assoc :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
[inst_3 : CategoryTheory.Limits.HasBiproduct g] (p : (j : J) → f j ⟶ g j) (j : J) {Z : C} (h : g j ⟶ Z),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.map p)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π g j) h) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j)
(CategoryTheory.CategoryStruct.comp (p j) h)
The theorem `CategoryTheory.Limits.biproduct.map_π_assoc` states that for any type `J` and any type `C` that forms a category with zero morphisms, given two functions `f` and `g` from `J` to `C` that have biproducts, and for any mapping `p` from each element of `J` to a morphism from `f j` to `g j` for each `j` in `J`, then for any `j` in `J` and any object `Z` in `C` with a morphism `h` from `g j` to `Z`, the composition of the biproduct map of `p` with the composition of the projection onto a summand of the biproduct of `g` at `j` and `h`, is equal to the composition of the projection onto a summand of the biproduct of `f` at `j` and the composition of `p j` and `h`. This theorem describes a property of category theory morphism composition in relation to biproduct maps and projections in the category.
More concisely: For any type `J`, given functions `f` and `g` from `J` to a category `C` with zero morphisms, and for any mapping `p : J -> Morp(C) (f _ to g _)`, the diagram commuting with both projections of the biproduct of `g` and `h` from `g j` to `Z` implies the commutativity of diagrams with the projections of the biproducts of `f` and `h` from `f j` to `Z`.
|
CategoryTheory.Limits.biprod.inr_desc_assoc
theorem CategoryTheory.Limits.biprod.inr_desc_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{W X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) {Z : C} (h : W ⟶ Z),
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.desc f g) h) =
CategoryTheory.CategoryStruct.comp g h
This theorem, `CategoryTheory.Limits.biprod.inr_desc_assoc`, states that for any category `C` with zero morphisms and binary biproducts, given three objects `X`, `Y`, `W` in `C` and a fourth object `Z`, and morphisms `f: X ⟶ W`, `g: Y ⟶ W`, `h: W ⟶ Z`, the composition of the inclusion into the second summand of the binary biproduct `Y ⟶ X ⊞ Y` (denoted as `CategoryTheory.Limits.biprod.inr`), with the composition of the morphism `CategoryTheory.Limits.biprod.desc f g` and `h`, is equal to the composition of the morphism `g` and `h`. In other words, this theorem is about the associativity property in the context of categorical biproducts.
More concisely: For any category with zero morphisms and binary biproducts, the inclusion into the second summand of a binary biproduct and the composition of two morphisms is equal to the composition of those morphisms in that order.
|
CategoryTheory.Limits.biprod.isoProd_hom
theorem CategoryTheory.Limits.biprod.isoProd_hom :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
(CategoryTheory.Limits.biprod.isoProd X Y).hom =
CategoryTheory.Limits.prod.lift CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd
The theorem `CategoryTheory.Limits.biprod.isoProd_hom` states that, in any category `C` with zero morphisms and binary biproducts, for any two objects `X` and `Y` in `C`, the morphism component of the isomorphism from the binary biproduct of `X` and `Y` to their binary product is given by lifting the pair of projections from the biproduct (i.e., the first and second projection morphisms). In other words, this theorem connects the concepts of binary biproduct and binary product in a category.
More concisely: In any category with zero morphisms and binary biproducts, the morphism component of the isomorphism from the binary biproduct of two objects to their binary product is given by the pair of projections from the biproduct.
|
CategoryTheory.Limits.BiconeMorphism.wπ
theorem CategoryTheory.Limits.BiconeMorphism.wπ :
∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {A B : CategoryTheory.Limits.Bicone F}
(self : CategoryTheory.Limits.BiconeMorphism A B) (j : J),
CategoryTheory.CategoryStruct.comp self.hom (B.π j) = A.π j
This theorem is about category theory and limits, specifically on the concept of a bicone morphism. It states that for any category `C` with zero morphisms, any functor `F` from type `J` to `C`, and any two bicones `A` and `B` over `F`, every bicone morphism from `A` to `B` has the property that its composition with the projection `B.π` at any index `j` is equal to the projection `A.π` at the same index. This means that the triangle formed by the two natural transformations `self.hom` and `B.π j`, and `A.π j`, commutes.
In other words, in the context of category theory, this theorem ensures the commutativity of a particular diagram involving bicones and bicone morphisms, which is an essential property in the study of limits and colimits of functors.
More concisely: For any category with zero morphisms, given a functor and two bicones over it, every bicone morphism makes the diagram commute where the projection of one bicone at an index equals the projection of the other bicone at the same index.
|
CategoryTheory.Limits.biproduct.ι_π_assoc
theorem CategoryTheory.Limits.biproduct.ι_π_assoc :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : DecidableEq J] (f : J → C)
[inst_3 : CategoryTheory.Limits.HasBiproduct f] (j j' : J) {Z : C} (h : f j' ⟶ Z),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j') h) =
CategoryTheory.CategoryStruct.comp (if h : j = j' then CategoryTheory.eqToHom ⋯ else 0) h
This theorem, `CategoryTheory.Limits.biproduct.ι_π_assoc`, states that in a category `C` (which is assumed to have zero morphisms and a biproduct for a certain function `f` from a type `J` to `C`), for any two objects `j` and `j'` from `J` and any morphism `h` from `f j'` to another object `Z` in `C`, the composition of the `ι` morphism for `j` and the composition of the `π` morphism for `j'` and `h` is equal to the composition of an equality morphism or zero (depending on whether `j` equals `j'`) and `h`. The `ι` and `π` morphisms here are the inclusion and projection morphisms for a summand of a biproduct, respectively. The equality check between `j` and `j'` is assumed to be decidable.
More concisely: For any category with zero morphisms and biproducts, the composition of the inclusion morphism for one summand and the composition of the projection morphism for another summand with any morphism between them is equal to the morphism between the summands if they are equal, and zero otherwise.
|
CategoryTheory.Limits.Bicone.ι_π
theorem CategoryTheory.Limits.Bicone.ι_π :
∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (self : CategoryTheory.Limits.Bicone F)
(j j' : J),
CategoryTheory.CategoryStruct.comp (self.ι j) (self.π j') = if h : j = j' then CategoryTheory.eqToHom ⋯ else 0
This theorem, `CategoryTheory.Limits.Bicone.ι_π`, states the following property in the context of category theory and its related structure known as a Bicone. Given a type `J` and a category `C` with zero morphisms, and a type function `F` from `J` to `C`, and a Bicone `F` structure `self`, for each pair of entities `j` and `j'` from `J`, the composition of the morphism `ι j` (from `F j` to the bicone's object `pt`) with the morphism `π j'` (from `pt` to `F j'`) is equivalent to the identity morphism if `j` and `j'` are the same, and it is equivalent to the zero morphism otherwise. In other words, the theorem is stating a property about the interplay of morphisms in a Bicone, which is a structure used to encapsulate the common pattern of a pair of "cones" (collections of morphisms) in category theory.
More concisely: For any Bicone `self` over a category `C` with zero morphisms and type `J`, the composition of `ι j` and `π j'` is the identity morphism if `j = j'`, and the zero morphism otherwise.
|
CategoryTheory.Limits.biprod.braid_natural
theorem CategoryTheory.Limits.biprod.braid_natural :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f g)
(CategoryTheory.Limits.biprod.braiding Y W).hom =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.braiding X Z).hom
(CategoryTheory.Limits.biprod.map g f)
This theorem asserts that in any category endowed with zero morphisms and binary biproducts, given any four objects `W`, `X`, `Y`, and `Z`, and any two morphisms `f : X ⟶ Y` and `g : Z ⟶ W`, the composition of the map induced by `f` and `g` and the braiding isomorphism between `Y` and `W` is equal to the composition of the braiding isomorphism between `X` and `Z` and the map induced by `g` and `f`. In other words, the braiding isomorphism can be "passed through" a map by changing the order of the morphisms. This statement is a fundamental property of braided monoidal categories, which are categories that have a tensor product and a notion of commutativity (the braiding) that is compatible with the tensor product.
More concisely: In a braided monoidal category with zero morphisms and binary biproducts, the composition of the braiding isomorphism between `X` and `Z`, the map induced by `f : X ⟶ Y`, and `g : Z ⟶ W` is equal to the composition of the map induced by `g` and `f`, and the braiding isomorphism between `Y` and `W`.
|
CategoryTheory.Limits.HasBiproduct.exists_biproduct
theorem CategoryTheory.Limits.HasBiproduct.exists_biproduct :
∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} [self : CategoryTheory.Limits.HasBiproduct F],
Nonempty (CategoryTheory.Limits.LimitBicone F)
The theorem `CategoryTheory.Limits.HasBiproduct.exists_biproduct` states that for any category `C` with zero morphisms and any functor `F` from a type `J` to `C` such that `F` has a biproduct, there exists a `LimitBicone` of `F`. In category theory, a `LimitBicone` represents a specific bicone which is both a limit and a colimit of a given diagram, indicating the existence of a biproduct.
More concisely: For any category with zero morphisms and any functor with a biproduct, there exists a limit-colimit pair (bicone) representing the biproduct.
|
CategoryTheory.Limits.BinaryBicone.inl_snd
theorem CategoryTheory.Limits.BinaryBicone.inl_snd :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q),
CategoryTheory.CategoryStruct.comp self.inl self.snd = 0
This theorem states that in the context of a category `C`, which is a mathematical structure that captures the abstract idea of composition, and where `C` has zero morphisms (maps between objects that are identity for composition), for any pair of objects `P` and `Q` in `C`, if we have a binary bicone (a structure with a cone point `X`, maps from `X` to both `P` and `Q`, and maps from both `P` and `Q` to `X`, satisfying certain conditions), the composition of the map `inl` (from `X` to `P`) and the map `snd` (from `Q` to `X`) is the zero morphism in `C`. This is one of the conditions defining a binary bicone.
More concisely: In a category with zero morphisms, the composition of the maps from a binary bicone's middle object to its two end objects is the identity morphism at the zero morphism.
|
CategoryTheory.Limits.biproduct.hom_ext
theorem CategoryTheory.Limits.biproduct.hom_ext :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
{Z : C} (g h : Z ⟶ ⨁ f),
(∀ (j : J),
CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.biproduct.π f j) =
CategoryTheory.CategoryStruct.comp h (CategoryTheory.Limits.biproduct.π f j)) →
g = h
The theorem `CategoryTheory.Limits.biproduct.hom_ext` states that in the context of a category `C` with zero morphisms and a function `f : J → C` for which a biproduct exists, for any object `Z` in `C` and any two morphisms `g, h : Z ⟶ ⨁ f`, if the composition of `g` and `h` with the projection onto every summand of the biproduct of `f` is the same, then `g` and `h` themselves must be equal. This theorem essentially asserts the uniqueness of morphisms into a biproduct in the category, up to composition with the biproduct's projections.
More concisely: In a category with zero morphisms, if two morphisms from an object to the biproduct of a function have the same composition with the projections of the biproduct, then they are equal.
|
CategoryTheory.Limits.biproduct.lift_π
theorem CategoryTheory.Limits.biproduct.lift_π :
∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
{P : C} (p : (b : J) → P ⟶ f b) (j : J),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift p)
(CategoryTheory.Limits.biproduct.π f j) =
p j
The theorem `CategoryTheory.Limits.biproduct.lift_π` states that for any category `C` with zero morphisms and a function `f : J → C` that has a biproduct, given a collection of morphisms `p : (b : J) → P ⟶ f b` from some object `P` in `C` to the objects in the image of `f`, if we first apply the lift operation to `p` to obtain a morphism from `P` to the biproduct of `f` and then apply the projection onto the `j`-th summand of the biproduct, the result is the same as applying the `j`-th morphism in the collection `p`. This theorem asserts a fundamental property of biproducts in a category, namely, the property that makes the lift operation a left inverse to the family of projection operations.
More concisely: For any category with zero morphisms and a biproduct, the lift of a collection of morphisms to the biproduct and subsequent projection onto a summand is equivalent to applying the corresponding morphism in the collection.
|
CategoryTheory.Limits.biprod.inl_fst
theorem CategoryTheory.Limits.biprod.inl_fst :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.fst =
CategoryTheory.CategoryStruct.id X
This theorem states that for any category `C` which has zero morphisms and a binary biproduct of `X` and `Y`, the composition of the morphism that includes `X` into the binary biproduct of `X` and `Y` (`CategoryTheory.Limits.biprod.inl`) and the morphism that projects the first summand of the binary biproduct onto `X` (`CategoryTheory.Limits.biprod.fst`) is the identity morphism on `X` (`CategoryTheory.CategoryStruct.id X`). In other words, if you include `X` into a binary biproduct and then project back to `X`, you get back where you started. This is a formal expression of one of the basic properties of biproducts in category theory.
More concisely: In any category with zero morphisms and binary biproducts, the inclusion morphism of one summand into the biproduct followed by the projection morphism of the biproduct onto that summand is the identity morphism on that summand.
|
CategoryTheory.Limits.biprod.associator_natural
theorem CategoryTheory.Limits.biprod.associator_natural :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {U V W X Y Z : C} (f : U ⟶ X) (g : V ⟶ Y) (h : W ⟶ Z),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (CategoryTheory.Limits.biprod.map f g) h)
(CategoryTheory.Limits.biprod.associator X Y Z).hom =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.associator U V W).hom
(CategoryTheory.Limits.biprod.map f (CategoryTheory.Limits.biprod.map g h))
This theorem is stating that in a category with zero morphisms and binary biproducts, for any objects `U`, `V`, `W`, `X`, `Y`, and `Z`, and morphisms `f : U ⟶ X`, `g : V ⟶ Y`, and `h : W ⟶ Z`, the composition of the `biprod.map` (which maps a pair of morphisms to a morphism between the biproducts) with the `associator` (which provides a canonical isomorphism asserting the associativity of the biproduct up to isomorphism) can be rearranged. More specifically, the order of the `map` and `associator` can be swapped while maintaining equivalence. This theorem is a part of the coherence conditions for the categorical concept of biproducts, which are a generalization of the concept of direct sum and product in an abelian category.
More concisely: In a category with zero morphisms and binary biproducts, the composition of `biprod.map` with the `associator` is equivalent to the composition of the `associator` with `biprod.map`.
|
CategoryTheory.Limits.biprod.symmetry
theorem CategoryTheory.Limits.biprod.symmetry :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] (P Q : C),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.braiding P Q).hom
(CategoryTheory.Limits.biprod.braiding Q P).hom =
CategoryTheory.CategoryStruct.id (P ⊞ Q)
This theorem, named `CategoryTheory.Limits.biprod.symmetry`, states a property about the structure of a category that has binary biproducts and zero morphisms. Specifically, given any type `C` that forms a category with binary biproducts and zero morphisms, and any two objects `P` and `Q` from `C`, the composition of the braiding isomorphism from `P` to `Q` and the braiding isomorphism from `Q` to `P` is the identity morphism on the biproduct of `P` and `Q`. In essence, it says that "undoing" the braiding operation by applying it again in the opposite direction gets you back to where you started, demonstrating the symmetry of the braiding operation.
More concisely: In a category with binary biproducts and zero morphisms, the composition of the braiding isomorphisms from objects P and Q is the identity morphism on their biproduct.
|
CategoryTheory.Limits.biprod.conePointUniqueUpToIso_inv
theorem CategoryTheory.Limits.biprod.conePointUniqueUpToIso_inv :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
(X Y : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] {b : CategoryTheory.Limits.BinaryBicone X Y}
(hb : b.IsBilimit),
(hb.isLimit.conePointUniqueUpToIso (CategoryTheory.Limits.BinaryBiproduct.isLimit X Y)).inv =
CategoryTheory.Limits.biprod.desc b.inl b.inr
This theorem, named `biprod.conePointUniqueUpToIso_inv`, is an auxiliary lemma for `biprod.uniqueUpToIso` in Category Theory, specifically for the limits of categories. Given a category `C` with zero morphisms and a binary biproduct `X Y`, along with a binary bicone `b` which has a bilimit, the theorem states that the inverse of the unique isomorphism from the limit cone of the given binary biproduct to the cone `b` is equal to the biproduct descriptor of the morphisms `inl` and `inr` of the binary bicone.
More concisely: Given a category with zero morphisms, a binary biproduct with a binary bicone having a bilimit, the inverse of the limit cone isomorphism to the binary bicone is equal to the biproduct descriptor of the morphisms `inl` and `inr`.
|
CategoryTheory.Limits.BiconeMorphism.wι
theorem CategoryTheory.Limits.BiconeMorphism.wι :
∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {A B : CategoryTheory.Limits.Bicone F}
(self : CategoryTheory.Limits.BiconeMorphism A B) (j : J),
CategoryTheory.CategoryStruct.comp (A.ι j) self.hom = B.ι j
The theorem `CategoryTheory.Limits.BiconeMorphism.wι` states that for any type `J`, category `C` (where `C` has zero morphisms), a functor `F` from `J` to `C`, and two bicones `A` and `B` over `F`, given a bicone morphism `self` from `A` to `B` and an object `j` of `J`, the composition of the morphism `A.ι j` and `self.hom` (where `A.ι j` is the morphism from the vertex of the bicone `A` to the object `F j`, and `self.hom` is the morphism from the vertex of `A` to that of `B`) equals the morphism `B.ι j` (the morphism from the vertex of the bicone `B` to the object `F j`). In simpler terms, it represents the commutativity of the diagram formed by the two natural transformations and `hom` in the context of category theory.
More concisely: Given a category `C` with zero morphisms, a functor `F` from a type `J` to `C`, two bicones `A` and `B` over `F`, a bicone morphism `self` from `A` to `B`, and an object `j` of `J`, the morphisms `A.ι j` and `B.ι j` from their respective vertices to `F j` are equal via `self.hom`.
|