Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_LocalNewvector_AdelicSpanCarrier.lean

definition module

Adelic function carrier and its -orbit span

For a number field F, LocalNewvector.AdelicFnCarrier F is the space of all complex-valued functions on the adelic group AdelicGL2 (π“ž F) F, introduced as a type synonym with mk and toFn the identity passages in the two directions, and equipped with the pointwise additive group and \mathbb{C}-module structures and with the right-translation action of AdelicGL2 (π“ž F) F given by (g\cdot\varphi)(x)=\varphi(xg); this action commutes with scalars in both directions. No automorphy, integrability or smoothness condition is imposed on the carrier: such conditions appear only as hypotheses on individual functions. For \varphi : AdelicGL2 (π“ž F) F \to\mathbb{C}, AdelicSpanSubmodule Ο† is the \mathbb{C}-span of the right-translation orbit \{g\cdot\varphi\}, shown to be stable under the group action, and AdelicSpan Ο† is that submodule viewed as a type, again with its module structure, the induced action of AdelicGL2 (π“ž F) F and the commuting-scalar properties. The distinguished element AdelicSpan.self Ο† is \varphi itself inside the span, and it is nonzero whenever \varphi is; adelicSpan_self_one_ne_zero records this for the constant function 1.

Over F=\mathbb{Q} and for a prime p, both AdelicFnCarrier β„š and each AdelicSpan Ο† are given an action of GL_2(\mathbb{Q}_p) obtained by composing the global action with the monoid homomorphism AdelicDock.padicToAdelic p, which places a local matrix at the place of \mathbb{Q} above p and the identity elsewhere; padic_smul_def states this on the nose, and the commuting-scalar properties are supplied. Two reflexivity statements record that, with these structures in place, HasNewvectorConductor p (AdelicSpan Ο†) c β€” the condition that the vectors fixed by K_1(p^c) are nonzero while those fixed by K_1(p^m) vanish for all m<c β€” and the fixed submodule fixedSubmodule (padicK1 p n) (AdelicSpan Ο†) are well formed for the orbit span.

Relation to Mathlib

Mathlib has no automorphic-function carrier of this kind, nor the newvector/conductor vocabulary; AdelicFnCarrier is a type synonym for the Pi type AdelicGL2 (π“ž F) F β†’ β„‚ whose module and action structures are transported from it, and AdelicSpan Ο† likewise a synonym for a Submodule β„‚.

Where it is used

These carriers let the local newvector vocabulary (conductor of a K_1(p^n)-fixed vector, fixed submodules) be applied to the GL_2(\mathbb{A})-orbit span of a single adelic function, which is how the automorphic side of the modularity statements is packaged in this development.

References

  1. W. Casselman, On some results of Atkin and Lehner, Mathematische Annalen 201 (1973), 301–314
  2. D. Bump, Automorphic Forms and Representations, Cambridge Studies in Advanced Mathematics 55, Cambridge University Press, 1997

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_AutomorphicForm_AutomorphicFnAt
import Definitions.Def_LocalNewvector_ConductorDatum
import Definitions.Def_AdelicDock_LocalEmbedding

open NumberField MeasureTheory AutomorphicForm

noncomputable section

namespace LocalNewvector

variable (F : Type*) [Field F] [NumberField F]

def AdelicFnCarrier : Type _ :=
  AdelicGL2 (π“ž F) F β†’ β„‚

namespace AdelicFnCarrier

variable {F}

def mk (Ο† : AdelicGL2 (π“ž F) F β†’ β„‚) : AdelicFnCarrier F := Ο†

def toFn (Ο† : AdelicFnCarrier F) : AdelicGL2 (π“ž F) F β†’ β„‚ := Ο†

@[simp] theorem toFn_mk (Ο† : AdelicGL2 (π“ž F) F β†’ β„‚) : (mk Ο†).toFn = Ο† := rfl

@[simp] theorem mk_toFn (Ο† : AdelicFnCarrier F) : mk Ο†.toFn = Ο† := rfl

@[ext] theorem ext {Ο† ψ : AdelicFnCarrier F} (h : βˆ€ g, Ο†.toFn g = ψ.toFn g) : Ο† = ψ :=
  funext h

instance : AddCommGroup (AdelicFnCarrier F) :=
  inferInstanceAs (AddCommGroup (AdelicGL2 (π“ž F) F β†’ β„‚))

instance : Module β„‚ (AdelicFnCarrier F) :=
  inferInstanceAs (Module β„‚ (AdelicGL2 (π“ž F) F β†’ β„‚))

@[simp] theorem toFn_zero : (0 : AdelicFnCarrier F).toFn = 0 := rfl

@[simp] theorem toFn_add (Ο† ψ : AdelicFnCarrier F) : (Ο† + ψ).toFn = Ο†.toFn + ψ.toFn := rfl

