English
If two pseudoelements map to the same image under a morphism, there exists a pseudoelement whose image is zero and which is mapped identically across postcompositions.
Русский
Если два псевдоэлемента отображаются в один образ под морфизмом, существует псевдоэлемент, образ которого ноль и который сохраняется после посткомпозиций.
LaTeX
$$$\\forall f\\; x,y:\\; f(x)=f(y) \\Rightarrow \\exists z, f(z)=0 \\land \\forall g, g(y)=0 \\Rightarrow g(z)=g(x)$$$
Lean4
/-- If `f : P ⟶ R` and `g : Q ⟶ R` are morphisms and `p : P` and `q : Q` are pseudoelements such
that `f p = g q`, then there is some `s : pullback f g` such that `fst s = p` and `snd s = q`.
Remark: Borceux claims that `s` is unique, but this is false. See
`Counterexamples/Pseudoelement.lean` for details. -/
theorem pseudo_pullback {P Q R : C} {f : P ⟶ R} {g : Q ⟶ R} {p : P} {q : Q} :
f p = g q → ∃ s, pullback.fst f g s = p ∧ pullback.snd f g s = q :=
Quotient.inductionOn₂ p q fun x y h =>
by
obtain ⟨Z, a, b, ea, eb, comm⟩ := Quotient.exact h
obtain ⟨l, hl₁, hl₂⟩ :=
@pullback.lift' _ _ _ _ _ _ f g _ (a ≫ x.hom) (b ≫ y.hom)
(by
simp only [Category.assoc]
exact comm)
exact
⟨l,
⟨Quotient.sound ⟨Z, 𝟙 Z, a, inferInstance, ea, by rwa [Category.id_comp]⟩,
Quotient.sound ⟨Z, 𝟙 Z, b, inferInstance, eb, by rwa [Category.id_comp]⟩⟩⟩
