Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.mem_smallGrothendieckTopology

∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  [inst : P.IsStableUnderBaseChange] [P.IsMultiplicative] [P.RespectsIso] [P.HasOfPostcompProperty P] (X : P.Over ⊤ S)
  (R : CategoryTheory.Sieve X),
  R ∈ (AlgebraicGeometry.Scheme.smallGrothendieckTopology P S) X ↔
    ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)), 𝒰.toPresieveOverProp h ≤ R.arrows

Defined in

Mathlib.AlgebraicGeometry.Sites.Small

Cited by

1 results in Mathlib

Foundations

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

Assumes

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