English
Membership criterion for small Grothendieck topology via a covering sieve.
Русский
Критерий принадлежности к малой топологии Гротендика через покрывающее сито.
LaTeX
$$$R \\in S.smallGrothendieckTopology P X \\iff \\exists 𝒰, 𝒰.Over S, 𝒰.toPresieveOver \\le R.arrows$$$
Lean4
theorem mem_toGrothendieck_smallPretopology (X : Q.Over ⊤ S) (R : Sieve X) :
R ∈ (S.smallPretopology P Q).toGrothendieck X ↔
∀ x : X.left, ∃ (Y : Q.Over ⊤ S) (f : Y ⟶ X) (y : Y.left), R f ∧ P f.left ∧ f.left.base y = x :=
by
rw [Pretopology.mem_toGrothendieck]
refine ⟨?_, fun h ↦ ?_⟩
· rintro ⟨T, ⟨𝒰, h, p, rfl⟩, hle⟩
intro x
obtain ⟨y, hy⟩ := 𝒰.covers x
refine ⟨(𝒰.X (𝒰.idx x)).asOverProp S (p _), (𝒰.f (𝒰.idx x)).asOverProp S, y, hle _ ?_, 𝒰.map_prop _, hy⟩
use 𝒰.idx x
· choose Y f y hf hP hy using h
let 𝒰 : X.left.Cover (precoverage P) :=
{ I₀ := X.left, X := fun i ↦ (Y i).left
f := fun i ↦ (f i).left
mem₀ := by
rw [presieve₀_mem_precoverage_iff]
refine ⟨fun x ↦ ⟨x, y x, hy x⟩, hP⟩ }
letI : 𝒰.Over S :=
{ over := fun i ↦ inferInstance
isOver_map := fun i ↦ inferInstance }
refine ⟨𝒰.toPresieveOverProp fun i ↦ MorphismProperty.Comma.prop _, ?_, ?_⟩
· use 𝒰, inferInstance, fun i ↦ MorphismProperty.Comma.prop _
· rintro - - ⟨i⟩
exact hf i
