The Eilenberg swindle

Let X be a retract of an object Y of a preadditive category, and let Y^(ℕ) be the coproduct of countably many copies of Y. Then X ⊞ Y^(ℕ) ≅ Y^(ℕ). Writing e for the idempotent of Y determined by the retraction, if 1 - e splits with image X', one can picture Y as X ⊕ X': the isomorphism moves the extra copy of X into slot 0 and moves the copy of X in slot n to slot n + 1, leaving the copies of X' in place. The actual construction uses only e and 1 - e, so no splitting of 1 - e has to exist.

This is the categorical form of the Eilenberg swindle. Its main use is that a triangulated subcategory closed under countable coproducts is closed under direct summands.

Main definitions

• CategoryTheory.Retract.biprodSigmaIso: the isomorphism X ⊞ ∐ (fun _ : ℕ ↦ Y) ≅ ∐ (fun _ : ℕ ↦ Y) for a retract X of Y. Its components on the summands are CategoryTheory.Retract.inl_biprodSigmaIso_hom, CategoryTheory.Retract.ι_inr_biprodSigmaIso_hom, CategoryTheory.Retract.ι_zero_biprodSigmaIso_inv and CategoryTheory.Retract.ι_succ_biprodSigmaIso_inv.

References

• A. Neeman, Triangulated categories, Annals of Mathematics Studies 148, Princeton University Press (2001), Proposition 1.6.8.

noncomputable def CategoryTheory.Retract.biprodSigmaIso {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} (h : Retract X Y) [Limits.HasCoproduct fun (x : ℕ) => Y] [Limits.HasBinaryBiproduct X (∐ fun (x : ℕ) => Y)] : (X ⊞ ∐ fun (x : ℕ) => Y) ≅ ∐ fun (x : ℕ) => Y

The Eilenberg swindle: if X is a retract of Y, then adding one copy of X to the countable coproduct of copies of Y does not change it up to isomorphism.

@[simp]

theorem CategoryTheory.Retract.inl_biprodSigmaIso_hom {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} (h : Retract X Y) [Limits.HasCoproduct fun (x : ℕ) => Y] [Limits.HasBinaryBiproduct X (∐ fun (x : ℕ) => Y)] : CategoryStruct.comp Limits.biprod.inl h.biprodSigmaIso.hom = CategoryStruct.comp h.i (Limits.Sigma.ι (fun (x : ℕ) => Y) 0)

@[simp]

theorem CategoryTheory.Retract.inl_biprodSigmaIso_hom_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} (h : Retract X Y) [Limits.HasCoproduct fun (x : ℕ) => Y] [Limits.HasBinaryBiproduct X (∐ fun (x : ℕ) => Y)] {Z : C} (h✝ : (∐ fun (x : ℕ) => Y) ⟶ Z) : CategoryStruct.comp Limits.biprod.inl (CategoryStruct.comp h.biprodSigmaIso.hom h✝) = CategoryStruct.comp h.i (CategoryStruct.comp (Limits.Sigma.ι (fun (x : ℕ) => Y) 0) h✝)

@[simp]

theorem CategoryTheory.Retract.ι_inr_biprodSigmaIso_hom {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} (h : Retract X Y) [Limits.HasCoproduct fun (x : ℕ) => Y] [Limits.HasBinaryBiproduct X (∐ fun (x : ℕ) => Y)] (n : ℕ) : CategoryStruct.comp (Limits.Sigma.ι (fun (x : ℕ) => Y) n) (CategoryStruct.comp Limits.biprod.inr h.biprodSigmaIso.hom) = CategoryStruct.comp (CategoryStruct.id Y - CategoryStruct.comp h.r h.i) (Limits.Sigma.ι (fun (x : ℕ) => Y) n) + CategoryStruct.comp h.r (CategoryStruct.comp h.i (Limits.Sigma.ι (fun (x : ℕ) => Y) (n + 1)))

@[simp]

