English
Under HasPairwisePullbacks, the analogous compatibility criterion holds for Presieve P and R: an element x in FirstObj P R is compatible iff firstMap P R x = secondMap P R x.
Русский
При наличии парных обратных диаграмм справедливое условие совместимости сохраняется для Presieve P и R: элемент x из FirstObj P R совместим тогда и только когда firstMap P R x = secondMap P R x.
LaTeX
$$$\\forall x:\\, FirstObj P R,\\ ((\\text{firstObjEqFamily } P R).hom x).Compatible \\iff (\\text{firstMap } P R x = \\text{secondMap } P R x)$$$
Lean4
/-- The family of elements given by `x : FirstObj P S` is compatible iff `firstMap` and `secondMap`
map it to the same point.
-/
theorem compatible_iff (x : FirstObj P R) :
((firstObjEqFamily P R).hom x).Compatible ↔ firstMap P R x = secondMap P R x :=
by
rw [Presieve.pullbackCompatible_iff]
constructor
· intro t
apply Limits.Types.limit_ext
rintro ⟨⟨Y, f, hf⟩, Z, g, hg⟩
simpa [firstMap, secondMap] using t hf hg
· intro t Y Z f g hf hg
rw [Types.limit_ext_iff'] at t
simpa [firstMap, secondMap] using t ⟨⟨⟨Y, f, hf⟩, Z, g, hg⟩⟩
