English
If pullback along f with g yields a mono map, the pullback projections realize a universal property on pseudoelements.
Русский
Если проекции pullback along f и g образуют моно, они реализуют универсальное свойство на псевдоэлементах.
LaTeX
$$$\\text{pullback projections are mono} \\Rightarrow \\text{pseudoelement pullback is well-behaved}$$$
Lean4
/-- If two pseudoelements `x` and `y` have the same image under some morphism `f`, then we can form
their "difference" `z`. This pseudoelement has the properties that `f z = 0` and for all
morphisms `g`, if `g y = 0` then `g z = g x`. -/
theorem sub_of_eq_image {P Q : C} (f : P ⟶ Q) (x y : P) :
f x = f y → ∃ z, f z = 0 ∧ ∀ (R : C) (g : P ⟶ R), (g : P ⟶ R) y = 0 → g z = g x :=
Quotient.inductionOn₂ x y fun a a' h =>
match Quotient.exact h with
| ⟨R, p, q, ep, _, comm⟩ =>
let a'' : R ⟶ P := (p ≫ a.hom : R ⟶ P) - (q ≫ a'.hom : R ⟶ P)
⟨a'',
⟨show ⟦(a'' ≫ f : Over Q)⟧ = ⟦↑(0 : Q ⟶ Q)⟧ by
dsimp at comm
simp [a'', sub_eq_zero.2 comm],
fun Z g hh => by
obtain ⟨X, p', q', ep', _, comm'⟩ := Quotient.exact hh
have : a'.hom ≫ g = 0 := by
apply (epi_iff_cancel_zero _).1 ep' _ (a'.hom ≫ g)
simpa using comm'
apply Quotient.sound
change app g (a'' : Over P) ≈ app g a
exact ⟨R, 𝟙 R, p, inferInstance, ep, by simp [a'', sub_eq_add_neg, this]⟩⟩⟩
