grothendieckTopology — Mathlib

English

The Grothendieck topology on X.AffineZariskiSite is defined as the topology induced from the topology on X.Opens via the toOpensFunctor.

Русский

Гротендикова топология на X.AffineZariskiSite определяется как топология, индуцированная от топологии на X.Opens через toOpensFunctor.

LaTeX

$$$\operatorname{grothendieckTopology}_X = (toOpensFunctor X).\text{inducedTopology}(Opens.grothendieckTopology X)$$$

Lean4

/-- The Grothendieck topology on `X.AffineZariskiSite` induced from the topology on `X.Opens`.
Also see `mem_grothendieckTopology_iff_sectionsOfPresieve`. -/
def grothendieckTopology : GrothendieckTopology X.AffineZariskiSite :=
  (toOpensFunctor X).inducedTopology (Opens.grothendieckTopology X)

Похожие утверждения