English
The key identity: σ ≫ f = (Limits.prod.map f f) ≫ σ for any f.
Русский
Ключевое тождество: σ ≫ f = Limits.prod.map f f ≫ σ для любого f.
LaTeX
$$$\\forall f,\\ \\sigma \\;\\circ\\; f = (\\mathrm{Limits.prod.map}\\ f\\ f) \\circ \\sigma$$$
Lean4
/-- This is the key identity satisfied by `σ`. -/
theorem σ_comp {X Y : C} (f : X ⟶ Y) : σ ≫ f = Limits.prod.map f f ≫ σ :=
by
obtain ⟨g, hg⟩ :=
CokernelCofork.IsColimit.desc' isColimitσ (Limits.prod.map f f ≫ σ) (by rw [prod.diag_map_assoc, diag_σ, comp_zero])
suffices hfg : f = g by rw [← hg, Cofork.π_ofπ, hfg]
calc
f = f ≫ prod.lift (𝟙 Y) 0 ≫ σ := by rw [lift_σ, Category.comp_id]
_ = prod.lift (𝟙 X) 0 ≫ Limits.prod.map f f ≫ σ := by rw [lift_map_assoc]
_ = prod.lift (𝟙 X) 0 ≫ σ ≫ g := by rw [← hg, CokernelCofork.π_ofπ]
_ = g := by rw [← Category.assoc, lift_σ, Category.id_comp]
