Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.smallPretopology

(P Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) →
  {S : AlgebraicGeometry.Scheme} →
    [P.IsStableUnderBaseChange] →
      [P.IsMultiplicative] →
        [P.RespectsIso] →
          [inst : Q.IsStableUnderComposition] →
            [inst_1 : Q.IsStableUnderBaseChange] →
              [inst_2 : Q.HasOfPostcompProperty Q] → CategoryTheory.Pretopology (Q.Over ⊤ S)

The pretopology defined on the subcategory of S-schemes satisfying Q where coverings are given by P-coverings in S-schemes satisfying Q. The most common case is P = Q. In this case, this is simply surjective families in S-schemes with P.

Defined in

Mathlib.AlgebraicGeometry.Sites.Small

Cited by

5 results in Mathlib

Foundations

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

Assumes

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