Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_Module_CommFamilyAnnPart.lean

definition module

Commuting endomorphism families and their annihilator parts

Fix a commutative ring K, a K-module V and an index type \sigma. The structure Module.End.CommFamily K V \sigma bundles a family T : \sigma \to Module.End K V together with a proof field comm asserting that T_a and T_b commute for all a,b \in \sigma; thus the commutativity theorem is carried as part of the data. For such a family F, adjoin is the K-subalgebra \mathrm{Algebra.adjoin}\,K\,(\mathrm{range}\,F.T) of \operatorname{End}_K(V) generated by the operators; isMulCommutative_adjoin records that this subalgebra is commutative (generators commute), and commRing_adjoin upgrades its ring structure to a CommRing instance. gen a is T_a regarded as an element of that subalgebra, and eval is the K-algebra homomorphism \mathrm{MvPolynomial}\,\sigma\,K \to \operatorname{End}_K(V) obtained by evaluating at the generators inside adjoin and then including into \operatorname{End}_K(V); eval_X, eval_C, commute_eval_T and eval_mem_adjoin state that X_a \mapsto T_a, that constants go to scalars, that every value commutes with each T_a, and that all values lie in adjoin.

The second definition assumes a prime p with \operatorname{char} K = p and a system of scalars \theta : \sigma \to K. Writing \iota : \mathbb{Z}/p \to K for the canonical ring homomorphism and Q^\iota for the coefficientwise image of Q \in (\mathbb{Z}/p)[X_a : a \in \sigma], the submodule F.\mathrm{annPart}\,p\,\theta \;=\; \bigcap_{\substack{Q \in (\mathbb{Z}/p)[X_\sigma]\\ Q^\iota(\theta)=0}} \ker\bigl(\mathrm{eval}(Q^\iota)\bigr) is formed as an infimum of kernels in the lattice of K-submodules of V, the index ranging over prime-field polynomials Q together with a proof that Q^\iota vanishes at \theta. The companion lemma mem_annPart_iff rewrites membership pointwise: v lies in the part exactly when \mathrm{eval}(Q^\iota)\,v = 0 for every such Q. So the cutting conditions are indexed by the ideal of polynomials with coefficients in the prime field that kill \theta, rather than by the K-linear conditions T_a v = \theta_a v.

Relation to Mathlib

The ingredients — Algebra.adjoin, MvPolynomial.aeval, ZMod.castHom and the submodule lattice — are Mathlib's; the bundled structure of a pairwise commuting family of endomorphisms and the annihilator part annPart attached to a system of scalars in characteristic p are the project's own.

Where it is used

The family structure packages the simultaneous action of a commuting system of operators (Hecke operators on a space of forms or on a cohomology module) in characteristic p, and annPart isolates the subspace annihilated by all prime-field polynomial relations satisfied by a prescribed system of eigenvalues \theta. Several later modules of the development work with this part when passing between eigenvalue systems mod p and the operators acting on them.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_Module_CommFamilyAnnPart.lean

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib

set_option autoImplicit false
set_option synthInstance.maxHeartbeats 400000
set_option maxHeartbeats 800000

namespace Module.End

variable (K : Type*) [CommRing K] (V : Type*) [AddCommGroup V] [Module K V] (σ : Type*)

structure CommFamily where

  T : σ → Module.End K V

  comm : ∀ a b : σ, Commute (T a) (T b)

variable {K V σ}

namespace CommFamily

variable (F : CommFamily K V σ)

def adjoin : Subalgebra K (Module.End K V) := Algebra.adjoin K (Set.range F.T)

theorem isMulCommutative_adjoin : IsMulCommutative F.adjoin := by
  refine Algebra.isMulCommutative_adjoin K ?_
  rintro x ⟨a, rfl⟩ y ⟨b, rfl⟩
  exact F.comm a b

instance commRing_adjoin : CommRing F.adjoin where
  __ := (inferInstance : Ring F.adjoin)
  mul_comm a b := F.isMulCommutative_adjoin.is_comm.comm a b

def gen (a : σ) : F.adjoin := ⟨F.T a, Algebra.subset_adjoin (Set.mem_range_self a)⟩

@[simp] theorem coe_gen (a : σ) : (F.gen a : Module.End K V) = F.T a := rfl

noncomputable def eval : MvPolynomial σ K →ₐ[K] Module.End K V :=
  F.adjoin.val.comp (MvPolynomial.aeval F.gen)

theorem eval_apply (Q : MvPolynomial σ K) : F.eval Q = (MvPolynomial.aeval F.gen Q : F.adjoin) := rfl

@[simp] theorem eval_X (a : σ) : F.eval (MvPolynomial.X a) = F.T a := by
  rw [eval_apply, MvPolynomial.aeval_X, coe_gen]

@[simp] theorem eval_C (c : K) : F.eval (MvPolynomial.C c) = algebraMap K (Module.End K V) c :=
  F.eval.commutes c

theorem commute_eval_T (Q : MvPolynomial σ K) (a : σ) : Commute (F.eval Q) (F.T a) := by
  have h := mul_comm (MvPolynomial.aeval F.gen Q : F.adjoin) (F.gen a)
  show F.eval Q * F.T a = F.T a * F.eval Q
  rw [F.eval_apply, ← F.coe_gen a, ← Subalgebra.coe_mul, ← Subalgebra.coe_mul, h]

theorem eval_mem_adjoin (Q : MvPolynomial σ K) : F.eval Q ∈ F.adjoin :=
  (MvPolynomial.aeval F.gen Q).2

noncomputable def annPart (p : ℕ) [Fact p.Prime] [CharP K p] (θ : σ → K) : Submodule K V :=
  ⨅ (Q : MvPolynomial σ (ZMod p))
    (_ : MvPolynomial.aeval θ (MvPolynomial.map (ZMod.castHom (dvd_refl p) K) Q) = 0),
    LinearMap.ker (F.eval (MvPolynomial.map (ZMod.castHom (dvd_refl p) K) Q))

theorem mem_annPart_iff (p : ℕ) [Fact p.Prime] [CharP K p] (θ : σ → K) (v : V) :
    v ∈ F.annPart p θ ↔ ∀ Q : MvPolynomial σ (ZMod p),
      MvPolynomial.aeval θ (MvPolynomial.map (ZMod.castHom (dvd_refl p) K) Q) = 0 →
        F.eval (MvPolynomial.map (ZMod.castHom (dvd_refl p) K) Q) v = 0 := by
  simp only [annPart, Submodule.mem_iInf, LinearMap.mem_ker]

end CommFamily

end Module.End

Statements phrased using this module (3)