Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AlgebraicGeometry_FppfSiteCohomology.lean

definition module

The small fppf site and fppf cohomology of schemes

The morphism property fppfProperty is the intersection \mathrm{Flat} \sqcap \mathrm{LocallyOfFinitePresentation} on schemes; it is recorded to be stable under base change and composition, to contain identities and respect isomorphisms, and Mathlib's fppfPrecoverage and fppfTopology on all schemes are identified with the precoverage and Grothendieck topology generated by this property, the latter also with the topology generated by the pretopology fppfPretopology. Since an étale morphism is flat and formally unramified, etale_le_fppfProperty gives \mathrm{Etale} \le fppfProperty, whence the étale and Zariski topologies are coarser than the fppf topology. For a scheme S, S.Fppf is the category MorphismProperty.Over fppfProperty ⊤ S of schemes equipped with a flat, locally of finite presentation morphism to S, with arbitrary S-morphisms between them; Fppf.mk builds an object from such a morphism, Fppf.forget is the full and faithful functor to Over S, and fppfTerminal S, the identity of S, is shown to be terminal. The small site topology smallFppfTopology S is S.smallGrothendieckTopology for fppfProperty, equal to the topology on S.Fppf restricted along Fppf.forget from the localised big topology fppfTopology.over S, with respect to which that functor is cocontinuous.

On abelian sheaves for smallFppfTopology S with values in Ab.{u+1} the module records sheafification, abelianness, Grothendieck abelianness (transported along an equivalence with a small model of S.Fppf) and hence HasExt. Then fppfCohomology S F n is Mathlib's Sheaf.H, the n-th Ext-group from the constant sheaf with value \mathbb{Z} to F, with its additive group structure; fppfCohomologyZeroAddEquiv identifies degree 0 with the sections F(S \xrightarrow{\mathrm{id}} S), via the constant-sheaf adjunction at the terminal object and the additive equivalence homULiftIntAddEquiv between \mathrm{Hom}(\mathbb{Z}, A) and A. Functoriality in the coefficients is given by composition with \mathrm{Ext}-classes of degree 0 (fppfCohomologyMap, with identity and composition laws) and by fppfCohomologyFunctor. Two comparison functors to sheaves on the localised big site are defined: pullback from the big fppf site and pushforward along the cocontinuous Fppf.forget. Small sanity lemmas record that all cohomology of the zero sheaf is a subsingleton and that nontrivial sections over the terminal object give nontrivial H^0; everything is instantiated at S = \operatorname{Spec}\mathbb{Z}.

Relation to Mathlib

Mathlib supplies the big fppf precoverage and topology on schemes, the generic small-site constructions (smallGrothendieckTopology, MorphismProperty.Over, restricted topologies, cocontinuous pushforward) and sheaf cohomology as Sheaf.H via Ext from the constant sheaf. What is added here is the packaging for the fppf case: the multiplicativity instance for LocallyOfFinitePresentation, the abbreviation fppfProperty with the identifications of Mathlib's fppf topology, the category S.Fppf with its terminal object, the Grothendieck-abelian and HasExt instances for abelian sheaves on the small fppf site, and named wrappers fppfCohomology, fppfCohomologyMap, fppfCohomologyFunctor together with the degree-zero identification.

Where it is used

This is the base layer for the flat-cohomology input to the Eisenstein-ideal study of modular Jacobians, where cohomology is taken for the fppf topology; companion developments add the long exact sequence with its connecting map and the Kummer sequence relating \mathbb{G}_m and \mu_p on the fppf site.

