Article II: Isomorphisms

1. Isomorphisms

Definition: Isomorphism, Inverse (p. 40)

A map {A \xrightarrow{f} B} is called an isomorphism, or invertible map, if there is a map {B \xrightarrow{g} A} for which {g \circ f = 1_A} and {f \circ g = 1_B}.

A map g related to f by satisfying these equations is called an inverse for f.

Two objects A and B are said to be isomorphic if there is at least one isomorphism {A \xrightarrow{f} B}.

The corresponding mathlib definition for isomorphism is Iso (and IsIso), which we print below for reference.

structure CategoryTheory.Iso.{v, u} {C : Type u} [Category.{v, u} C] (X Y : C) : Type v
number of parameters: 4
fields:
  CategoryTheory.Iso.hom : X ⟶ Y
  CategoryTheory.Iso.inv : Y ⟶ X
  CategoryTheory.Iso.hom_inv_id : self.inv ⊚ self.hom = 𝟙 X := by
    cat_disch
  CategoryTheory.Iso.inv_hom_id : self.hom ⊚ self.inv = 𝟙 Y := by
    cat_disch
constructor:
  CategoryTheory.Iso.mk.{v, u} {C : Type u} [Category.{v, u} C] {X Y : C} (hom : X ⟶ Y) (inv : Y ⟶ X)
    (hom_inv_id : inv ⊚ hom = 𝟙 X := by cat_disch) (inv_hom_id : hom ⊚ inv = 𝟙 Y := by cat_disch) : X ≅ Y#print Iso

structure CategoryTheory.Iso.{v, u} {C : Type u} [Category.{v, u} C] (X Y : C) : Type v
number of parameters: 4
fields:
  CategoryTheory.Iso.hom : X ⟶ Y
  CategoryTheory.Iso.inv : Y ⟶ X
  CategoryTheory.Iso.hom_inv_id : self.inv ⊚ self.hom = 𝟙 X := by
    cat_disch
  CategoryTheory.Iso.inv_hom_id : self.hom ⊚ self.inv = 𝟙 Y := by
    cat_disch
constructor:
  CategoryTheory.Iso.mk.{v, u} {C : Type u} [Category.{v, u} C] {X Y : C} (hom : X ⟶ Y) (inv : Y ⟶ X)
    (hom_inv_id : inv ⊚ hom = 𝟙 X := by cat_disch) (inv_hom_id : hom ⊚ inv = 𝟙 Y := by cat_disch) : X ≅ Y

