English
The generated pullback arrows of a presieve commute with pullback along f, giving a stable pullback.
Русский
Генерируемые стрелки обратного сита совместимы с обратным по f.
LaTeX
$$$ \\text{generate}(\\text{Presieve}.pullbackArrows f R) = \\text{pullback} f (\\text{generate } R) $$$
Lean4
theorem pullbackArrows_comm {X Y : C} (f : Y ⟶ X) (R : Presieve X) [R.HasPullbacks f] :
Sieve.generate (R.pullbackArrows f) = (Sieve.generate R).pullback f :=
by
ext W g
constructor
· rintro ⟨_, h, k, ⟨W, g, hg⟩, rfl⟩
have := R.hasPullback f hg
rw [Sieve.pullback_apply, assoc, ← pullback.condition, ← assoc]
exact Sieve.downward_closed _ (by exact Sieve.le_generate R W hg) (h ≫ pullback.fst g f)
· rintro ⟨W, h, k, hk, comm⟩
have := R.hasPullback f hk
exact ⟨_, _, _, Presieve.pullbackArrows.mk _ _ hk, pullback.lift_snd _ _ comm⟩
