English
In a relative cell complex, equality of two morphisms φ1, φ2 from X2 to Z is determined by their equalities after composing with all cells γ.ι, given equality after precomposition with f.
Русский
В относительном клеточном комплексе равенство двух морфизмов определяется по совпадению после композиции с каждым γ.ι, если они согласованы с f.
LaTeX
$$$\forall Z,\; φ_1,φ_2:\ X_2\to Z,\; (f\circ φ_1 = f\circ φ_2) \Rightarrow (\forall γ:\, c.Cells,\; γ.ι\circ φ_1 = γ.ι\circ φ_2) \Rightarrow φ_1 = φ_2$$$
Lean4
theorem hom_ext {Z : C} {φ₁ φ₂ : Y ⟶ Z} (h₀ : f ≫ φ₁ = f ≫ φ₂) (h : ∀ (γ : Cells c), γ.ι ≫ φ₁ = γ.ι ≫ φ₂) : φ₁ = φ₂ :=
by
refine c.isColimit.hom_ext (fun j ↦ ?_)
dsimp
induction j using SuccOrder.limitRecOn with
| isMin j hj =>
obtain rfl := hj.eq_bot
simpa [← cancel_epi c.isoBot.inv] using h₀
| succ j hj hj' =>
apply (c.attachCells j hj).hom_ext
· simpa using hj'
· intro i
simpa only [Category.assoc, Cells.ι] using h ({ hj := hj, k := i, .. })
| isSuccLimit j hj hj' =>
exact (c.F.isColimitOfIsWellOrderContinuous j hj).hom_ext (fun ⟨k, hk⟩ ↦ by simpa using hj' k hk)