class CategoryTheory.IsIso.{v, u} {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : Prop
number of parameters: 5
fields:
  CategoryTheory.IsIso.out : ∃ inv, inv ⊚ f = 𝟙 X ∧ f ⊚ inv = 𝟙 Y
constructor:
  CategoryTheory.IsIso.mk.{v, u} {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
    (out : ∃ inv, inv ⊚ f = 𝟙 X ∧ f ⊚ inv = 𝟙 Y) : IsIso f#print IsIso

class CategoryTheory.IsIso.{v, u} {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : Prop
number of parameters: 5
fields:
  CategoryTheory.IsIso.out : ∃ inv, inv ⊚ f = 𝟙 X ∧ f ⊚ inv = 𝟙 Y
constructor:
  CategoryTheory.IsIso.mk.{v, u} {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
    (out : ∃ inv, inv ⊚ f = 𝟙 X ∧ f ⊚ inv = 𝟙 Y) : IsIso f

Excerpt (p. 41)

Reflexive: A is isomorphic to A.

Symmetric: If A is isomorphic to B, then B is isomorphic to A.

Transitive: If A is isomorphic to B, and B is isomorphic to C, then A is isomorphic to C.

The respective mathlib definitions are Iso.refl, Iso.symm, and Iso.trans, which we print below for reference.

def CategoryTheory.Iso.refl.{v, u} : {C : Type u} → [inst : Category.{v, u} C] → (X : C) → X ≅ X :=
fun {C} [Category.{v, u} C] X ↦ { hom := 𝟙 X, inv := 𝟙 X, hom_inv_id := ⋯, inv_hom_id := ⋯ }#print Iso.refl

def CategoryTheory.Iso.refl.{v, u} : {C : Type u} → [inst : Category.{v, u} C] → (X : C) → X ≅ X :=
fun {C} [Category.{v, u} C] X ↦ { hom := 𝟙 X, inv := 𝟙 X, hom_inv_id := ⋯, inv_hom_id := ⋯ }

def CategoryTheory.Iso.symm.{v, u} : {C : Type u} → [inst : Category.{v, u} C] → {X Y : C} → (X ≅ Y) → (Y ≅ X) :=
fun {C} [Category.{v, u} C] {X Y} I ↦ { hom := I.inv, inv := I.hom, hom_inv_id := ⋯, inv_hom_id := ⋯ }#print Iso.symm

def CategoryTheory.Iso.symm.{v, u} : {C : Type u} → [inst : Category.{v, u} C] → {X Y : C} → (X ≅ Y) → (Y ≅ X) :=
fun {C} [Category.{v, u} C] {X Y} I ↦ { hom := I.inv, inv := I.hom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

def CategoryTheory.Iso.trans.{v, u} : {C : Type u} →
  [inst : Category.{v, u} C] → {X Y Z : C} → (X ≅ Y) → (Y ≅ Z) → (X ≅ Z) :=
fun {C} [Category.{v, u} C] {X Y Z} α β ↦
  { hom := β.hom ⊚ α.hom, inv := α.inv ⊚ β.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }#print Iso.trans

def CategoryTheory.Iso.trans.{v, u} : {C : Type u} →
  [inst : Category.{v, u} C] → {X Y Z : C} → (X ≅ Y) → (Y ≅ Z) → (X ≅ Z) :=
fun {C} [Category.{v, u} C] {X Y Z} α β ↦
  { hom := β.hom ⊚ α.hom, inv := α.inv ⊚ β.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Exercise 1 (p. 41)

(R) Show that {A \xrightarrow{1_A} A} is an isomorphism. (Hint: find an inverse for 1_A.)

(S) Show that if {A \xrightarrow{f} B} is an isomorphism, and {B \xrightarrow{g} A} is an inverse for f; then g is also an isomorphism. (Hint: find an inverse for g.)

(T) Show that if {A \xrightarrow{f} B} and {B \xrightarrow{k} C} are isomorphisms, {A \xrightarrow{k \circ f} C} is also an isomorphism.

Solution: Exercise 1

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

(R) 1_A is an inverse for itself, so 1_A is an isomorphism.

example : IsIso (𝟙 A) := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞⊢ IsIso (𝟙 A)
  use 𝟙 Ah𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞⊢ 𝟙 A ⊚ 𝟙 A = 𝟙 A ∧ 𝟙 A ⊚ 𝟙 A = 𝟙 A
  constructorh.left𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞⊢ 𝟙 A ⊚ 𝟙 A = 𝟙 Ah.right𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞⊢ 𝟙 A ⊚ 𝟙 A = 𝟙 A <;>h.left𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞⊢ 𝟙 A ⊚ 𝟙 A = 𝟙 Ah.right𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞⊢ 𝟙 A ⊚ 𝟙 A = 𝟙 A exact Category.id_comp (𝟙 A)All goals completed! 🐙

(S) f is an inverse for g, so g is an isomorphism. (Note that the hypothesis "f is an isomorphism" is redundant here and could be omitted.)

example (f : A ⟶ B) (_ : IsIso f)
    (g : B ⟶ A) (hg : g ⊚ f = 𝟙 A ∧ f ⊚ g = 𝟙 B)
    : IsIso g := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bx✝:IsIso fg:B ⟶ Ahg:g ⊚ f = 𝟙 A ∧ f ⊚ g = 𝟙 B⊢ IsIso g
  use fh𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bx✝:IsIso fg:B ⟶ Ahg:g ⊚ f = 𝟙 A ∧ f ⊚ g = 𝟙 B⊢ f ⊚ g = 𝟙 B ∧ g ⊚ f = 𝟙 A
  exact ⟨hg.2, hg.1⟩All goals completed! 🐙

(T) Composition of isomorphisms is transitive, so {k \circ f} is an isomorphism.

example (f : A ⟶ B) (hf : IsIso f) (k : B ⟶ C) (hk : IsIso k)
    : IsIso (k ⊚ f) := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bhf:IsIso fk:B ⟶ Chk:IsIso k⊢ IsIso (k ⊚ f)
  obtain ⟨finv, hfinv⟩ := hf𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bk:B ⟶ Chk:IsIso kfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 B⊢ IsIso (k ⊚ f)
  obtain ⟨kinv, hkinv⟩ := hk𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bk:B ⟶ Cfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Bkinv:C ⟶ Bhkinv:kinv ⊚ k = 𝟙 B ∧ k ⊚ kinv = 𝟙 C⊢ IsIso (k ⊚ f)
  use finv ⊚ kinvh𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bk:B ⟶ Cfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Bkinv:C ⟶ Bhkinv:kinv ⊚ k = 𝟙 B ∧ k ⊚ kinv = 𝟙 C⊢ (finv ⊚ kinv) ⊚ k ⊚ f = 𝟙 A ∧ (k ⊚ f) ⊚ finv ⊚ kinv = 𝟙 C
  constructorh.left𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bk:B ⟶ Cfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Bkinv:C ⟶ Bhkinv:kinv ⊚ k = 𝟙 B ∧ k ⊚ kinv = 𝟙 C⊢ (finv ⊚ kinv) ⊚ k ⊚ f = 𝟙 Ah.right𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bk:B ⟶ Cfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Bkinv:C ⟶ Bhkinv:kinv ⊚ k = 𝟙 B ∧ k ⊚ kinv = 𝟙 C⊢ (k ⊚ f) ⊚ finv ⊚ kinv = 𝟙 C
  ·h.left𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bk:B ⟶ Cfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Bkinv:C ⟶ Bhkinv:kinv ⊚ k = 𝟙 B ∧ k ⊚ kinv = 𝟙 C⊢ (finv ⊚ kinv) ⊚ k ⊚ f = 𝟙 A rw [Category.assoc, ← Category.assoc k]h.left𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bk:B ⟶ Cfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Bkinv:C ⟶ Bhkinv:kinv ⊚ k = 𝟙 B ∧ k ⊚ kinv = 𝟙 C⊢ (finv ⊚ kinv ⊚ k) ⊚ f = 𝟙 A
    rw [hkinv.1, Category.id_comp, hfinv.1]All goals completed! 🐙
  ·h.right𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bk:B ⟶ Cfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Bkinv:C ⟶ Bhkinv:kinv ⊚ k = 𝟙 B ∧ k ⊚ kinv = 𝟙 C⊢ (k ⊚ f) ⊚ finv ⊚ kinv = 𝟙 C rw [Category.assoc, ← Category.assoc finv]h.right𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bk:B ⟶ Cfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Bkinv:C ⟶ Bhkinv:kinv ⊚ k = 𝟙 B ∧ k ⊚ kinv = 𝟙 C⊢ (k ⊚ f ⊚ finv) ⊚ kinv = 𝟙 C
    rw [hfinv.2, Category.id_comp, hkinv.2]All goals completed! 🐙

Exercise 2 (p. 42)

Suppose {B \xrightarrow{g} A} and {B \xrightarrow{k} A} are both inverses for {A \xrightarrow{f} B}. Show that {g = k}.

Solution: Exercise 2

The inverse of a map is unique (when it exists).

example {𝒞 : Type u} [Category.{v, u} 𝒞] {A B : 𝒞} (f : A ⟶ B)
    (g : B ⟶ A) (hg : g ⊚ f = 𝟙 A ∧ f ⊚ g = 𝟙 B)
    (k : B ⟶ A) (hk : k ⊚ f = 𝟙 A ∧ f ⊚ k = 𝟙 B)
    : g = k := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Bg:B ⟶ Ahg:g ⊚ f = 𝟙 A ∧ f ⊚ g = 𝟙 Bk:B ⟶ Ahk:k ⊚ f = 𝟙 A ∧ f ⊚ k = 𝟙 B⊢ g = k
  calc
    g = 𝟙 A ⊚ g := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Bg:B ⟶ Ahg:g ⊚ f = 𝟙 A ∧ f ⊚ g = 𝟙 Bk:B ⟶ Ahk:k ⊚ f = 𝟙 A ∧ f ⊚ k = 𝟙 B⊢ g = 𝟙 A ⊚ g rw [Category.comp_id]All goals completed! 🐙
    _ = (k ⊚ f) ⊚ g := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Bg:B ⟶ Ahg:g ⊚ f = 𝟙 A ∧ f ⊚ g = 𝟙 Bk:B ⟶ Ahk:k ⊚ f = 𝟙 A ∧ f ⊚ k = 𝟙 B⊢ 𝟙 A ⊚ g = (k ⊚ f) ⊚ g rw [hk.1]All goals completed! 🐙
    _ = k ⊚ (f ⊚ g) := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Bg:B ⟶ Ahg:g ⊚ f = 𝟙 A ∧ f ⊚ g = 𝟙 Bk:B ⟶ Ahk:k ⊚ f = 𝟙 A ∧ f ⊚ k = 𝟙 B⊢ (k ⊚ f) ⊚ g = k ⊚ f ⊚ g rw [Category.assoc]All goals completed! 🐙
    _ = k ⊚ 𝟙 B := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Bg:B ⟶ Ahg:g ⊚ f = 𝟙 A ∧ f ⊚ g = 𝟙 Bk:B ⟶ Ahk:k ⊚ f = 𝟙 A ∧ f ⊚ k = 𝟙 B⊢ k ⊚ f ⊚ g = k ⊚ 𝟙 B rw [hg.2]All goals completed! 🐙
    _ = k := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Bg:B ⟶ Ahg:g ⊚ f = 𝟙 A ∧ f ⊚ g = 𝟙 Bk:B ⟶ Ahk:k ⊚ f = 𝟙 A ∧ f ⊚ k = 𝟙 B⊢ k ⊚ 𝟙 B = k rw [Category.id_comp]All goals completed! 🐙

Exercise 3 (p. 43)

If f has an inverse, then f satisfies the two cancellation laws:

(a) If {f \circ h = f \circ k}, then {h = k}.

(b) If {h \circ f = k \circ f}, then {h = k}.

Warning: The following 'cancellation law' is not correct, even if f has an inverse.

Solution: Exercise 3

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

(a) We show that f is left-cancellative.

example (f : A ⟶ B)
    (hf : ∃ finv : B ⟶ A, finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 B)
    (h : B ⟶ A) (k : B ⟶ A)
    : f ⊚ h = f ⊚ k → h = k := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Bhf:∃ finv, finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Bh:B ⟶ Ak:B ⟶ A⊢ f ⊚ h = f ⊚ k → h = k
  obtain ⟨finv, hfinv₁, hfinv₂⟩ := hf𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Bh:B ⟶ Ak:B ⟶ Afinv:B ⟶ Ahfinv₁:finv ⊚ f = 𝟙 Ahfinv₂:f ⊚ finv = 𝟙 B⊢ f ⊚ h = f ⊚ k → h = k
  intro h₁𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Bh:B ⟶ Ak:B ⟶ Afinv:B ⟶ Ahfinv₁:finv ⊚ f = 𝟙 Ahfinv₂:f ⊚ finv = 𝟙 Bh₁:f ⊚ h = f ⊚ k⊢ h = k
  have h₂ : finv ⊚ f ⊚ h = finv ⊚ f ⊚ k := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Bhf:∃ finv, finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Bh:B ⟶ Ak:B ⟶ A⊢ f ⊚ h = f ⊚ k → h = k rw [h₁]All goals completed! 🐙
  repeat rw [Category.assoc] at h₂𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Bh:B ⟶ Ak:B ⟶ Afinv:B ⟶ Ahfinv₁:finv ⊚ f = 𝟙 Ahfinv₂:f ⊚ finv = 𝟙 Bh₁:f ⊚ h = f ⊚ kh₂:(finv ⊚ f) ⊚ h = (finv ⊚ f) ⊚ k⊢ h = k
  rw [hfinv₁] at h₂𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Bh:B ⟶ Ak:B ⟶ Afinv:B ⟶ Ahfinv₁:finv ⊚ f = 𝟙 Ahfinv₂:f ⊚ finv = 𝟙 Bh₁:f ⊚ h = f ⊚ kh₂:𝟙 A ⊚ h = 𝟙 A ⊚ k⊢ h = k
  repeat rw [Category.comp_id] at h₂𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Bh:B ⟶ Ak:B ⟶ Afinv:B ⟶ Ahfinv₁:finv ⊚ f = 𝟙 Ahfinv₂:f ⊚ finv = 𝟙 Bh₁:f ⊚ h = f ⊚ kh₂:h = k⊢ h = k
  exact h₂All goals completed! 🐙

(b) We show that f is right-cancellative.

example (f : A ⟶ B)
    (hf : ∃ finv : B ⟶ A, finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 B)
    (h : B ⟶ A) (k : B ⟶ A)
    : h ⊚ f = k ⊚ f → h = k := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Bhf:∃ finv, finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Bh:B ⟶ Ak:B ⟶ A⊢ h ⊚ f = k ⊚ f → h = k
  obtain ⟨finv, hfinv₁, hfinv₂⟩ := hf𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Bh:B ⟶ Ak:B ⟶ Afinv:B ⟶ Ahfinv₁:finv ⊚ f = 𝟙 Ahfinv₂:f ⊚ finv = 𝟙 B⊢ h ⊚ f = k ⊚ f → h = k
  intro h₁𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Bh:B ⟶ Ak:B ⟶ Afinv:B ⟶ Ahfinv₁:finv ⊚ f = 𝟙 Ahfinv₂:f ⊚ finv = 𝟙 Bh₁:h ⊚ f = k ⊚ f⊢ h = k
  have h₂ : (h ⊚ f) ⊚ finv = (k ⊚ f) ⊚ finv := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Bhf:∃ finv, finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Bh:B ⟶ Ak:B ⟶ A⊢ h ⊚ f = k ⊚ f → h = k rw [h₁]All goals completed! 🐙
  repeat rw [← Category.assoc] at h₂𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Bh:B ⟶ Ak:B ⟶ Afinv:B ⟶ Ahfinv₁:finv ⊚ f = 𝟙 Ahfinv₂:f ⊚ finv = 𝟙 Bh₁:h ⊚ f = k ⊚ fh₂:h ⊚ f ⊚ finv = k ⊚ f ⊚ finv⊢ h = k
  rw [hfinv₂] at h₂𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Bh:B ⟶ Ak:B ⟶ Afinv:B ⟶ Ahfinv₁:finv ⊚ f = 𝟙 Ahfinv₂:f ⊚ finv = 𝟙 Bh₁:h ⊚ f = k ⊚ fh₂:h ⊚ 𝟙 B = k ⊚ 𝟙 B⊢ h = k
  repeat rw [Category.id_comp] at h₂𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Bh:B ⟶ Ak:B ⟶ Afinv:B ⟶ Ahfinv₁:finv ⊚ f = 𝟙 Ahfinv₂:f ⊚ finv = 𝟙 Bh₁:h ⊚ f = k ⊚ fh₂:h = k⊢ h = k
  exact h₂All goals completed! 🐙

def f : Fin 2 ⟶ Fin 2
  | 0 => 1
  | 1 => 0

f has an inverse, as required. (f is self-inverse.)

example : f ⊚ f = 𝟙 (Fin 2) := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞⊢ f ⊚ f = 𝟙 (Fin 2)
  funext xh𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞x:Fin 2⊢ (f ⊚ f) x = 𝟙 (Fin 2) x
  fin_cases xh.«0»𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞⊢ (f ⊚ f) ((fun i ↦ i) ⟨0, ⋯⟩) = 𝟙 (Fin 2) ((fun i ↦ i) ⟨0, ⋯⟩)h.«1»𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞⊢ (f ⊚ f) ((fun i ↦ i) ⟨1, ⋯⟩) = 𝟙 (Fin 2) ((fun i ↦ i) ⟨1, ⋯⟩) <;>h.«0»𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞⊢ (f ⊚ f) ((fun i ↦ i) ⟨0, ⋯⟩) = 𝟙 (Fin 2) ((fun i ↦ i) ⟨0, ⋯⟩)h.«1»𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞⊢ (f ⊚ f) ((fun i ↦ i) ⟨1, ⋯⟩) = 𝟙 (Fin 2) ((fun i ↦ i) ⟨1, ⋯⟩) dsimp [f]All goals completed! 🐙

def h : Fin 2 ⟶ Fin 2
  | 0 => 1
  | 1 => 1

def k : Fin 2 ⟶ Fin 2
  | 0 => 0
  | 1 => 0

example : ¬(h ⊚ f = f ⊚ k → h = k) := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞⊢ ¬(h ⊚ f = f ⊚ k → h = k)
  push_neg𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞⊢ h ⊚ f = f ⊚ k ∧ h ≠ k
  constructorleft𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞⊢ h ⊚ f = f ⊚ kright𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞⊢ h ≠ k
  ·left𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞⊢ h ⊚ f = f ⊚ k funext xleft.h𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞x:Fin 2⊢ (h ⊚ f) x = (f ⊚ k) x
    fin_cases xleft.h.«0»𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞⊢ (h ⊚ f) ((fun i ↦ i) ⟨0, ⋯⟩) = (f ⊚ k) ((fun i ↦ i) ⟨0, ⋯⟩)left.h.«1»𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞⊢ (h ⊚ f) ((fun i ↦ i) ⟨1, ⋯⟩) = (f ⊚ k) ((fun i ↦ i) ⟨1, ⋯⟩) <;>left.h.«0»𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞⊢ (h ⊚ f) ((fun i ↦ i) ⟨0, ⋯⟩) = (f ⊚ k) ((fun i ↦ i) ⟨0, ⋯⟩)left.h.«1»𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞⊢ (h ⊚ f) ((fun i ↦ i) ⟨1, ⋯⟩) = (f ⊚ k) ((fun i ↦ i) ⟨1, ⋯⟩) dsimp [f, h, k]All goals completed! 🐙
  ·right𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞⊢ h ≠ k by_contra h₀right𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞h₀:h = k⊢ False
    have h₁ : h 0 = 1 := rflright𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞h₀:h = kh₁:h 0 = 1 := rfl⊢ False
    have h₂ : k 0 = 0 := rflright𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞h₀:h = kh₁:h 0 = 1 := rflh₂:k 0 = 0 := rfl⊢ False
    rw [← h₀, h₁] at h₂right𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞h₀:h = kh₁:h 0 = 1 := rflh₂:1 = 0⊢ False
    contradictionAll goals completed! 🐙

Exercise 4 (p. 44)

For each of the five maps below: decide whether it is invertible; and if it is invertible, find a 'formula' for the inverse map.

\mathbb{R} \xrightarrow{f} \mathbb{R},\; f(x) = 3x + 7
\mathbb{R}_{\ge 0} \xrightarrow{g} \mathbb{R}_{\ge 0},\; g(x) = x^2
\mathbb{R} \xrightarrow{h} \mathbb{R},\; h(x) = x^2
\mathbb{R} \xrightarrow{k} \mathbb{R}_{\ge 0},\; k(x) = x^2
\mathbb{R}_{\ge 0} \xrightarrow{l} \mathbb{R}_{\ge 0},\; l(x) = \dfrac{1}{x + 1}

Solution: Exercise 4

Since all five maps have their domain and codomain as the real numbers (or a subset of the real numbers), we implement them as functions in Lean.

f is invertible, with inverse {f^{-1}(x) = \dfrac{x - 7}{3}}.

example (f : ℝ → ℝ) (hf : ∀ x : ℝ, f x = 3 * x + 7)
    : ∃ finv : ℝ → ℝ, finv ∘ f = id ∧ f ∘ finv = id := byf:ℝ → ℝhf:∀ (x : ℝ), f x = 3 * x + 7⊢ ∃ finv, finv ∘ f = id ∧ f ∘ finv = id
  use fun x ↦ (x - 7) / 3hf:ℝ → ℝhf:∀ (x : ℝ), f x = 3 * x + 7⊢ (fun x ↦ (x - 7) / 3) ∘ f = id ∧ (f ∘ fun x ↦ (x - 7) / 3) = id -- f⁻¹(x)
  constructorh.leftf:ℝ → ℝhf:∀ (x : ℝ), f x = 3 * x + 7⊢ (fun x ↦ (x - 7) / 3) ∘ f = idh.rightf:ℝ → ℝhf:∀ (x : ℝ), f x = 3 * x + 7⊢ (f ∘ fun x ↦ (x - 7) / 3) = id
  ·h.leftf:ℝ → ℝhf:∀ (x : ℝ), f x = 3 * x + 7⊢ (fun x ↦ (x - 7) / 3) ∘ f = id funext xh.left.hf:ℝ → ℝhf:∀ (x : ℝ), f x = 3 * x + 7x:ℝ⊢ ((fun x ↦ (x - 7) / 3) ∘ f) x = id x
    rw [Function.comp_apply, id_eq, hf x]h.left.hf:ℝ → ℝhf:∀ (x : ℝ), f x = 3 * x + 7x:ℝ⊢ (3 * x + 7 - 7) / 3 = x
    ringAll goals completed! 🐙
  ·h.rightf:ℝ → ℝhf:∀ (x : ℝ), f x = 3 * x + 7⊢ (f ∘ fun x ↦ (x - 7) / 3) = id funext xh.right.hf:ℝ → ℝhf:∀ (x : ℝ), f x = 3 * x + 7x:ℝ⊢ (f ∘ fun x ↦ (x - 7) / 3) x = id x
    rw [Function.comp_apply, id_eq, hf ((x - 7) / 3)]h.right.hf:ℝ → ℝhf:∀ (x : ℝ), f x = 3 * x + 7x:ℝ⊢ 3 * ((x - 7) / 3) + 7 = x
    ringAll goals completed! 🐙

g is invertible, with inverse {g^{-1}(x) = \sqrt{x}}.

open NNReal in
example (g : ℝ≥0 → ℝ≥0) (hg : ∀ x : ℝ≥0, g x = x * x)
  : ∃ ginv : ℝ≥0 → ℝ≥0, ginv ∘ g = id ∧ g ∘ ginv = id := byg:ℝ≥0 → ℝ≥0hg:∀ (x : ℝ≥0), g x = x * x⊢ ∃ ginv, ginv ∘ g = id ∧ g ∘ ginv = id
  use fun x ↦ NNReal.sqrt xhg:ℝ≥0 → ℝ≥0hg:∀ (x : ℝ≥0), g x = x * x⊢ (fun x ↦ sqrt x) ∘ g = id ∧ (g ∘ fun x ↦ sqrt x) = id -- g⁻¹(x)
  constructorh.leftg:ℝ≥0 → ℝ≥0hg:∀ (x : ℝ≥0), g x = x * x⊢ (fun x ↦ sqrt x) ∘ g = idh.rightg:ℝ≥0 → ℝ≥0hg:∀ (x : ℝ≥0), g x = x * x⊢ (g ∘ fun x ↦ sqrt x) = id
  ·h.leftg:ℝ≥0 → ℝ≥0hg:∀ (x : ℝ≥0), g x = x * x⊢ (fun x ↦ sqrt x) ∘ g = id funext xh.left.hg:ℝ≥0 → ℝ≥0hg:∀ (x : ℝ≥0), g x = x * xx:ℝ≥0⊢ ((fun x ↦ sqrt x) ∘ g) x = id x
    rw [Function.comp_apply, id_eq, hg x]h.left.hg:ℝ≥0 → ℝ≥0hg:∀ (x : ℝ≥0), g x = x * xx:ℝ≥0⊢ sqrt (x * x) = x
    exact NNReal.sqrt_mul_self xAll goals completed! 🐙
  ·h.rightg:ℝ≥0 → ℝ≥0hg:∀ (x : ℝ≥0), g x = x * x⊢ (g ∘ fun x ↦ sqrt x) = id funext xh.right.hg:ℝ≥0 → ℝ≥0hg:∀ (x : ℝ≥0), g x = x * xx:ℝ≥0⊢ (g ∘ fun x ↦ sqrt x) x = id x
    rw [Function.comp_apply, id_eq, hg (sqrt x)]h.right.hg:ℝ≥0 → ℝ≥0hg:∀ (x : ℝ≥0), g x = x * xx:ℝ≥0⊢ sqrt x * sqrt x = x
    exact mul_self_sqrt xAll goals completed! 🐙

h is not invertible, since {h(1) = h(-1) = 1}.

example (h : ℝ → ℝ) (hh : ∀ x : ℝ, h x = x * x)
    : ¬(∃ hinv : ℝ → ℝ, hinv ∘ h = id ∧ h ∘ hinv = id) := byh:ℝ → ℝhh:∀ (x : ℝ), h x = x * x⊢ ¬∃ hinv, hinv ∘ h = id ∧ h ∘ hinv = id
  push_negh:ℝ → ℝhh:∀ (x : ℝ), h x = x * x⊢ ∀ (hinv : ℝ → ℝ), hinv ∘ h = id → h ∘ hinv ≠ id
  intro hinv h_inv_lefth:ℝ → ℝhh:∀ (x : ℝ), h x = x * xhinv:ℝ → ℝh_inv_left:hinv ∘ h = id⊢ h ∘ hinv ≠ id _h:ℝ → ℝhh:∀ (x : ℝ), h x = x * xhinv:ℝ → ℝh_inv_left:hinv ∘ h = ida✝:h ∘ hinv = id⊢ False
  have h₁ : h 1 = 1 := byh:ℝ → ℝhh:∀ (x : ℝ), h x = x * x⊢ ¬∃ hinv, hinv ∘ h = id ∧ h ∘ hinv = id
    rw [hh 1]h:ℝ → ℝhh:∀ (x : ℝ), h x = x * xhinv:ℝ → ℝh_inv_left:hinv ∘ h = ida✝:h ∘ hinv = id⊢ 1 * 1 = 1
    norm_num1All goals completed! 🐙
  have h₂ : h (-1) = 1 := byh:ℝ → ℝhh:∀ (x : ℝ), h x = x * x⊢ ¬∃ hinv, hinv ∘ h = id ∧ h ∘ hinv = id
    rw [hh (-1)]h:ℝ → ℝhh:∀ (x : ℝ), h x = x * xhinv:ℝ → ℝh_inv_left:hinv ∘ h = ida✝:h ∘ hinv = idh₁:h 1 = 1 := 
  Eq.mpr (id (congrArg (fun _a ↦ _a = 1) (hh 1)))
    (Mathlib.Meta.NormNum.isNat_eq_true
      (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl 1))
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))⊢ -1 * -1 = 1
    norm_num1All goals completed! 🐙
  have h₃ : (hinv ∘ h) 1 = 1:= byh:ℝ → ℝhh:∀ (x : ℝ), h x = x * x⊢ ¬∃ hinv, hinv ∘ h = id ∧ h ∘ hinv = id
    rw [h_inv_left, id_eq]All goals completed! 🐙
  have h₄ : (hinv ∘ h) (-1) = -1 := byh:ℝ → ℝhh:∀ (x : ℝ), h x = x * x⊢ ¬∃ hinv, hinv ∘ h = id ∧ h ∘ hinv = id
    rw [h_inv_left, id_eq]All goals completed! 🐙
  dsimp at h₃ h₄h:ℝ → ℝhh:∀ (x : ℝ), h x = x * xhinv:ℝ → ℝh_inv_left:hinv ∘ h = ida✝:h ∘ hinv = idh₁:h 1 = 1 := 
  Eq.mpr (id (congrArg (fun _a ↦ _a = 1) (hh 1)))
    (Mathlib.Meta.NormNum.isNat_eq_true
      (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl 1))
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))h₂:h (-1) = 1 := 
  Eq.mpr (id (congrArg (fun _a ↦ _a = 1) (hh (-1))))
    (Mathlib.Meta.NormNum.isNat_eq_true
      (Mathlib.Meta.NormNum.IsInt.to_isNat
        (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
          (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
            (Eq.refl (Int.negOfNat 1)))
          (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
            (Eq.refl (Int.negOfNat 1)))
          (Eq.refl (Int.ofNat 1))))
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))h₃:hinv (h 1) = 1 := Eq.mpr (id (congrArg (fun _a ↦ _a 1 = 1) h_inv_left)) (Eq.mpr (id (congrArg (fun _a ↦ _a = 1) (id_eq 1))) (Eq.refl 1))h₄:hinv (h (-1)) = -1 := 
  Eq.mpr (id (congrArg (fun _a ↦ _a (-1) = -1) h_inv_left))
    (Eq.mpr (id (congrArg (fun _a ↦ _a = -1) (id_eq (-1)))) (Eq.refl (-1)))⊢ False
  rw [h₁] at h₃h:ℝ → ℝhh:∀ (x : ℝ), h x = x * xhinv:ℝ → ℝh_inv_left:hinv ∘ h = ida✝:h ∘ hinv = idh₁:h 1 = 1 := 
  Eq.mpr (id (congrArg (fun _a ↦ _a = 1) (hh 1)))
    (Mathlib.Meta.NormNum.isNat_eq_true
      (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl 1))
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))h₂:h (-1) = 1 := 
  Eq.mpr (id (congrArg (fun _a ↦ _a = 1) (hh (-1))))
    (Mathlib.Meta.NormNum.isNat_eq_true
      (Mathlib.Meta.NormNum.IsInt.to_isNat
        (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
          (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
            (Eq.refl (Int.negOfNat 1)))
          (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
            (Eq.refl (Int.negOfNat 1)))
          (Eq.refl (Int.ofNat 1))))
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))h₃:hinv 1 = 1h₄:hinv (h (-1)) = -1⊢ False
  rw [h₂] at h₄h:ℝ → ℝhh:∀ (x : ℝ), h x = x * xhinv:ℝ → ℝh_inv_left:hinv ∘ h = ida✝:h ∘ hinv = idh₁:h 1 = 1 := 
  Eq.mpr (id (congrArg (fun _a ↦ _a = 1) (hh 1)))
    (Mathlib.Meta.NormNum.isNat_eq_true
      (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl 1))
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))h₂:h (-1) = 1 := 
  Eq.mpr (id (congrArg (fun _a ↦ _a = 1) (hh (-1))))
    (Mathlib.Meta.NormNum.isNat_eq_true
      (Mathlib.Meta.NormNum.IsInt.to_isNat
        (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
          (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
            (Eq.refl (Int.negOfNat 1)))
          (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
            (Eq.refl (Int.negOfNat 1)))
          (Eq.refl (Int.ofNat 1))))
      (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))h₃:hinv 1 = 1h₄:hinv 1 = -1⊢ False
  linarithAll goals completed! 🐙

