Quiz

Problem 1 (p. 108)

Give an example of two explicit sets A and B and an explicit map {A \xrightarrow{f} B} satisfying both:

(a) there is a retraction for f, and

(b) there is no section for f.

Then explain how you know that f satisfies (a) and (b).

Solution: Problem 1

We use Fintypes here instead of sets.

We give explicit types A and B and an explicit map f.

inductive A
  | a
  deriving Fintype

inductive B
  | b₁ | b₂
  deriving Fintype

def f : A ⟶ B
  | A.a => B.b₁

Our candidate retraction for f is

def r : B ⟶ A
  | B.b₁ => A.a
  | B.b₂ => A.a

and we show that (a) is satisfied.

example : IsRetraction f := by⊢ IsRetraction f
  use rid⊢ autoParam (r ⊚ f = 𝟙 A) SplitMono.id._autoParam
  change r ⊚ f = 𝟙 Aid⊢ r ⊚ f = 𝟙 A
  funext xid.hx:A⊢ (r ⊚ f) x = 𝟙 A x
  fin_cases xid.h.«0»⊢ (r ⊚ f) A.a = 𝟙 A A.a
  dsimp [f, r]All goals completed! 🐙

We show that f also satisfies (b).

example : ¬(IsSection f) := by⊢ ¬IsSection f
  by_contra hh:IsSection f⊢ False
  obtain ⟨s, hs⟩ := hs:B ⟶ Ahs:f ⊚ s = 𝟙 B⊢ False
  have h_false := congrFun hs B.b₂s:B ⟶ Ahs:f ⊚ s = 𝟙 Bh_false:(f ⊚ s) B.b₂ = 𝟙 B B.b₂ := congrFun hs B.b₂⊢ False
  cases h_falseAll goals completed! 🐙

Problem 2 (p. 108)

If {C \xrightarrow{p} D \xrightarrow{q} C} satisfy {p \circ q \circ p = p}, can you conclude that

(a) {p \circ q} is idempotent? If so, how?

(b) {q \circ p} is idempotent? If so, how?

Solution: Problem 2

variable {𝒞 : Type u} [Category.{v, u} 𝒞] {C D : 𝒞}
         (p : C ⟶ D) (q : D ⟶ C) (hpq : p ⊚ q ⊚ p = p)

We show that {p \circ q} is idempotent.

example : IsIdempotent (p ⊚ q) := {
  idem := by𝒞:Type uinst✝:Category.{v, u} 𝒞C:𝒞D:𝒞p:C ⟶ Dq:D ⟶ Chpq:p ⊚ q ⊚ p = p⊢ (p ⊚ q) ⊚ p ⊚ q = p ⊚ q
    calc (p ⊚ q) ⊚ p ⊚ q
      _ = ((p ⊚ q) ⊚ p) ⊚ q := by𝒞:Type uinst✝:Category.{v, u} 𝒞C:𝒞D:𝒞p:C ⟶ Dq:D ⟶ Chpq:p ⊚ q ⊚ p = p⊢ (p ⊚ q) ⊚ p ⊚ q = ((p ⊚ q) ⊚ p) ⊚ q rw [Category.assoc]All goals completed! 🐙
      _ = (p ⊚ q ⊚ p) ⊚ q := by𝒞:Type uinst✝:Category.{v, u} 𝒞C:𝒞D:𝒞p:C ⟶ Dq:D ⟶ Chpq:p ⊚ q ⊚ p = p⊢ ((p ⊚ q) ⊚ p) ⊚ q = (p ⊚ q ⊚ p) ⊚ q rw [← Category.assoc p]All goals completed! 🐙
      _ = p ⊚ q := by𝒞:Type uinst✝:Category.{v, u} 𝒞C:𝒞D:𝒞p:C ⟶ Dq:D ⟶ Chpq:p ⊚ q ⊚ p = p⊢ (p ⊚ q ⊚ p) ⊚ q = p ⊚ q rw [hpq]All goals completed! 🐙
}

We show that {q \circ p} is idempotent.

example : IsIdempotent (q ⊚ p) := {
  idem := by𝒞:Type uinst✝:Category.{v, u} 𝒞C:𝒞D:𝒞p:C ⟶ Dq:D ⟶ Chpq:p ⊚ q ⊚ p = p⊢ (q ⊚ p) ⊚ q ⊚ p = q ⊚ p
    calc (q ⊚ p) ⊚ q ⊚ p
      _ = q ⊚ p ⊚ q ⊚ p := by𝒞:Type uinst✝:Category.{v, u} 𝒞C:𝒞D:𝒞p:C ⟶ Dq:D ⟶ Chpq:p ⊚ q ⊚ p = p⊢ (q ⊚ p) ⊚ q ⊚ p = q ⊚ p ⊚ q ⊚ p rw [Category.assoc (q ⊚ p)]All goals completed! 🐙
      _ = q ⊚ p := by𝒞:Type uinst✝:Category.{v, u} 𝒞C:𝒞D:𝒞p:C ⟶ Dq:D ⟶ Chpq:p ⊚ q ⊚ p = p⊢ q ⊚ p ⊚ q ⊚ p = q ⊚ p rw [hpq]All goals completed! 🐙
}

