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) [P.IsStableUnderBaseChange] [P.IsMultiplicative] :
    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_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
        theorem AlgebraicGeometry.Scheme.Cover.mem_grothendieckTopology {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {X : Scheme} {𝒰 : Cover (precoverage P) X} :
        CategoryTheory.Sieve.ofArrows 𝒰.X 𝒰.f ∈ (grothendieckTopology P) X
        source
        @[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
        @[deprecated AlgebraicGeometry.Scheme.Cover.mem_grothendieckTopology (since := "2025-08-28")]
        theorem AlgebraicGeometry.Scheme.grothendieckTopology_cover {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {X : Scheme} {𝒰 : Cover (precoverage P) X} :
        CategoryTheory.Sieve.ofArrows 𝒰.X 𝒰.f ∈ (grothendieckTopology P) X

        Alias of AlgebraicGeometry.Scheme.Cover.mem_grothendieckTopology.

        source
        @[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
          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 ↔ jointlySurjectivePretopology.coverings X s.arrows
            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 the intersection of the pretopology of surjective families with the pretopology defined by P.

            source
            @[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 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.pretopology_monotone {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {Q : CategoryTheory.MorphismProperty Scheme} [Q.IsMultiplicative] [Q.IsStableUnderBaseChange] (hPQ : P ≤ Q) :
            pretopology P ≤ pretopology Q
            source
            @[deprecated AlgebraicGeometry.Scheme.pretopology_monotone (since := "2025-09-22")]
            theorem AlgebraicGeometry.Scheme.pretopology_le_pretopology {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {Q : CategoryTheory.MorphismProperty Scheme} [Q.IsMultiplicative] [Q.IsStableUnderBaseChange] (hPQ : P ≤ Q) :
            pretopology P ≤ pretopology Q

            Alias of AlgebraicGeometry.Scheme.pretopology_monotone.

            source
            theorem AlgebraicGeometry.Scheme.grothendieckTopology_monotone {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {Q : CategoryTheory.MorphismProperty Scheme} [Q.IsMultiplicative] [Q.IsStableUnderBaseChange] (hPQ : P ≤ Q) :
            grothendieckTopology P ≤ grothendieckTopology Q
            source
            @[deprecated AlgebraicGeometry.Scheme.grothendieckTopology_monotone (since := "2025-09-22")]
            theorem AlgebraicGeometry.Scheme.grothendieckTopology_le_grothendieckTopology {P : CategoryTheory.MorphismProperty Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {Q : CategoryTheory.MorphismProperty Scheme} [Q.IsMultiplicative] [Q.IsStableUnderBaseChange] (hPQ : P ≤ Q) :
            grothendieckTopology P ≤ grothendieckTopology Q

            Alias of AlgebraicGeometry.Scheme.grothendieckTopology_monotone.