k is not invertible, since {k(1) = k(-1) = 1}.

open NNReal in
example (k : ℝ → ℝ≥0) (hk : ∀ x : ℝ, k x = x * x)
    : ¬(∃ kinv : ℝ≥0 → ℝ, kinv ∘ k = id ∧ k ∘ kinv = id) := byk:ℝ → ℝ≥0hk:∀ (x : ℝ), ↑(k x) = x * x⊢ ¬∃ kinv, kinv ∘ k = id ∧ k ∘ kinv = id
  push_negk:ℝ → ℝ≥0hk:∀ (x : ℝ), ↑(k x) = x * x⊢ ∀ (kinv : ℝ≥0 → ℝ), kinv ∘ k = id → k ∘ kinv ≠ id
  intro kinv h_inv_leftk:ℝ → ℝ≥0hk:∀ (x : ℝ), ↑(k x) = x * xkinv:ℝ≥0 → ℝh_inv_left:kinv ∘ k = id⊢ k ∘ kinv ≠ id _k:ℝ → ℝ≥0hk:∀ (x : ℝ), ↑(k x) = x * xkinv:ℝ≥0 → ℝh_inv_left:kinv ∘ k = ida✝:k ∘ kinv = id⊢ False
  have h₁ : k 1 = 1 := byk:ℝ → ℝ≥0hk:∀ (x : ℝ), ↑(k x) = x * x⊢ ¬∃ kinv, kinv ∘ k = id ∧ k ∘ kinv = id
    rw [← coe_eq_one, hk 1]k:ℝ → ℝ≥0hk:∀ (x : ℝ), ↑(k x) = x * xkinv:ℝ≥0 → ℝh_inv_left:kinv ∘ k = ida✝:k ∘ kinv = id⊢ 1 * 1 = 1
    norm_num1All goals completed! 🐙
  have h₂ : k (-1) = 1 := byk:ℝ → ℝ≥0hk:∀ (x : ℝ), ↑(k x) = x * x⊢ ¬∃ kinv, kinv ∘ k = id ∧ k ∘ kinv = id
    rw [← coe_eq_one, hk (-1)]k:ℝ → ℝ≥0hk:∀ (x : ℝ), ↑(k x) = x * xkinv:ℝ≥0 → ℝh_inv_left:kinv ∘ k = ida✝:k ∘ kinv = idh₁:k 1 = 1 := 
  Eq.mpr (id (congrArg (fun _a ↦ _a) (Eq.symm (propext coe_eq_one))))
    (Eq.mpr (id (congrArg (fun _a ↦ _a = 1) (hk 1)))
      (Mathlib.Meta.NormNum.isNat_eq_true
        (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
          (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)))⊢ -1 * -1 = 1
    norm_num1All goals completed! 🐙
  have h₃ : (kinv ∘ k) 1 = 1:= byk:ℝ → ℝ≥0hk:∀ (x : ℝ), ↑(k x) = x * x⊢ ¬∃ kinv, kinv ∘ k = id ∧ k ∘ kinv = id
    rw [h_inv_left, id_eq]All goals completed! 🐙
  have h₄ : (kinv ∘ k) (-1) = -1 := byk:ℝ → ℝ≥0hk:∀ (x : ℝ), ↑(k x) = x * x⊢ ¬∃ kinv, kinv ∘ k = id ∧ k ∘ kinv = id
    rw [h_inv_left, id_eq]All goals completed! 🐙
  dsimp at h₃ h₄k:ℝ → ℝ≥0hk:∀ (x : ℝ), ↑(k x) = x * xkinv:ℝ≥0 → ℝh_inv_left:kinv ∘ k = ida✝:k ∘ kinv = idh₁:k 1 = 1 := 
  Eq.mpr (id (congrArg (fun _a ↦ _a) (Eq.symm (propext coe_eq_one))))
    (Eq.mpr (id (congrArg (fun _a ↦ _a = 1) (hk 1)))
      (Mathlib.Meta.NormNum.isNat_eq_true
        (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
          (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)))h₂:k (-1) = 1 := 
  Eq.mpr (id (congrArg (fun _a ↦ _a) (Eq.symm (propext coe_eq_one))))
    (Eq.mpr (id (congrArg (fun _a ↦ _a = 1) (hk (-1))))
      (Mathlib.Meta.NormNum.isNat_eq_true
        (Mathlib.Meta.NormNum.IsInt.to_isNat
          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
            (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
              (Eq.refl (Int.negOfNat 1)))
            (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
              (Eq.refl (Int.negOfNat 1)))
            (Eq.refl (Int.ofNat 1))))
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)))h₃:kinv (k 1) = 1 := Eq.mpr (id (congrArg (fun _a ↦ _a 1 = 1) h_inv_left)) (Eq.mpr (id (congrArg (fun _a ↦ _a = 1) (id_eq 1))) (Eq.refl 1))h₄:kinv (k (-1)) = -1 := 
  Eq.mpr (id (congrArg (fun _a ↦ _a (-1) = -1) h_inv_left))
    (Eq.mpr (id (congrArg (fun _a ↦ _a = -1) (id_eq (-1)))) (Eq.refl (-1)))⊢ False
  rw [h₁] at h₃k:ℝ → ℝ≥0hk:∀ (x : ℝ), ↑(k x) = x * xkinv:ℝ≥0 → ℝh_inv_left:kinv ∘ k = ida✝:k ∘ kinv = idh₁:k 1 = 1 := 
  Eq.mpr (id (congrArg (fun _a ↦ _a) (Eq.symm (propext coe_eq_one))))
    (Eq.mpr (id (congrArg (fun _a ↦ _a = 1) (hk 1)))
      (Mathlib.Meta.NormNum.isNat_eq_true
        (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
          (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)))h₂:k (-1) = 1 := 
  Eq.mpr (id (congrArg (fun _a ↦ _a) (Eq.symm (propext coe_eq_one))))
    (Eq.mpr (id (congrArg (fun _a ↦ _a = 1) (hk (-1))))
      (Mathlib.Meta.NormNum.isNat_eq_true
        (Mathlib.Meta.NormNum.IsInt.to_isNat
          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
            (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
              (Eq.refl (Int.negOfNat 1)))
            (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
              (Eq.refl (Int.negOfNat 1)))
            (Eq.refl (Int.ofNat 1))))
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)))h₃:kinv 1 = 1h₄:kinv (k (-1)) = -1⊢ False
  rw [h₂] at h₄k:ℝ → ℝ≥0hk:∀ (x : ℝ), ↑(k x) = x * xkinv:ℝ≥0 → ℝh_inv_left:kinv ∘ k = ida✝:k ∘ kinv = idh₁:k 1 = 1 := 
  Eq.mpr (id (congrArg (fun _a ↦ _a) (Eq.symm (propext coe_eq_one))))
    (Eq.mpr (id (congrArg (fun _a ↦ _a = 1) (hk 1)))
      (Mathlib.Meta.NormNum.isNat_eq_true
        (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)
          (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl 1))
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)))h₂:k (-1) = 1 := 
  Eq.mpr (id (congrArg (fun _a ↦ _a) (Eq.symm (propext coe_eq_one))))
    (Eq.mpr (id (congrArg (fun _a ↦ _a = 1) (hk (-1))))
      (Mathlib.Meta.NormNum.isNat_eq_true
        (Mathlib.Meta.NormNum.IsInt.to_isNat
          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
            (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
              (Eq.refl (Int.negOfNat 1)))
            (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
              (Eq.refl (Int.negOfNat 1)))
            (Eq.refl (Int.ofNat 1))))
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)))h₃:kinv 1 = 1h₄:kinv 1 = -1⊢ False
  linarithAll goals completed! 🐙