Optional questions

Problem 2* (p. 108)

If {C \xrightarrow{p} D \xrightarrow{q} C} satisfy {p \circ q \circ p = p}, use the given maps p and q to devise a map q' satisfying both: p \circ q' \circ p = p and q' \circ p \circ q' = q' (and explain how you know that your q' has these properties).

Solution: Problem 2*

variable {𝒞 : Type u} [Category.{v, u} 𝒞] {C D : 𝒞}
         (p : C ⟶ D) (q : D ⟶ C) (hpq : p ⊚ q ⊚ p = p)

We show that {q' = q \circ p \circ q} has the required properties.

example : ∃ q', p ⊚ q' ⊚ p = p ∧ q' ⊚ p ⊚ q' = q' := by𝒞:Type uinst✝:Category.{v, u} 𝒞C:𝒞D:𝒞p:C ⟶ Dq:D ⟶ Chpq:p ⊚ q ⊚ p = p⊢ ∃ q', p ⊚ q' ⊚ p = p ∧ q' ⊚ p ⊚ q' = q'
  use q ⊚ p ⊚ qh𝒞:Type uinst✝:Category.{v, u} 𝒞C:𝒞D:𝒞p:C ⟶ Dq:D ⟶ Chpq:p ⊚ q ⊚ p = p⊢ p ⊚ (q ⊚ p ⊚ q) ⊚ p = p ∧ (q ⊚ p ⊚ q) ⊚ p ⊚ q ⊚ p ⊚ q = q ⊚ p ⊚ q -- q'
  constructorh.left𝒞:Type uinst✝:Category.{v, u} 𝒞C:𝒞D:𝒞p:C ⟶ Dq:D ⟶ Chpq:p ⊚ q ⊚ p = p⊢ p ⊚ (q ⊚ p ⊚ q) ⊚ p = ph.right𝒞:Type uinst✝:Category.{v, u} 𝒞C:𝒞D:𝒞p:C ⟶ Dq:D ⟶ Chpq:p ⊚ q ⊚ p = p⊢ (q ⊚ p ⊚ q) ⊚ p ⊚ q ⊚ p ⊚ q = q ⊚ p ⊚ q
  ·h.left𝒞:Type uinst✝:Category.{v, u} 𝒞C:𝒞D:𝒞p:C ⟶ Dq:D ⟶ Chpq:p ⊚ q ⊚ p = p⊢ p ⊚ (q ⊚ p ⊚ q) ⊚ p = p rw [← Category.assoc p, ← Category.assoc, hpq, hpq]All goals completed! 🐙
  ·h.right𝒞:Type uinst✝:Category.{v, u} 𝒞C:𝒞D:𝒞p:C ⟶ Dq:D ⟶ Chpq:p ⊚ q ⊚ p = p⊢ (q ⊚ p ⊚ q) ⊚ p ⊚ q ⊚ p ⊚ q = q ⊚ p ⊚ q rw [Category.assoc (q ⊚ p ⊚ q)]h.right𝒞:Type uinst✝:Category.{v, u} 𝒞C:𝒞D:𝒞p:C ⟶ Dq:D ⟶ Chpq:p ⊚ q ⊚ p = p⊢ ((q ⊚ p ⊚ q) ⊚ p) ⊚ q ⊚ p ⊚ q = q ⊚ p ⊚ q
    repeat rw [← Category.assoc p]h.right𝒞:Type uinst✝:Category.{v, u} 𝒞C:𝒞D:𝒞p:C ⟶ Dq:D ⟶ Chpq:p ⊚ q ⊚ p = p⊢ (q ⊚ p ⊚ q ⊚ p) ⊚ q ⊚ p ⊚ q = q ⊚ p ⊚ q
    rw [hpq]h.right𝒞:Type uinst✝:Category.{v, u} 𝒞C:𝒞D:𝒞p:C ⟶ Dq:D ⟶ Chpq:p ⊚ q ⊚ p = p⊢ (q ⊚ p) ⊚ q ⊚ p ⊚ q = q ⊚ p ⊚ q
    repeat rw [Category.assoc q]h.right𝒞:Type uinst✝:Category.{v, u} 𝒞C:𝒞D:𝒞p:C ⟶ Dq:D ⟶ Chpq:p ⊚ q ⊚ p = p⊢ ((q ⊚ p) ⊚ q ⊚ p) ⊚ q = (q ⊚ p) ⊚ q
    rw [← Category.assoc (q ⊚ p), hpq]All goals completed! 🐙

Problem 1* (p. 108)

Same question as Problem 1 at top of page, except that both sets A and B are required to be infinite sets.

Solution: Problem 1*

We use (non-finite) types here instead of infinite sets.

We give explicit types A and B and an explicit map f.

abbrev A := ℕ
abbrev B := ℝ

def f : A ⟶ B
  | 0 => 0
  | n + 1 => n + 1

Our candidate retraction for f is

noncomputable def r : B ⟶ A
  | r => ⌊abs r⌋₊

and we show that (a) is satisfied.

example : IsRetraction f := by⊢ IsRetraction f
  use rid⊢ autoParam (r ⊚ f = 𝟙 A) SplitMono.id._autoParam
  change r ⊚ f = 𝟙 Aid⊢ r ⊚ f = 𝟙 A
  funext xid.hx:A⊢ (r ⊚ f) x = 𝟙 A x
  dsimp [f, r]id.hx:A⊢ ⌊|match x with
      | 0 => 0
      | Nat.succ n => ↑n + 1|⌋₊ =
  x
  induction x with
  | zero =>id.h.zero⊢ ⌊|match Nat.zero with
      | 0 => 0
      | Nat.succ n => ↑n + 1|⌋₊ =
  Nat.zero rw [abs_zero, Nat.floor_zero]All goals completed! 🐙
  | succ n =>id.h.succn:ℕn_ih✝:⌊|match n with
      | 0 => 0
      | Nat.succ n => ↑n + 1|⌋₊ =
  n⊢ ⌊|match n.succ with
      | 0 => 0
      | Nat.succ n => ↑n + 1|⌋₊ =
  n.succ
      dsimpid.h.succn:ℕn_ih✝:⌊|match n with
      | 0 => 0
      | Nat.succ n => ↑n + 1|⌋₊ =
  n⊢ ⌊|↑n + 1|⌋₊ = n + 1
      norm_castid.h.succn:ℕn_ih✝:⌊|match n with
      | 0 => 0
      | Nat.succ n => ↑n + 1|⌋₊ =
  n⊢ ⌊↑(n + 1)⌋₊ = n + 1
      rw [Nat.floor_natCast]All goals completed! 🐙

We show that f also satisfies (b).

example : ¬(IsSection f) := by⊢ ¬IsSection f
  by_contra hh:IsSection f⊢ False
  obtain ⟨s, hs⟩ := hs:B ⟶ Ahs:f ⊚ s = 𝟙 B⊢ False
  have h_false := congrFun hs 0.5s:B ⟶ Ahs:f ⊚ s = 𝟙 Bh_false:(f ⊚ s) 0.5 = 𝟙 B 0.5 := congrFun hs 0.5⊢ False
  cases hx : s 0.5 with
  | zero =>zeros:B ⟶ Ahs:f ⊚ s = 𝟙 Bh_false:(f ⊚ s) 0.5 = 𝟙 B 0.5 := congrFun hs 0.5hx:s 0.5 = Nat.zero⊢ False
      rw [types_comp_apply, hx] at h_falsezeros:B ⟶ Ahs:f ⊚ s = 𝟙 Bh_false:f Nat.zero = 𝟙 B 0.5hx:s 0.5 = Nat.zero⊢ False
      dsimp [f] at h_falsezeros:B ⟶ Ahs:f ⊚ s = 𝟙 Bh_false:0 = 0.5hx:s 0.5 = Nat.zero⊢ False
      linarithAll goals completed! 🐙
  | succ n =>succs:B ⟶ Ahs:f ⊚ s = 𝟙 Bh_false:(f ⊚ s) 0.5 = 𝟙 B 0.5 := congrFun hs 0.5n:ℕhx:s 0.5 = n.succ⊢ False
      rw [types_comp_apply, hx] at h_falsesuccs:B ⟶ Ahs:f ⊚ s = 𝟙 Bn:ℕh_false:f n.succ = 𝟙 B 0.5hx:s 0.5 = n.succ⊢ False
      dsimp [f] at h_falsesuccs:B ⟶ Ahs:f ⊚ s = 𝟙 Bn:ℕh_false:↑n + 1 = 0.5hx:s 0.5 = n.succ⊢ False
      have h_ge_1 : (1 : B) ≤ n + 1 := by⊢ ¬IsSection f linarithAll goals completed! 🐙
      linarithAll goals completed! 🐙