References

  1. B. Mazur, Modular curves and the Eisenstein ideal, Publications Mathématiques de l'IHÉS 47 (1977), 33–186
  2. M. Demazure and A. Grothendieck (eds.), Schémas en groupes I (SGA 3), Lecture Notes in Mathematics 151, Springer, 1970, Exposé IV
  3. J. S. Milne, Étale Cohomology, Princeton Mathematical Series 33, Princeton University Press, 1980

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_AlgebraicGeometry_FppfSiteCohomology.lean

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib.AlgebraicGeometry.Sites.Fpqc ↗
import Mathlib.AlgebraicGeometry.Sites.Etale ↗
import Mathlib.AlgebraicGeometry.Sites.Small ↗
import Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation ↗
import Mathlib.AlgebraicGeometry.Morphisms.Flat ↗
import Mathlib.CategoryTheory.Sites.SheafCohomology.Basic ↗
import Mathlib.CategoryTheory.Sites.ConstantSheaf ↗
import Mathlib.CategoryTheory.Sites.Over ↗
import Mathlib.CategoryTheory.Limits.MorphismProperty ↗
import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf ↗
import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.HasExt ↗
import Mathlib.CategoryTheory.Adjunction.Additive ↗
import Mathlib.Algebra.Category.Grp.AB ↗
import Mathlib.Algebra.Category.Grp.Ulift ↗
import Mathlib.Algebra.Category.Grp.ForgetCorepresentable ↗

universe u

open CategoryTheory CategoryTheory.Limits Opposite

namespace AlgebraicGeometry.Scheme

instance : MorphismProperty.IsMultiplicative @LocallyOfFinitePresentation where
  id_mem _ := inferInstance

abbrev fppfProperty : MorphismProperty Scheme.{u} := @Flat ⊓ @LocallyOfFinitePresentation

example : fppfProperty.{u}.IsStableUnderBaseChange := inferInstance
example : fppfProperty.{u}.IsMultiplicative := inferInstance
example : fppfProperty.{u}.IsStableUnderComposition := inferInstance
example : fppfProperty.{u}.RespectsIso := inferInstance
example : fppfProperty.{u}.ContainsIdentities := inferInstance
example : fppfProperty.{u}.HasPullbacks := inferInstance

theorem fppfPrecoverage_eq_precoverage_fppfProperty :
    fppfPrecoverage.{u} = Scheme.precoverage fppfProperty := rfl

instance : fppfPrecoverage.{u}.HasIsos :=
  inferInstanceAs (Scheme.precoverage fppfProperty.{u}).HasIsos

instance : fppfPrecoverage.{u}.HasPullbacks :=
  inferInstanceAs (Scheme.precoverage fppfProperty.{u}).HasPullbacks

def fppfPretopology : Pretopology Scheme.{u} := Scheme.pretopology fppfProperty

theorem fppfTopology_eq_grothendieckTopology :
    fppfTopology.{u} = Scheme.grothendieckTopology fppfProperty := rfl

theorem fppfTopology_eq_toGrothendieck_fppfPretopology :
    fppfTopology.{u} = fppfPretopology.toGrothendieck :=
  Precoverage.toGrothendieck_toPretopology_eq_toGrothendieck.symm

theorem etale_le_fppfProperty : @Etale ≤ fppfProperty.{u} := by
  intro X Y f hf
  have h := Etale.iff_flat_and_formallyUnramified.mp hf
  exact ⟨h.1, h.2.2⟩

theorem etalePrecoverage_le_fppfPrecoverage : etalePrecoverage.{u} ≤ fppfPrecoverage :=
  Scheme.precoverage_mono etale_le_fppfProperty

theorem etaleTopology_le_fppfTopology : etaleTopology.{u} ≤ fppfTopology :=
  Precoverage.toGrothendieck_mono etalePrecoverage_le_fppfPrecoverage

theorem zariskiTopology_le_fppfTopology : zariskiTopology.{u} ≤ fppfTopology :=
  Precoverage.toGrothendieck_mono zariskiPrecoverage_le_fppfPrecoverage

example : fppfTopology.{u}.Subcanonical := inferInstance

protected def Fppf (S : Scheme.{u}) : Type (u + 1) := MorphismProperty.Over fppfProperty ⊤ S

instance (S : Scheme.{u}) : Category.{u} S.Fppf :=
  inferInstanceAs <| Category.{u} (MorphismProperty.Over fppfProperty ⊤ S)

namespace Fppf

variable (S : Scheme.{u})

instance (U : S.Fppf) : Flat U.hom := U.prop.1
instance (U : S.Fppf) : LocallyOfFinitePresentation U.hom := U.prop.2

variable {S} in

