Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_GaloisRep_RatLocalizedAtResidue.lean

definition module

The residue homomorphism from onto

Fix a natural number q carrying the instance Fact q.Prime. The subring ratLocalizedAt q of \mathbb{Q} consists of those rationals whose denominator is coprime to q, i.e. the localisation \mathbb{Z}_{(q)} of \mathbb{Z} at the prime (q) realised concretely inside \mathbb{Q}. Three things are recorded here. First, an instance stating that the ideal (q)\subseteq\mathbb{Z} generated by the integer q is prime; this is deduced from primality of q in \mathbb{Z}, which in turn follows from primality of q as a natural number. Second, ratLocalizedAtResidue q, a ring homomorphism \mathbb{Z}_{(q)} \to \mathbb{Z}/q. It is obtained by universality of localisation: ratLocalizedAt q is a localisation of \mathbb{Z} at the complement of the prime (q) (the theorem GaloisRep.isLocalization_ratLocalizedAt supplies this), and the reduction map \mathbb{Z}\to\mathbb{Z}/q carries every element outside (q) to a unit, since \mathbb{Z}/q is a field and an integer reduces to 0 exactly when it is divisible by q. Concretely, the map sends a/b with \gcd(b,q)=1 to \bar a\,\bar b^{-1}. Third, the induced algebra structure instAlgebraRatLocalizedAtZMod, making \mathbb{Z}/q an algebra over ratLocalizedAt q via this residue map. Two subsidiary statements record that, with this instance in place, \mathbb{Z}_{(q)}-algebra structure on AlgebraicClosure (ZMod q) and the scalar tower \mathbb{Z}_{(q)} \to \mathbb{Z}/q \to \overline{\mathbb{Z}/q} are available automatically.

Relation to Mathlib

ratLocalizedAt is the project's concrete model of \mathbb{Z}_{(q)} as a subring of \mathbb{Q} rather than Mathlib's abstract Localization; the residue map is constructed from Mathlib's IsLocalization.lift applied to the reduction homomorphism \mathbb{Z}\to\mathbb{Z}/q.

Where it is used

The flat local condition at a prime p used in the deformation-theoretic part of the argument is phrased in terms of finite flat cocommutative Hopf algebras over ratLocalizedAt p. Working with points of such Hopf algebras in characteristic p requires \mathbb{Z}_{(p)}-algebra structures on \mathbb{Z}/p and on its algebraic closure, which this module supplies.

References

  1. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154

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

Imports

Theorems imported by this definition module

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_GaloisRep_Flat
import Theorems.Thm_GaloisRep_isLocalization_ratLocalizedAt

namespace GaloisRep

noncomputable section

instance ratLocalizedAt.span_isPrime (q : ℕ) [Fact q.Prime] : (Ideal.span {(q : ℤ)}).IsPrime := by
  have hq : Prime (q : ℤ) := by
    rw [Int.prime_iff_natAbs_prime]
    simpa using (Fact.out : q.Prime)
  exact (Ideal.span_singleton_prime hq.ne_zero).mpr hq

def ratLocalizedAtResidue (q : ℕ) [Fact q.Prime] : ↥(ratLocalizedAt q) →+* ZMod q :=
  haveI := GaloisRep.isLocalization_ratLocalizedAt (p := q) Fact.out
  IsLocalization.lift (M := (Ideal.span {(q : ℤ)}).primeCompl) (S := ↥(ratLocalizedAt q))
    (g := Int.castRingHom (ZMod q))
    (fun y => by
      refine isUnit_iff_ne_zero.mpr ?_
      simp only [Int.coe_castRingHom, Ne, ZMod.intCast_zmod_eq_zero_iff_dvd]
      intro h
      exact y.2 (Ideal.mem_span_singleton.mpr (by exact_mod_cast h)))

instance instAlgebraRatLocalizedAtZMod (q : ℕ) [Fact q.Prime] :
    Algebra ↥(ratLocalizedAt q) (ZMod q) :=
  (ratLocalizedAtResidue q).toAlgebra

example (q : ℕ) [Fact q.Prime] : Algebra ↥(ratLocalizedAt q) (AlgebraicClosure (ZMod q)) :=
  inferInstance
example (q : ℕ) [Fact q.Prime] :
    IsScalarTower ↥(ratLocalizedAt q) (ZMod q) (AlgebraicClosure (ZMod q)) :=
  inferInstance

end

end GaloisRep

Statements phrased using this module (44)