Session 9: Retracts and idempotents

1. Retracts and comparisons

Exercise 1 (p. 99)

(In the category of sets) Show that unless the set A has a point and B has none, then there is at least one map from A to B.

Solution: Exercise 1

TODO Exercise 9.1

cases: A = ∅ => single map A ≠ ∅, B = ∅ => no map A ≠ ∅, B ≠ ∅ => at least one map

Definition: Retract (p. 99)

A is a retract of B means that there are maps {A \xrightarrow{s} B \xrightarrow{r} A} with {r s = 1_A}.

The corresponding mathlib definition is Retract, which we print below for reference.

structure CategoryTheory.Retract.{v, u} {C : Type u} [Category.{v, u} C] (X Y : C) : Type v
number of parameters: 4
fields:
  CategoryTheory.Retract.i : X ⟶ Y
  CategoryTheory.Retract.r : Y ⟶ X
  CategoryTheory.Retract.retract : self.r ⊚ self.i = 𝟙 X := by
    cat_disch
constructor:
  CategoryTheory.Retract.mk.{v, u} {C : Type u} [Category.{v, u} C] {X Y : C} (i : X ⟶ Y) (r : Y ⟶ X)
    (retract : r ⊚ i = 𝟙 X := by cat_disch) : Retract X Y#print Retract

structure CategoryTheory.Retract.{v, u} {C : Type u} [Category.{v, u} C] (X Y : C) : Type v
number of parameters: 4
fields:
  CategoryTheory.Retract.i : X ⟶ Y
  CategoryTheory.Retract.r : Y ⟶ X
  CategoryTheory.Retract.retract : self.r ⊚ self.i = 𝟙 X := by
    cat_disch
constructor:
  CategoryTheory.Retract.mk.{v, u} {C : Type u} [Category.{v, u} C] {X Y : C} (i : X ⟶ Y) (r : Y ⟶ X)
    (retract : r ⊚ i = 𝟙 X := by cat_disch) : Retract X Y

Exercise 2 (p. 100)

(In any category) Show that

(R) A is a retract of A.

(T) If A is a retract of B and B is a retract of C then A is a retract of C.

Hint: You already proved (T) when you proved that if a composable pair of maps each has a retraction, then so does their composite.

Solution: Exercise 2

variable {𝒞 : Type u} [Category.{v, u} 𝒞] {A B C : 𝒞}

We show that (R) holds.

example : Retract A A := {
  i := 𝟙 A
  r := 𝟙 A
}

We show that (T) holds (cf. Proposition 3 in Article II).

example (h₁ : Retract A B) (h₂ : Retract B C) : Retract A C := {
  i := h₂.i ⊚ h₁.i
  r := h₁.r ⊚ h₂.r
}

2. Idempotents as records of retracts

Definition: Splitting (p. 102)

(In any category) If {B \xrightarrow{e} B} is an idempotent map, a splitting of e consists of an object A together with two maps {A \xrightarrow{s} B \xrightarrow{r} A} with {r s = 1_A} and {s r = e}.

We implement Splitting in Lean as follows:

structure Splitting {𝒞 : Type u} [Category.{v, u} 𝒞] {B : 𝒞}
    (e : B ⟶ B) [IsIdempotent e] where
  A : 𝒞
  s : A ⟶ B
  r : B ⟶ A
  rs : r ⊚ s = 𝟙 A
  sr : s ⊚ r = e

Exercise 3 (p. 102)