l is invertible, with inverse {l^{-1}(x) = \dfrac{1}{x} - 1}, provided that we restrict the codomain of l to the interval {(0,1]}.

TODO Exercise II.4.5

2. General division problems: Determination and choice

Exercise 5 concerns counting the number of sections and retractions for a map (though those terms aren't formally defined until a short while later on p. 49). Rather than providing an exhaustive list of maps, we introduce here two formulas — what the book later calls Chad's formula and Danilo's formula (p. 117).

The former states that the number of sections for a map p is given by \prod_{\mathbf{1} \xrightarrow{a} A} \#(p^{-1}a), where A is the codomain of p.

def Chad's_formula {α χ : Type*} [DecidableEq α]
    [Fintype α] [Fintype χ] (X : Finset χ) (A : Finset α)
    (p : χ → α)
    : ℕ :=
  ∏ a ∈ A, pinvCount a
where
  pinvCount (a : α) : ℕ := X.filter (fun x ↦ p x = a) |>.card

The latter states that the number of retractions for a map j, assuming j is injective, is given by (\#A)^{(\#X - \#A)}, where A is the domain of j and X is the codomain of j.

open Finset in
def Danilo's_formula {α χ : Type*}
    [Fintype α] [Fintype χ] (A : Finset α) (X : Finset χ)
    (j : α → χ) (p : χ → α) (_ : p ∘ j = id) (_ : Function.Injective j)
    : ℕ :=
  #A ^ (#X - #A)

Exercise 5 (p. 47)

Given

\{b, p, q, r, s\} \xrightarrow{g} \{0, 1\}\\\ \qquad b \mapsto 0\\\ \qquad p \mapsto 0\\\ \qquad q \mapsto 0\\\ \qquad r \mapsto 1\\\ \qquad s \mapsto 1,

how many maps f are there with {g \circ f = 1_{\{0, 1\}}}?

Choosing a particular such f, how many maps g (including the given one) satisfy the same equation?

Solution: Exercise 5

inductive XElems
  | b | p | q | r | s
  deriving Fintype

def A : Finset (Fin 2) := Finset.univ
def X : Finset XElems := Finset.univ

open XElems in
def g : XElems → Fin 2
  | b => 0
  | p => 0
  | q => 0
  | r => 1
  | s => 1

By Chad's formula, we have 6 different maps f with {g \circ f = 1_{\{0, 1\}}}.

6#eval Chad's_formula X A g

We choose f to be

open XElems in
def f : Fin 2 → XElems
  | 0 => b
  | 1 => r

Then, by Danilo's formula, we have {(\#A)^{(\#X - \#A)} = 2^3 = 8} different maps g.

8#eval Danilo's_formula A X f g
  (by⊢ g ∘ f = id
    funext xhx:Fin 2⊢ (g ∘ f) x = id x
    fin_cases xh.«0»⊢ (g ∘ f) ((fun i ↦ i) ⟨0, ⋯⟩) = id ((fun i ↦ i) ⟨0, ⋯⟩)h.«1»⊢ (g ∘ f) ((fun i ↦ i) ⟨1, ⋯⟩) = id ((fun i ↦ i) ⟨1, ⋯⟩) <;>h.«0»⊢ (g ∘ f) ((fun i ↦ i) ⟨0, ⋯⟩) = id ((fun i ↦ i) ⟨0, ⋯⟩)h.«1»⊢ (g ∘ f) ((fun i ↦ i) ⟨1, ⋯⟩) = id ((fun i ↦ i) ⟨1, ⋯⟩) rflAll goals completed! 🐙)
  (by⊢ Function.Injective f
    intro x yx:Fin 2y:Fin 2⊢ f x = f y → x = y _x:Fin 2y:Fin 2a✝:f x = f y⊢ x = y
    fin_cases x«0»y:Fin 2a✝:f ((fun i ↦ i) ⟨0, ⋯⟩) = f y⊢ (fun i ↦ i) ⟨0, ⋯⟩ = y«1»y:Fin 2a✝:f ((fun i ↦ i) ⟨1, ⋯⟩) = f y⊢ (fun i ↦ i) ⟨1, ⋯⟩ = y <;>«0»y:Fin 2a✝:f ((fun i ↦ i) ⟨0, ⋯⟩) = f y⊢ (fun i ↦ i) ⟨0, ⋯⟩ = y«1»y:Fin 2a✝:f ((fun i ↦ i) ⟨1, ⋯⟩) = f y⊢ (fun i ↦ i) ⟨1, ⋯⟩ = y fin_cases y«1».«0»a✝:f ((fun i ↦ i) ⟨1, ⋯⟩) = f ((fun i ↦ i) ⟨0, ⋯⟩)⊢ (fun i ↦ i) ⟨1, ⋯⟩ = (fun i ↦ i) ⟨0, ⋯⟩«1».«1»a✝:f ((fun i ↦ i) ⟨1, ⋯⟩) = f ((fun i ↦ i) ⟨1, ⋯⟩)⊢ (fun i ↦ i) ⟨1, ⋯⟩ = (fun i ↦ i) ⟨1, ⋯⟩
    all_goals
      first | rflAll goals completed! 🐙
            | simp only [Fin.zero_eta, Fin.isValue, Fin.mk_one,
                         zero_ne_one]«1».«0»a✝:f ((fun i ↦ i) ⟨1, ⋯⟩) = f ((fun i ↦ i) ⟨0, ⋯⟩)⊢ 1 = 0; trivialAll goals completed! 🐙)

3. Retractions, sections, and idempotents

Definition: Retraction, Section (p. 49)

If {A \xrightarrow{f} B}:

a retraction for f is a map {B \xrightarrow{r} A} for which {r \circ f = 1_A};

a section for f is a map {B \xrightarrow{s} A} for which {f \circ s = 1_B}.

The mathlib definition corresponding to retraction is SplitMono (and IsSplitMono), which we print below for reference.

structure CategoryTheory.SplitMono.{v₁, u₁} {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : Type v₁
number of parameters: 5
fields:
  CategoryTheory.SplitMono.retraction : Y ⟶ X
  CategoryTheory.SplitMono.id : self.retraction ⊚ f = 𝟙 X := by
    cat_disch
constructor:
  CategoryTheory.SplitMono.mk.{v₁, u₁} {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (retraction : Y ⟶ X)
    (id : retraction ⊚ f = 𝟙 X := by cat_disch) : SplitMono f#print SplitMono

structure CategoryTheory.SplitMono.{v₁, u₁} {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : Type v₁
number of parameters: 5
fields:
  CategoryTheory.SplitMono.retraction : Y ⟶ X
  CategoryTheory.SplitMono.id : self.retraction ⊚ f = 𝟙 X := by
    cat_disch
constructor:
  CategoryTheory.SplitMono.mk.{v₁, u₁} {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (retraction : Y ⟶ X)
    (id : retraction ⊚ f = 𝟙 X := by cat_disch) : SplitMono f

class CategoryTheory.IsSplitMono.{v₁, u₁} {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : Prop
number of parameters: 5
fields:
  CategoryTheory.IsSplitMono.exists_splitMono : Nonempty (SplitMono f)
constructor:
  CategoryTheory.IsSplitMono.mk.{v₁, u₁} {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y}
    (exists_splitMono : Nonempty (SplitMono f)) : IsSplitMono f#print IsSplitMono

class CategoryTheory.IsSplitMono.{v₁, u₁} {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : Prop
number of parameters: 5
fields:
  CategoryTheory.IsSplitMono.exists_splitMono : Nonempty (SplitMono f)
constructor:
  CategoryTheory.IsSplitMono.mk.{v₁, u₁} {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y}
    (exists_splitMono : Nonempty (SplitMono f)) : IsSplitMono f

We alias SplitMono and IsSplitMono as Retraction and IsRetraction, respectively, to remain aligned with the terminology in the book.

abbrev Retraction {𝒞 : Type u} [Category.{v, u} 𝒞] {A B : 𝒞}
    (f : A ⟶ B) :=
  SplitMono f
abbrev IsRetraction {𝒞 : Type u} [Category.{v, u} 𝒞] {A B : 𝒞}
    (f : A ⟶ B) :=
  IsSplitMono f

The mathlib definition corresponding to section is SplitEpi (and IsSplitEpi), which we print below for reference.

structure CategoryTheory.SplitEpi.{v₁, u₁} {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : Type v₁
number of parameters: 5
fields:
  CategoryTheory.SplitEpi.section_ : Y ⟶ X
  CategoryTheory.SplitEpi.id : f ⊚ self.section_ = 𝟙 Y := by
    cat_disch
constructor:
  CategoryTheory.SplitEpi.mk.{v₁, u₁} {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (section_ : Y ⟶ X)
    (id : f ⊚ section_ = 𝟙 Y := by cat_disch) : SplitEpi f#print SplitEpi

structure CategoryTheory.SplitEpi.{v₁, u₁} {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : Type v₁
number of parameters: 5
fields:
  CategoryTheory.SplitEpi.section_ : Y ⟶ X
  CategoryTheory.SplitEpi.id : f ⊚ self.section_ = 𝟙 Y := by
    cat_disch
constructor:
  CategoryTheory.SplitEpi.mk.{v₁, u₁} {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (section_ : Y ⟶ X)
    (id : f ⊚ section_ = 𝟙 Y := by cat_disch) : SplitEpi f

class CategoryTheory.IsSplitEpi.{v₁, u₁} {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : Prop
number of parameters: 5
fields:
  CategoryTheory.IsSplitEpi.exists_splitEpi : Nonempty (SplitEpi f)
constructor:
  CategoryTheory.IsSplitEpi.mk.{v₁, u₁} {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y}
    (exists_splitEpi : Nonempty (SplitEpi f)) : IsSplitEpi f#print IsSplitEpi

class CategoryTheory.IsSplitEpi.{v₁, u₁} {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : Prop
number of parameters: 5
fields:
  CategoryTheory.IsSplitEpi.exists_splitEpi : Nonempty (SplitEpi f)
constructor:
  CategoryTheory.IsSplitEpi.mk.{v₁, u₁} {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y}
    (exists_splitEpi : Nonempty (SplitEpi f)) : IsSplitEpi f

We alias SplitEpi and IsSplitEpi as Section and IsSection, respectively, to remain aligned with the terminology in the book.

abbrev Section {𝒞 : Type u} [Category.{v, u} 𝒞] {A B : 𝒞}
    (f : A ⟶ B) :=
  SplitEpi f
abbrev IsSection {𝒞 : Type u} [Category.{v, u} 𝒞] {A B : 𝒞}
    (f : A ⟶ B) :=
  IsSplitEpi f

Proposition 1 (p. 51)

If a map {A \xrightarrow{f} B} has a section, then for any T and for any map {T \xrightarrow{y} B} there exists a map {T \xrightarrow{x} A} for which {f \circ x = y}.

Proof (p. 51)

The assumption means that we have a map s for which {f \circ s = 1_B}. Thus for any given map {T \xrightarrow{y} B} we see that we could define a map x with at least the correct domain and codomain by taking the composite s following y x = s \circ y. Does this map x actually satisfy the required equation? Calculating f \circ x = f \circ (s \circ y) = (f \circ s) \circ y = 1_B \circ y = y we see that it does.

Our implementation in Lean faithfully follows the argument of the book proof given above.

theorem prop1 {𝒞 : Type u} [Category.{v, u} 𝒞] {A B T : 𝒞}
    (f : A ⟶ B) [hf : IsSection f]
    : ∀ y : T ⟶ B, ∃ x : T ⟶ A, f ⊚ x = y := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞T:𝒞f:A ⟶ Bhf:IsSection f⊢ ∀ (y : T ⟶ B), ∃ x, f ⊚ x = y
  obtain ⟨s, hf⟩ := hf𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞T:𝒞f:A ⟶ Bs:B ⟶ Ahf:f ⊚ s = 𝟙 B⊢ ∀ (y : T ⟶ B), ∃ x, f ⊚ x = y
  intro y𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞T:𝒞f:A ⟶ Bs:B ⟶ Ahf:f ⊚ s = 𝟙 By:T ⟶ B⊢ ∃ x, f ⊚ x = y
  use s ⊚ yh𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞T:𝒞f:A ⟶ Bs:B ⟶ Ahf:f ⊚ s = 𝟙 By:T ⟶ B⊢ f ⊚ s ⊚ y = y
  rw [Category.assoc]h𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞T:𝒞f:A ⟶ Bs:B ⟶ Ahf:f ⊚ s = 𝟙 By:T ⟶ B⊢ (f ⊚ s) ⊚ y = y
  rw [hf]h𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞T:𝒞f:A ⟶ Bs:B ⟶ Ahf:f ⊚ s = 𝟙 By:T ⟶ B⊢ 𝟙 B ⊚ y = y
  exact Category.comp_id yAll goals completed! 🐙

Exercise 6 (p. 52)

If the map {A \xrightarrow{f} B} has a retraction, then for any map {A \xrightarrow{g} T}, there is a map {B \xrightarrow{t} T} for which {t \circ f = g}. (This is Proposition 1*.)

Solution: Exercise 6

Put {t = g \circ r}.

theorem «prop1*» {𝒞 : Type u} [Category.{v, u} 𝒞] {A B T : 𝒞}
    (f : A ⟶ B) [hf : IsRetraction f]
    : ∀ g : A ⟶ T, ∃ t : B ⟶ T, t ⊚ f = g := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞T:𝒞f:A ⟶ Bhf:IsRetraction f⊢ ∀ (g : A ⟶ T), ∃ t, t ⊚ f = g
  obtain ⟨r, hf⟩ := hf𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞T:𝒞f:A ⟶ Br:B ⟶ Ahf:r ⊚ f = 𝟙 A⊢ ∀ (g : A ⟶ T), ∃ t, t ⊚ f = g
  intro g𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞T:𝒞f:A ⟶ Br:B ⟶ Ahf:r ⊚ f = 𝟙 Ag:A ⟶ T⊢ ∃ t, t ⊚ f = g
  use g ⊚ rh𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞T:𝒞f:A ⟶ Br:B ⟶ Ahf:r ⊚ f = 𝟙 Ag:A ⟶ T⊢ (g ⊚ r) ⊚ f = g
  rw [← Category.assoc, hf, Category.id_comp]All goals completed! 🐙

Proposition 2 (p. 52)

Suppose a map {A \xrightarrow{f} B} has a retraction. Then for any set T and for any pair of maps {T \xrightarrow{x_1} A}, {T \xrightarrow{x_2} A} from any set T to A \text{if}\; f \circ x_1 = f \circ x_2 \;\text{then}\; x_1 = x_2.

Proof (p. 52)

Looking back at the definition, we see that the assumption means that we have a map r for which {r \circ f = 1_A}. Using the assumption that x_1 and x_2 are such that f composes with them to get the same {T \rightarrow B}, we can compose further with r as follows: x_1 = 1_A \circ x_1 = (r \circ f) \circ x_1 = r \circ (f \circ x_1) = r \circ (f \circ x_2) = (r \circ f) \circ x_2 = 1_A \circ x_2 = x_2.

Our implementation in Lean generalises the proposition from sets to any categorical object but otherwise faithfully follows the argument of the book proof given above.

theorem prop2 {𝒞 : Type u} [Category.{v, u} 𝒞] {A B T : 𝒞}
    (f : A ⟶ B) [hf : IsRetraction f]
    : ∀ x₁ x₂ : T ⟶ A, f ⊚ x₁ = f ⊚ x₂ → x₁ = x₂ := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞T:𝒞f:A ⟶ Bhf:IsRetraction f⊢ ∀ (x₁ x₂ : T ⟶ A), f ⊚ x₁ = f ⊚ x₂ → x₁ = x₂
  obtain ⟨r, hf⟩ := hf𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞T:𝒞f:A ⟶ Br:B ⟶ Ahf:r ⊚ f = 𝟙 A⊢ ∀ (x₁ x₂ : T ⟶ A), f ⊚ x₁ = f ⊚ x₂ → x₁ = x₂
  intro x₁ x₂𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞T:𝒞f:A ⟶ Br:B ⟶ Ahf:r ⊚ f = 𝟙 Ax₁:T ⟶ Ax₂:T ⟶ A⊢ f ⊚ x₁ = f ⊚ x₂ → x₁ = x₂ h𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞T:𝒞f:A ⟶ Br:B ⟶ Ahf:r ⊚ f = 𝟙 Ax₁:T ⟶ Ax₂:T ⟶ Ah:f ⊚ x₁ = f ⊚ x₂⊢ x₁ = x₂
  rw [← Category.comp_id x₁]𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞T:𝒞f:A ⟶ Br:B ⟶ Ahf:r ⊚ f = 𝟙 Ax₁:T ⟶ Ax₂:T ⟶ Ah:f ⊚ x₁ = f ⊚ x₂⊢ 𝟙 A ⊚ x₁ = x₂
  rw [← hf]𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞T:𝒞f:A ⟶ Br:B ⟶ Ahf:r ⊚ f = 𝟙 Ax₁:T ⟶ Ax₂:T ⟶ Ah:f ⊚ x₁ = f ⊚ x₂⊢ (r ⊚ f) ⊚ x₁ = x₂
  rw [← Category.assoc]𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞T:𝒞f:A ⟶ Br:B ⟶ Ahf:r ⊚ f = 𝟙 Ax₁:T ⟶ Ax₂:T ⟶ Ah:f ⊚ x₁ = f ⊚ x₂⊢ r ⊚ f ⊚ x₁ = x₂
  rw [h]𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞T:𝒞f:A ⟶ Br:B ⟶ Ahf:r ⊚ f = 𝟙 Ax₁:T ⟶ Ax₂:T ⟶ Ah:f ⊚ x₁ = f ⊚ x₂⊢ r ⊚ f ⊚ x₂ = x₂
  rw [Category.assoc]𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞T:𝒞f:A ⟶ Br:B ⟶ Ahf:r ⊚ f = 𝟙 Ax₁:T ⟶ Ax₂:T ⟶ Ah:f ⊚ x₁ = f ⊚ x₂⊢ (r ⊚ f) ⊚ x₂ = x₂
  rw [hf]𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞T:𝒞f:A ⟶ Br:B ⟶ Ahf:r ⊚ f = 𝟙 Ax₁:T ⟶ Ax₂:T ⟶ Ah:f ⊚ x₁ = f ⊚ x₂⊢ 𝟙 A ⊚ x₂ = x₂
  exact Category.comp_id x₂All goals completed! 🐙

Definition: Injective, Monomorphism (p. 52)

A map f satisfying the conclusion of Proposition 2 (for any pair of maps {T \xrightarrow{x_1} A} and {T \xrightarrow{x_2} A}, if {f \circ x_1 = f \circ x_2} then {x_1 = x_2}) is said to be injective for maps from T.

If f is injective for maps from T for every T, one says that f is injective, or is a monomorphism.

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

class CategoryTheory.Mono.{v, u} {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : Prop
number of parameters: 5
fields:
  CategoryTheory.Mono.right_cancellation : ∀ {Z : C} (g h : Z ⟶ X), f ⊚ g = f ⊚ h → g = h
constructor:
  CategoryTheory.Mono.mk.{v, u} {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
    (right_cancellation : ∀ {Z : C} (g h : Z ⟶ X), f ⊚ g = f ⊚ h → g = h) : Mono f#print Mono

class CategoryTheory.Mono.{v, u} {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : Prop
number of parameters: 5
fields:
  CategoryTheory.Mono.right_cancellation : ∀ {Z : C} (g h : Z ⟶ X), f ⊚ g = f ⊚ h → g = h
constructor:
  CategoryTheory.Mono.mk.{v, u} {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
    (right_cancellation : ∀ {Z : C} (g h : Z ⟶ X), f ⊚ g = f ⊚ h → g = h) : Mono f

Exercise 7 (p. 53)

Suppose the map {A \xrightarrow{f} B} has a section. Then for any set T and any pair {B \xrightarrow{t_1} T}, {B \xrightarrow{t_2} T} of maps from B to T, if {t_1 \circ f = t_2 \circ f} then {t_1 = t_2}. (This is Proposition 2*.)

Solution: Exercise 7

A proof of Proposition 2* is given below.

theorem «prop2*» {𝒞 : Type u} [Category.{v, u} 𝒞] {A B T : 𝒞}
    (f : A ⟶ B) [hf : IsSection f]
    : ∀ t₁ t₂ : B ⟶ T, t₁ ⊚ f = t₂ ⊚ f → t₁ = t₂ := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞T:𝒞f:A ⟶ Bhf:IsSection f⊢ ∀ (t₁ t₂ : B ⟶ T), t₁ ⊚ f = t₂ ⊚ f → t₁ = t₂
  obtain ⟨s, hf⟩ := hf𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞T:𝒞f:A ⟶ Bs:B ⟶ Ahf:f ⊚ s = 𝟙 B⊢ ∀ (t₁ t₂ : B ⟶ T), t₁ ⊚ f = t₂ ⊚ f → t₁ = t₂
  intro t₁ t₂𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞T:𝒞f:A ⟶ Bs:B ⟶ Ahf:f ⊚ s = 𝟙 Bt₁:B ⟶ Tt₂:B ⟶ T⊢ t₁ ⊚ f = t₂ ⊚ f → t₁ = t₂ h𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞T:𝒞f:A ⟶ Bs:B ⟶ Ahf:f ⊚ s = 𝟙 Bt₁:B ⟶ Tt₂:B ⟶ Th:t₁ ⊚ f = t₂ ⊚ f⊢ t₁ = t₂
  rw [← Category.id_comp t₁, ← hf]𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞T:𝒞f:A ⟶ Bs:B ⟶ Ahf:f ⊚ s = 𝟙 Bt₁:B ⟶ Tt₂:B ⟶ Th:t₁ ⊚ f = t₂ ⊚ f⊢ t₁ ⊚ f ⊚ s = t₂
  rw [Category.assoc, h, ← Category.assoc]𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞T:𝒞f:A ⟶ Bs:B ⟶ Ahf:f ⊚ s = 𝟙 Bt₁:B ⟶ Tt₂:B ⟶ Th:t₁ ⊚ f = t₂ ⊚ f⊢ t₂ ⊚ f ⊚ s = t₂
  rw [hf, Category.id_comp]All goals completed! 🐙

Definition: Surjective, Epimorphism (p. 53)

A map f with this cancellation property (if {t_1 \circ f = t_2 \circ f} then {t_1 = t_2}) for every T is called an epimorphism.

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

class CategoryTheory.Epi.{v, u} {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : Prop
number of parameters: 5
fields:
  CategoryTheory.Epi.left_cancellation : ∀ {Z : C} (g h : Y ⟶ Z), g ⊚ f = h ⊚ f → g = h
constructor:
  CategoryTheory.Epi.mk.{v, u} {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
    (left_cancellation : ∀ {Z : C} (g h : Y ⟶ Z), g ⊚ f = h ⊚ f → g = h) : Epi f#print Epi

class CategoryTheory.Epi.{v, u} {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : Prop
number of parameters: 5
fields:
  CategoryTheory.Epi.left_cancellation : ∀ {Z : C} (g h : Y ⟶ Z), g ⊚ f = h ⊚ f → g = h
constructor:
  CategoryTheory.Epi.mk.{v, u} {C : Type u} [Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
    (left_cancellation : ∀ {Z : C} (g h : Y ⟶ Z), g ⊚ f = h ⊚ f → g = h) : Epi f

Excerpt (p. 53)

Thus both 'monomorphism' and 'epimorphism' are 'cancellation' properties.

The mathlib theorems cancel_mono and cancel_epi are relevant here.

example {𝒞 : Type u} [Category.{v, u} 𝒞] {X Y Z : 𝒞}
    (f : X ⟶ Y) [Mono f] {g h : Z ⟶ X}
    : f ⊚ g = f ⊚ h ↔ g = h := cancel_mono f

example {𝒞 : Type u} [Category.{v, u} 𝒞] {X Y Z : 𝒞}
    (f : X ⟶ Y) [Epi f] {g h : Y ⟶ Z}
    : g ⊚ f = h ⊚ f ↔ g = h := cancel_epi f

Proposition 3 (p. 53)

If {A \xrightarrow{f} B} has a retraction and if {B \xrightarrow{g} C} has a retraction, then {A \xrightarrow{g \circ f} C} has a retraction.

Proof (p. 53)

Let {r_1 \circ f = 1_A} and {r_2 \circ g = 1_B}. Then a good guess for a retraction of the composite would be the composite of the retractions in the opposite order (which is anyway the only order in which they can be composed). Does it in fact work? r \circ (g \circ f) = (r_1 \circ r_2) \circ (g \circ f) = r_1 \circ (r_2 \circ g) \circ f = r_1 \circ 1_B \circ f = r_1 \circ f = 1_A proves that r is a retraction for {g \circ f}.

Our implementation in Lean faithfully follows the argument of the book proof given above.

theorem prop3 {𝒞 : Type u} [Category.{v, u} 𝒞] {A B C : 𝒞}
    (f : A ⟶ B) [hf : IsRetraction f] (g : B ⟶ C) [hg : IsRetraction g]
    : IsRetraction (g ⊚ f) := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bhf:IsRetraction fg:B ⟶ Chg:IsRetraction g⊢ IsRetraction (g ⊚ f)
  obtain ⟨r₁, hf⟩ := hf𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bg:B ⟶ Chg:IsRetraction gr₁:B ⟶ Ahf:r₁ ⊚ f = 𝟙 A⊢ IsRetraction (g ⊚ f)
  obtain ⟨r₂, hg⟩ := hg𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bg:B ⟶ Cr₁:B ⟶ Ahf:r₁ ⊚ f = 𝟙 Ar₂:C ⟶ Bhg:r₂ ⊚ g = 𝟙 B⊢ IsRetraction (g ⊚ f)
  use r₁ ⊚ r₂id𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bg:B ⟶ Cr₁:B ⟶ Ahf:r₁ ⊚ f = 𝟙 Ar₂:C ⟶ Bhg:r₂ ⊚ g = 𝟙 B⊢ autoParam ((r₁ ⊚ r₂) ⊚ g ⊚ f = 𝟙 A) SplitMono.id._autoParam
  change (r₁ ⊚ r₂) ⊚ (g ⊚ f) = 𝟙 Aid𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bg:B ⟶ Cr₁:B ⟶ Ahf:r₁ ⊚ f = 𝟙 Ar₂:C ⟶ Bhg:r₂ ⊚ g = 𝟙 B⊢ (r₁ ⊚ r₂) ⊚ g ⊚ f = 𝟙 A
  rw [Category.assoc, ← Category.assoc g]id𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bg:B ⟶ Cr₁:B ⟶ Ahf:r₁ ⊚ f = 𝟙 Ar₂:C ⟶ Bhg:r₂ ⊚ g = 𝟙 B⊢ (r₁ ⊚ r₂ ⊚ g) ⊚ f = 𝟙 A
  rw [hg]id𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bg:B ⟶ Cr₁:B ⟶ Ahf:r₁ ⊚ f = 𝟙 Ar₂:C ⟶ Bhg:r₂ ⊚ g = 𝟙 B⊢ (r₁ ⊚ 𝟙 B) ⊚ f = 𝟙 A
  rw [Category.id_comp]id𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bg:B ⟶ Cr₁:B ⟶ Ahf:r₁ ⊚ f = 𝟙 Ar₂:C ⟶ Bhg:r₂ ⊚ g = 𝟙 B⊢ r₁ ⊚ f = 𝟙 A
  exact hfAll goals completed! 🐙

We note that the corresponding mathlib instance is instIsSplitMonoComp.

example {𝒞 : Type u} [Category.{v, u} 𝒞] {A B C : 𝒞}
    (f : A ⟶ B) [hf : IsRetraction f] (g : B ⟶ C) [hg : IsRetraction g]
    : IsRetraction (g ⊚ f) := instIsSplitMonoComp

Exercise 8 (p. 54)

Prove that the composite of two maps, each having sections, has itself a section.

Solution: Exercise 8

The section of the composite is the composite of the sections in the opposite order (cf. Proposition 3).

example {𝒞 : Type u} [Category.{v, u} 𝒞] {A B C : 𝒞}
    (f : A ⟶ B) [hf : IsSection f] (g : B ⟶ C) [hg : IsSection g]
    : IsSection (g ⊚ f) := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bhf:IsSection fg:B ⟶ Chg:IsSection g⊢ IsSection (g ⊚ f)
  obtain ⟨s₁, hf⟩ := hf𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bg:B ⟶ Chg:IsSection gs₁:B ⟶ Ahf:f ⊚ s₁ = 𝟙 B⊢ IsSection (g ⊚ f)
  obtain ⟨s₂, hg⟩ := hg𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bg:B ⟶ Cs₁:B ⟶ Ahf:f ⊚ s₁ = 𝟙 Bs₂:C ⟶ Bhg:g ⊚ s₂ = 𝟙 C⊢ IsSection (g ⊚ f)
  use s₁ ⊚ s₂id𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bg:B ⟶ Cs₁:B ⟶ Ahf:f ⊚ s₁ = 𝟙 Bs₂:C ⟶ Bhg:g ⊚ s₂ = 𝟙 C⊢ autoParam ((g ⊚ f) ⊚ s₁ ⊚ s₂ = 𝟙 C) SplitEpi.id._autoParam
  change (g ⊚ f) ⊚ (s₁ ⊚ s₂) = 𝟙 Cid𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bg:B ⟶ Cs₁:B ⟶ Ahf:f ⊚ s₁ = 𝟙 Bs₂:C ⟶ Bhg:g ⊚ s₂ = 𝟙 C⊢ (g ⊚ f) ⊚ s₁ ⊚ s₂ = 𝟙 C
  rw [Category.assoc, ← Category.assoc s₁]id𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bg:B ⟶ Cs₁:B ⟶ Ahf:f ⊚ s₁ = 𝟙 Bs₂:C ⟶ Bhg:g ⊚ s₂ = 𝟙 C⊢ (g ⊚ f ⊚ s₁) ⊚ s₂ = 𝟙 C
  rw [hf]id𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bg:B ⟶ Cs₁:B ⟶ Ahf:f ⊚ s₁ = 𝟙 Bs₂:C ⟶ Bhg:g ⊚ s₂ = 𝟙 C⊢ (g ⊚ 𝟙 B) ⊚ s₂ = 𝟙 C
  rw [Category.id_comp]id𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bg:B ⟶ Cs₁:B ⟶ Ahf:f ⊚ s₁ = 𝟙 Bs₂:C ⟶ Bhg:g ⊚ s₂ = 𝟙 C⊢ g ⊚ s₂ = 𝟙 C
  exact hgAll goals completed! 🐙

We note that the corresponding mathlib instance is instIsSplitEpiComp.

example {𝒞 : Type u} [Category.{v, u} 𝒞] {A B C : 𝒞}
    (f : A ⟶ B) [hf : IsSection f] (g : B ⟶ C) [hg : IsSection g]
    : IsSection (g ⊚ f) := instIsSplitEpiComp

Definition: Idempotent (p. 54)

An endomap e is called idempotent if {e \circ e = e}.

We implement Idempotent and IsIdempotent in Lean as follows:

structure Idempotent {𝒞 : Type u} [Category.{v, u} 𝒞] (A : 𝒞) where
  e : A ⟶ A
  idem : e ⊚ e = e

class IsIdempotent {𝒞 : Type u} [Category.{v, u} 𝒞] {A : 𝒞}
    (e : A ⟶ A) where
  idem : e ⊚ e = e

Exercise 9 (p. 54)

Suppose r is a retraction of f (equivalently f is a section of r) and let {e = f \circ r}. Show that e is an idempotent.... Show that if f is an isomorphism, then e is the identity.

Solution: Exercise 9

variable {𝒞 : Type u} [Category.{v, u} 𝒞] {A B : 𝒞}
         (f : A ⟶ B) (e : B ⟶ B)

We show that e is an idempotent.

example (r : Retraction f) (he : e = f ⊚ r.retraction)
    : IsIdempotent e := {
  idem := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Be:B ⟶ Br:Retraction fhe:e = f ⊚ r.retraction⊢ e ⊚ e = e
    rw [he, Category.assoc, ← Category.assoc f, r.id,
        Category.id_comp]All goals completed! 🐙
}

We show that e is the identity if f is an isomorphism.

example [hf : IsIso f]
    (r : Retraction f) (he : e = f ⊚ r.retraction)
    : e = 𝟙 B := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Be:B ⟶ Bhf:IsIso fr:Retraction fhe:e = f ⊚ r.retraction⊢ e = 𝟙 B
  have ⟨finv, hfinv⟩ := hf𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Be:B ⟶ Bhf:IsIso fr:Retraction fhe:e = f ⊚ r.retractionfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 B⊢ e = 𝟙 B
  rw [← hfinv.2, ← Category.id_comp f, ← r.id]𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Be:B ⟶ Bhf:IsIso fr:Retraction fhe:e = f ⊚ r.retractionfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 B⊢ e = (f ⊚ r.retraction ⊚ f) ⊚ finv
  repeat rw [← Category.assoc]𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Be:B ⟶ Bhf:IsIso fr:Retraction fhe:e = f ⊚ r.retractionfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 B⊢ e = f ⊚ r.retraction ⊚ f ⊚ finv
  rwa [hfinv.2, Category.id_comp]𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Be:B ⟶ Bhf:IsIso fr:Retraction fhe:e = f ⊚ r.retractionfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 B⊢ e = f ⊚ r.retraction

Theorem (uniqueness of inverses) (p. 54)

If f has both a retraction r and a section s then {r = s}.

Proof (p. 54)

From the definition we have, if {A \xrightarrow{f} B}, both of the equations r \circ f = 1_A \quad\text{and}\quad f \circ s = 1_B. Then by the identity laws and the associative law r = r \circ 1_B = r \circ (f \circ s) = (r \circ f) \circ s = 1_A \circ s = s.

Our implementation in Lean faithfully follows the argument of the book proof given above.

theorem uniqueness_of_inverses {𝒞 : Type u} [Category.{v, u} 𝒞]
    {A B : 𝒞} (f : A ⟶ B) (r : Retraction f) (s : Section f)
    : r.retraction = s.section_ := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Br:Retraction fs:Section f⊢ r.retraction = s.section_
  obtain ⟨r, hr⟩ := r𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Bs:Section fr:B ⟶ Ahr:r ⊚ f = 𝟙 A⊢ { retraction := r, id := hr }.retraction = s.section_
  obtain ⟨s, hs⟩ := s𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Br:B ⟶ Ahr:r ⊚ f = 𝟙 As:B ⟶ Ahs:f ⊚ s = 𝟙 B⊢ { retraction := r, id := hr }.retraction = { section_ := s, id := hs }.section_
  change r = s𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Br:B ⟶ Ahr:r ⊚ f = 𝟙 As:B ⟶ Ahs:f ⊚ s = 𝟙 B⊢ r = s
  calc
    r = r ⊚ 𝟙 B := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Br:B ⟶ Ahr:r ⊚ f = 𝟙 As:B ⟶ Ahs:f ⊚ s = 𝟙 B⊢ r = r ⊚ 𝟙 B rw [Category.id_comp]All goals completed! 🐙
    _ = r ⊚ (f ⊚ s) := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Br:B ⟶ Ahr:r ⊚ f = 𝟙 As:B ⟶ Ahs:f ⊚ s = 𝟙 B⊢ r ⊚ 𝟙 B = r ⊚ f ⊚ s rw [hs]All goals completed! 🐙
    _ = (r ⊚ f) ⊚ s := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Br:B ⟶ Ahr:r ⊚ f = 𝟙 As:B ⟶ Ahs:f ⊚ s = 𝟙 B⊢ r ⊚ f ⊚ s = (r ⊚ f) ⊚ s rw [← Category.assoc]All goals completed! 🐙
    _ = 𝟙 A ⊚ s := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Br:B ⟶ Ahr:r ⊚ f = 𝟙 As:B ⟶ Ahs:f ⊚ s = 𝟙 B⊢ (r ⊚ f) ⊚ s = 𝟙 A ⊚ s rw [← hr]All goals completed! 🐙
    _ = s := Category.comp_id s

4. Isomorphisms and automorphisms

Definition: Isomorphism, Inverse (p. 54)

A map {A \xrightarrow{f} B} is called an isomorphism if there exists another map {B \xrightarrow{f^{-1}} A} which is both a retraction and a section for f: f \circ f⁻¹ = 1_B,\\\ f⁻¹ \circ f = 1_A. Such a map f^{-1} is called the inverse map for f; since both of the two equations are required, the theorem of uniqueness of inverses shows that there is only one inverse.

We compare these definitions of isomorphism and inverse with the earlier definitions on p. 40. A proof that the two definitions of isomorphism are equivalent is given below.

example {𝒞 : Type u} [Category.{v, u} 𝒞] {A B : 𝒞}
    (f : A ⟶ B) (r : Retraction f) (s : Section f)
    : r.retraction = s.section_ ↔ IsIso f := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Br:Retraction fs:Section f⊢ r.retraction = s.section_ ↔ IsIso f
  constructormp𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Br:Retraction fs:Section f⊢ r.retraction = s.section_ → IsIso fmpr𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Br:Retraction fs:Section f⊢ IsIso f → r.retraction = s.section_
  ·mp𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Br:Retraction fs:Section f⊢ r.retraction = s.section_ → IsIso f intro hmp𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Br:Retraction fs:Section fh:r.retraction = s.section_⊢ IsIso f
    exact {
      out := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Br:Retraction fs:Section fh:r.retraction = s.section_⊢ ∃ inv, inv ⊚ f = 𝟙 A ∧ f ⊚ inv = 𝟙 B
        use r.retractionh𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Br:Retraction fs:Section fh:r.retraction = s.section_⊢ r.retraction ⊚ f = 𝟙 A ∧ f ⊚ r.retraction = 𝟙 B
        constructorh.left𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Br:Retraction fs:Section fh:r.retraction = s.section_⊢ r.retraction ⊚ f = 𝟙 Ah.right𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Br:Retraction fs:Section fh:r.retraction = s.section_⊢ f ⊚ r.retraction = 𝟙 B
        ·h.left𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Br:Retraction fs:Section fh:r.retraction = s.section_⊢ r.retraction ⊚ f = 𝟙 A exact r.idAll goals completed! 🐙
        ·h.right𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Br:Retraction fs:Section fh:r.retraction = s.section_⊢ f ⊚ r.retraction = 𝟙 B rw [h]h.right𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Br:Retraction fs:Section fh:r.retraction = s.section_⊢ f ⊚ s.section_ = 𝟙 B
          exact s.idAll goals completed! 🐙
    }
  ·mpr𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Br:Retraction fs:Section f⊢ IsIso f → r.retraction = s.section_ rintro ⟨finv, hfinv⟩mpr𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Br:Retraction fs:Section ffinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 B⊢ r.retraction = s.section_
    obtain ⟨r, hr⟩ := rmpr𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Bs:Section ffinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Br:B ⟶ Ahr:r ⊚ f = 𝟙 A⊢ { retraction := r, id := hr }.retraction = s.section_
    obtain ⟨s, hs⟩ := smpr𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Bfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Br:B ⟶ Ahr:r ⊚ f = 𝟙 As:B ⟶ Ahs:f ⊚ s = 𝟙 B⊢ { retraction := r, id := hr }.retraction = { section_ := s, id := hs }.section_
    change r = smpr𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Bfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Br:B ⟶ Ahr:r ⊚ f = 𝟙 As:B ⟶ Ahs:f ⊚ s = 𝟙 B⊢ r = s
    calc
      r = r ⊚ 𝟙 B := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Bfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Br:B ⟶ Ahr:r ⊚ f = 𝟙 As:B ⟶ Ahs:f ⊚ s = 𝟙 B⊢ r = r ⊚ 𝟙 B rw [Category.id_comp]All goals completed! 🐙
      _ = r ⊚ (f ⊚ s) := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Bfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Br:B ⟶ Ahr:r ⊚ f = 𝟙 As:B ⟶ Ahs:f ⊚ s = 𝟙 B⊢ r ⊚ 𝟙 B = r ⊚ f ⊚ s rw [hs]All goals completed! 🐙
      _ = (r ⊚ f) ⊚ s := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Bfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Br:B ⟶ Ahr:r ⊚ f = 𝟙 As:B ⟶ Ahs:f ⊚ s = 𝟙 B⊢ r ⊚ f ⊚ s = (r ⊚ f) ⊚ s rw [← Category.assoc]All goals completed! 🐙
      _ = 𝟙 A ⊚ s := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞f:A ⟶ Bfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Br:B ⟶ Ahr:r ⊚ f = 𝟙 As:B ⟶ Ahs:f ⊚ s = 𝟙 B⊢ (r ⊚ f) ⊚ s = 𝟙 A ⊚ s rw [← hr]All goals completed! 🐙
      _ = s := Category.comp_id s

When working with inverse maps in Excercise 10, we make use of mathlib's CategoryTheory.inv, which we print below for reference.

def CategoryTheory.inv.{v, u} : {C : Type u} →
  [inst : Category.{v, u} C] → {X Y : C} → (f : X ⟶ Y) → [I : IsIso f] → Y ⟶ X :=
fun {C} [Category.{v, u} C] {X Y} f [IsIso f] ↦ Classical.choose ⋯#print CategoryTheory.inv

def CategoryTheory.inv.{v, u} : {C : Type u} →
  [inst : Category.{v, u} C] → {X Y : C} → (f : X ⟶ Y) → [I : IsIso f] → Y ⟶ X :=
fun {C} [Category.{v, u} C] {X Y} f [IsIso f] ↦ Classical.choose ⋯

Exercise 10 (p. 55)

If {A \xrightarrow{f} B \xrightarrow{g} C} are both isomorphisms, then {g \circ f} is an isomorphism too, and {(g \circ f)^{-1} = f^{-1} \circ g^{-1}}.

Solution: Exercise 10

The inverse of the composite is the composite of the inverses in the opposite order.

open CategoryTheory in
example {𝒞 : Type u} [Category.{v, u} 𝒞] {A B C : 𝒞}
    (f : A ⟶ B) [hf : IsIso f] (g : B ⟶ C) [hg : IsIso g]
    : IsIso (g ⊚ f) ∧ inv (g ⊚ f) = inv f ⊚ inv g := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bhf:IsIso fg:B ⟶ Chg:IsIso g⊢ IsIso (g ⊚ f) ∧ inv (g ⊚ f) = inv f ⊚ inv g
  constructorleft𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bhf:IsIso fg:B ⟶ Chg:IsIso g⊢ IsIso (g ⊚ f)right𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bhf:IsIso fg:B ⟶ Chg:IsIso g⊢ inv (g ⊚ f) = inv f ⊚ inv g
  ·left𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bhf:IsIso fg:B ⟶ Chg:IsIso g⊢ IsIso (g ⊚ f) obtain ⟨finv, hfinv⟩ := hfleft𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bg:B ⟶ Chg:IsIso gfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 B⊢ IsIso (g ⊚ f)
    obtain ⟨ginv, hginv⟩ := hgleft𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bg:B ⟶ Cfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Bginv:C ⟶ Bhginv:ginv ⊚ g = 𝟙 B ∧ g ⊚ ginv = 𝟙 C⊢ IsIso (g ⊚ f)
    exact {
      out := by𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bg:B ⟶ Cfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Bginv:C ⟶ Bhginv:ginv ⊚ g = 𝟙 B ∧ g ⊚ ginv = 𝟙 C⊢ ∃ inv, inv ⊚ g ⊚ f = 𝟙 A ∧ (g ⊚ f) ⊚ inv = 𝟙 C
        use finv ⊚ ginvh𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bg:B ⟶ Cfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Bginv:C ⟶ Bhginv:ginv ⊚ g = 𝟙 B ∧ g ⊚ ginv = 𝟙 C⊢ (finv ⊚ ginv) ⊚ g ⊚ f = 𝟙 A ∧ (g ⊚ f) ⊚ finv ⊚ ginv = 𝟙 C
        constructorh.left𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bg:B ⟶ Cfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Bginv:C ⟶ Bhginv:ginv ⊚ g = 𝟙 B ∧ g ⊚ ginv = 𝟙 C⊢ (finv ⊚ ginv) ⊚ g ⊚ f = 𝟙 Ah.right𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bg:B ⟶ Cfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Bginv:C ⟶ Bhginv:ginv ⊚ g = 𝟙 B ∧ g ⊚ ginv = 𝟙 C⊢ (g ⊚ f) ⊚ finv ⊚ ginv = 𝟙 C
        ·h.left𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bg:B ⟶ Cfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Bginv:C ⟶ Bhginv:ginv ⊚ g = 𝟙 B ∧ g ⊚ ginv = 𝟙 C⊢ (finv ⊚ ginv) ⊚ g ⊚ f = 𝟙 A rw [Category.assoc, ← Category.assoc g]h.left𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bg:B ⟶ Cfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Bginv:C ⟶ Bhginv:ginv ⊚ g = 𝟙 B ∧ g ⊚ ginv = 𝟙 C⊢ (finv ⊚ ginv ⊚ g) ⊚ f = 𝟙 A
          rw [hginv.1]h.left𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bg:B ⟶ Cfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Bginv:C ⟶ Bhginv:ginv ⊚ g = 𝟙 B ∧ g ⊚ ginv = 𝟙 C⊢ (finv ⊚ 𝟙 B) ⊚ f = 𝟙 A
          rw [Category.id_comp]h.left𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bg:B ⟶ Cfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Bginv:C ⟶ Bhginv:ginv ⊚ g = 𝟙 B ∧ g ⊚ ginv = 𝟙 C⊢ finv ⊚ f = 𝟙 A
          exact hfinv.1All goals completed! 🐙
        ·h.right𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bg:B ⟶ Cfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Bginv:C ⟶ Bhginv:ginv ⊚ g = 𝟙 B ∧ g ⊚ ginv = 𝟙 C⊢ (g ⊚ f) ⊚ finv ⊚ ginv = 𝟙 C rw [Category.assoc, ← Category.assoc finv]h.right𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bg:B ⟶ Cfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Bginv:C ⟶ Bhginv:ginv ⊚ g = 𝟙 B ∧ g ⊚ ginv = 𝟙 C⊢ (g ⊚ f ⊚ finv) ⊚ ginv = 𝟙 C
          rw [hfinv.2]h.right𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bg:B ⟶ Cfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Bginv:C ⟶ Bhginv:ginv ⊚ g = 𝟙 B ∧ g ⊚ ginv = 𝟙 C⊢ (g ⊚ 𝟙 B) ⊚ ginv = 𝟙 C
          rw [Category.id_comp]h.right𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bg:B ⟶ Cfinv:B ⟶ Ahfinv:finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 Bginv:C ⟶ Bhginv:ginv ⊚ g = 𝟙 B ∧ g ⊚ ginv = 𝟙 C⊢ g ⊚ ginv = 𝟙 C
          exact hginv.2All goals completed! 🐙
    }
  ·right𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞B:𝒞C:𝒞f:A ⟶ Bhf:IsIso fg:B ⟶ Chg:IsIso g⊢ inv (g ⊚ f) = inv f ⊚ inv g exact IsIso.inv_compAll goals completed! 🐙

Exercise 11 (p. 55)

If {A = \{\mathit{Fatima}, \mathit{Omer}, \mathit{Alysia}\}} and {B = \{\mathit{coffee}, \mathit{tea}, \mathit{cocoa}\}}, find an example of an isomorphism {A \xrightarrow{f} B}. If {C = \{\mathit{true}, \mathit{false}\}}, can you find any isomorphism {A \rightarrow C}?

Solution: Exercise 11

namespace ExII_11

For convenience, we use finite types here instead of finite sets.

inductive A
  | Fatima | Omer | Alysia
  deriving Fintype

inductive B
  | coffee | tea | cocoa
  deriving Fintype

We give a map f and its inverse f^{-1} below, along with a proof that f is an isomorphism.

def f : A ⟶ B
  | A.Fatima => B.coffee
  | A.Omer => B.tea
  | A.Alysia => B.cocoa

def finv : B ⟶ A
  | B.coffee => A.Fatima
  | B.tea => A.Omer
  | B.cocoa => A.Alysia

example : IsIso f := {
  out := by⊢ ∃ inv, inv ⊚ f = 𝟙 A ∧ f ⊚ inv = 𝟙 B
    use finvh⊢ finv ⊚ f = 𝟙 A ∧ f ⊚ finv = 𝟙 B
    constructorh.left⊢ finv ⊚ f = 𝟙 Ah.right⊢ f ⊚ finv = 𝟙 B
    all_goals
      funext xh.right.hx:B⊢ (f ⊚ finv) x = 𝟙 B x
      fin_cases xh.right.h.«0»⊢ (f ⊚ finv) B.coffee = 𝟙 B B.coffeeh.right.h.«1»⊢ (f ⊚ finv) B.tea = 𝟙 B B.teah.right.h.«2»⊢ (f ⊚ finv) B.cocoa = 𝟙 B B.cocoa <;>h.right.h.«0»⊢ (f ⊚ finv) B.coffee = 𝟙 B B.coffeeh.right.h.«1»⊢ (f ⊚ finv) B.tea = 𝟙 B B.teah.right.h.«2»⊢ (f ⊚ finv) B.cocoa = 𝟙 B B.cocoa dsimp [f, finv]All goals completed! 🐙
}

end ExII_11

Since {\#A > \#C}, there can be no pair {A \xrightarrow{j} C}, {C \xrightarrow{p} A} such that {p \circ j = 1_A}; hence there is no isomorphism {A \rightarrow C}.

Excerpt (p. 55)

A map which is both an endomap and at the same time an isomorphism is usually called by the one word automorphism.

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

def CategoryTheory.Aut.{v, u} : {C : Type u} → [Category.{v, u} C] → C → Type v :=
fun {C} [Category.{v, u} C] X ↦ X ≅ X#print Aut

def CategoryTheory.Aut.{v, u} : {C : Type u} → [Category.{v, u} C] → C → Type v :=
fun {C} [Category.{v, u} C] X ↦ X ≅ X

Compare this to the mathlib definition End for endomorphisms of an object in a category.

def CategoryTheory.End.{v, u} : {C : Type u} → [CategoryStruct.{v, u} C] → C → Type v :=
fun {C} [CategoryStruct.{v, u} C] X ↦ X ⟶ X#print End

def CategoryTheory.End.{v, u} : {C : Type u} → [CategoryStruct.{v, u} C] → C → Type v :=
fun {C} [CategoryStruct.{v, u} C] X ↦ X ⟶ X

Exercise 12 (p. 56)

How many isomorphisms are there from {A = \{\mathit{Fatima}, \mathit{Omer}, \mathit{Alysia}\}} to {B = \{\mathit{coffee}, \mathit{tea}, \mathit{cocoa}\}}? How many automorphisms of A are there? The answers should be less than 27 — why?

Solution: Exercise 12

Provided two sets/types have the same number n of elements, the number of isomorphisms between them is n!; if the sets/types have different numbers of elements, then there are no isomorphisms between them. We implement this formula in Lean as follows:

def isoCount (α β : Type*) [Fintype α] [Fintype β] : ℕ :=
  if Fintype.card α = Fintype.card β then
    Nat.factorial (Fintype.card α)
  else
    0

By the formula above, we have 6 different isomorphisms.

open ExII_11

6#eval isoCount A B

Essentially the same formula applies to automorphisms, since an automorphism is just an isomorphism from a set/type to itself. Thus, there are also 6 different automorphisms of A.

abbrev autCount (α : Type*) [Fintype α] := isoCount α α

open ExII_11

6#eval autCount A

By Alysia's formula, {3^3 = 27} is the number of distinct maps {A \rightarrow B} (or {A \rightarrow A}), so the number of isomorphisms between A and B (or automorphisms of A) must be less than 27.

Excerpt (p. 57)

An automorphism in the category of sets is also traditionally called a permutation, suggesting that it shifts the elements of its set around in a specified way.

Repeating the second part of Exercise 12, now using sets instead of types, we have

def permCount {α : Type*} (s : Finset α) : ℕ :=
  if 0 < Finset.card s then
    Nat.factorial (Finset.card s)
  else
    0

open ExII_11

6#eval permCount (Finset.univ (α := A))