Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_NeronModelInfra_TopFormOrder.lean

definition module

Integral top forms and order along a discrete valuation ring

Throughout, R' \to K' and R' \to O \to F are commutative rings with F simultaneously a K'-algebra and an O-algebra, compatibly with the maps from R', and d : \mathbb{N}. The helper moduleAlong records the O-module structure obtained on an F-module by restriction along \operatorname{algebraMap} O F; it is used to regard \bigwedge^d_F \Omega_{F/K'} as an O-module. With that structure, ιMultiAlong is the O-multilinear alternating map in d arguments sending (\omega_1,\dots,\omega_d) \in (\Omega_{O/R'})^d to the wedge of the images of the \omega_i under the functoriality map \Omega_{O/R'} \to \Omega_{F/K'} attached to R' \to K', O \to F, and topFormMap is the induced O-linear map \bigwedge^d_O \Omega_{O/R'} \to \bigwedge^d_F \Omega_{F/K'} obtained from it by the universal property of the exterior power. Its range is integralTopForms, the O-submodule of integral top forms inside \bigwedge^d_F \Omega_{F/K'}.

In the second section O is in addition a discrete valuation domain and L a fraction field of O, again a K'-algebra compatibly over R'. Here maximalSpectrum packages the maximal ideal of O as a point of the height-one spectrum, and addOrd is the induced normalised additive valuation L \to \mathbb{Z}: for a \neq 0 it is the negative of the additive form of the multiplicative valuation of a at that point, and 0 is sent to 0. Finally ord assigns to \omega \in \bigwedge^d_L \Omega_{L/K'} an integer: if some \rho generates integralTopForms as an O-module and \omega = a \cdot \rho for some a \in L, then ord \omega is addOrd of such a chosen a (chosen classically), and otherwise it is the junk value 0; so ord is a genuine order only when the lattice of integral top forms is free of rank one, and independence of the choices is a separate matter. Two lemmas fix the normalisation: if the maximal ideal of O is generated by \varpi, then addOrd of the image of \varpi in L is 1, and of its square is 2.

Relation to Mathlib

Mathlib supplies the ingredients — Kähler differentials with their functoriality KaehlerDifferential.map, exterior powers with exteriorPower.ιMulti and exteriorPower.alternatingMapLinearEquiv, and the valuation attached to a point of IsDedekindDomain.HeightOneSpectrum — while the lattice of integral top forms and the resulting order of a top form along a discrete valuation ring are the project's own notions.

Where it is used

This is the ring-theoretic form of the order of a section of a line bundle on the generic fibre at a generic point of the special fibre, as in the theory of Néron models: all the objects involved are the discrete valuation rings sitting inside a function field, so comparisons between models and base-change statements can be phrased in commutative algebra. It underlies the Néron-model infrastructure used for the elliptic curves occurring in the Frey-curve argument.

References

  1. S. Bosch, W. Lütkebohmert and M. Raynaud, Néron Models, Ergebnisse der Mathematik und ihrer Grenzgebiete (3) 21, Springer, 1990, §4.3

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_NeronModelInfra_TopFormOrder.lean

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib

set_option autoImplicit false

noncomputable section

universe u

open scoped TensorProduct

namespace NeronModelInfra.TopFormOrder

variable (R' K' O F : Type u) [CommRing R'] [CommRing K'] [Algebra R' K']
  [CommRing O] [Algebra R' O] [CommRing F] [Algebra O F] [Algebra K' F] [Algebra R' F]
  [IsScalarTower R' O F] [IsScalarTower R' K' F] (d : ℕ)

@[reducible] def moduleAlong (N : Type u) [AddCommGroup N] [Module F N] : Module O N :=
  Module.compHom N (algebraMap O F)

set_option backward.isDefEq.respectTransparency false in
def ιMultiAlong :
    letI := moduleAlong O F (⋀[F]^d (Ω[F⁄K']))
    (Ω[O⁄R']) [⋀^Fin d]→ₗ[O] (⋀[F]^d (Ω[F⁄K'])) :=
  letI := moduleAlong O F (⋀[F]^d (Ω[F⁄K']))
  haveI : IsScalarTower O F (⋀[F]^d (Ω[F⁄K'])) := IsScalarTower.of_algebraMap_smul fun _ _ => rfl
  { ((exteriorPower.ιMulti F d (M := Ω[F⁄K'])).toMultilinearMap.restrictScalars O).compLinearMap
      (fun _ => KaehlerDifferential.map R' K' O F) with
    map_eq_zero_of_eq' := fun v i j h hij =>
      (exteriorPower.ιMulti F d (M := Ω[F⁄K'])).map_eq_zero_of_eq _ (by simp [h]) hij }

def topFormMap :
    letI := moduleAlong O F (⋀[F]^d (Ω[F⁄K']))
    ⋀[O]^d (Ω[O⁄R']) →ₗ[O] ⋀[F]^d (Ω[F⁄K']) :=
  letI := moduleAlong O F (⋀[F]^d (Ω[F⁄K']))
  exteriorPower.alternatingMapLinearEquiv (ιMultiAlong R' K' O F d)

def integralTopForms :
    letI := moduleAlong O F (⋀[F]^d (Ω[F⁄K']))
    Submodule O (⋀[F]^d (Ω[F⁄K'])) :=
  letI := moduleAlong O F (⋀[F]^d (Ω[F⁄K']))
  LinearMap.range (topFormMap R' K' O F d)

section Order

variable [IsDomain O] [IsDiscreteValuationRing O]
variable (L : Type u) [Field L] [Algebra O L] [IsFractionRing O L] [Algebra K' L] [Algebra R' L]
  [IsScalarTower R' O L] [IsScalarTower R' K' L]

open IsDedekindDomain IsLocalRing in

def maximalSpectrum : HeightOneSpectrum O :=
  ⟨maximalIdeal O, inferInstance, IsDiscreteValuationRing.not_a_field O⟩

open IsDedekindDomain in

def addOrd (a : L) : ℤ :=
  open scoped Classical in
  if h : a = 0 then 0
  else -(Multiplicative.toAdd (WithZero.unzero
    (((maximalSpectrum O).valuation L).ne_zero_iff.mpr h)))

def ord (ω : ⋀[L]^d (Ω[L⁄K'])) : ℤ :=
  open scoped Classical in
  letI := moduleAlong O L (⋀[L]^d (Ω[L⁄K']))
  if h : ∃ ρ : ⋀[L]^d (Ω[L⁄K']), integralTopForms R' K' O L d = Submodule.span O {ρ} ∧ ∃ a : L, ω = a • ρ
  then addOrd O L (a := h.choose_spec.2.choose)
  else 0

omit K' d in

theorem addOrd_uniformizer (ϖ : O) (hϖ : IsLocalRing.maximalIdeal O = Ideal.span {ϖ}) :
    addOrd O L (algebraMap O L ϖ) = 1 := by
  have hϖ0 : ϖ ≠ 0 := by
    intro h; apply IsDiscreteValuationRing.not_a_field O; simpa [h] using hϖ
  have hne : algebraMap O L ϖ ≠ 0 := by
    simpa using (IsFractionRing.injective O L).ne hϖ0
  unfold addOrd
  rw [dif_neg hne]
  have hv : (maximalSpectrum O).valuation L (algebraMap O L ϖ) = Multiplicative.ofAdd (-1 : ℤ) := by
    rw [IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap]
    exact (maximalSpectrum O).intValuation_singleton hϖ0 hϖ
  have : WithZero.unzero (((maximalSpectrum O).valuation L).ne_zero_iff.mpr hne) =
      Multiplicative.ofAdd (-1 : ℤ) := by
    apply WithZero.coe_injective
    rw [WithZero.coe_unzero, hv]
  rw [this]; simp

omit K' d in

theorem addOrd_uniformizer_sq (ϖ : O) (hϖ : IsLocalRing.maximalIdeal O = Ideal.span {ϖ}) :
    addOrd O L (algebraMap O L ϖ ^ 2) = 2 := by
  have hϖ0 : ϖ ≠ 0 := by
    intro h; apply IsDiscreteValuationRing.not_a_field O; simpa [h] using hϖ
  have hne : algebraMap O L ϖ ≠ 0 := by
    simpa using (IsFractionRing.injective O L).ne hϖ0
  have hne2 : algebraMap O L ϖ ^ 2 ≠ 0 := pow_ne_zero 2 hne
  unfold addOrd
  rw [dif_neg hne2]
  have hv : (maximalSpectrum O).valuation L (algebraMap O L ϖ ^ 2) = Multiplicative.ofAdd (-2 : ℤ) := by
    rw [map_pow, IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap,
      (maximalSpectrum O).intValuation_singleton hϖ0 hϖ]; rfl
  have : WithZero.unzero (((maximalSpectrum O).valuation L).ne_zero_iff.mpr hne2) =
      Multiplicative.ofAdd (-2 : ℤ) := by
    apply WithZero.coe_injective
    rw [WithZero.coe_unzero, hv]
  rw [this]; simp

end Order

end NeronModelInfra.TopFormOrder

end

/-- info: 'NeronModelInfra.TopFormOrder.addOrd_uniformizer' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in
#print axioms NeronModelInfra.TopFormOrder.addOrd_uniformizer

Statements phrased using this module (35)