A Lean Companion to Conceptual Mathematics

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 2variable {π’ž : 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 := π’ž: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 π’ž: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 π’ž:Type uinst✝¹:Category.{v, u} π’žB:π’že:B ⟢ Binst✝:IsIdempotent ehsr:Splitting ehsr':Splitting e| (hsr.r ⊚ e) ⊚ hsr.s = πŸ™ hsr.A π’ž:Type uinst✝¹:Category.{v, u} π’žB:π’že:B ⟢ Binst✝:IsIdempotent ehsr:Splitting ehsr':Splitting e| (hsr.r ⊚ e) ⊚ hsr.s π’ž:Type uinst✝¹:Category.{v, u} π’žB:π’že:B ⟢ Binst✝:IsIdempotent ehsr:Splitting ehsr':Splitting e| hsr.r ⊚ e π’ž:Type uinst✝¹:Category.{v, u} π’žB:π’že:B ⟢ Binst✝:IsIdempotent ehsr:Splitting ehsr':Splitting e| e π’ž:Type uinst✝¹:Category.{v, u} π’žB:π’že:B ⟢ Binst✝:IsIdempotent ehsr:Splitting ehsr':Splitting e| hsr.s ⊚ hsr.r π’ž:Type uinst✝¹:Category.{v, u} π’žB:π’že:B ⟢ Binst✝:IsIdempotent ehsr:Splitting ehsr':Splitting e⊒ (πŸ™ hsr.A ⊚ hsr.r) ⊚ hsr.s = πŸ™ hsr.A All goals completed! πŸ™ inv_hom_id := π’ž: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 π’ž: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 π’ž:Type uinst✝¹:Category.{v, u} π’žB:π’že:B ⟢ Binst✝:IsIdempotent ehsr:Splitting ehsr':Splitting e| (hsr'.r ⊚ e) ⊚ hsr'.s = πŸ™ hsr'.A π’ž:Type uinst✝¹:Category.{v, u} π’žB:π’že:B ⟢ Binst✝:IsIdempotent ehsr:Splitting ehsr':Splitting e| (hsr'.r ⊚ e) ⊚ hsr'.s π’ž:Type uinst✝¹:Category.{v, u} π’žB:π’že:B ⟢ Binst✝:IsIdempotent ehsr:Splitting ehsr':Splitting e| hsr'.r ⊚ e π’ž:Type uinst✝¹:Category.{v, u} π’žB:π’že:B ⟢ Binst✝:IsIdempotent ehsr:Splitting ehsr':Splitting e| e π’ž:Type uinst✝¹:Category.{v, u} π’žB:π’že:B ⟢ Binst✝:IsIdempotent ehsr:Splitting ehsr':Splitting e| hsr'.s ⊚ hsr'.r π’ž:Type uinst✝¹:Category.{v, u} π’žB:π’že:B ⟢ Binst✝:IsIdempotent ehsr:Splitting ehsr':Splitting e⊒ (πŸ™ hsr'.A ⊚ hsr'.r) ⊚ hsr'.s = πŸ™ hsr'.A All goals completed! πŸ™ }