A Lean Companion to Conceptual Mathematics

Summary: On the equation p ∘ j = 1A

Excerpt (p. 117)

If maps {A \xrightarrow{j} X \xrightarrow{p} A} satisfy {p \circ j = 1_A}, several consequences follow:

Excerpt (p. 117)

In any category

variable {𝒞 : Type u} [Category.{v, u} 𝒞] {A X : 𝒞} {j : A ⟶ X} {p : X ⟶ A}
Excerpt (p. 117)

The endomap {X \xrightarrow{j \circ p} X} (call it '\alpha' for short) satisfies {\alpha \circ \alpha = \alpha}; we say \alpha is idempotent. Written out in full, this is {(j \circ p) \circ (j \circ p) = (j \circ p)}.

example (hpj : p ⊚ j = 𝟙 A) : (j ⊚ p) ⊚ (j ⊚ p) = (j ⊚ p) := 𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞X:𝒞j:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 A⊢ (j ⊚ p) ⊚ j ⊚ p = j ⊚ p 𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞X:𝒞j:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 Aα:X ⟶ X := j ⊚ p⊢ α ⊚ α = α 𝒞:Type uinst✝:Category.{v, u} 𝒞A:𝒞X:𝒞j:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 Aα:X ⟶ X := j ⊚ p⊢ α ⊚ α = α All goals completed! 🐙
Excerpt (p. 117)

In the category of finite sets

We use Fintypes instead of finite sets.

variable {A X : Type u} [Fintype A] [Fintype X] {j : A ⟶ X} {p : X ⟶ A}
Excerpt (p. 117)

(1) p satisfies: for each member a of A, there is at least one member x of X for which {p(x) = a}; (We say p is surjective.)

example (hpj : p ⊚ j = 𝟙 A) : ∀ a : A, ∃ x : X, p x = a := A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 A⊢ ∀ (a : A), ∃ x, p x = a A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 Aa:A⊢ ∃ x, p x = a A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 Aa:A⊢ p (j a) = a A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 Aa:A⊢ 𝟙 A a = a All goals completed! 🐙

A morphism with this property in the category Type (and also in the category of sets) is a surjective function, defined in mathlib as Function.Surjective, which we print below for reference.

def Function.Surjective.{u_1, u_2} : {α : Sort u_1} → {β : Sort u_2} → (α → β) → Prop := fun {α} {β} f ↦ ∀ (b : β), ∃ a, f a = b#print Function.Surjective 
def Function.Surjective.{u_1, u_2} : {α : Sort u_1} → {β : Sort u_2} → (α → β) → Prop :=
fun {α} {β} f ↦ ∀ (b : β), ∃ a, f a = b

Hence we can restate our proof of (1) above as

example (hpj : p ⊚ j = 𝟙 A) : Function.Surjective p := A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 A⊢ Function.Surjective p A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 Aa:A⊢ ∃ a_1, p a_1 = a A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 Aa:A⊢ p (j a) = a A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 Aa:A⊢ 𝟙 A a = a All goals completed! 🐙

The mathlib theorem epi_iff_surjective is also relevant here.

example {X Y : Type u} (f : X ⟶ Y) : Epi f ↔ Function.Surjective f := epi_iff_surjective f
Excerpt (p. 117)

(2) j satisfies: if {j(a_1) = j(a_2)}, then {a_1 = a_2}; (We say j is injective.)

example (hpj : p ⊚ j = 𝟙 A) : ∀ a₁ a₂ : A, j a₁ = j a₂ → a₁ = a₂ := A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 A⊢ ∀ (a₁ a₂ : A), j a₁ = j a₂ → a₁ = a₂ intro a₁ A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 Aa₁:Aa₂:A⊢ j a₁ = j a₂ → a₁ = a₂ A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 Aa₁:Aa₂:Ah:j a₁ = j a₂⊢ a₁ = a₂ calc a₁ _ = 𝟙 A a₁ := rfl _ = (p ⊚ j) a₁ := A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 Aa₁:Aa₂:Ah:j a₁ = j a₂⊢ 𝟙 A a₁ = (p ⊚ j) a₁ All goals completed! 🐙 _ = p (j a₁) := rfl _ = p (j a₂) := A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 Aa₁:Aa₂:Ah:j a₁ = j a₂⊢ p (j a₁) = p (j a₂) All goals completed! 🐙 _ = (p ⊚ j) a₂ := rfl _ = 𝟙 A a₂ := A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 Aa₁:Aa₂:Ah:j a₁ = j a₂⊢ (p ⊚ j) a₂ = 𝟙 A a₂ All goals completed! 🐙 _ = a₂ := rfl

A morphism with this property in the category Type (and also in the category of sets) is an injective function, defined in mathlib as Function.Injective, which we print below for reference.

def Function.Injective.{u_1, u_2} : {α : Sort u_1} → {β : Sort u_2} → (α → β) → Prop := fun {α} {β} f ↦ ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂#print Function.Injective 
def Function.Injective.{u_1, u_2} : {α : Sort u_1} → {β : Sort u_2} → (α → β) → Prop :=
fun {α} {β} f ↦ ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂

