English
Extensionality for the first object in arrows setup: equality reduces to componentwise equality of projections.
Русский
Расширение для первого объекта в схеме стрел: равенство сводится к покомпонентной эквивалентности проекций.
LaTeX
$$$\forall i,\; (P.map(π_i).op)\!\text{ext}$$$
Lean4
/-- The family of elements given by `x : FirstObj P S` is compatible iff `firstMap` and `secondMap`
map it to the same point.
See `CategoryTheory.Equalizer.Presieve.Arrows.compatible_iff_of_small` for a version with
less universe assumptions.
-/
theorem compatible_iff {I : Type w} (X : I → C) (π : (i : I) → X i ⟶ B) [(Presieve.ofArrows X π).HasPairwisePullbacks]
(x : FirstObj P X) : (Arrows.Compatible P π ((Types.productIso _).hom x)) ↔ firstMap P X π x = secondMap P X π x :=
by
rw [Arrows.pullbackCompatible_iff]
constructor
· intro t
ext ij
simpa [firstMap, secondMap] using t ij.1 ij.2
· intro t i j
apply_fun Pi.π (fun (ij : I × I) ↦ P.obj (op (pullback (π ij.1) (π ij.2)))) ⟨i, j⟩ at t
simpa [firstMap, secondMap] using t
