Grothendieck topology 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.

Implementation details

The pretopology is obtained from the precoverage AlgebraicGeometry.Scheme.precoverage defined in Mathlib.AlgebraicGeometry.Sites.MorphismProperty. The definition is postponed to this file, because the former does not have HasPullbacks Scheme.

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

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

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.grothendieckTopology (P : CategoryTheory.MorphismProperty Scheme) : CategoryTheory.GrothendieckTopology Scheme

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

instance AlgebraicGeometry.Scheme.instIsStableUnderBaseChangeJointlySurjectivePrecoverage : jointlySurjectivePrecoverage.IsStableUnderBaseChange

def AlgebraicGeometry.Scheme.jointlySurjectivePretopology : CategoryTheory.Pretopology Scheme

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

theorem AlgebraicGeometry.Scheme.Cover.mem_grothendieckTopology {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) : CategoryTheory.Sieve.ofArrows 𝒰.X 𝒰.f ∈ (grothendieckTopology P) X

theorem AlgebraicGeometry.Scheme.bot_mem_grothendieckTopology {P : CategoryTheory.MorphismProperty Scheme} (X : Scheme) [IsEmpty ↥X] : ⊥ ∈ (grothendieckTopology P) X

theorem AlgebraicGeometry.Scheme.Cover.mem_pretopology {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {X : Scheme} {𝒰 : Cover (precoverage P) X} : CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f ∈ (pretopology P).coverings X

theorem AlgebraicGeometry.Scheme.mem_pretopology_iff {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {X : Scheme} {R : CategoryTheory.Presieve X} : R ∈ (pretopology P).coverings X ↔ ∃ (𝒰 : Cover (precoverage P) X), R = CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f

theorem AlgebraicGeometry.Scheme.exists_cover_of_mem_pretopology {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {X : Scheme} {R : CategoryTheory.Presieve X} : R ∈ (pretopology P).coverings X → ∃ (𝒰 : Cover (precoverage P) X), R = CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f

Alias of the forward direction of AlgebraicGeometry.Scheme.mem_pretopology_iff.

theorem AlgebraicGeometry.Scheme.mem_grothendieckTopology_iff {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {X : Scheme} {S : CategoryTheory.Sieve X} : S ∈ (grothendieckTopology P) X ↔ ∃ (𝒰 : Cover (precoverage P) X), CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows

theorem AlgebraicGeometry.Scheme.exists_cover_of_mem_grothendieckTopology {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {X : Scheme} {S : CategoryTheory.Sieve X} : S ∈ (grothendieckTopology P) X → ∃ (𝒰 : Cover (precoverage P) X), CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows

Alias of the forward direction of AlgebraicGeometry.Scheme.mem_grothendieckTopology_iff.

def AlgebraicGeometry.Scheme.jointlySurjectiveTopology : CategoryTheory.GrothendieckTopology Scheme

The jointly surjective topology on Scheme is defined by the same condition as the jointly surjective pretopology.

theorem AlgebraicGeometry.Scheme.mem_jointlySurjectiveTopology_iff_jointlySurjectivePretopology {X : Scheme} {s : CategoryTheory.Sieve X} : s ∈ jointlySurjectiveTopology X ↔ s.arrows ∈ jointlySurjectivePretopology.coverings X

theorem AlgebraicGeometry.Scheme.jointlySurjectiveTopology_eq_toGrothendieck_jointlySurjectivePretopology : jointlySurjectiveTopology = jointlySurjectivePretopology.toGrothendieck

theorem AlgebraicGeometry.Scheme.pretopology_eq_inf (P : CategoryTheory.MorphismProperty Scheme) [P.IsStableUnderBaseChange] [P.IsMultiplicative] : pretopology P = jointlySurjectivePretopology ⊓ P.pretopology

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

theorem AlgebraicGeometry.Scheme.grothendieckTopology_eq_inf (P : CategoryTheory.MorphismProperty Scheme) [P.IsStableUnderBaseChange] [P.IsMultiplicative] : grothendieckTopology P = (jointlySurjectivePretopology ⊓ P.pretopology).toGrothendieck

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.

theorem AlgebraicGeometry.Scheme.grothendieckTopology_monotone {P Q : CategoryTheory.MorphismProperty Scheme} (hPQ : P ≤ Q) : grothendieckTopology P ≤ grothendieckTopology Q

theorem AlgebraicGeometry.Scheme.pretopology_monotone {P Q : CategoryTheory.MorphismProperty Scheme} [P.IsMultiplicative] [P.IsStableUnderBaseChange] [Q.IsMultiplicative] [Q.IsStableUnderBaseChange] (hPQ : P ≤ Q) : pretopology P ≤ pretopology Q