mathlib3 documentation

category_theory.preadditive.biproducts

Basic facts about biproducts in preadditive categories. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In (or between) preadditive categories,

There are connections between this material and the special case of the category whose morphisms are matrices over a ring, in particular the Schur complement (see linear_algebra.matrix.schur_complement). In particular, the declarations category_theory.biprod.iso_elim, category_theory.biprod.gaussian and matrix.invertible_of_from_blocks₁₁_invertible are all closely related.

In a preadditive category, we can construct a biproduct for f : J → C from any bicone b for f satisfying total : ∑ j : J, b.π j ≫ b.ι j = 𝟙 b.X.

(That is, such a bicone is a limit cone and a colimit cocone.)

Equations

In a preadditive category, we can construct a biproduct for f : J → C from any bicone b for f satisfying total : ∑ j : J, b.π j ≫ b.ι j = 𝟙 b.X.

(That is, such a bicone is a limit cone and a colimit cocone.)

In a preadditive category, any finite bicone which is a limit cone is in fact a bilimit bicone.

Equations

In a preadditive category, if the product over f : J → C exists, then the biproduct over f exists.

In a preadditive category, any finite bicone which is a colimit cocone is in fact a bilimit bicone.

Equations

In a preadditive category, if the coproduct over f : J → C exists, then the biproduct over f exists.

@[simp]

In any preadditive category, any biproduct satsifies ∑ j : J, biproduct.π f j ≫ biproduct.ι f j = 𝟙 (⨁ f)

