Basic facts about morphisms between biproducts in preadditive categories.
- In any category (with zero morphisms), if
biprod.map f gis an isomorphism, then bothfandgare isomorphisms.
The remaining lemmas hold in any preadditive category.
If
fis a morphismX₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂whoseX₁ ⟶ Y₁entry is an isomorphism, then we can construct isomorphismsL : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂andR : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂so thatL.hom ≫ g ≫ R.homis diagonal (withX₁ ⟶ Y₁component stillf), via Gaussian elimination.As a corollary of the previous two facts, if we have an isomorphism
X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂whoseX₁ ⟶ Y₁entry is an isomorphism, we can construct an isomorphismX₂ ≅ Y₂.If
f : W ⊞ X ⟶ Y ⊞ Zis an isomorphism, either𝟙 W = 0, or at least one of the component mapsW ⟶ YandW ⟶ Zis nonzero.If
f : ⨁ S ⟶ ⨁ Tis an isomorphism, then every column (corresponding to a nonzero summand in the domain) has some nonzero matrix entry.
def
category_theory.is_iso_left_of_is_iso_biprod_map
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_binary_biproducts C]
{W X Y Z : C}
(f : W ⟶ Y)
(g : X ⟶ Z)
[category_theory.is_iso (category_theory.limits.biprod.map f g)] :
If
(f 0)
(0 g)
is invertible, then f is invertible.
def
category_theory.is_iso_right_of_is_iso_biprod_map
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_binary_biproducts C]
{W X Y Z : C}
(f : W ⟶ Y)
(g : X ⟶ Z)
[category_theory.is_iso (category_theory.limits.biprod.map f g)] :
If
(f 0)
(0 g)
is invertible, then g is invertible.
Equations
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} :
The "matrix" morphism X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂ with specified components.
Equations
- category_theory.biprod.of_components f₁₁ f₁₂ f₂₁ f₂₂ = category_theory.limits.biprod.fst ≫ f₁₁ ≫ category_theory.limits.biprod.inl + category_theory.limits.biprod.fst ≫ f₁₂ ≫ category_theory.limits.biprod.inr + category_theory.limits.biprod.snd ≫ f₂₁ ≫ category_theory.limits.biprod.inl + category_theory.limits.biprod.snd ≫ f₂₂ ≫ category_theory.limits.biprod.inr
@[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_eq
{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₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂) :
category_theory.biprod.of_components (category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.fst) (category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.snd) (category_theory.limits.biprod.inr ≫ f ≫ category_theory.limits.biprod.fst) (category_theory.limits.biprod.inr ≫ f ≫ category_theory.limits.biprod.snd) = f
@[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₂) :
@[simp]
theorem
category_theory.biprod.unipotent_upper_hom
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_binary_biproducts C]
{X₁ X₂ : C}
(r : X₁ ⟶ X₂) :
(category_theory.biprod.unipotent_upper r).hom = category_theory.biprod.of_components (𝟙 X₁) r 0 (𝟙 X₂)
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} :
The unipotent upper triangular matrix
(1 r)
(0 1)
as an isomorphism.
Equations
- category_theory.biprod.unipotent_upper r = {hom := category_theory.biprod.of_components (𝟙 X₁) r 0 (𝟙 X₂), inv := category_theory.biprod.of_components (𝟙 X₁) (-r) 0 (𝟙 X₂), hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.biprod.unipotent_upper_inv
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_binary_biproducts C]
{X₁ X₂ : C}
(r : X₁ ⟶ X₂) :
(category_theory.biprod.unipotent_upper r).inv = category_theory.biprod.of_components (𝟙 X₁) (-r) 0 (𝟙 X₂)
@[simp]
theorem
category_theory.biprod.unipotent_lower_hom
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_binary_biproducts C]
{X₁ X₂ : C}
(r : X₂ ⟶ X₁) :
(category_theory.biprod.unipotent_lower r).hom = category_theory.biprod.of_components (𝟙 X₁) 0 r (𝟙 X₂)
@[simp]
theorem
category_theory.biprod.unipotent_lower_inv
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_binary_biproducts C]
{X₁ X₂ : C}
(r : X₂ ⟶ X₁) :
(category_theory.biprod.unipotent_lower r).inv = category_theory.biprod.of_components (𝟙 X₁) 0 (-r) (𝟙 X₂)
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} :
The unipotent lower triangular matrix
(1 0)
(r 1)
as an isomorphism.
Equations
- category_theory.biprod.unipotent_lower r = {hom := category_theory.biprod.of_components (𝟙 X₁) 0 r (𝟙 X₂), inv := category_theory.biprod.of_components (𝟙 X₁) 0 (-r) (𝟙 X₂), hom_inv_id' := _, inv_hom_id' := _}
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₁₁] :
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
- category_theory.biprod.gaussian' f₁₁ f₁₂ f₂₁ f₂₂ = ⟨category_theory.biprod.unipotent_lower (-f₂₁ ≫ category_theory.is_iso.inv f₁₁), ⟨category_theory.biprod.unipotent_upper (-category_theory.is_iso.inv f₁₁ ≫ f₁₂), ⟨f₂₂ - f₂₁ ≫ category_theory.is_iso.inv f₁₁ ≫ f₁₂, _⟩⟩⟩
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₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂)
[category_theory.is_iso (category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.fst)] :
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
- category_theory.biprod.gaussian f = let this : Σ' (L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂) (R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) (g₂₂ : X₂ ⟶ Y₂), L.hom ≫ category_theory.biprod.of_components (category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.fst) (category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.snd) (category_theory.limits.biprod.inr ≫ f ≫ category_theory.limits.biprod.fst) (category_theory.limits.biprod.inr ≫ f ≫ category_theory.limits.biprod.snd) ≫ R.hom = category_theory.limits.biprod.map (category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.fst) g₂₂ := category_theory.biprod.gaussian' (category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.fst) (category_theory.limits.biprod.inl ≫ f ≫ category_theory.limits.biprod.snd) (category_theory.limits.biprod.inr ≫ f ≫ category_theory.limits.biprod.fst) (category_theory.limits.biprod.inr ≫ f ≫ category_theory.limits.biprod.snd) in _.mp this
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
- category_theory.biprod.iso_elim' f₁₁ f₁₂ f₂₁ f₂₂ = (category_theory.biprod.gaussian' f₁₁ f₁₂ f₂₁ f₂₂).cases_on (λ (L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂) (snd : Σ' (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₂₂), snd.cases_on (λ (R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) (snd_snd : Σ' (g₂₂ : X₂ ⟶ Y₂), L.hom ≫ category_theory.biprod.of_components f₁₁ f₁₂ f₂₁ f₂₂ ≫ R.hom = category_theory.limits.biprod.map f₁₁ g₂₂), snd_snd.cases_on (λ (g : X₂ ⟶ Y₂) (w : L.hom ≫ category_theory.biprod.of_components f₁₁ f₁₂ f₂₁ f₂₂ ≫ R.hom = category_theory.limits.biprod.map f₁₁ g), let _inst : category_theory.is_iso (category_theory.limits.biprod.map f₁₁ g) := _.mpr category_theory.is_iso.comp_is_iso, _inst_6 : category_theory.is_iso g := category_theory.is_iso_right_of_is_iso_biprod_map f₁₁ g in category_theory.as_iso g)))
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₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂)
[category_theory.is_iso (category_theory.limits.biprod.inl ≫ f.hom ≫ category_theory.limits.biprod.fst)] :
X₂ ≅ Y₂
If f is an isomorphism X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂ whose X₁ ⟶ Y₁ entry is an isomorphism,
then we can construct an isomorphism X₂ ≅ Y₂, via Gaussian elimination.
Equations
- category_theory.biprod.iso_elim f = let _inst : category_theory.is_iso (category_theory.biprod.of_components (category_theory.limits.biprod.inl ≫ f.hom ≫ category_theory.limits.biprod.fst) (category_theory.limits.biprod.inl ≫ f.hom ≫ category_theory.limits.biprod.snd) (category_theory.limits.biprod.inr ≫ f.hom ≫ category_theory.limits.biprod.fst) (category_theory.limits.biprod.inr ≫ f.hom ≫ category_theory.limits.biprod.snd)) := _.mpr (category_theory.is_iso.of_iso f) in category_theory.biprod.iso_elim' (category_theory.limits.biprod.inl ≫ f.hom ≫ category_theory.limits.biprod.fst) (category_theory.limits.biprod.inl ≫ f.hom ≫ category_theory.limits.biprod.snd) (category_theory.limits.biprod.inr ≫ f.hom ≫ category_theory.limits.biprod.fst) (category_theory.limits.biprod.inr ≫ f.hom ≫ category_theory.limits.biprod.snd)
theorem
category_theory.biprod.column_nonzero_of_iso
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_binary_biproducts C]
{W X Y Z : C}
(f : W ⊞ X ⟶ Y ⊞ Z)
[category_theory.is_iso f] :
theorem
category_theory.biproduct.column_nonzero_of_iso'
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{σ τ : Type v}
[decidable_eq σ]
[decidable_eq τ]
[fintype τ]
{S : σ → C}
[category_theory.limits.has_biproduct S]
{T : τ → C}
[category_theory.limits.has_biproduct T]
(s : σ)
(f : ⨁ S ⟶ ⨁ T)
[category_theory.is_iso f] :
(∀ (t : τ), category_theory.limits.biproduct.ι S s ≫ f ≫ category_theory.limits.biproduct.π T t = 0) → 𝟙 (S s) = 0
def
category_theory.biproduct.column_nonzero_of_iso
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
{σ τ : Type v}
[decidable_eq σ]
[decidable_eq τ]
[fintype τ]
{S : σ → C}
[category_theory.limits.has_biproduct S]
{T : τ → C}
[category_theory.limits.has_biproduct T]
(s : σ)
(nz : 𝟙 (S s) ≠ 0)
[Π (t : τ), decidable_eq (S s ⟶ T t)]
(f : ⨁ S ⟶ ⨁ T)
[category_theory.is_iso f] :
trunc (Σ' (t : τ), category_theory.limits.biproduct.ι S s ≫ f ≫ category_theory.limits.biproduct.π T t ≠ 0)
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.