Hence we can restate our proof of (2) above as

example (hpj : p ⊚ j = 𝟙 A) : Function.Injective j := A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 A⊢ Function.Injective j intro a₁ A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 Aa₁:Aa₂:A⊢ j a₁ = j a₂ → a₁ = a₂ A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 Aa₁:Aa₂:Ah:j a₁ = j a₂⊢ a₁ = a₂ calc a₁ _ = 𝟙 A a₁ := rfl _ = (p ⊚ j) a₁ := A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 Aa₁:Aa₂:Ah:j a₁ = j a₂⊢ 𝟙 A a₁ = (p ⊚ j) a₁ All goals completed! 🐙 _ = p (j a₁) := rfl _ = p (j a₂) := A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 Aa₁:Aa₂:Ah:j a₁ = j a₂⊢ p (j a₁) = p (j a₂) All goals completed! 🐙 _ = (p ⊚ j) a₂ := rfl _ = 𝟙 A a₂ := A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 Aa₁:Aa₂:Ah:j a₁ = j a₂⊢ (p ⊚ j) a₂ = 𝟙 A a₂ All goals completed! 🐙 _ = a₂ := rfl

The mathlib theorem mono_iff_injective is also relevant here.

example {X Y : Type u} (f : X ⟶ Y) : Mono f ↔ Function.Injective f := mono_iff_injective f
Excerpt (p. 117)

(3) {\#A \le \#X}, and if {\#A = 0}, then {\#X = 0} too!

The key step in our proof below that {\#A \le \#X} is provided by the mathlib theorem Cardinal.mk_le_of_surjective, which states that the number of elements of the codomain of a surjective function is less than or equal to the number of elements of its domain, as follows:

example {α β : Type u} {f : α → β} (hf_surj : Function.Surjective f) : Cardinal.mk β ≤ Cardinal.mk α := Cardinal.mk_le_of_surjective hf_surj

Hence our proof is

open Cardinal in example (hpj : p ⊚ j = 𝟙 A) : #A ≤ #X := A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 A⊢ #A ≤ #X A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 Ahp₁:Section p := { section_ := j, id := ⋯ }⊢ #A ≤ #X A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 Ahp₁:Section p := { section_ := j, id := ⋯ }hp₂:Epi p := SplitEpi.epi hp₁⊢ #A ≤ #X A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 Ahp₁:Section p := { section_ := j, id := ⋯ }hp₂:Epi p := SplitEpi.epi hp₁hp₃:Function.Surjective p := (epi_iff_surjective p).mp hp₂⊢ #A ≤ #X All goals completed! 🐙

or, alternatively, using the counterpart mathlib theorem Cardinal.mk_le_of_injective,

open Cardinal in example (hpj : p ⊚ j = 𝟙 A) : #A ≤ #X := A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 A⊢ #A ≤ #X A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 Ahj₁:Retraction j := { retraction := p, id := ⋯ }⊢ #A ≤ #X A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 Ahj₁:Retraction j := { retraction := p, id := ⋯ }hj₂:Mono j := SplitMono.mono hj₁⊢ #A ≤ #X A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ahpj:p ⊚ j = 𝟙 Ahj₁:Retraction j := { retraction := p, id := ⋯ }hj₂:Mono j := SplitMono.mono hj₁hj₃:Function.Injective j := (mono_iff_injective j).mp hj₂⊢ #A ≤ #X All goals completed! 🐙

For the second part of (3) — that is, if {\#A = 0}, then {\#X = 0} — we first define the following lemma:

open Cardinal in theorem h_cardinal_zero_eq_zero_iff {α : Type u} [Fintype α] : #α = 0 ↔ IsEmpty α := α:Type uinst✝:Fintype α⊢ #α = 0 ↔ IsEmpty α α:Type uinst✝:Fintype α⊢ ↑(Fintype.card α) = 0 ↔ IsEmpty α α:Type uinst✝:Fintype α⊢ Fintype.card α = 0 ↔ IsEmpty α All goals completed! 🐙

We can then proceed as below. (Note that the primary assumption {p \circ j = 1_A} is not required here, since any p that maps to an empty codomain must have an empty domain.)

open Cardinal in example (_ : p ⊚ j = 𝟙 A) : #A = 0 → #X = 0 := A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ax✝:p ⊚ j = 𝟙 A⊢ #A = 0 → #X = 0 repeat A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ax✝:p ⊚ j = 𝟙 A⊢ IsEmpty A → IsEmpty X A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ax✝:p ⊚ j = 𝟙 AhA:IsEmpty A⊢ IsEmpty X A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ax✝:p ⊚ j = 𝟙 AhA:IsEmpty A⊢ ∀ (a : X), False A:Type uX:Type uinst✝¹:Fintype Ainst✝:Fintype Xj:A ⟶ Xp:X ⟶ Ax✝:p ⊚ j = 𝟙 AhA:IsEmpty Ax:X⊢ False All goals completed! 🐙