@[simp] theorem toFn_csmul (c : β„‚) (Ο† : AdelicFnCarrier F) : (c β€’ Ο†).toFn = c β€’ Ο†.toFn := rfl

instance : DistribMulAction (AdelicGL2 (π“ž F) F) (AdelicFnCarrier F) where
  smul g Ο† := mk fun x => Ο†.toFn (x * g)
  one_smul Ο† := ext fun x => congrArg Ο†.toFn (mul_one x)
  mul_smul g h Ο† := ext fun x => congrArg Ο†.toFn (mul_assoc x g h).symm
  smul_zero _ := ext fun _ => rfl
  smul_add _ _ _ := ext fun _ => rfl

@[simp] theorem toFn_smul (g : AdelicGL2 (π“ž F) F) (Ο† : AdelicFnCarrier F) (x : AdelicGL2 (π“ž F) F) :
    (g β€’ Ο†).toFn x = Ο†.toFn (x * g) := rfl

instance : SMulCommClass β„‚ (AdelicGL2 (π“ž F) F) (AdelicFnCarrier F) where
  smul_comm _ _ _ := ext fun _ => rfl

instance : SMulCommClass (AdelicGL2 (π“ž F) F) β„‚ (AdelicFnCarrier F) :=
  SMulCommClass.symm _ _ _

theorem mk_ne_zero_of_ne_zero {Ο† : AdelicGL2 (π“ž F) F β†’ β„‚} (hΟ† : Ο† β‰  0) : mk Ο† β‰  0 :=
  fun h => hφ (congrArg toFn h)

end AdelicFnCarrier

variable {F}

def AdelicSpanSubmodule (Ο† : AdelicGL2 (π“ž F) F β†’ β„‚) : Submodule β„‚ (AdelicFnCarrier F) :=
  Submodule.span β„‚ {ψ | βˆƒ g : AdelicGL2 (π“ž F) F, ψ = g β€’ AdelicFnCarrier.mk Ο†}

theorem mk_mem_adelicSpanSubmodule (Ο† : AdelicGL2 (π“ž F) F β†’ β„‚) :
    AdelicFnCarrier.mk Ο† ∈ AdelicSpanSubmodule Ο† :=
  Submodule.subset_span ⟨1, (one_smul _ _).symm⟩

theorem smul_mem_adelicSpanSubmodule (Ο† : AdelicGL2 (π“ž F) F β†’ β„‚) (g : AdelicGL2 (π“ž F) F)
    {ψ : AdelicFnCarrier F} (hψ : ψ ∈ AdelicSpanSubmodule Ο†) :
    g β€’ ψ ∈ AdelicSpanSubmodule Ο† := by
  refine Submodule.span_induction
    (fun x ⟨h, hh⟩ => Submodule.subset_span ⟨g * h, by rw [hh, mul_smul]⟩)
    (by rw [smul_zero]; exact zero_mem _)
    (fun x y _ _ hx hy => by rw [smul_add]; exact add_mem hx hy)
    (fun c x _ hx => by rw [smul_comm]; exact Submodule.smul_mem _ c hx) hψ

def AdelicSpan (Ο† : AdelicGL2 (π“ž F) F β†’ β„‚) : Type _ :=
  AdelicSpanSubmodule Ο†

namespace AdelicSpan

variable (Ο† : AdelicGL2 (π“ž F) F β†’ β„‚)

def mk (ψ : AdelicFnCarrier F) (hψ : ψ ∈ AdelicSpanSubmodule Ο†) : AdelicSpan Ο† :=
  ⟨ψ, hψ⟩

def toFn (ψ : AdelicSpan Ο†) : AdelicFnCarrier F :=
  (ψ : AdelicSpanSubmodule Ο†).val

@[ext] theorem ext {Οˆβ‚ Οˆβ‚‚ : AdelicSpan Ο†} (h : toFn Ο† Οˆβ‚ = toFn Ο† Οˆβ‚‚) : Οˆβ‚ = Οˆβ‚‚ :=
  Subtype.ext h

instance : AddCommGroup (AdelicSpan Ο†) :=
  inferInstanceAs (AddCommGroup (AdelicSpanSubmodule Ο†))

instance : Module β„‚ (AdelicSpan Ο†) :=
  inferInstanceAs (Module β„‚ (AdelicSpanSubmodule Ο†))

