Lean4
/-- The pretopology defined on the subcategory of `S`-schemes satisfying `Q` where coverings
are given by `P`-coverings in `S`-schemes satisfying `Q`.
The most common case is `P = Q`. In this case, this is simply surjective families
in `S`-schemes with `P`. -/
def smallPretopology : Pretopology (Q.Over ⊤ S)
where
coverings Y
R :=
∃ (𝒰 : Cover.{u} (precoverage P) Y.left) (_ : 𝒰.Over S) (h : ∀ j : 𝒰.I₀, Q (𝒰.X j ↘ S)), R = 𝒰.toPresieveOverProp h
has_isos {X Y} f := ⟨coverOfIsIso f.left, inferInstance, fun _ ↦ Y.prop, (Presieve.ofArrows_pUnit _).symm⟩
pullbacks := by
rintro Y X f _ ⟨𝒰, h, p, rfl⟩
refine ⟨𝒰.pullbackCoverOverProp' S f.left (Q := Q) Y.prop X.prop p, inferInstance, ?_, ?_⟩
· intro j
apply MorphismProperty.Comma.prop
·
exact
(Presieve.ofArrows_pullback f (fun i ↦ ⟨(𝒰.X i).asOver S, p i⟩)
(fun i ↦ ⟨(𝒰.f i).asOver S, trivial, trivial⟩)).symm
transitive := by
rintro X _ T ⟨𝒰, h, p, rfl⟩ H
choose V h pV hV using H
let 𝒱j (j : 𝒰.I₀) : (Cover (precoverage P) ((𝒰.X j).asOverProp S (p j)).left) := V ((𝒰.f j).asOverProp S) ⟨j⟩
refine ⟨𝒰.bind (fun j ↦ 𝒱j j), inferInstance, fun j ↦ pV _ _ _, ?_⟩
convert
Presieve.ofArrows_bind _ (fun j ↦ ((𝒰.f j).asOverProp S)) _ (fun Y f H j ↦ ((V f H).X j).asOverProp S (pV _ _ _))
(fun Y f H j ↦ ((V f H).f j).asOverProp S)
apply hV