protected noncomputable def mk {X : Scheme.{u}} (f : X ⟶ S) [Flat f]
    [LocallyOfFinitePresentation f] : S.Fppf :=
  MorphismProperty.Over.mk ⊤ f ⟨‹_›, ‹_›⟩

protected def forget : S.Fppf ⥤ Over S := MorphismProperty.Over.forget fppfProperty ⊤ S

instance : (Fppf.forget S).Full :=
  inferInstanceAs (MorphismProperty.Over.forget _ _ _).Full

instance : (Fppf.forget S).Faithful :=
  inferInstanceAs (MorphismProperty.Over.forget _ _ _).Faithful

end Fppf

def smallFppfTopology (S : Scheme.{u}) : GrothendieckTopology S.Fppf :=
  S.smallGrothendieckTopology (P := fppfProperty)

theorem overGrothendieckTopology_fppfProperty_eq (S : Scheme.{u}) :
    S.overGrothendieckTopology fppfProperty = fppfTopology.over S := rfl

instance (S : Scheme.{u}) :
    (Fppf.forget S).LocallyCoverDense (fppfTopology.over S) :=
  inferInstanceAs <|
    (MorphismProperty.Over.forget fppfProperty ⊤ S).LocallyCoverDense
      (S.overGrothendieckTopology fppfProperty)

theorem smallFppfTopology_eq_restrictedTopology (S : Scheme.{u}) :
    smallFppfTopology S = (Fppf.forget S).restrictedTopology (fppfTopology.over S) := rfl

instance (S : Scheme.{u}) :
    (Fppf.forget S).IsCocontinuous (smallFppfTopology S) (fppfTopology.over S) :=
  inferInstanceAs <|
    (MorphismProperty.Over.forget fppfProperty ⊤ S).IsCocontinuous
      ((MorphismProperty.Over.forget fppfProperty ⊤ S).restrictedTopology
        (S.overGrothendieckTopology fppfProperty))
      (S.overGrothendieckTopology fppfProperty)

example (S : Scheme.{u}) : EssentiallySmall.{u + 1} S.Fppf := inferInstance

noncomputable def fppfTerminal (S : Scheme.{u}) : S.Fppf :=
  MorphismProperty.Over.mk ⊤ (𝟙 S) (fppfProperty.id_mem S)

noncomputable def fppfTerminalIsTerminal (S : Scheme.{u}) : IsTerminal (fppfTerminal S) :=
  MorphismProperty.Over.mkIdTerminal fppfProperty S

instance (S : Scheme.{u}) : HasTerminal S.Fppf :=
  (fppfTerminalIsTerminal S).hasTerminal

variable (S : Scheme.{u})

instance hasSheafify_smallFppfTopology : HasSheafify (smallFppfTopology S) Ab.{u + 1} :=
  inferInstance

noncomputable instance abelian_sheaf_smallFppfTopology :
    Abelian (Sheaf (smallFppfTopology S) Ab.{u + 1}) :=
  inferInstance

set_option maxHeartbeats 800000 in
set_option synthInstance.maxHeartbeats 200000 in

instance isGrothendieckAbelian_sheaf_smallFppfTopology :
    IsGrothendieckAbelian.{u + 1} (Sheaf (smallFppfTopology S) Ab.{u + 1}) := by
  have : EssentiallySmall.{u + 1} S.Fppf := inferInstance
  exact IsGrothendieckAbelian.of_equivalence
    ((equivSmallModel.{u + 1} S.Fppf).inverse.sheafInducedTopologyEquivOfIsCoverDense
      (smallFppfTopology S) Ab.{u + 1})

instance hasExt_sheaf_smallFppfTopology :
    HasExt.{u + 1} (Sheaf (smallFppfTopology S) Ab.{u + 1}) :=
  IsGrothendieckAbelian.hasExt _

noncomputable def fppfCohomology (F : Sheaf (smallFppfTopology S) Ab.{u + 1}) (n : ℕ) :
    Type (u + 1) :=
  F.H n

noncomputable instance (F : Sheaf (smallFppfTopology S) Ab.{u + 1}) (n : ℕ) :
    AddCommGroup (fppfCohomology S F n) :=
  inferInstanceAs <| AddCommGroup (F.H n)