@[simp]
theorem category_theory.limits.biproduct.lift_desc_assoc {C : Type u} [category_theory.category C] [category_theory.preadditive C] {J : Type} [fintype J] {f : J C} [category_theory.limits.has_biproduct f] {T U : C} {g : Π (j : J), T f j} {h : Π (j : J), f j U} {X' : C} (f' : U X') :
@[simp]
theorem category_theory.limits.biproduct.matrix_desc_assoc {C : Type u} [category_theory.category C] [category_theory.preadditive C] {J : Type} [fintype J] {K : Type} [fintype K] [category_theory.limits.has_finite_biproducts C] {f : J C} {g : K C} (m : Π (j : J) (k : K), f j g k) {P : C} (x : Π (k : K), g k P) {X' : C} (f' : P X') :
@[simp]
theorem category_theory.limits.biproduct.lift_matrix_assoc {C : Type u} [category_theory.category C] [category_theory.preadditive C] {J : Type} [fintype J] {K : Type} [fintype K] [category_theory.limits.has_finite_biproducts C] {f : J C} {g : K C} {P : C} (x : Π (j : J), P f j) (m : Π (j : J) (k : K), f j g k) {X' : C} (f' : ( λ (k : K), g k) X') :
theorem category_theory.limits.biproduct.matrix_map_assoc {C : Type u} [category_theory.category C] [category_theory.preadditive C] {J : Type} [fintype J] {K : Type} [fintype K] [category_theory.limits.has_finite_biproducts C] {f : J C} {g h : K C} (m : Π (j : J) (k : K), f j g k) (n : Π (k : K), g k h k) {X' : C} (f' : ( λ (k : K), h k) X') :
theorem category_theory.limits.biproduct.map_matrix_assoc {C : Type u} [category_theory.category C] [category_theory.preadditive C] {J : Type} [fintype J] {K : Type} [fintype K] [category_theory.limits.has_finite_biproducts C] {f g : J C} {h : K C} (m : Π (k : J), f k g k) (n : Π (j : J) (k : K), g j h k) {X' : C} (f' : ( λ (k : K), h k) X') :

In a preadditive category, we can construct a binary biproduct for X Y : C from any binary bicone b satisfying total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.X.

(That is, such a bicone is a limit cone and a colimit cocone.)

Equations

In a preadditive category, we can construct a binary biproduct for X Y : C from any binary bicone b satisfying total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.X.

(That is, such a bicone is a limit cone and a colimit cocone.)

In a preadditive category, if the product of X and Y exists, then the binary biproduct of X and Y exists.

In a preadditive category, if the coproduct of X and Y exists, then the binary biproduct of X and Y exists.

@[simp]

In any preadditive category, any binary biproduct satsifies biprod.fst ≫ biprod.inl + biprod.snd ≫ biprod.inr = 𝟙 (X ⊞ Y).

@[simp]

Every split mono f with a cokernel induces a binary bicone with f as its inl and the cokernel map as its snd. We will show in is_bilimit_binary_bicone_of_split_mono_of_cokernel that this binary bicone is in fact already a biproduct.

Equations

Every split epi f with a kernel induces a binary bicone with f as its snd and the kernel map as its inl. We will show in binary_bicone_of_is_split_mono_of_cokernel that this binary bicone is in fact already a biproduct.

Equations

The existence of binary biproducts implies that there is at most one preadditive structure.

The existence of binary biproducts implies that there is at most one preadditive structure.

@[protected, instance]

The existence of binary biproducts implies that there is at most one preadditive structure.

noncomputable def category_theory.biprod.of_components {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_binary_biproducts C] {X₁ X₂ Y₁ Y₂ : C} (f₁₁ : X₁ Y₁) (f₁₂ : X₁ Y₂) (f₂₁ : X₂ Y₁) (f₂₂ : X₂ Y₂) :
X₁ X₂ Y₁ Y₂

The "matrix" morphism X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂ with specified components.

Equations
@[simp]
theorem category_theory.biprod.inl_of_components {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_binary_biproducts C] {X₁ X₂ Y₁ Y₂ : C} (f₁₁ : X₁ Y₁) (f₁₂ : X₁ Y₂) (f₂₁ : X₂ Y₁) (f₂₂ : X₂ Y₂) :
@[simp]
theorem category_theory.biprod.inr_of_components {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_binary_biproducts C] {X₁ X₂ Y₁ Y₂ : C} (f₁₁ : X₁ Y₁) (f₁₂ : X₁ Y₂) (f₂₁ : X₂ Y₁) (f₂₂ : X₂ Y₂) :
@[simp]
theorem category_theory.biprod.of_components_fst {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_binary_biproducts C] {X₁ X₂ Y₁ Y₂ : C} (f₁₁ : X₁ Y₁) (f₁₂ : X₁ Y₂) (f₂₁ : X₂ Y₁) (f₂₂ : X₂ Y₂) :
@[simp]
theorem category_theory.biprod.of_components_snd {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_binary_biproducts C] {X₁ X₂ Y₁ Y₂ : C} (f₁₁ : X₁ Y₁) (f₁₂ : X₁ Y₂) (f₂₁ : X₂ Y₁) (f₂₂ : X₂ Y₂) :
@[simp]
theorem category_theory.biprod.of_components_comp {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_binary_biproducts 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₂) :
category_theory.biprod.of_components f₁₁ f₁₂ f₂₁ f₂₂ category_theory.biprod.of_components g₁₁ g₁₂ g₂₁ g₂₂ = category_theory.biprod.of_components (f₁₁ g₁₁ + f₁₂ g₂₁) (f₁₁ g₁₂ + f₁₂ g₂₂) (f₂₁ g₁₁ + f₂₂ g₂₁) (f₂₁ g₁₂ + f₂₂ g₂₂)
noncomputable def category_theory.biprod.unipotent_upper {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_binary_biproducts C] {X₁ X₂ : C} (r : X₁ X₂) :
X₁ X₂ X₁ X₂

The unipotent upper triangular matrix

(1 r)
(0 1)

as an isomorphism.

Equations
noncomputable def category_theory.biprod.unipotent_lower {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_binary_biproducts C] {X₁ X₂ : C} (r : X₂ X₁) :
X₁ X₂ X₁ X₂

The unipotent lower triangular matrix

(1 0)
(r 1)

as an isomorphism.

Equations
noncomputable def category_theory.biprod.gaussian' {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_binary_biproducts C] {X₁ X₂ Y₁ Y₂ : C} (f₁₁ : X₁ Y₁) (f₁₂ : X₁ Y₂) (f₂₁ : X₂ Y₁) (f₂₂ : X₂ Y₂) [category_theory.is_iso f₁₁] :
Σ' (L : X₁ X₂ X₁ X₂) (R : Y₁ Y₂ Y₁ Y₂) (g₂₂ : X₂ Y₂), L.hom category_theory.biprod.of_components f₁₁ f₁₂ f₂₁ f₂₂ R.hom = category_theory.limits.biprod.map f₁₁ g₂₂

If f is a morphism X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂ whose X₁ ⟶ Y₁ entry is an isomorphism, then we can construct isomorphisms L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂ and R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂ so that L.hom ≫ g ≫ R.hom is diagonal (with X₁ ⟶ Y₁ component still f), via Gaussian elimination.

(This is the version of biprod.gaussian written in terms of components.)

Equations

If f is a morphism X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂ whose X₁ ⟶ Y₁ entry is an isomorphism, then we can construct isomorphisms L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂ and R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂ so that L.hom ≫ g ≫ R.hom is diagonal (with X₁ ⟶ Y₁ component still f), via Gaussian elimination.

Equations
noncomputable def category_theory.biprod.iso_elim' {C : Type u} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_binary_biproducts C] {X₁ X₂ Y₁ Y₂ : C} (f₁₁ : X₁ Y₁) (f₁₂ : X₁ Y₂) (f₂₁ : X₂ Y₁) (f₂₂ : X₂ Y₂) [category_theory.is_iso f₁₁] [category_theory.is_iso (category_theory.biprod.of_components f₁₁ f₁₂ f₂₁ f₂₂)] :
X₂ Y₂

If X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂ via a two-by-two matrix whose X₁ ⟶ Y₁ entry is an isomorphism, then we can construct an isomorphism X₂ ≅ Y₂, via Gaussian elimination.

Equations

If f : ⨁ S ⟶ ⨁ T is an isomorphism, and s is a non-trivial summand of the source, then there is some t in the target so that the s, t matrix entry of f is nonzero.

Equations