Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_GaloisRep_GlobalUnramifiedAt.lean

definition module

Unramifiedness at a rational prime for global Galois representations

For a field extension L/K and a monoid G, this module defines when a monoid homomorphism \rho \colon (L \simeq_{\mathrm{alg}[K]} L) \to G out of the group of K-algebra automorphisms of L is unramified at a natural number q. The definition GlobalGaloisRep.IsUnramifiedAt reads: for every valuation subring A of L satisfying A.LiesOverPrime q — that is, with the image of q in L a non-unit of A, equivalently q \in \mathfrak{m}_A — the subgroup A.inertiaSubgroupIn K is contained in the kernel of \rho. Here A.inertiaSubgroupIn K is the subgroup of K-automorphisms of L obtained as the image of Mathlib's inertia subgroup of A (a subgroup of the decomposition subgroup of A over K) under the inclusion of that decomposition subgroup into the whole automorphism group; so its elements are the K-automorphisms preserving A and inducing the identity on the residue field of A. The condition is thus a universally quantified statement over all places of L above q, formulated with valuation subrings of L rather than with completions or with a choice of embedding of a local Galois group.

The accompanying lemma GlobalGaloisRep.isUnramifiedAt_iff restates the definition in pointwise form: \rho is unramified at q if and only if for every valuation subring A of L lying over q and every \sigma in A.inertiaSubgroupIn K one has \rho(\sigma) = 1. Note that no hypothesis forces q to be prime, nor L/K to be normal or algebraic; these are conditions imposed by the users of the predicate.

Relation to Mathlib

Mathlib provides the decomposition and inertia subgroups of a valuation subring; the project adds ValuationSubring.inertiaSubgroupIn, the image of the inertia subgroup inside the full group of K-algebra automorphisms, and the predicates ValuationSubring.LiesOverPrime and GlobalGaloisRep.IsUnramifiedAt, which Mathlib does not have. Galois representations here are bare MonoidHoms out of L \simeq_{\mathrm{alg}[K]} L, with no bundled representation type.

Where it is used

This is the language in which ramification hypotheses on global mod-p representations are stated in the project, in particular the assertion that the mod-p representation attached to the Frey curve is unramified outside 2p, which is an input to level lowering. A parallel predicate for the n-torsion of a Weierstrass curve, WeierstrassCurve.Affine.Point.GaloisRepUnramifiedAt, and its specialisation FreyPackage.GaloisRepUnramifiedAt to the Frey curve over \mathbb{Q} inside \overline{\mathbb{Q}}, are defined in the imported ramification module in the same style.

References

  1. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154, §2
  2. J.-P. Serre, Local Fields, Graduate Texts in Mathematics 67, Springer, 1979, Ch. I, §7
  3. O. Zariski and P. Samuel, Commutative Algebra II, Van Nostrand, 1960

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

Imports

Imported by

Declarations

Source

import Definitions.Def_FLTPrelim_Ramification

set_option autoImplicit false

namespace GlobalGaloisRep

variable {K L : Type*} [Field K] [Field L] [Algebra K L]

def IsUnramifiedAt {G : Type*} [Monoid G] (ρ : (L ≃ₐ[K] L) →* G) (q : ℕ) : Prop :=
  ∀ A : ValuationSubring L, A.LiesOverPrime q → A.inertiaSubgroupIn K ≤ ρ.ker

lemma isUnramifiedAt_iff {G : Type*} [Monoid G] {ρ : (L ≃ₐ[K] L) →* G} {q : ℕ} :
    IsUnramifiedAt ρ q ↔
      ∀ A : ValuationSubring L, A.LiesOverPrime q →
        ∀ σ : L ≃ₐ[K] L, σ ∈ A.inertiaSubgroupIn K → ρ σ = 1 :=
  Iff.rfl

end GlobalGaloisRep

Statements phrased using this module (4)