English
A family of elements given by an arrow-indexed object is compatible iff all corresponding pullback projections match under the product isomorphism.
Русский
Семейство элементов, заданное стрелочным индексированием, совместимо тогда и только тогда, когда все соответствующие проекции вытяжки совпадают под произведением.
LaTeX
$$Compat := (Arrows.Compatible P π (productIso _).hom x) ↔ firstMap P X π x = secondMap P X π x$$
Lean4
/-- Version of `CategoryTheory.Equalizer.Presieve.Arrows.compatible_iff` for a small
indexing type. -/
theorem compatible_iff_of_small (x : FirstObj P X) :
(Arrows.Compatible P π ((equivShrink _).symm ((Types.Small.productIso _).hom x))) ↔
firstMap P X π x = secondMap P X π x :=
by
rw [Arrows.pullbackCompatible_iff]
refine ⟨fun t ↦ ?_, fun t i j ↦ ?_⟩
· ext ij
simpa [firstMap, secondMap] using t ij.1 ij.2
· apply_fun Pi.π (fun (ij : I × I) ↦ P.obj (op (pullback (π ij.1) (π ij.2)))) ⟨i, j⟩ at t
simpa [firstMap, secondMap] using t
