English
Let J be a pretopology on a category C that is stable under base change. If R is a presieve on an object Y with R ∈ J Y and the pullbacks along a morphism f : X → Y exist for every arrow in R, then the pullback arrows R.pullbackArrows f form a covering of X, i.e. R.pullbackArrows f ∈ J X.
Русский
Пусть J является предпаттерном на категорию C, устойчивым по основанию. Если R — пресив на объекте Y и R ∈ J Y, и для каждого стрелы из R существуют пуллбэки по стрелке f: X → Y, тогда стрелы-пуллбэки R.pullbackArrows f образуют покрытие над X, то есть R.pullbackArrows f ∈ J X.
LaTeX
$$$\forall {C} [\text{Cat}(C)], J, X, Y, f, R.\; J \text{ стабильен по основанию}
\Rightarrow (R \in J(Y) \; \wedge\; R \text{HasPullbacks along } f) \Rightarrow R.pullbackArrows(f) \in J(X).$$$
Lean4
theorem pullbackArrows_mem {J : Precoverage C} [IsStableUnderBaseChange.{max u v} J] {X Y : C} (f : X ⟶ Y)
{R : Presieve Y} (hR : R ∈ J Y) [R.HasPullbacks f] : R.pullbackArrows f ∈ J X :=
by
obtain ⟨ι, Z, g, rfl⟩ := R.exists_eq_ofArrows
have (i : ι) : Limits.HasPullback (g i) f := Presieve.hasPullback f (Presieve.ofArrows.mk i)
rw [← Presieve.ofArrows_pullback]
exact mem_coverings_of_isPullback _ hR _ _ _ fun i ↦ (IsPullback.of_hasPullback _ _).flip
