English
Let W be an object and g,h: image f → W be two arrows. If factorThroughImage f ≫ g = factorThroughImage f ≫ h, then g = h.
Русский
Пусть W — произвольный объект, а g,h: image f → W две стрелки. Если factorThruImage f ≫ g = factorThruImage f ≫ h, то g = h.
LaTeX
$$$ (\\mathrm{factorThruImage}(f)) \\; \\circ \\; g = (\\mathrm{factorThruImage}(f)) \\; \\circ \\; h \\implies g = h $$$
Lean4
@[ext (iff := false)]
theorem ext [HasImage f] {W : C} {g h : image f ⟶ W} [HasLimit (parallelPair g h)]
(w : factorThruImage f ≫ g = factorThruImage f ≫ h) : g = h :=
by
let q := equalizer.ι g h
let e' := equalizer.lift _ w
let F' : MonoFactorisation f :=
{ I := equalizer g h
m := q ≫ image.ι f
m_mono := mono_comp _ _
e := e' }
let v := image.lift F'
have t₀ : v ≫ q ≫ image.ι f = image.ι f := image.lift_fac F'
have t : v ≫ q = 𝟙 (image f) :=
(cancel_mono_id (image.ι f)).1
(by
convert t₀ using 1
rw [Category.assoc])
-- The proof from wikipedia next proves `q ≫ v = 𝟙 _`,
-- and concludes that `equalizer g h ≅ image f`,
-- but this isn't necessary.
calc
g = 𝟙 (image f) ≫ g := by rw [Category.id_comp]
_ = v ≫ q ≫ g := by rw [← t, Category.assoc]
_ = v ≫ q ≫ h := by rw [equalizer.condition g h]
_ = 𝟙 (image f) ≫ h := by rw [← Category.assoc, t]
_ = h := by rw [Category.id_comp]