instance : (Functor.const (S.Fppf)ᵒᵖ : Ab.{u + 1} ⥤ ((S.Fppf)ᵒᵖ ⥤ Ab.{u + 1})).Additive where
  map_add := by intros; ext; rfl

instance : (constantSheaf (smallFppfTopology S) Ab.{u + 1}).Additive :=
  inferInstanceAs
    (Functor.const (S.Fppf)ᵒᵖ ⋙ presheafToSheaf (smallFppfTopology S) Ab.{u + 1}).Additive

universe w in

noncomputable def homULiftIntAddEquiv (A : Ab.{w}) :
    (AddCommGrpCat.of (ULift.{w} ℤ) ⟶ A) ≃+ A :=
  { ConcreteCategory.homEquiv.trans (uliftZMultiplesHom A.carrier).symm with
    map_add' := fun f g => by
      have h : ConcreteCategory.homEquiv (f + g) =
          ConcreteCategory.homEquiv f + ConcreteCategory.homEquiv g := rfl
      show (uliftZMultiplesHom A.carrier).symm (ConcreteCategory.homEquiv (f + g)) = _
      rw [h]
      rfl }

open Abelian in

noncomputable def sheafHZeroAddEquiv (F : Sheaf (smallFppfTopology S) Ab.{u + 1}) :
    F.H 0 ≃+ F.obj.obj (op (fppfTerminal S)) :=
  (Ext.addEquiv₀.trans
    ((constantSheafAdj _ _ (fppfTerminalIsTerminal S)).homAddEquiv _ _)).trans
    (homULiftIntAddEquiv.{u + 1} (F.obj.obj (op (fppfTerminal S))))

open Abelian in

noncomputable def fppfCohomologyZeroAddEquiv (F : Sheaf (smallFppfTopology S) Ab.{u + 1}) :
    fppfCohomology S F 0 ≃+ F.obj.obj (op (fppfTerminal S)) :=
  sheafHZeroAddEquiv S F

open Abelian in

noncomputable def sheafHMap {F G : Sheaf (smallFppfTopology S) Ab.{u + 1}} (φ : F ⟶ G)
    (n : ℕ) : F.H n →+ G.H n :=
  AddMonoidHom.mk' (fun α => Ext.comp α (Ext.mk₀ φ) (add_zero n))
    (fun α β => by exact Ext.add_comp α β (Ext.mk₀ φ) (add_zero n))

open Abelian in

noncomputable def fppfCohomologyMap {F G : Sheaf (smallFppfTopology S) Ab.{u + 1}} (φ : F ⟶ G)
    (n : ℕ) : fppfCohomology S F n →+ fppfCohomology S G n :=
  sheafHMap S φ n

open Abelian in

theorem sheafHMap_id {F : Sheaf (smallFppfTopology S) Ab.{u + 1}} (n : ℕ)
    (α : F.H n) :
    sheafHMap S (𝟙 F) n α = α := by
  show Ext.comp α (Ext.mk₀ (𝟙 F)) (add_zero n) = α
  exact Ext.comp_mk₀_id α

open Abelian in

theorem fppfCohomologyMap_id {F : Sheaf (smallFppfTopology S) Ab.{u + 1}} (n : ℕ)
    (α : fppfCohomology S F n) :
    fppfCohomologyMap S (𝟙 F) n α = α :=
  sheafHMap_id S n α

open Abelian in

