CategoryTheory.Limits.HasBinaryBiproduct.of_hasBinaryProduct
theorem CategoryTheory.Limits.HasBinaryBiproduct.of_hasBinaryProduct :
β {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (X Y : C)
[inst_2 : CategoryTheory.Limits.HasBinaryProduct X Y], CategoryTheory.Limits.HasBinaryBiproduct X Y
This theorem states that in a preadditive category, if a binary product exists for two objects `X` and `Y`, then a binary biproduct also exists for these two objects. Here, a preadditive category is a category where all hom-sets are provided with an abelian group structure, and composition of morphisms is bilinear. The binary product of `X` and `Y` is essentially a limit of the pair `(X, Y)`, while a binary biproduct is a specific type of limit that exists in preadditive categories.
More concisely: In a preadditive category, the existence of a binary product for two objects implies the existence of a binary biproduct.
|
CategoryTheory.Limits.HasBiproduct.of_hasCoproduct
theorem CategoryTheory.Limits.HasBiproduct.of_hasCoproduct :
β {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {J : Type}
[inst_2 : Finite J] (f : J β C) [inst_3 : CategoryTheory.Limits.HasCoproduct f],
CategoryTheory.Limits.HasBiproduct f
The theorem `CategoryTheory.Limits.HasBiproduct.of_hasCoproduct` states that in a preadditive category, if a coproduct exists for a functor `f : J β C` (where `J` is a finite type), then a biproduct also exists for the same functor `f`. Here, a preadditive category is a category in which all hom-sets have an additive structure, and biproducts and coproducts are special types of limits and colimits respectively. This theorem asserts a particular condition under which the existence of a coproduct ensures the existence of a biproduct.
More concisely: In a preadditive category, the existence of a coproduct for a functor from a finite type guarantees the existence of a biproduct for the same functor.
|
CategoryTheory.Limits.biproduct.total
theorem CategoryTheory.Limits.biproduct.total :
β {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {J : Type}
[inst_2 : Fintype J] {f : J β C} [inst_3 : CategoryTheory.Limits.HasBiproduct f],
(Finset.univ.sum fun j =>
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.Ο f j)
(CategoryTheory.Limits.biproduct.ΞΉ f j)) =
CategoryTheory.CategoryStruct.id (β¨ f)
This theorem states that in any preadditive category, for any collection of objects indexed by a finite set `J`, the sum over `J` of the compositions of the projection and the inclusion morphisms for each object is the identity morphism on the biproduct of the collection. In other words, if we consider a biproduct of objects in the category and map each object to itself through the biproduct (project down to the object, then include it back into the biproduct), the sum of these operations over all objects is the same as doing nothing (the identity operation on the biproduct).
More concisely: In any preadditive category, the sum of the composition of projection and inclusion morphisms for all objects in a finite indexed collection equals the identity morphism on the biproduct of those objects.
|
CategoryTheory.Limits.biprod.add_eq_lift_desc_id
theorem CategoryTheory.Limits.biprod.add_eq_lift_desc_id :
β {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
(f g : X βΆ Y) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct Y Y],
f + g =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift f g)
(CategoryTheory.Limits.biprod.desc (CategoryTheory.CategoryStruct.id Y)
(CategoryTheory.CategoryStruct.id Y))
The theorem `CategoryTheory.Limits.biprod.add_eq_lift_desc_id` states that for any category `C` with a preadditive structure and binary biproducts, and for any objects `X` and `Y` in `C` and morphisms `f` and `g` from `X` to `Y`, the sum of `f` and `g` is equal to the composition of the lift of `f` and `g` with the descendent of the identity morphism on `Y`. This demonstrates that the existence of binary biproducts in `C` implies the uniqueness of the preadditive structure on `C`, as the sum operation in the preadditive category is uniquely determined by the binary biproduct structure.
More concisely: For any preadditive category with binary biproducts, the sum of two morphisms is equal to the composition of their lift and the descendant of the identity morphism on the second object.
|
CategoryTheory.Limits.hasBiproduct_of_total
theorem CategoryTheory.Limits.hasBiproduct_of_total :
β {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {J : Type}
[inst_2 : Fintype J] {f : J β C} (b : CategoryTheory.Limits.Bicone f),
(Finset.univ.sum fun j => CategoryTheory.CategoryStruct.comp (b.Ο j) (b.ΞΉ j)) =
CategoryTheory.CategoryStruct.id b.pt β
CategoryTheory.Limits.HasBiproduct f
This theorem states that in the context of a preadditive category, given a function `f` from a finite set `J` to the category `C`, and a bicone `b` for `f`, if the sum of compositions of morphisms in `b` over all elements in `J` equals the identity morphism on the object `b.pt` (which is represented as `β j : J, b.Ο j β« b.ΞΉ j = π b.X` in mathematical notation), then `f` has a biproduct. In other words, such a bicone is a limit cone and a colimit cocone.
Let me give a bit more context: A preadditive category is a category in which the homsets have the structure of an abelian group, and the composition of morphisms distributes over the group operation. A bicone is a generalization of the notion of a cone and a co-cone in category theory. A biproduct in category theory extends the notion of a product and coproduct. In other words, this theorem provides a condition under which we can construct a biproduct in a preadditive category.
More concisely: In a preadditive category, if for a function from a finite set to the category and a bicone for that function, the sum of compositions of morphisms in the bicone equals the identity on the target object, then the function has a biproduct and the bicone is both a limit cone and a colimit cocone.
|
CategoryTheory.Limits.biprod.lift_desc
theorem CategoryTheory.Limits.biprod.lift_desc :
β {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
[inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] {T U : C} {f : T βΆ X} {g : T βΆ Y} {h : X βΆ U} {i : Y βΆ U},
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift f g)
(CategoryTheory.Limits.biprod.desc h i) =
CategoryTheory.CategoryStruct.comp f h + CategoryTheory.CategoryStruct.comp g i
The theorem `CategoryTheory.Limits.biprod.lift_desc` states that for any category `C` that is preadditive (meaning that it has a binary operation compatible with its categorical structure) and has binary biproducts, given objects `X`, `Y`, `T`, and `U` in `C`, and morphisms `f` from `T` to `X`, `g` from `T` to `Y`, `h` from `X` to `U`, and `i` from `Y` to `U`, the composition of the biproduct lift of `f` and `g` with the biproduct descendent of `h` and `i` is equal to the sum of the compositions of `f` and `h` with `g` and `i`. In other words, it asserts the equality between two specific ways of completing a commutative square in a preadditive category with binary biproducts.
More concisely: In a preadditive category with binary biproducts, the composition of the biproduct lift of a morphism with the biproduct descent of another morphism is equal to the sum of the compositions of the two morphisms.
|
CategoryTheory.Limits.IsBilimit.total
theorem CategoryTheory.Limits.IsBilimit.total :
β {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {J : Type}
[inst_2 : Fintype J] {f : J β C} {b : CategoryTheory.Limits.Bicone f},
b.IsBilimit β
(Finset.univ.sum fun j => CategoryTheory.CategoryStruct.comp (b.Ο j) (b.ΞΉ j)) =
CategoryTheory.CategoryStruct.id b.pt
This theorem states that for any category `C` that is preadditive, any finite type `J`, any function `f` from `J` to `C`, and any bicone `b` of `f`, if `b` is a bilimit, then the sum of the compositions of `b.Ο j` and `b.ΞΉ j` over all elements `j` in the universal finite set of `J` is equal to the identity morphism on the apex of `b`. In other words, for a given bilimit bicone, the total of all compositions of outgoing and incoming morphisms for all objects is equal to the identity of the apex of the bicone.
More concisely: For any preadditive category `C`, given a finite type `J`, a function `f : J -> C`, a bicone `b` on `f` that is a bilimit, the sum of the compositions of `b.Ο j` and `b.ΞΉ j` for all `j` in `J` equals the identity morphism on the apex of `b`.
|
CategoryTheory.Limits.HasBiproduct.of_hasProduct
theorem CategoryTheory.Limits.HasBiproduct.of_hasProduct :
β {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {J : Type}
[inst_2 : Finite J] (f : J β C) [inst_3 : CategoryTheory.Limits.HasProduct f],
CategoryTheory.Limits.HasBiproduct f
The theorem `CategoryTheory.Limits.HasBiproduct.of_hasProduct` states that in a preadditive category (a category with a binary operation compatible with composition) C, if the product over a function `f : J -> C` exists, then the biproduct over `f` also exists. Here, `J` is a finite set and `f` maps elements of this set to objects in category `C`. The existence of a product over `f` is denoted by `CategoryTheory.Limits.HasProduct f` and the existence of a biproduct over `f` is denoted by `CategoryTheory.Limits.HasBiproduct f`. In essence, this theorem links the existence of products and biproducts in the realm of preadditive categories.
More concisely: In a preadditive category, the existence of a product implies the existence of a biproduct for any function from a finite set to objects in the category.
|
CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteProducts
theorem CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteProducts :
β {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
[inst_2 : CategoryTheory.Limits.HasFiniteProducts C], CategoryTheory.Limits.HasFiniteBiproducts C
This theorem states that for any Type 'C', if 'C' is a category, preadditive (a mathematical property indicating that the operation of addition is available and behaves as expected), and has finite products (an operation in category theory that generalizes the cartesian product), then 'C' necessarily has finite biproducts (a concept in category theory that generalizes the notions of product and coproduct).
In other words, the presence of finite products in a preadditive category implies the presence of finite biproducts.
More concisely: In a preadditive category with finite products, finite biproducts exist.
|
CategoryTheory.Limits.HasBinaryBiproducts.of_hasBinaryProducts
theorem CategoryTheory.Limits.HasBinaryBiproducts.of_hasBinaryProducts :
β {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
[inst_2 : CategoryTheory.Limits.HasBinaryProducts C], CategoryTheory.Limits.HasBinaryBiproducts C
This theorem states that for any type `C` which has the structure of a category, if this category is preadditive (meaning that it has a compatible addition operation on the morphisms) and it has binary products (meaning that for each pair of objects, there is another object that represents their product in some sense), then it has binary biproducts. In other words, in a preadditive category, the existence of binary products guarantees the existence of binary biproducts. A biproduct in a category is both a product and a coproduct, and can be thought of as a generalization of the concept of a direct sum in linear algebra.
More concisely: In a preadditive category with binary products, binary biproducts exist.
|
CategoryTheory.Limits.HasBinaryBiproducts.of_hasBinaryCoproducts
theorem CategoryTheory.Limits.HasBinaryBiproducts.of_hasBinaryCoproducts :
β {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
[inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C], CategoryTheory.Limits.HasBinaryBiproducts C
The theorem `CategoryTheory.Limits.HasBinaryBiproducts.of_hasBinaryCoproducts` states that in the context of a preadditive category, if all binary coproducts exist, then all binary biproducts also exist. Here, a preadditive category is a category in which every hom-set has the structure of an abelian group, and composition of morphisms is bilinear. Binary coproducts and binary biproducts are specific kinds of limits and colimits in category theory.
More concisely: In a preadditive category, the existence of binary coproducts implies the existence of binary biproducts.
|
CategoryTheory.Biprod.ofComponents_comp
theorem CategoryTheory.Biprod.ofComponents_comp :
β {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
[inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {Xβ Xβ Yβ Yβ Zβ Zβ : C} (fββ : Xβ βΆ Yβ) (fββ : Xβ βΆ Yβ)
(fββ : Xβ βΆ Yβ) (fββ : Xβ βΆ Yβ) (gββ : Yβ βΆ Zβ) (gββ : Yβ βΆ Zβ) (gββ : Yβ βΆ Zβ) (gββ : Yβ βΆ Zβ),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Biprod.ofComponents fββ fββ fββ fββ)
(CategoryTheory.Biprod.ofComponents gββ gββ gββ gββ) =
CategoryTheory.Biprod.ofComponents
(CategoryTheory.CategoryStruct.comp fββ gββ + CategoryTheory.CategoryStruct.comp fββ gββ)
(CategoryTheory.CategoryStruct.comp fββ gββ + CategoryTheory.CategoryStruct.comp fββ gββ)
(CategoryTheory.CategoryStruct.comp fββ gββ + CategoryTheory.CategoryStruct.comp fββ gββ)
(CategoryTheory.CategoryStruct.comp fββ gββ + CategoryTheory.CategoryStruct.comp fββ gββ)
This theorem, `CategoryTheory.Biprod.ofComponents_comp`, states that for any type `C` that is a category, is preadditive, and has binary biproducts, and for any objects `Xβ`, `Xβ`, `Yβ`, `Yβ`, `Zβ`, `Zβ` in `C`, given eight morphisms `fββ : Xβ βΆ Yβ`, `fββ : Xβ βΆ Yβ`, `fββ : Xβ βΆ Yβ`, `fββ : Xβ βΆ Yβ`, `gββ : Yβ βΆ Zβ`, `gββ : Yβ βΆ Zβ`, `gββ : Yβ βΆ Zβ`, `gββ : Yβ βΆ Zβ`, the composition of the biproducts of the first four morphisms and the latter four morphisms equals the biproduct of the sum of compositions of the morphisms. The specific compositions that make up the components of the resulting biproduct are determined by combining the morphisms in a certain pattern: the first component is the sum of the composition of `fββ` and `gββ` and the composition of `fββ` and `gββ`, and similarly for the other components.
More concisely: For any preadditive category `C` with binary biproducts, the composition of the biproducts of four morphisms and the latter four morphisms equals the biproduct of the sum of their compositions, where the first (respectively, second) component is the sum of the compositions of the first and third (respectively, second and fourth) pairs of morphisms.
|
CategoryTheory.Limits.HasBinaryBiproduct.of_hasBinaryCoproduct
theorem CategoryTheory.Limits.HasBinaryBiproduct.of_hasBinaryCoproduct :
β {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (X Y : C)
[inst_2 : CategoryTheory.Limits.HasBinaryCoproduct X Y], CategoryTheory.Limits.HasBinaryBiproduct X Y
In the context of a preadditive category (a category in which every hom-set is equipped with an abelian group structure), the theorem `CategoryTheory.Limits.HasBinaryBiproduct.of_hasBinaryCoproduct` states that given any two objects `X` and `Y` in the category, if the binary coproduct of `X` and `Y` exists (symbolized as `CategoryTheory.Limits.HasBinaryCoproduct X Y`), then the binary biproduct of `X` and `Y` also exists (indicated as `CategoryTheory.Limits.HasBinaryBiproduct X Y`). In other words, the existence of a binary coproduct implies the existence of a binary biproduct in a preadditive category.
More concisely: In a preadditive category, the existence of a binary coproduct implies the existence of a binary biproduct for any two objects.
|
CategoryTheory.Biprod.inl_ofComponents
theorem CategoryTheory.Biprod.inl_ofComponents :
β {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
[inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {Xβ Xβ Yβ Yβ : C} (fββ : Xβ βΆ Yβ) (fββ : Xβ βΆ Yβ)
(fββ : Xβ βΆ Yβ) (fββ : Xβ βΆ Yβ),
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
(CategoryTheory.Biprod.ofComponents fββ fββ fββ fββ) =
CategoryTheory.CategoryStruct.comp fββ CategoryTheory.Limits.biprod.inl +
CategoryTheory.CategoryStruct.comp fββ CategoryTheory.Limits.biprod.inr
This theorem in category theory states that for any category `C` that is 'preadditive' (i.e., its morphisms have an additive structure) and has binary biproducts (a kind of limit), for any four objects `Xβ, Xβ, Yβ, Yβ` in `C` and morphisms `fββ : Xβ βΆ Yβ`, `fββ : Xβ βΆ Yβ`, `fββ : Xβ βΆ Yβ`, `fββ : Xβ βΆ Yβ` in this category, the composition of the morphism for the inclusion into the first part of a binary biproduct ('inl') with the morphism `fββ` plus the composition of `fββ` with the morphism for the inclusion into the second part of a binary biproduct ('inr') is equal to the composition of 'inl' with a binary biproduct of the four morphisms. That is, morphisms in a preadditive category with binary biproducts distribute over the biproduct in a specific way.
More concisely: In a preadditive category with binary biproducts, the diagram commutes, where the inclusion morphisms into the first and second parts of a binary biproduct, and the given morphisms compose with these inclusions, is equal to the binary biproduct of the given morphisms.
|
CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteCoproducts
theorem CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteCoproducts :
β {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
[inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C], CategoryTheory.Limits.HasFiniteBiproducts C
This theorem states that for any type `C` that is a category with preadditive properties and finite coproducts, this category `C` also has finite biproducts. In mathematical terms, if a category is preadditive (meaning it has a binary operation that is both associative and commutative, and has an identity element, like addition in the set of real numbers), and has finite coproducts (i.e., it has a 'sum' or 'union' operation for any finite collection of its objects), then it necessarily also has finite biproducts (which are simultaneously products and coproducts).
More concisely: If a preadditive category with finite coproducts has objects `A` and `B`, then there exists an object `P` and morphisms `i : A β P`, `j : B β P` such that `P` is the biproduct of `A` and `B`, i.e., `A β B β
A ββ B`.
|
CategoryTheory.Limits.biprod.total
theorem CategoryTheory.Limits.biprod.total :
β {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
[inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.inl +
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.inr =
CategoryTheory.CategoryStruct.id (X β Y)
This theorem states that in any preadditive category, for any binary biproduct of objects X and Y, the sum of the composition of the projection onto the first summand of the binary biproduct followed by the inclusion into the first summand, and the composition of the projection onto the second summand of the binary biproduct followed by the inclusion into the second summand, is equal to the identity morphism on the binary biproduct. In mathematical terms, it claims that `biprod.fst β« biprod.inl + biprod.snd β« biprod.inr = π (X β Y)`.
More concisely: In any preadditive category, the projections and inclusions of a binary biproduct sum up to the identity morphism: `biprod.fst β« biprod.inl + biprod.snd β« biprod.inr = π (X β Y)`.
|
CategoryTheory.Limits.biprod.add_eq_lift_id_desc
theorem CategoryTheory.Limits.biprod.add_eq_lift_id_desc :
β {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
(f g : X βΆ Y) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X X],
f + g =
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X))
(CategoryTheory.Limits.biprod.desc f g)
The theorem `CategoryTheory.Limits.biprod.add_eq_lift_id_desc` states that in the context of a category `C` which has a binary biproduct structure for objects `X` and `X`, and is preadditive, the sum of two morphisms `f` and `g` from `X` to `Y` equals the composition of two operations: first lifting the identity morphism on `X` to the biproduct of `X` and `X`, and then descends to `Y` via the morphisms `f` and `g`. This implies that in the presence of binary biproducts, a preadditive structure is unique if it exists.
More concisely: In a preadditive category with binary biproducts for objects X and X, the sum of morphisms f and g from X to Y is equal to the composition of lifting the identity on X to the biproduct and descending via f and g.
|
CategoryTheory.Limits.hasBinaryBiproduct_of_total
theorem CategoryTheory.Limits.hasBinaryBiproduct_of_total :
β {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
(b : CategoryTheory.Limits.BinaryBicone X Y),
CategoryTheory.CategoryStruct.comp b.fst b.inl + CategoryTheory.CategoryStruct.comp b.snd b.inr =
CategoryTheory.CategoryStruct.id b.pt β
CategoryTheory.Limits.HasBinaryBiproduct X Y
The theorem `CategoryTheory.Limits.hasBinaryBiproduct_of_total` states that in any preadditive category (a category where the hom-sets are abelian groups and composition of morphisms distributes over the group operation), for any two objects `X` and `Y`, and any binary bicone `b` for `X` and `Y`, if the condition `total` holds (i.e., the composition `b.fst β« b.inl + b.snd β« b.inr` is equal to the identity morphism on `b.X`), then `X` and `Y` have a binary biproduct. That is, the binary bicone `b` is both a limit cone and a colimit cocone.
In terms of category theory, this theorem essentially provides a condition under which a binary biproduct (a concept that combines both product and coproduct) can be constructed in a preadditive category.
More concisely: In a preadditive category, if a binary bicone between two objects satisfies the condition of having total morphisms, then it induces a binary biproduct.
|
CategoryTheory.Limits.biproduct.lift_desc
theorem CategoryTheory.Limits.biproduct.lift_desc :
β {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {J : Type}
[inst_2 : Fintype J] {f : J β C} [inst_3 : CategoryTheory.Limits.HasBiproduct f] {T U : C} {g : (j : J) β T βΆ f j}
{h : (j : J) β f j βΆ U},
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift g)
(CategoryTheory.Limits.biproduct.desc h) =
Finset.univ.sum fun j => CategoryTheory.CategoryStruct.comp (g j) (h j)
The theorem `CategoryTheory.Limits.biproduct.lift_desc` states that for any category `C` that is also preadditive, and for any finite type `J`, if we have objects and morphisms in `C` given by the functions `f`, `g`, and `h`, then the composition of 'lifting' the `g` morphisms into a biproduct and then 'descending' the `h` morphisms from the biproduct is equal to the sum (over all elements in the universal finite set of `J`) of the individual compositions of the `g` and `h` morphisms. In formal mathematical terms, if we lift `g` to a biproduct and then map this to `U` using `h`, it's the same as if we composed `g` and `h` for each element in `J` and then took their sum. This theorem is essentially a statement about the commutativity of diagrams in a preadditive category.
More concisely: For any preadditive category `C` and finite type `J`, the composition of lifting morphisms `g` to a biproduct and descending morphisms `h` from the biproduct is equal to the sum of the compositions of `g` and `h` for all elements in `J`.
|
CategoryTheory.Biprod.inr_ofComponents
theorem CategoryTheory.Biprod.inr_ofComponents :
β {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
[inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {Xβ Xβ Yβ Yβ : C} (fββ : Xβ βΆ Yβ) (fββ : Xβ βΆ Yβ)
(fββ : Xβ βΆ Yβ) (fββ : Xβ βΆ Yβ),
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr
(CategoryTheory.Biprod.ofComponents fββ fββ fββ fββ) =
CategoryTheory.CategoryStruct.comp fββ CategoryTheory.Limits.biprod.inl +
CategoryTheory.CategoryStruct.comp fββ CategoryTheory.Limits.biprod.inr
The theorem `CategoryTheory.Biprod.inr_ofComponents` states that in a category `C` with binary biproducts and preadditive structure, for any objects `Xβ`, `Xβ`, `Yβ`, `Yβ` in `C` and morphisms `fββ : Xβ βΆ Yβ`, `fββ : Xβ βΆ Yβ`, `fββ : Xβ βΆ Yβ`, `fββ : Xβ βΆ Yβ`, the composition of the inclusion morphism from the second component of the biproduct (`CategoryTheory.Limits.biprod.inr`) with the morphism defined by the matrix (`CategoryTheory.Biprod.ofComponents fββ fββ fββ fββ`) is equal to the sum of the composition of `fββ` and the inclusion morphism from the first component of the biproduct (`CategoryTheory.Limits.biprod.inl`) and the composition of `fββ` and `CategoryTheory.Limits.biprod.inr`. This theorem is essentially a property of morphisms between biproducts in an additive category, expressing how such morphisms interact with the canonical inclusion morphisms.
More concisely: In a preadditive category with binary biproducts, the composition of the inclusion morphism from the second component of a biproduct with a morphism defined by a matrix and the inclusion morphism from the first component, is equal to the sum of the composition of the second component inclusion with the given morphism and the composition of the second morphism and the inclusion morphism from the second component.
|