Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.overGrothendieckTopology_eq_toGrothendieck_overPretopology

∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) (S : AlgebraicGeometry.Scheme)
  [inst : P.IsStableUnderBaseChange] [inst_1 : P.IsMultiplicative] [inst_2 : P.RespectsIso],
  AlgebraicGeometry.Scheme.overGrothendieckTopology P S = (AlgebraicGeometry.Scheme.overPretopology P S).toGrothendieck

Defined in

Mathlib.AlgebraicGeometry.Sites.Small

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.MorphismProperty.IsStableUnderBaseChangeCategoryTheory.MorphismProperty.IsMultiplicativeCategoryTheory.MorphismProperty.RespectsIso