English
Equality of small Grothendieck topology with the small pretopology via appropriate base-change properties.
Русский
Эквивалентность малой топологии Гротендика и малой препотопологии через базопеременные свойства.
LaTeX
$$$S.smallGrothendieckTopologyOfLE hPQ = (S.smallPretopology P Q).toGrothendieck$$$
Lean4
theorem smallGrothendieckTopologyOfLE_eq_toGrothendieck_smallPretopology (hPQ : P ≤ Q) :
S.smallGrothendieckTopologyOfLE hPQ = (S.smallPretopology P Q).toGrothendieck :=
by
ext X R
simp only [Pretopology.mem_toGrothendieck, Functor.mem_inducedTopology_sieves_iff, MorphismProperty.Comma.forget_obj,
mem_overGrothendieckTopology]
constructor
· intro ⟨𝒰, h, le⟩
have hj (j : 𝒰.I₀) : Q (𝒰.X j ↘ S) := by
rw [← comp_over (𝒰.f j)]
exact Q.comp_mem _ _ (hPQ _ <| 𝒰.map_prop _) X.prop
refine ⟨𝒰.toPresieveOverProp hj, ?_, ?_⟩
· use 𝒰, h, hj
· rintro - - ⟨i⟩
let fi : (𝒰.X i).asOverProp S (hj i) ⟶ X := (𝒰.f i).asOverProp S
have : R.functorPushforward _ ((MorphismProperty.Over.forget Q ⊤ S).map fi) := le _ ⟨i⟩
rwa [Sieve.functorPushforward_apply, Sieve.mem_functorPushforward_iff_of_full_of_faithful] at this
· rintro ⟨T, ⟨𝒰, h, p, rfl⟩, le⟩
use 𝒰, h
rintro - - ⟨i⟩
exact ⟨(𝒰.X i).asOverProp S (p i), (𝒰.f i).asOverProp S, 𝟙 _, le _ ⟨i⟩, rfl⟩