(In any category) Suppose that both {A \xrightarrow{s} B \xrightarrow{r} A} and {A' \xrightarrow{s'} B \xrightarrow{r'} A'} split the same idempotent {B \xrightarrow{e} B}. Use these maps to construct an isomorphism {A \xrightarrow{f} A'}.

Solution: Exercise 3

We construct an isomorphism f as follows:

example {𝒞 : Type u} [Category.{v, u} 𝒞] {B : 𝒞}
    {e : B ⟶ B} [IsIdempotent e]
    (hsr : Splitting e) (hsr' : Splitting e)
    : Iso hsr.A hsr'.A := {
  hom := hsr'.r ⊚ hsr.s
  inv := hsr.r ⊚ hsr'.s
  hom_inv_id := by𝒞:Type uinst✝¹:Category.{v, u} 𝒞B:𝒞e:B ⟶ Binst✝:IsIdempotent ehsr:Splitting ehsr':Splitting e⊢ (hsr.r ⊚ hsr'.s) ⊚ hsr'.r ⊚ hsr.s = 𝟙 hsr.A
    rw [Category.assoc, ← Category.assoc hsr'.r, hsr'.sr]𝒞:Type uinst✝¹:Category.{v, u} 𝒞B:𝒞e:B ⟶ Binst✝:IsIdempotent ehsr:Splitting ehsr':Splitting e⊢ (hsr.r ⊚ e) ⊚ hsr.s = 𝟙 hsr.A
    -- rw [← hsr.sr] needs a bit of hand-holding here
    conv =>𝒞:Type uinst✝¹:Category.{v, u} 𝒞B:𝒞e:B ⟶ Binst✝:IsIdempotent ehsr:Splitting ehsr':Splitting e| (hsr.r ⊚ e) ⊚ hsr.s = 𝟙 hsr.A
      lhs𝒞:Type uinst✝¹:Category.{v, u} 𝒞B:𝒞e:B ⟶ Binst✝:IsIdempotent ehsr:Splitting ehsr':Splitting e| (hsr.r ⊚ e) ⊚ hsr.s
      arg 2𝒞:Type uinst✝¹:Category.{v, u} 𝒞B:𝒞e:B ⟶ Binst✝:IsIdempotent ehsr:Splitting ehsr':Splitting e| hsr.r ⊚ e
      arg 1𝒞:Type uinst✝¹:Category.{v, u} 𝒞B:𝒞e:B ⟶ Binst✝:IsIdempotent ehsr:Splitting ehsr':Splitting e| e
      rw [← hsr.sr]𝒞:Type uinst✝¹:Category.{v, u} 𝒞B:𝒞e:B ⟶ Binst✝:IsIdempotent ehsr:Splitting ehsr':Splitting e| hsr.s ⊚ hsr.r
    rw [Category.assoc, hsr.rs]𝒞:Type uinst✝¹:Category.{v, u} 𝒞B:𝒞e:B ⟶ Binst✝:IsIdempotent ehsr:Splitting ehsr':Splitting e⊢ (𝟙 hsr.A ⊚ hsr.r) ⊚ hsr.s = 𝟙 hsr.A
    rw [← Category.assoc, hsr.rs, Category.id_comp]All goals completed! 🐙
  inv_hom_id := by𝒞:Type uinst✝¹:Category.{v, u} 𝒞B:𝒞e:B ⟶ Binst✝:IsIdempotent ehsr:Splitting ehsr':Splitting e⊢ (hsr'.r ⊚ hsr.s) ⊚ hsr.r ⊚ hsr'.s = 𝟙 hsr'.A
    rw [Category.assoc, ← Category.assoc hsr.r, hsr.sr]𝒞:Type uinst✝¹:Category.{v, u} 𝒞B:𝒞e:B ⟶ Binst✝:IsIdempotent ehsr:Splitting ehsr':Splitting e⊢ (hsr'.r ⊚ e) ⊚ hsr'.s = 𝟙 hsr'.A
    -- rw [← hsr'.sr] likewise needs a bit of hand-holding here
    conv =>𝒞:Type uinst✝¹:Category.{v, u} 𝒞B:𝒞e:B ⟶ Binst✝:IsIdempotent ehsr:Splitting ehsr':Splitting e| (hsr'.r ⊚ e) ⊚ hsr'.s = 𝟙 hsr'.A
      lhs𝒞:Type uinst✝¹:Category.{v, u} 𝒞B:𝒞e:B ⟶ Binst✝:IsIdempotent ehsr:Splitting ehsr':Splitting e| (hsr'.r ⊚ e) ⊚ hsr'.s
      arg 2𝒞:Type uinst✝¹:Category.{v, u} 𝒞B:𝒞e:B ⟶ Binst✝:IsIdempotent ehsr:Splitting ehsr':Splitting e| hsr'.r ⊚ e
      arg 1𝒞:Type uinst✝¹:Category.{v, u} 𝒞B:𝒞e:B ⟶ Binst✝:IsIdempotent ehsr:Splitting ehsr':Splitting e| e
      rw [← hsr'.sr]𝒞:Type uinst✝¹:Category.{v, u} 𝒞B:𝒞e:B ⟶ Binst✝:IsIdempotent ehsr:Splitting ehsr':Splitting e| hsr'.s ⊚ hsr'.r
    rw [Category.assoc, hsr'.rs]𝒞:Type uinst✝¹:Category.{v, u} 𝒞B:𝒞e:B ⟶ Binst✝:IsIdempotent ehsr:Splitting ehsr':Splitting e⊢ (𝟙 hsr'.A ⊚ hsr'.r) ⊚ hsr'.s = 𝟙 hsr'.A
    rw [← Category.assoc, hsr'.rs, Category.id_comp]All goals completed! 🐙
}