Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_GaloisRep_ResidualEquiv.lean

definition module

Equivalence of residual Galois representations, and base change

Fix a field k and two residual Galois representations \rho_1,\rho_2 over k, i.e. two terms of the project's own type ResidualGaloisRep k (defined in the imported module, and whose data is used here through the carrier ρ.V, a k-module, and the assignment ρ.ρ sending each \mathbb{Q}-algebra automorphism \sigma of AlgebraicClosure ℚ to a k-linear map on ρ.V). The structure ResidualGaloisRep.Equiv ρ₁ ρ₂ packages an intertwining isomorphism as data: a field toLinearEquiv, which is a k-linear equivalence e : \rho_1.V \simeq \rho_2.V, together with a field map_apply asserting the intertwining relation in pointwise form, e(\rho_1(\sigma)x) = \rho_2(\sigma)(e\,x) for every \sigma in the Galois group as spelled above and every x \in \rho_1.V. Thus the theorem-like condition is carried as a field of the structure, and an Equiv is a chosen isomorphism rather than the mere assertion that one exists. The latter is the separate proposition ResidualGaloisRep.IsEquiv ρ₁ ρ₂, defined as Nonempty (Equiv ρ₁ ρ₂).

The remaining declarations are the groupoid operations: Equiv.refl (the identity linear equivalence), Equiv.symm (the inverse linear equivalence, whose intertwining property is obtained by applying injectivity of e), and Equiv.trans (composition), so that IsEquiv is reflexive, symmetric and transitive, although no Equiv-relation instance is registered here. Finally Equiv.baseChangeAlong transports an equivalence along a ring homomorphism \psi : k \to k' of fields: regarding k' as a k-algebra via \psi, it produces an equivalence between the base-changed representations ρ₁.baseChangeAlong ψ and ρ₂.baseChangeAlong ψ, with underlying map e \otimes \mathrm{id} (Mathlib's LinearEquiv.baseChange), the intertwining relation being checked on pure tensors and extended additively. Nothing else is declared.

Relation to Mathlib

Mathlib has no type of residual Galois representations, so this notion of equivalence between them is the project's own; its underlying maps are Mathlib's LinearEquiv, and the base-change construction is built from Mathlib's LinearEquiv.baseChange and LinearMap.baseChange.

Where it is used

This is the single notion in which statements comparing residual representations are phrased: that the mod-\mathfrak{m} representation attached to a modular form and the mod-p representation of an elliptic curve agree (after extension of the coefficient field, via Equiv.baseChangeAlong), and that the reduction of a deformation is the given residual representation. It is imported by the great majority of the statement modules on the Galois side of the argument.

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. J.-P. Serre, Sur les représentations modulaires de degré 2 de \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}), Duke Mathematical Journal 54 (1987), 179–230

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

Imports

Imported by

Declarations

Source

import Definitions.Def_GaloisRep_Residual

open scoped TensorProduct

namespace ResidualGaloisRep

variable {k : Type} [Field k]

structure Equiv (ρ₁ ρ₂ : ResidualGaloisRep k) where

  toLinearEquiv : ρ₁.V ≃ₗ[k] ρ₂.V

  map_apply : ∀ (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) (x : ρ₁.V),
    toLinearEquiv (ρ₁.ρ σ x) = ρ₂.ρ σ (toLinearEquiv x)

def IsEquiv (ρ₁ ρ₂ : ResidualGaloisRep k) : Prop :=
  Nonempty (Equiv ρ₁ ρ₂)

namespace Equiv

def refl (ρ : ResidualGaloisRep k) : Equiv ρ ρ where
  toLinearEquiv := LinearEquiv.refl k ρ.V
  map_apply _ _ := rfl

def symm {ρ₁ ρ₂ : ResidualGaloisRep k} (e : Equiv ρ₁ ρ₂) : Equiv ρ₂ ρ₁ where
  toLinearEquiv := e.toLinearEquiv.symm
  map_apply σ x := by
    apply e.toLinearEquiv.injective
    rw [e.map_apply, LinearEquiv.apply_symm_apply, LinearEquiv.apply_symm_apply]

def trans {ρ₁ ρ₂ ρ₃ : ResidualGaloisRep k} (e₁₂ : Equiv ρ₁ ρ₂) (e₂₃ : Equiv ρ₂ ρ₃) :
    Equiv ρ₁ ρ₃ where
  toLinearEquiv := e₁₂.toLinearEquiv.trans e₂₃.toLinearEquiv
  map_apply σ x := by
    rw [LinearEquiv.trans_apply, e₁₂.map_apply, e₂₃.map_apply, LinearEquiv.trans_apply]

noncomputable def baseChangeAlong {k' : Type} [Field k'] (ψ : k →+* k')
    {ρ₁ ρ₂ : ResidualGaloisRep k} (e : Equiv ρ₁ ρ₂) :
    Equiv (ρ₁.baseChangeAlong ψ) (ρ₂.baseChangeAlong ψ) :=
  letI : Algebra k k' := ψ.toAlgebra
  { toLinearEquiv := e.toLinearEquiv.baseChange k k' ρ₁.V ρ₂.V
    map_apply := fun σ x => by
      show e.toLinearEquiv.baseChange k k' ρ₁.V ρ₂.V ((ρ₁.ρ σ).baseChange k' x) =
        (ρ₂.ρ σ).baseChange k' (e.toLinearEquiv.baseChange k k' ρ₁.V ρ₂.V x)
      induction x using TensorProduct.induction_on with
      | zero => simp only [map_zero]
      | tmul b v =>
        rw [LinearMap.baseChange_tmul, LinearEquiv.baseChange_tmul, LinearEquiv.baseChange_tmul,
          LinearMap.baseChange_tmul, e.map_apply]
      | add x y hx hy => simp only [map_add, hx, hy] }

end Equiv

end ResidualGaloisRep

Statements phrased using this module (65)