instance : DistribMulAction (AdelicGL2 (π“ž F) F) (AdelicSpan Ο†) where
  smul g ψ := mk Ο† (g β€’ toFn Ο† ψ)
    (smul_mem_adelicSpanSubmodule Ο† g (ψ : AdelicSpanSubmodule Ο†).2)
  one_smul ψ := ext Ο† (one_smul (AdelicGL2 (π“ž F) F) (toFn Ο† ψ))
  mul_smul g h ψ := ext Ο† (mul_smul (Ξ± := AdelicGL2 (π“ž F) F) g h (toFn Ο† ψ))
  smul_zero g := ext Ο† (smul_zero (A := AdelicFnCarrier F) g)
  smul_add g Οˆβ‚ Οˆβ‚‚ := ext Ο† (smul_add (A := AdelicFnCarrier F) g (toFn Ο† Οˆβ‚) (toFn Ο† Οˆβ‚‚))

@[simp] theorem toFn_smul (g : AdelicGL2 (π“ž F) F) (ψ : AdelicSpan Ο†) :
    toFn Ο† (g β€’ ψ) = g β€’ toFn Ο† ψ := rfl

instance : SMulCommClass β„‚ (AdelicGL2 (π“ž F) F) (AdelicSpan Ο†) where
  smul_comm c g ψ := ext Ο† (smul_comm (Ξ± := AdelicFnCarrier F) c g (toFn Ο† ψ))

instance : SMulCommClass (AdelicGL2 (π“ž F) F) β„‚ (AdelicSpan Ο†) :=
  SMulCommClass.symm _ _ _

def self : AdelicSpan Ο† :=
  mk Ο† (AdelicFnCarrier.mk Ο†) (mk_mem_adelicSpanSubmodule Ο†)

@[simp] theorem toFn_self : toFn Ο† (self Ο†) = AdelicFnCarrier.mk Ο† := rfl

theorem self_ne_zero_of_ne_zero (hφ : φ ≠ 0) : self φ ≠ 0 := by
  intro h
  exact AdelicFnCarrier.mk_ne_zero_of_ne_zero hφ (congrArg (toFn φ) h)

end AdelicSpan

variable (F)

theorem adelicSpan_self_one_ne_zero :
    AdelicSpan.self (F := F) (fun _ => (1 : β„‚)) β‰  0 :=
  AdelicSpan.self_ne_zero_of_ne_zero _ (by intro h; exact one_ne_zero (congrFun h 1))

section PadicAction

variable (p : β„•) [Fact p.Prime]

instance : DistribMulAction (GL (Fin 2) β„š_[p]) (AdelicFnCarrier β„š) :=
  DistribMulAction.compHom _ (AdelicDock.padicToAdelic p)

theorem AdelicFnCarrier.padic_smul_def (g : GL (Fin 2) β„š_[p]) (Ο† : AdelicFnCarrier β„š) :
    g β€’ Ο† = (AdelicDock.padicToAdelic p g : AdelicGL2 (π“ž β„š) β„š) β€’ Ο† := rfl

instance : SMulCommClass β„‚ (GL (Fin 2) β„š_[p]) (AdelicFnCarrier β„š) where
  smul_comm c g Ο† := smul_comm (Ξ± := AdelicFnCarrier β„š) c (AdelicDock.padicToAdelic p g) Ο†

instance : SMulCommClass (GL (Fin 2) β„š_[p]) β„‚ (AdelicFnCarrier β„š) :=
  SMulCommClass.symm _ _ _

variable {Ο† : AdelicGL2 (π“ž β„š) β„š β†’ β„‚}

instance : DistribMulAction (GL (Fin 2) β„š_[p]) (AdelicSpan Ο†) :=
  DistribMulAction.compHom _ (AdelicDock.padicToAdelic p)

theorem AdelicSpan.padic_smul_def (g : GL (Fin 2) β„š_[p]) (ψ : AdelicSpan Ο†) :
    g β€’ ψ = (AdelicDock.padicToAdelic p g : AdelicGL2 (π“ž β„š) β„š) β€’ ψ := rfl

instance : SMulCommClass β„‚ (GL (Fin 2) β„š_[p]) (AdelicSpan Ο†) where
  smul_comm c g ψ := smul_comm (Ξ± := AdelicSpan Ο†) c (AdelicDock.padicToAdelic p g) ψ

instance : SMulCommClass (GL (Fin 2) β„š_[p]) β„‚ (AdelicSpan Ο†) :=
  SMulCommClass.symm _ _ _

theorem AdelicSpan.typeOf_hasNewvectorConductor (c : β„•) :
    (HasNewvectorConductor p (AdelicSpan Ο†) c) = (HasNewvectorConductor p (AdelicSpan Ο†) c) := rfl

theorem AdelicSpan.typeOf_fixedSubmodule_padicK1 (n : β„•) :
    (fixedSubmodule (padicK1 p n) (AdelicSpan Ο†) : Submodule β„‚ (AdelicSpan Ο†))
      = fixedSubmodule (padicK1 p n) (AdelicSpan Ο†) := rfl

end PadicAction

end LocalNewvector

end

Statements phrased using this module (87)