grothendieckTopology_eq_inf — Mathlib

English

The Grothendieck topology defined by P-covers equals the Grothendieck topology obtained from the infimum of jointlySurjectivePretopology and P.pretopology.

Русский

Топология Гротендлик, определяемая по покрытиям P, равна топологии Гротендлик, полученной из инфимума jointlySurjectivePretopology и P.pretopology.

LaTeX

$$$grothendieckTopology P = (jointlySurjectivePretopology \\cap P.pretopology).toGrothendieck$$$

Lean4

/-- The Grothendieck topology defined by `P`-covers agrees with the Grothendieck
topology induced by the intersection of the pretopology of surjective families with
the pretopology defined by `P`.
-/
theorem grothendieckTopology_eq_inf :
    grothendieckTopology P = (jointlySurjectivePretopology ⊓ P.pretopology).toGrothendieck := by
  rw [grothendieckTopology, pretopology_eq_inf]

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