English
For any x in FirstObj P S.arrows, the element obtained by applying firstObjEqFamily to x is compatible if and only if the two maps firstMap P S x and secondMap P S x agree.
Русский
Пусть x — элемент из FirstObj P S.arrows. Тогда образ x через family, полученный с помощью firstObjEqFamily, совместим тогда и только тогда, когда firstMap P S x = secondMap P S x.
LaTeX
$$$((\\text{firstObjEqFamily } P S.arrows).hom x).Compatible \\iff (\\text{firstMap } P S x = \\text{secondMap } P S 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 S.arrows) :
((firstObjEqFamily P S.arrows).hom x).Compatible ↔ firstMap P S x = secondMap P S x :=
by
rw [Presieve.compatible_iff_sieveCompatible]
constructor
· intro t
apply SecondObj.ext
intro Y Z g f hf
simpa [firstMap, secondMap] using t _ g hf
· intro t Y Z f g hf
rw [Types.limit_ext_iff'] at t
simpa [firstMap, secondMap] using t ⟨⟨Y, Z, g, f, hf⟩⟩
