Documentation

Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Site defined by a morphism property #

Given a multiplicative morphism property P that is stable under base change, we define the associated (pre)topology on the category of schemes, where coverings are given by jointly surjective families of morphisms satisfying P.

TODO #

source
def AlgebraicGeometry.Scheme.pretopology (P : CategoryTheory.MorphismProperty Scheme) [P.IsMultiplicative] [P.RespectsIso] [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] :
CategoryTheory.Pretopology Scheme

The pretopology on the category of schemes defined by covering families where the components satisfy P.

The coverings are defined via existence of a P-cover. This is convenient in practice, as one directly has the cover available. For a pretopology generating the same Grothendieck topology, see AlgebraicGeometry.Scheme.grothendieckTopology_eq_inf.

Equations
    Instances For
      source
      @[reducible, inline]
      abbrev AlgebraicGeometry.Scheme.grothendieckTopology (P : CategoryTheory.MorphismProperty Scheme) [P.IsMultiplicative] [P.RespectsIso] [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] :
      CategoryTheory.GrothendieckTopology Scheme

      The Grothendieck topology on the category of schemes induced by the pretopology defined by P-covers.

      Equations
        Instances For
          source
          def AlgebraicGeometry.Scheme.surjectiveFamiliesPretopology [IsJointlySurjectivePreserving ⊤] :
          CategoryTheory.Pretopology Scheme

          The pretopology on the category of schemes defined by jointly surjective families.

          Note: The assumption IsJointlySurjectivePreserving ⊤ is mathematically unneeded, and only here to reduce imports. To satisfy it, use AlgebraicGeometry.Scheme.isJointlySurjectivePreserving.

          Equations
            Instances For
              source
              theorem AlgebraicGeometry.Scheme.pretopology_le_inf (P : CategoryTheory.MorphismProperty Scheme) [P.IsMultiplicative] [P.RespectsIso] [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] [IsJointlySurjectivePreserving ⊤] :
              pretopology P ≤ surjectiveFamiliesPretopology ⊓ P.pretopology
              source
              theorem AlgebraicGeometry.Scheme.grothendieckTopology_eq_inf (P : CategoryTheory.MorphismProperty Scheme) [P.IsMultiplicative] [P.RespectsIso] [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] [IsJointlySurjectivePreserving ⊤] :
              grothendieckTopology P = CategoryTheory.Pretopology.toGrothendieck Scheme (surjectiveFamiliesPretopology ⊓ P.pretopology)

              The Grothendieck topology defined by P-covers agrees with the Grothendieck topology induced by the intersection of the pretopology of surjective families with the pretopology defined by P.

              Note: Because of size issues, this does not hold on the level of pretopologies: A presieve in the intersection can have up to Type (u + 1) many components, while in the definition of AlgebraicGeometry.Scheme.pretopology we only allow Type u many components.

              source
              theorem AlgebraicGeometry.Scheme.pretopology_cover {P : CategoryTheory.MorphismProperty Scheme} [P.IsMultiplicative] [P.RespectsIso] [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {Y : Scheme} (𝒰 : Cover P Y) :
              (pretopology P).coverings Y (CategoryTheory.Presieve.ofArrows 𝒰.obj 𝒰.map)
              source
              theorem AlgebraicGeometry.Scheme.grothendieckTopology_cover {P : CategoryTheory.MorphismProperty Scheme} [P.IsMultiplicative] [P.RespectsIso] [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {X : Scheme} (𝒰 : Cover P X) :
              (grothendieckTopology P) X (CategoryTheory.Sieve.generate (CategoryTheory.Presieve.ofArrows 𝒰.obj 𝒰.map))
              source
              theorem AlgebraicGeometry.Scheme.pretopology_le_pretopology {P : CategoryTheory.MorphismProperty Scheme} [P.IsMultiplicative] [P.RespectsIso] [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {Q : CategoryTheory.MorphismProperty Scheme} [Q.IsMultiplicative] [Q.RespectsIso] [Q.IsStableUnderBaseChange] [IsJointlySurjectivePreserving Q] (hPQ : P ≤ Q) :
              pretopology P ≤ pretopology Q
              source
              theorem AlgebraicGeometry.Scheme.grothendieckTopology_le_grothendieckTopology {P : CategoryTheory.MorphismProperty Scheme} [P.IsMultiplicative] [P.RespectsIso] [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] {Q : CategoryTheory.MorphismProperty Scheme} [Q.IsMultiplicative] [Q.RespectsIso] [Q.IsStableUnderBaseChange] [IsJointlySurjectivePreserving Q] (hPQ : P ≤ Q) :
              grothendieckTopology P ≤ grothendieckTopology Q