theorem CategoryTheory.Retract.ι_inr_biprodSigmaIso_hom_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} (h : Retract X Y) [Limits.HasCoproduct fun (x : ℕ) => Y] [Limits.HasBinaryBiproduct X (∐ fun (x : ℕ) => Y)] (n : ℕ) {Z : C} (h✝ : (∐ fun (x : ℕ) => Y) ⟶ Z) : CategoryStruct.comp (Limits.Sigma.ι (fun (x : ℕ) => Y) n) (CategoryStruct.comp Limits.biprod.inr (CategoryStruct.comp h.biprodSigmaIso.hom h✝)) = CategoryStruct.comp (CategoryStruct.comp (CategoryStruct.id Y - CategoryStruct.comp h.r h.i) (Limits.Sigma.ι (fun (x : ℕ) => Y) n) + CategoryStruct.comp h.r (CategoryStruct.comp h.i (Limits.Sigma.ι (fun (x : ℕ) => Y) (n + 1)))) h✝

@[simp]

theorem CategoryTheory.Retract.ι_zero_biprodSigmaIso_inv {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} (h : Retract X Y) [Limits.HasCoproduct fun (x : ℕ) => Y] [Limits.HasBinaryBiproduct X (∐ fun (x : ℕ) => Y)] : CategoryStruct.comp (Limits.Sigma.ι (fun (x : ℕ) => Y) 0) h.biprodSigmaIso.inv = Limits.biprod.lift h.r (CategoryStruct.comp (CategoryStruct.id Y - CategoryStruct.comp h.r h.i) (Limits.Sigma.ι (fun (x : ℕ) => Y) 0))

@[simp]

theorem CategoryTheory.Retract.ι_zero_biprodSigmaIso_inv_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} (h : Retract X Y) [Limits.HasCoproduct fun (x : ℕ) => Y] [Limits.HasBinaryBiproduct X (∐ fun (x : ℕ) => Y)] {Z : C} (h✝ : (X ⊞ ∐ fun (x : ℕ) => Y) ⟶ Z) : CategoryStruct.comp (Limits.Sigma.ι (fun (x : ℕ) => Y) 0) (CategoryStruct.comp h.biprodSigmaIso.inv h✝) = CategoryStruct.comp (Limits.biprod.lift h.r (CategoryStruct.comp (CategoryStruct.id Y - CategoryStruct.comp h.r h.i) (Limits.Sigma.ι (fun (x : ℕ) => Y) 0))) h✝

@[simp]

theorem CategoryTheory.Retract.ι_succ_biprodSigmaIso_inv {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} (h : Retract X Y) [Limits.HasCoproduct fun (x : ℕ) => Y] [Limits.HasBinaryBiproduct X (∐ fun (x : ℕ) => Y)] (n : ℕ) : CategoryStruct.comp (Limits.Sigma.ι (fun (x : ℕ) => Y) (n + 1)) h.biprodSigmaIso.inv = Limits.biprod.lift 0 (CategoryStruct.comp (CategoryStruct.id Y - CategoryStruct.comp h.r h.i) (Limits.Sigma.ι (fun (x : ℕ) => Y) (n + 1)) + CategoryStruct.comp h.r (CategoryStruct.comp h.i (Limits.Sigma.ι (fun (x : ℕ) => Y) n)))

@[simp]

theorem CategoryTheory.Retract.ι_succ_biprodSigmaIso_inv_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} (h : Retract X Y) [Limits.HasCoproduct fun (x : ℕ) => Y] [Limits.HasBinaryBiproduct X (∐ fun (x : ℕ) => Y)] (n : ℕ) {Z : C} (h✝ : (X ⊞ ∐ fun (x : ℕ) => Y) ⟶ Z) : CategoryStruct.comp (Limits.Sigma.ι (fun (x : ℕ) => Y) (n + 1)) (CategoryStruct.comp h.biprodSigmaIso.inv h✝) = CategoryStruct.comp (Limits.biprod.lift 0 (CategoryStruct.comp (CategoryStruct.id Y - CategoryStruct.comp h.r h.i) (Limits.Sigma.ι (fun (x : ℕ) => Y) (n + 1)) + CategoryStruct.comp h.r (CategoryStruct.comp h.i (Limits.Sigma.ι (fun (x : ℕ) => Y) n)))) h✝