English
Under Faithful F, the hom-ext principle holds for arrows in hf.pullback g, expressed via the ext lemma for morphisms over g.
Русский
При Faithful F принцип гом-экстенсиональности справедлив для стрел в hf.pullback g, выражаемый через лемму экст для морфизмов над g.
LaTeX
$$$$\\text{(Over version) } \\text{hom\_ext}: \\forall c\\; a,b:\\; c \\to hf.pullback g,\\; (F.map a \\to hf.fst g) = (F.map b \\to hf.fst g) \\Rightarrow (a \\to hf.snd g) = (b \\to hf.snd g) \\Rightarrow a=b.$$$$
Lean4
/-- Two morphisms `a b : c ⟶ hf.pullback g` are equal if
* Their compositions (in `C`) with `hf.snd g : hf.pullback ⟶ X` are equal.
* The compositions of `F.map a` and `F.map b` with `hf.fst g` are equal. -/
@[ext 100]
theorem hom_ext [Faithful F] {c : C} {a b : c ⟶ hf.pullback g} (h₁ : F.map a ≫ hf.fst g = F.map b ≫ hf.fst g)
(h₂ : a ≫ hf.snd g = b ≫ hf.snd g) : a = b :=
F.map_injective <| PullbackCone.IsLimit.hom_ext (hf.isPullback g).isLimit h₁ (by simpa using F.congr_map h₂)
