Documentation

Mathlib.AlgebraicGeometry.Sites.Fpqc

Fpqc topology #

In this file we define the fpqc topology and show it is subcanonical. It is the quasi-compact topology for flat morphisms.

Main declarations #

source
def AlgebraicGeometry.Scheme.fppfPrecoverage :
CategoryTheory.Precoverage Scheme

The fppf precoverage on the category of schemes. The covering families are jointly-surjective families of flat morphisms, locally of finite presentation.

Equations
Instances For
    source
    @[implicit_reducible]
    instance AlgebraicGeometry.Scheme.instIsStableUnderBaseChangeFppfPrecoverage :
    fppfPrecoverage.IsStableUnderBaseChange
    Equations
    source
    @[implicit_reducible]
    instance AlgebraicGeometry.Scheme.instIsStableUnderCompositionFppfPrecoverage :
    fppfPrecoverage.IsStableUnderComposition
    Equations
    source
    theorem AlgebraicGeometry.Scheme.zariskiPrecoverage_le_fppfPrecoverage :
    zariskiPrecoverage ≤ fppfPrecoverage
    source
    theorem AlgebraicGeometry.Scheme.fppfPrecoverage_eq_inf :
    fppfPrecoverage = precoverage @Flat ⊓ precoverage @LocallyOfFinitePresentation
    source
    @[reducible, inline]
    abbrev AlgebraicGeometry.Scheme.fppfTopology :
    CategoryTheory.GrothendieckTopology Scheme

    The fppf topology on the category of schemes is topology generated by the fppf precoverage.

    Equations
    Instances For
      source
      def AlgebraicGeometry.Scheme.fpqcPrecoverage :
      CategoryTheory.Precoverage Scheme

      The fpqc precoverage on the category of schemes is the quasi-compact precoverage on flat morphisms. The covering families are jointly-surjective, quasi-compact families of flat morphisms.

      Equations
      Instances For
        source
        @[implicit_reducible]
        instance AlgebraicGeometry.Scheme.instHasIsosFpqcPrecoverage :
        fpqcPrecoverage.HasIsos
        Equations
        source
        @[implicit_reducible]
        instance AlgebraicGeometry.Scheme.instIsStableUnderBaseChangeFpqcPrecoverage :
        fpqcPrecoverage.IsStableUnderBaseChange
        Equations
        source
        @[implicit_reducible]
        instance AlgebraicGeometry.Scheme.instIsStableUnderCompositionFpqcPrecoverage :
        fpqcPrecoverage.IsStableUnderComposition
        Equations
        source
        theorem AlgebraicGeometry.Scheme.fppfPrecoverage_le_fpqcPrecoverage :
        fppfPrecoverage ≤ fpqcPrecoverage
        source
        theorem AlgebraicGeometry.Scheme.zariskiPrecoverage_le_fpqcPrecoverage :
        zariskiPrecoverage ≤ fpqcPrecoverage
        source
        @[reducible, inline]
        abbrev AlgebraicGeometry.Scheme.fpqcTopology :
        CategoryTheory.GrothendieckTopology Scheme

        The fpqc topology on the category of schemes is topology generated by the fpqc precoverage.

        Equations
        Instances For
          source
          theorem AlgebraicGeometry.Scheme.fpqcTopology_eq_propQCTopology :
          fpqcTopology = propQCTopology @Flat
          source
          theorem AlgebraicGeometry.Scheme.zariskiTopology_le_fpqcTopology :
          zariskiTopology ≤ fpqcTopology
          source
          theorem AlgebraicGeometry.Scheme.fppfTopology_le_fpqcTopology :
          fppfTopology ≤ fpqcTopology
          source
          instance AlgebraicGeometry.Scheme.instSubcanonicalFpqcTopology :
          fpqcTopology.Subcanonical
          source
          instance AlgebraicGeometry.Scheme.instSubcanonicalFppfTopology :
          fppfTopology.Subcanonical
          source
          @[simp]
          theorem AlgebraicGeometry.Scheme.Hom.singleton_mem_fppfPrecoverage {X Y : Scheme} (f : X ⟶ Y) [Flat f] [Surjective f] [LocallyOfFinitePresentation f] :
          CategoryTheory.Presieve.singleton f ∈ fppfPrecoverage.coverings Y
          source
          @[simp]
          theorem AlgebraicGeometry.Scheme.Hom.singleton_mem_fpqcPrecoverage {X Y : Scheme} (f : X ⟶ Y) [Flat f] [Surjective f] [QuasiCompact f] :
          CategoryTheory.Presieve.singleton f ∈ fpqcPrecoverage.coverings Y
          source
          instance AlgebraicGeometry.Scheme.instEffectiveEpiOfQuasiCompactOfSurjectiveOfFlat {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [Surjective f] [Flat f] :
          CategoryTheory.EffectiveEpi f

          Any surjective, quasi-compact and flat morphism is an effective epimorphism.

          source
          instance AlgebraicGeometry.Scheme.instEffectiveEpiOfLocallyOfFinitePresentationOfSurjectiveOfFlat {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Surjective f] [Flat f] :
          CategoryTheory.EffectiveEpi f

          Any surjective, flat morphism locally of finite presentation is an effective epimorphism. In particular, étale surjections satisfy this.