Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_Representation_AbsolutelyIrreducible.lean

definition moduleadapted from the Imperial College London FLT project: FLT/Mathlib/RepresentationTheory/Basic.lean

Base change and absolute irreducibility of representations

Two notions are introduced for abstract representations of a group. First, for a commutative ring R, an R-module V, a group G and a representation \rho : G \to \mathrm{GL}_R(V) (in Mathlib's sense, a monoid homomorphism from G to V \to_{\ell} V units), and for any commutative R-algebra R', Representation.baseChange R' ρ is the representation of G on R' \otimes_R V which sends g to the R'-linear extension \mathrm{id}_{R'} \otimes \rho(g) of \rho(g); multiplicativity and preservation of the identity are inherited from \rho. The scoped notation R' ⊗ᵣ' ρ denotes this representation. Second, for a field k and a representation \rho of G on a k-module W, the class Representation.IsAbsolutelyIrreducible ρ is a Prop-valued structure with a single field: for every type k' in a fixed universe u (a universe parameter of the class itself), every field structure on k' and every k-algebra structure on k', the base-changed representation k' \otimes_k \rho of G on k' \otimes_k W is irreducible in the sense of Mathlib's IsIrreducible. Thus absolute irreducibility is phrased as stability of irreducibility under arbitrary field extensions of k, the field structure and the algebra structure being quantified over rather than fixed, so that a single type may be used with several k-algebra structures; the quantification ranges over fields whose carrier lies in the universe u.

Relation to Mathlib

Built on Mathlib's Representation.IsIrreducible and LinearMap.baseChange; the base change of a representation and the predicate of absolute irreducibility are defined here rather than taken from Mathlib.

Where it is used

These notions are the ambient form of absolute irreducibility used in the representation-theoretic parts of the argument, notably the Brauer–Nesbitt type results and the Taylor–Wiles patching input, where absolute irreducibility of a residual representation is the standing hypothesis; the two-dimensional residual Galois case is treated by a separate, specialised predicate.

References

  1. C. W. Curtis and I. Reiner, Representation Theory of Finite Groups and Associative Algebras, Pure and Applied Mathematics XI, Interscience, 1962, §29
  2. 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_Representation_AbsolutelyIrreducible.lean

Declarations

Source

import Mathlib.RepresentationTheory.Irreducible ↗
import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs ↗

set_option autoImplicit false

section

open LinearMap
open scoped TensorProduct

namespace Representation

universe u

variable {R V G : Type*} [CommRing R] [AddCommMonoid V] [Module R V] [Group G]

noncomputable def baseChange (R' : Type*) [CommRing R'] [Algebra R R'] (ρ : Representation R G V)
    : Representation R' G (R' ⊗[R] V) where
  toFun g := LinearMap.baseChange R' (ρ g)
  map_one' := by aesop
  map_mul' := by aesop

scoped notation R' "⊗ᵣ'" ρ => baseChange R' ρ

variable {k : Type*} [Field k] {W : Type*} [AddCommMonoid W] [Module k W]

class IsAbsolutelyIrreducible (ρ : Representation k G W) : Prop where
  absolutelyIrreducible :
    ∀ k' : Type u, ∀ _ : Field k', ∀ _ : Algebra k k', IsIrreducible (k' ⊗ᵣ' ρ)

end Representation

end

Statements phrased using this module (12)