Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.mem_overGrothendieckTopology

∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {S : AlgebraicGeometry.Scheme}
  [inst : P.IsStableUnderBaseChange] [P.IsMultiplicative] [P.RespectsIso] (X : CategoryTheory.Over S)
  (R : CategoryTheory.Sieve X),
  R ∈ (AlgebraicGeometry.Scheme.overGrothendieckTopology P S) X ↔ ∃ 𝒰 x, 𝒰.toPresieveOver ≤ R.arrows

Defined in

Mathlib.AlgebraicGeometry.Sites.Small

Cited by

1 results in Mathlib

Foundations

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

Assumes

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