Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_Deformations_LocalSplitting.lean

definition module

Eigen-idempotents of a matrix over a commutative ring

Let A be a commutative ring and write \mathrm{M}_2(A) for 2\times 2 matrices over A. The module introduces a predicate TaylorWiles.IsEigenIdempotent M a b e, for M, e \in \mathrm{M}_2(A) and a, b \in A, recorded as a structure in Prop with four fields: idem, asserting e \cdot e = e; trace_eq_one, asserting \operatorname{tr}(e) = 1; mul_left, asserting M e = a \cdot e (scalar action of a on the matrix e); and mul_right, asserting M(1 - e) = b\,(1 - e), with 1 the identity matrix. Thus e is an idempotent of trace 1 for which M acts by the scalar a on the image of e and by b on the image of the complementary idempotent 1 - e. Note that the pair (a,b) is ordered: if e satisfies the conditions for (a,b), then 1 - e satisfies them for (b,a), and the two conditions are in general different.

Secondly, for M \in \mathrm{M}_2(A) and b, v \in A, the matrix TaylorWiles.eigenIdempotent M b v is defined to be v \cdot (M - b \cdot 1), that is, the scalar v times M minus b times the identity; this is a candidate for an eigen-idempotent in the above sense, the intended value of v being the inverse of the difference a - b of the two eigenvalues. The accompanying lemma eigenIdempotent_def states this defining equality. No relation between the predicate and the explicit matrix is asserted in this module; verifying that v \cdot (M - b\cdot 1) satisfies IsEigenIdempotent under suitable hypotheses on a, b, v and the characteristic polynomial of M is the business of later results.

Relation to Mathlib

Mathlib has no notion of an eigen-idempotent attached to an ordered pair of eigenvalues of a 2\times2 matrix; both the predicate and the explicit matrix are the project's own, formulated for Mathlib's Matrix (Fin 2) (Fin 2) A.

Where it is used

These definitions serve the splitting of a two-dimensional local situation at an auxiliary Taylor–Wiles prime q, where a matrix (the image of a Frobenius element, or a Hecke operator) has two eigenvalues that are distinct modulo the maximal ideal: the idempotent of trace 1 attached to the ordered pair isolates one of the two diagonal characters, and the ordering convention fixed here is used consistently downstream.

References

  1. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154, §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_Deformations_LocalSplitting.lean

Declarations

Source

import Mathlib

set_option autoImplicit false

open Module

namespace TaylorWiles

variable {A : Type*} [CommRing A]

local notation "M₂ " A => Matrix (Fin 2) (Fin 2) A

structure IsEigenIdempotent (M : M₂ A) (a b : A) (e : M₂ A) : Prop where

  idem : e * e = e

  trace_eq_one : e.trace = 1

  mul_left : M * e = a • e

  mul_right : M * ((1 : M₂ A) - e) = b • ((1 : M₂ A) - e)

def eigenIdempotent (M : M₂ A) (b v : A) : M₂ A := v • (M - b • (1 : M₂ A))

theorem eigenIdempotent_def (M : M₂ A) (b v : A) :
    eigenIdempotent M b v = v • (M - b • (1 : M₂ A)) := rfl

end TaylorWiles

Statements phrased using this module (2)