Small sites

In this file we define the small sites associated to morphism properties and give generating pretopologies.

Main definitions

• AlgebraicGeometry.Scheme.overGrothendieckTopology: the Grothendieck topology on Over S obtained by localizing the topology on Scheme induced by P at S.
• AlgebraicGeometry.Scheme.overPretopology: the pretopology on Over S defined by P-coverings of S-schemes. The induced topology agrees with AlgebraicGeometry.Scheme.overGrothendieckTopology.
• AlgebraicGeometry.Scheme.smallGrothendieckTopology: the by the inclusion P.Over ⊤ S ⥤ Over S induced topology on P.Over ⊤ S.
• AlgebraicGeometry.Scheme.smallPretopology: the pretopology on P.Over ⊤ S defined by P-coverings of S-schemes with P. The induced topology agrees with AlgebraicGeometry.Scheme.smallGrothendieckTopology.

def AlgebraicGeometry.Scheme.Cover.toPresieveOver {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [P.IsStableUnderBaseChange] {X : CategoryTheory.Over S} (𝒰 : Cover (precoverage P) X.left) [Cover.Over S 𝒰] : CategoryTheory.Presieve X

The presieve defined by a P-cover of S-schemes.

Equations

• 𝒰.toPresieveOver = CategoryTheory.Presieve.ofArrows (fun (i : 𝒰.I₀) => (𝒰.X i).asOver S) fun (i : 𝒰.I₀) => AlgebraicGeometry.Scheme.Hom.asOver (𝒰.f i) S

def AlgebraicGeometry.Scheme.Cover.toPresieveOverProp {P Q : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [P.IsStableUnderBaseChange] {X : Q.Over ⊤ S} (𝒰 : Cover (precoverage P) X.left) [Cover.Over S 𝒰] (h : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)) : CategoryTheory.Presieve X

The presieve defined by a P-cover of S-schemes with Q.

Equations

• 𝒰.toPresieveOverProp h = CategoryTheory.Presieve.ofArrows (fun (i : 𝒰.I₀) => (𝒰.X i).asOverProp S ⋯) fun (i : 𝒰.I₀) => AlgebraicGeometry.Scheme.Hom.asOverProp (𝒰.f i) S

theorem AlgebraicGeometry.Scheme.Cover.overEquiv_generate_toPresieveOver_eq_ofArrows {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [P.IsStableUnderBaseChange] {X : CategoryTheory.Over S} (𝒰 : Cover (precoverage P) X.left) [Cover.Over S 𝒰] : (CategoryTheory.Sieve.overEquiv X) (CategoryTheory.Sieve.generate 𝒰.toPresieveOver) = CategoryTheory.Sieve.ofArrows 𝒰.X 𝒰.f

theorem AlgebraicGeometry.Scheme.Cover.toPresieveOver_le_arrows_iff {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [P.IsStableUnderBaseChange] {X : CategoryTheory.Over S} (R : CategoryTheory.Sieve X) (𝒰 : Cover (precoverage P) X.left) [Cover.Over S 𝒰] : 𝒰.toPresieveOver ≤ R.arrows ↔ CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f ≤ ((CategoryTheory.Sieve.overEquiv X) R).arrows

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.overPretopology (P : CategoryTheory.MorphismProperty Scheme) (S : Scheme) [P.IsStableUnderBaseChange] [P.IsMultiplicative] : CategoryTheory.Pretopology (CategoryTheory.Over S)

The pretopology on Over S induced by P where coverings are given by P-covers of S-schemes.

Equations

• AlgebraicGeometry.Scheme.overPretopology P S = CategoryTheory.Precoverage.toPretopology (CategoryTheory.Over S) (CategoryTheory.Precoverage.over S (AlgebraicGeometry.Scheme.precoverage P))

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.overGrothendieckTopology (P : CategoryTheory.MorphismProperty Scheme) (S : Scheme) : CategoryTheory.GrothendieckTopology (CategoryTheory.Over S)

The topology on Over S induced from the topology on Scheme defined by P. This agrees with the topology induced by S.overPretopology P, see AlgebraicGeometry.Scheme.overGrothendieckTopology_eq_toGrothendieck_overPretopology.

Equations

• AlgebraicGeometry.Scheme.overGrothendieckTopology P S = (AlgebraicGeometry.Scheme.grothendieckTopology P).over S

theorem AlgebraicGeometry.Scheme.overGrothendieckTopology_eq_toGrothendieck_overPretopology (P : CategoryTheory.MorphismProperty Scheme) (S : Scheme) [P.IsStableUnderBaseChange] [P.IsMultiplicative] : overGrothendieckTopology P S = (overPretopology P S).toGrothendieck

theorem AlgebraicGeometry.Scheme.mem_overGrothendieckTopology (P : CategoryTheory.MorphismProperty Scheme) {S : Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] (X : CategoryTheory.Over S) (R : CategoryTheory.Sieve X) : R ∈ (overGrothendieckTopology P S) X ↔ ∃ (𝒰 : Cover (precoverage P) X.left) (x : Cover.Over S 𝒰), 𝒰.toPresieveOver ≤ R.arrows

theorem AlgebraicGeometry.Scheme.locallyCoverDense_of_le {P Q : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [Q.IsStableUnderComposition] [P.IsStableUnderBaseChange] [P.IsMultiplicative] (hPQ : P ≤ Q) : (CategoryTheory.MorphismProperty.Over.forget Q ⊤ S).LocallyCoverDense (overGrothendieckTopology P S)

instance AlgebraicGeometry.Scheme.instLocallyCoverDenseOverTopMorphismPropertyOverForgetOverGrothendieckTopology (P : CategoryTheory.MorphismProperty Scheme) {S : Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] : (CategoryTheory.MorphismProperty.Over.forget P ⊤ S).LocallyCoverDense (overGrothendieckTopology P S)

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.smallGrothendieckTopology (P : CategoryTheory.MorphismProperty Scheme) {Q : CategoryTheory.MorphismProperty Scheme} (S : Scheme) : CategoryTheory.GrothendieckTopology (Q.Over ⊤ S)

If P and Q are morphism properties with P ≤ Q, this is the Grothendieck topology induced via the forgetful functor Q.Over ⊤ S ⥤ Over S by the topology defined by P.

Equations

• AlgebraicGeometry.Scheme.smallGrothendieckTopology P S = (CategoryTheory.MorphismProperty.Over.forget Q ⊤ S).restrictedTopology (AlgebraicGeometry.Scheme.overGrothendieckTopology P S)

@[deprecated AlgebraicGeometry.Scheme.smallGrothendieckTopology (since := "2026-05-28")]

def AlgebraicGeometry.Scheme.smallGrothendieckTopologyOfLE (P : CategoryTheory.MorphismProperty Scheme) {Q : CategoryTheory.MorphismProperty Scheme} (S : Scheme) : CategoryTheory.GrothendieckTopology (Q.Over ⊤ S)

Alias of AlgebraicGeometry.Scheme.smallGrothendieckTopology.

---

If P and Q are morphism properties with P ≤ Q, this is the Grothendieck topology induced via the forgetful functor Q.Over ⊤ S ⥤ Over S by the topology defined by P.

Equations

• AlgebraicGeometry.Scheme.smallGrothendieckTopologyOfLE = AlgebraicGeometry.Scheme.smallGrothendieckTopology

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.smallPretopology (P Q : CategoryTheory.MorphismProperty Scheme) {S : Scheme} [Q.IsStableUnderComposition] [P.IsStableUnderBaseChange] [P.IsMultiplicative] [Q.IsStableUnderBaseChange] [Q.HasOfPostcompProperty Q] : CategoryTheory.Pretopology (Q.Over ⊤ S)

The pretopology defined on the subcategory of S-schemes satisfying Q where coverings are given by P-coverings in S-schemes satisfying Q. The most common case is P = Q. In this case, this is simply surjective families in S-schemes with P.

Equations

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

theorem AlgebraicGeometry.Scheme.smallGrothendieckTopology_eq_toGrothendieck_smallPretopology {P Q : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [Q.IsStableUnderComposition] [P.IsStableUnderBaseChange] [P.IsMultiplicative] [Q.IsStableUnderBaseChange] [Q.HasOfPostcompProperty Q] (hPQ : P ≤ Q) : smallGrothendieckTopology P S = (smallPretopology P Q).toGrothendieck

@[deprecated AlgebraicGeometry.Scheme.smallGrothendieckTopology_eq_toGrothendieck_smallPretopology (since := "2026-05-28")]

theorem AlgebraicGeometry.Scheme.smallGrothendieckTopologyOfLE_eq_toGrothendieck_smallPretopology {P Q : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [Q.IsStableUnderComposition] [P.IsStableUnderBaseChange] [P.IsMultiplicative] [Q.IsStableUnderBaseChange] [Q.HasOfPostcompProperty Q] (hPQ : P ≤ Q) : smallGrothendieckTopology P S = (smallPretopology P Q).toGrothendieck

Alias of AlgebraicGeometry.Scheme.smallGrothendieckTopology_eq_toGrothendieck_smallPretopology.

theorem AlgebraicGeometry.Scheme.mem_toGrothendieck_smallPretopology {P Q : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [Q.IsStableUnderComposition] [P.IsStableUnderBaseChange] [P.IsMultiplicative] [Q.IsStableUnderBaseChange] [Q.HasOfPostcompProperty Q] (X : Q.Over ⊤ S) (R : CategoryTheory.Sieve X) : R ∈ (smallPretopology P Q).toGrothendieck X ↔ ∀ (x : ↥X.left), ∃ (Y : Q.Over ⊤ S) (f : Y ⟶ X) (y : ↥Y.left), R.arrows f ∧ P f.left ∧ f.left y = x

theorem AlgebraicGeometry.Scheme.mem_smallGrothendieckTopology {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] (X : P.Over ⊤ S) (R : CategoryTheory.Sieve X) : R ∈ (smallGrothendieckTopology P S) X ↔ ∃ (𝒰 : Cover (precoverage P) X.left) (x : Cover.Over S 𝒰) (h : ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)), 𝒰.toPresieveOverProp h ≤ R.arrows