Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.mem_toGrothendieck_smallPretopology

∀ {P Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  [inst : P.IsStableUnderBaseChange] [inst_1 : P.IsMultiplicative] [inst_2 : P.RespectsIso]
  [inst_3 : Q.IsStableUnderComposition] [inst_4 : Q.IsStableUnderBaseChange] [inst_5 : Q.HasOfPostcompProperty Q]
  (X : Q.Over ⊤ S) (R : CategoryTheory.Sieve X),
  R ∈ (AlgebraicGeometry.Scheme.smallPretopology P Q).toGrothendieck X ↔
    ∀ (x : ↥X.left), ∃ Y f y, R.arrows f ∧ P f.left ∧ f.left y = x

Defined in

Mathlib.AlgebraicGeometry.Sites.Small

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.MorphismProperty.IsStableUnderBaseChangeCategoryTheory.MorphismProperty.IsMultiplicativeCategoryTheory.MorphismProperty.RespectsIsoCategoryTheory.MorphismProperty.IsStableUnderCompositionCategoryTheory.MorphismProperty.IsStableUnderBaseChangeCategoryTheory.MorphismProperty.HasOfPostcompProperty