theorem sheafHMap_comp {F G H' : Sheaf (smallFppfTopology S) Ab.{u + 1}}
    (φ : F ⟶ G) (ψ : G ⟶ H') (n : ℕ) (α : F.H n) :
    sheafHMap S (φ ≫ ψ) n α = sheafHMap S ψ n (sheafHMap S φ n α) := by
  show Ext.comp α (Ext.mk₀ (φ ≫ ψ)) (add_zero n) =
    Ext.comp (Ext.comp α (Ext.mk₀ φ) (add_zero n)) (Ext.mk₀ ψ) (add_zero n)
  rw [← Ext.mk₀_comp_mk₀, Ext.comp_assoc_of_third_deg_zero]

open Abelian in

theorem fppfCohomologyMap_comp {F G H' : Sheaf (smallFppfTopology S) Ab.{u + 1}}
    (φ : F ⟶ G) (ψ : G ⟶ H') (n : ℕ) (α : fppfCohomology S F n) :
    fppfCohomologyMap S (φ ≫ ψ) n α = fppfCohomologyMap S ψ n (fppfCohomologyMap S φ n α) :=
  sheafHMap_comp S φ ψ n α

noncomputable def fppfCohomologyFunctor (n : ℕ) :
    Sheaf (smallFppfTopology S) Ab.{u + 1} ⥤ Ab.{u + 1} :=
  Sheaf.functorH (smallFppfTopology S) n

theorem fppfCohomologyFunctor_obj_carrier (n : ℕ) (F : Sheaf (smallFppfTopology S) Ab.{u + 1}) :
    ((fppfCohomologyFunctor S n).obj F : Type (u + 1)) = F.H n :=
  rfl

noncomputable def fppfBigToOverRestriction :
    Sheaf fppfTopology.{u} Ab.{u + 1} ⥤ Sheaf (fppfTopology.{u}.over S) Ab.{u + 1} :=
  fppfTopology.overPullback Ab.{u + 1} S

noncomputable def fppfSmallToOverPushforward :
    Sheaf (smallFppfTopology S) Ab.{u + 1} ⥤ Sheaf (fppfTopology.{u}.over S) Ab.{u + 1} :=
  (Fppf.forget S).sheafPushforwardCocontinuous Ab.{u + 1} (smallFppfTopology S)
    (fppfTopology.over S)

open ZeroObject in

theorem gate_zero_sheaf_subsingleton (n : ℕ) :
    Subsingleton (fppfCohomology S (0 : Sheaf (smallFppfTopology S) Ab.{u + 1}) n) := by
  show Subsingleton ((0 : Sheaf (smallFppfTopology S) Ab.{u + 1}).H n)
  exact Sheaf.subsingleton_H_of_isZero (Limits.isZero_zero _) n

theorem gate_H0_nontrivial_of_sections_nontrivial (F : Sheaf (smallFppfTopology S) Ab.{u + 1})
    (h : Nontrivial (F.obj.obj (op (fppfTerminal S)))) :
    Nontrivial (fppfCohomology S F 0) :=
  (fppfCohomologyZeroAddEquiv S F).toEquiv.nontrivial

open ZeroObject in

theorem gate_H0_equiv_fires_on_zero_sheaf :
    Subsingleton
      (((0 : Sheaf (smallFppfTopology S) Ab.{u + 1}).obj.obj (op (fppfTerminal S))) :
        Type (u + 1)) :=
  have : Subsingleton (fppfCohomology S (0 : Sheaf (smallFppfTopology S) Ab.{u + 1}) 0) :=
    gate_zero_sheaf_subsingleton S 0
  (fppfCohomologyZeroAddEquiv S
    (0 : Sheaf (smallFppfTopology S) Ab.{u + 1})).symm.toEquiv.subsingleton

section SpecInt

noncomputable abbrev specInt : Scheme.{0} := Spec (CommRingCat.of ℤ)

noncomputable example (F : Sheaf (smallFppfTopology specInt) Ab.{1}) :
    AddCommGroup (fppfCohomology specInt F 1) :=
  inferInstance

open Abelian in

noncomputable def fppfCohomologySpecIntZeroAddEquiv
    (F : Sheaf (smallFppfTopology specInt) Ab.{1}) :
    fppfCohomology specInt F 0 ≃+ F.obj.obj (op (fppfTerminal specInt)) :=
  fppfCohomologyZeroAddEquiv specInt F

open ZeroObject in

theorem gate_specInt_H1_zero_sheaf_subsingleton :
    Subsingleton (fppfCohomology specInt (0 : Sheaf (smallFppfTopology specInt) Ab.{1}) 1) :=
  gate_zero_sheaf_subsingleton specInt 1

end SpecInt

end AlgebraicGeometry.Scheme

Statements phrased using this module (40)