Documentation

Mathlib.AlgebraicGeometry.Sites.Pretopology

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
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
    @[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
      instance AlgebraicGeometry.Scheme.instIsStableUnderBaseChangeJointlySurjectivePrecoverage :
      jointlySurjectivePrecoverage.IsStableUnderBaseChange
      source
      def AlgebraicGeometry.Scheme.jointlySurjectivePretopology :
      CategoryTheory.Pretopology Scheme

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

      Equations
      Instances For
        source
        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
        theorem AlgebraicGeometry.Scheme.bot_mem_grothendieckTopology {P : CategoryTheory.MorphismProperty Scheme} (X : Scheme) [IsEmpty ↥X] :
        ⊥ ∈ (grothendieckTopology P) X
        source
        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
        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
        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
        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
        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
        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
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem AlgebraicGeometry.Scheme.mem_jointlySurjectiveTopology_iff_jointlySurjectivePretopology {X : Scheme} {s : CategoryTheory.Sieve X} :
          s ∈ jointlySurjectiveTopology X ↔ s.arrows ∈ jointlySurjectivePretopology.coverings X
          source
          theorem AlgebraicGeometry.Scheme.jointlySurjectiveTopology_eq_toGrothendieck_jointlySurjectivePretopology :
          jointlySurjectiveTopology = jointlySurjectivePretopology.toGrothendieck
          source
          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
          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
          theorem AlgebraicGeometry.Scheme.grothendieckTopology_monotone {P Q : CategoryTheory.MorphismProperty Scheme} (hPQ : P ≤ Q) :
          grothendieckTopology P ≤ grothendieckTopology Q
          source
          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