English
The Grothendieck topology associated to a space is obtained from the pretopology by a canonical equivalence.
Русский
Гротендикова топология, связанная с пространством, получается из препотопологии каноническим эквивалентом.
LaTeX
$$$(Opens.grothendieckTopology T).toPretopology = Opens.pretopology T$$$
Lean4
/-- The Grothendieck pretopology associated to a topological space. -/
def pretopology : Pretopology (Opens T)
where
coverings X R := ∀ x ∈ X, ∃ (U : _) (f : U ⟶ X), R f ∧ x ∈ U
has_isos _ _ f _ _ hx := ⟨_, _, Presieve.singleton_self _, (inv f).le hx⟩
pullbacks X Y f S hS x
hx := by
rcases hS _ (f.le hx) with ⟨U, g, hg, hU⟩
refine ⟨_, _, Presieve.pullbackArrows.mk _ _ hg, ?_⟩
have : U ⊓ Y ≤ pullback g f := leOfHom (pullback.lift (homOfLE inf_le_left) (homOfLE inf_le_right) rfl)
apply this ⟨hU, hx⟩
transitive X S Ti hS hTi x
hx := by
rcases hS x hx with ⟨U, f, hf, hU⟩
rcases hTi f hf x hU with ⟨V, g, hg, hV⟩
exact ⟨_, _, ⟨_, g, f, hf, hg, rfl⟩, hV⟩
