Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.grothendieckTopology_eq_inf

∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative],
  AlgebraicGeometry.Scheme.grothendieckTopology P =
    (AlgebraicGeometry.Scheme.jointlySurjectivePretopology ⊓ P.pretopology).toGrothendieck

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.

Defined in

Mathlib.AlgebraicGeometry.Sites.Pretopology

Cited by

0 results in Mathlib

Foundations

Depth 196 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.MorphismProperty.IsStableUnderBaseChangeCategoryTheory.MorphismProperty.IsMultiplicative