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.

source

🔸 coverage

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.

Equations

Instances For

source

🔸 coverage

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

Equations

Instances For

source

📐 coverage

instance AlgebraicGeometry.Scheme.instIsStableUnderBaseChangeJointlySurjectivePrecoverage :

jointlySurjectivePrecoverage.IsStableUnderBaseChange

source

🔸 coverage

def AlgebraicGeometry.Scheme.jointlySurjectivePretopology :

CategoryTheory.Pretopology Scheme

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

Equations

Instances For

source

📐 coverage

theorem AlgebraicGeometry.Scheme.Cover.mem_grothendieckTopology {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) :

CategoryTheory.Sieve.ofArrows 𝒰.X 𝒰.f ∈ (grothendieckTopology P) X

source

📐 coverage

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

⊥ ∈ (grothendieckTopology P) X

source

📐 coverage

@[deprecated AlgebraicGeometry.Scheme.Cover.mem_grothendieckTopology (since := "2025-08-28")]

theorem AlgebraicGeometry.Scheme.grothendieckTopology_cover {P : CategoryTheory.MorphismProperty Scheme} {X : Scheme} (𝒰 : Cover (precoverage P) X) :

CategoryTheory.Sieve.ofArrows 𝒰.X 𝒰.f ∈ (grothendieckTopology P) X

Alias of AlgebraicGeometry.Scheme.Cover.mem_grothendieckTopology.

source

📐 coverage

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

source

📐 coverage

@[deprecated AlgebraicGeometry.Scheme.Cover.mem_pretopology (since := "2025-08-28")]

theorem AlgebraicGeometry.Scheme.pretopology_cover {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {X : Scheme} {𝒰 : Cover (precoverage P) X} :

CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f ∈ (pretopology P).coverings X

Alias of AlgebraicGeometry.Scheme.Cover.mem_pretopology.

source

📐 coverage

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

source

📐 coverage

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.

source

📐 coverage

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

source

📐 coverage

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.

source

🔸 coverage

@[deprecated AlgebraicGeometry.Scheme.jointlySurjectivePretopology (since := "2025-08-18")]

def AlgebraicGeometry.Scheme.surjectiveFamiliesPretopology :

CategoryTheory.Pretopology Scheme

Alias of AlgebraicGeometry.Scheme.jointlySurjectivePretopology.

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

Equations

Instances For

source

🔸 coverage

def AlgebraicGeometry.Scheme.jointlySurjectiveTopology :

CategoryTheory.GrothendieckTopology Scheme

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

Equations

Instances For

source

📐 coverage

theorem AlgebraicGeometry.Scheme.mem_jointlySurjectiveTopology_iff_jointlySurjectivePretopology {X : Scheme} {s : CategoryTheory.Sieve X} :

s ∈ jointlySurjectiveTopology X ↔ jointlySurjectivePretopology.coverings X s.arrows

source

📐 coverage

theorem AlgebraicGeometry.Scheme.jointlySurjectiveTopology_eq_toGrothendieck_jointlySurjectivePretopology :

jointlySurjectiveTopology = jointlySurjectivePretopology.toGrothendieck

source

📐 coverage

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.

source

📐 coverage

@[deprecated AlgebraicGeometry.Scheme.pretopology_eq_inf (since := "2025-08-28")]

theorem AlgebraicGeometry.Scheme.pretopology_le_inf (P : CategoryTheory.MorphismProperty Scheme) [P.IsStableUnderBaseChange] [P.IsMultiplicative] :

pretopology P = jointlySurjectivePretopology ⊓ P.pretopology

Alias of AlgebraicGeometry.Scheme.pretopology_eq_inf.

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

source

📐 coverage

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.

source

📐 coverage