English
Pseudoequality is transitive: if a is pseudoequal to b and b to c, then a is pseudoequal to c.
Русский
Псевдоэквивалентность транзитивна: если a псевдоэквивалентно b и b псевдоэквивалентно c, то a псевдоэквивалентно c.
LaTeX
$$$\\forall a,b,c:\\; \\mathrm{PseudoEqual}(P)(a,b) \\land \\mathrm{PseudoEqual}(P)(b,c) \\Rightarrow \\mathrm{PseudoEqual}(P)(a,c)$$$
Lean4
/-- Pseudoequality is transitive: Just take the pullback. The pullback morphisms will
be epimorphisms since in an abelian category, pullbacks of epimorphisms are epimorphisms. -/
theorem pseudoEqual_trans {P : C} : Transitive (PseudoEqual P) :=
by
intro f g h ⟨R, p, q, ep, Eq, comm⟩ ⟨R', p', q', ep', eq', comm'⟩
refine ⟨pullback q p', pullback.fst _ _ ≫ p, pullback.snd _ _ ≫ q', epi_comp _ _, epi_comp _ _, ?_⟩
rw [Category.assoc, comm, ← Category.assoc, pullback.condition, Category.assoc, comm', Category.assoc]
