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} {X : CategoryTheory.Over S} (𝒰 : Cover 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 : 𝒰.J) => (𝒰.obj i).asOver S) fun (i : 𝒰.J) => AlgebraicGeometry.Scheme.Hom.asOver (𝒰.map i) S

def AlgebraicGeometry.Scheme.Cover.toPresieveOverProp {P Q : CategoryTheory.MorphismProperty Scheme} {S : Scheme} {X : Q.Over ⊤ S} (𝒰 : Cover P X.left) [Cover.Over S 𝒰] (h : ∀ (j : 𝒰.J), Q (𝒰.obj 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 : 𝒰.J) => (𝒰.obj i).asOverProp S ⋯) fun (i : 𝒰.J) => AlgebraicGeometry.Scheme.Hom.asOverProp (𝒰.map i) S

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

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

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

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

Equations

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

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.overGrothendieckTopology (P : CategoryTheory.MorphismProperty Scheme) (S : Scheme) [P.IsMultiplicative] [P.RespectsIso] [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] : 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.IsMultiplicative] [P.RespectsIso] [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] : overGrothendieckTopology P S = CategoryTheory.Pretopology.toGrothendieck (CategoryTheory.Over S) (overPretopology P S)

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

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

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

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.smallGrothendieckTopologyOfLE {P Q : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsMultiplicative] [P.RespectsIso] [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] [Q.IsStableUnderComposition] (hPQ : P ≤ Q) : 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

• S.smallGrothendieckTopologyOfLE hPQ = (CategoryTheory.MorphismProperty.Over.forget Q ⊤ S).inducedTopology (AlgebraicGeometry.Scheme.overGrothendieckTopology P S)

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.smallGrothendieckTopology (P : CategoryTheory.MorphismProperty Scheme) {S : Scheme} [P.IsMultiplicative] [P.RespectsIso] [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] : CategoryTheory.GrothendieckTopology (P.Over ⊤ S)

The Grothendieck topology on the category of schemes over S with P induced by P, i.e. coverings are simply surjective families. This is the induced topology by the topology on S defined by P via the inclusion P.Over ⊤ S ⥤ Over S.

This is a special case of smallGrothendieckTopologyOfLE for the case P = Q.

Equations

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

def AlgebraicGeometry.Scheme.smallPretopology (P Q : CategoryTheory.MorphismProperty Scheme) {S : Scheme} [P.IsMultiplicative] [P.RespectsIso] [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] [Q.IsStableUnderComposition] [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.smallGrothendieckTopologyOfLE_eq_toGrothendieck_smallPretopology {P Q : CategoryTheory.MorphismProperty Scheme} (S : Scheme) [P.IsMultiplicative] [P.RespectsIso] [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] [Q.IsStableUnderComposition] [Q.IsStableUnderBaseChange] [Q.HasOfPostcompProperty Q] (hPQ : P ≤ Q) : S.smallGrothendieckTopologyOfLE hPQ = CategoryTheory.Pretopology.toGrothendieck (Q.Over ⊤ S) (smallPretopology P Q)

theorem AlgebraicGeometry.Scheme.smallGrothendieckTopology_eq_toGrothendieck_smallPretopology (P : CategoryTheory.MorphismProperty Scheme) {S : Scheme} [P.IsMultiplicative] [P.RespectsIso] [P.IsStableUnderBaseChange] [IsJointlySurjectivePreserving P] [P.HasOfPostcompProperty P] : smallGrothendieckTopology P = CategoryTheory.Pretopology.toGrothendieck (P.Over ⊤ S) (smallPretopology P P)

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

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