Sums of orthogonal split idempotents #
An idempotent e of X splits when e = r ≫ i for morphisms i : Y ⟶ X and r : X ⟶ Y with
i ≫ r = 𝟙 Y, as in Mathlib's CategoryTheory.IsIdempotentComplete. In a preadditive category
with binary biproducts, the sum of two orthogonal split idempotents splits through the biproduct
of their images.
Main results #
TauCeti.exists_split_add_of_comp_eq_zero: the sum of two orthogonal split idempotents splits.
theorem
TauCeti.exists_split_add_of_comp_eq_zero
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X : C}
{e₁ e₂ : X ⟶ X}
(h₁ :
∃ (Y : C) (i : Y ⟶ X) (r : X ⟶ Y),
CategoryTheory.CategoryStruct.comp i r = CategoryTheory.CategoryStruct.id Y ∧ CategoryTheory.CategoryStruct.comp r i = e₁)
(h₂ :
∃ (Y : C) (i : Y ⟶ X) (r : X ⟶ Y),
CategoryTheory.CategoryStruct.comp i r = CategoryTheory.CategoryStruct.id Y ∧ CategoryTheory.CategoryStruct.comp r i = e₂)
(h₁₂ : CategoryTheory.CategoryStruct.comp e₁ e₂ = 0)
(h₂₁ : CategoryTheory.CategoryStruct.comp e₂ e₁ = 0)
:
∃ (Y : C) (i : Y ⟶ X) (r : X ⟶ Y),
CategoryTheory.CategoryStruct.comp i r = CategoryTheory.CategoryStruct.id Y ∧ CategoryTheory.CategoryStruct.comp r i = e₁ + e₂
Orthogonal split idempotents have a split sum: if e₁ and e₂ split and e₁ ≫ e₂ = 0 = e₂ ≫ e₁, then e₁ + e₂ splits, through the biproduct of the two images.