Documentation

Mathlib.AlgebraicGeometry.Sites.Affine

Small affine site induced by a morphism property #

Let P be a morphism property of schemes and S be a scheme. In this file we study the small affine P-site of S: its objects are rings R with a structure morphism Spec R ⟶ S that satisfies P.

We don't make a separate definition for this site, but use CategoryTheory.MorphismProperty.CostructuredArrow P ⊤ Scheme.Spec S.

Under suitable assumptions on P, the lemmas here can be used to show that the small affine P-site has the same category of sheaves as the general small P-site. If P implies finitely generated, the small affine P-site is essentially small, so in particular this can be used to show that the P-site admits sheafification. For an example, see the file Mathlib.AlgebraicGeometry.Sites.AffineEtale.

source
noncomputable def AlgebraicGeometry.Scheme.affineOverMk {S : Scheme} {P : CategoryTheory.MorphismProperty Scheme} {R : CommRingCat} (f : Spec R ⟶ S) (hf : P f) :
P.CostructuredArrow ⊤ Scheme.Spec S

Construct an object of affine P-schemes over S by giving a morphism Spec R ⟶ S.

Equations
Instances For
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.affineOverMk_hom {S : Scheme} {P : CategoryTheory.MorphismProperty Scheme} {R : CommRingCat} (f : Spec R ⟶ S) (hf : P f) :
    (affineOverMk f hf).hom = f
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.affineOverMk_left {S : Scheme} {P : CategoryTheory.MorphismProperty Scheme} {R : CommRingCat} (f : Spec R ⟶ S) (hf : P f) :
    (affineOverMk f hf).left = Opposite.op R
    source
    instance AlgebraicGeometry.Scheme.isCoverDense_toOver_Spec {S : Scheme} (P : CategoryTheory.MorphismProperty Scheme) [P.IsMultiplicative] [IsZariskiLocalAtSource P] [P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P] :
    (CategoryTheory.MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S).IsCoverDense (smallGrothendieckTopology P)

    The Spec functor from affine P-schemes over S to P-schemes over S is dense if P is local at the source.

    source
    instance AlgebraicGeometry.Scheme.isOneHypercoverDense_toOver_Spec {S : Scheme} (P : CategoryTheory.MorphismProperty Scheme) [P.IsMultiplicative] [IsZariskiLocalAtSource P] [P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P] :
    (CategoryTheory.MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S).IsOneHypercoverDense ((CategoryTheory.MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S).inducedTopology (smallGrothendieckTopology P)) (smallGrothendieckTopology P)