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

• Define the small site on Over P Q X.

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

• One or more equations did not get rendered due to their size.

@[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

• AlgebraicGeometry.Scheme.grothendieckTopology P = CategoryTheory.Pretopology.toGrothendieck AlgebraicGeometry.Scheme (AlgebraicGeometry.Scheme.pretopology P)

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

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.pretopology_le_inf (P : CategoryTheory.MorphismProperty Scheme) [P.IsMultiplicative] [P.RespectsIso] [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] [IsJointlySurjectivePreserving ⊤] : pretopology P ≤ surjectiveFamiliesPretopology ⊓ P.pretopology

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.

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)

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))

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

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