Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_DrinfeldCurve_FunctionField.lean

definition module

Function field of the Drinfeld curve and its group action

Fix a natural number q and a field k. The coordinate ring CoordRing q k is the quotient of k[X_0,X_1] by the ideal generated by X_0X_1^q - X_0^qX_1 - 1, and drinfeldFunctionField q k is defined as FractionRing (CoordRing q k), i.e. the localisation of that quotient at its non-zero divisors; it is a field exactly when the coordinate ring is a domain, and in general it is the total ring of fractions. Under the standing assumptions that q is prime and that k is an algebra over the field GaloisField q 2 with q^2 elements, the module transports the coordinate-ring action to this fraction ring. Here hSubgroup q is the kernel of the character \mathrm{GL}_2(\mathbb{Z}/q)\times\mathbb{F}_{q^2}^{\times}\to\mathbb{F}_{q^2}^{\times}, (g,\zeta)\mapsto \det(g)\,\zeta^{q+1}, and hAction q k is its action on CoordRing q k by k-algebra automorphisms, where (g,\zeta) acts by the linear substitution of g in (X_0,X_1) followed by scaling both variables by the image of \zeta in k.

The definition hFunctionFieldAction q k is the monoid homomorphism from hSubgroup q to the group of k-algebra automorphisms of drinfeldFunctionField q k sending h to the unique extension of hAction q k h to fractions, via IsFractionRing.algEquivOfAlgEquiv; multiplicativity and preservation of the identity are part of the data. Three accompanying identities record its characterisation: hFunctionFieldAction_algebraMap says it agrees with hAction q k h on the image of the coordinate ring; hFunctionFieldAction_sl and hFunctionFieldAction_mu identify its values at the pairs (g,1) with g\in\mathrm{SL}_2(\mathbb{Z}/q) and at the pairs (1,\zeta) with \zeta^{q+1}=1 with the extensions of slAction q k g and muAction q k ζ respectively.

Relation to Mathlib

Mathlib has no Drinfeld curve; the curve, its coordinate ring and the group hSubgroup are the project's own, while the fraction ring and the extension of an algebra equivalence to fraction rings (FractionRing, IsFractionRing.algEquivOfAlgEquiv) are taken from Mathlib.

Where it is used

The action of hSubgroup q on the function field by k-algebra automorphisms is the basic datum from which the induced actions on places, divisors, degree-zero divisor classes and their torsion are obtained in later modules; the convention throughout is that the group acts on functions by pullback, so that geometric eigenvalues are inverted relative to this action.

References

  1. P. Deligne and G. Lusztig, Representations of reductive groups over finite fields, Annals of Mathematics 103 (1976), 103–161

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

Imports

Imported by

Declarations

Source

import Definitions.Def_DrinfeldCurve_CoordRing
import Mathlib.RingTheory.Localization.FractionRing ↗

set_option autoImplicit false

noncomputable section

namespace DrinfeldCurve

variable (q : ℕ) (k : Type) [Field k]

abbrev drinfeldFunctionField : Type := FractionRing (CoordRing q k)

variable [Fact q.Prime] [Algebra (GaloisField q 2) k]

def hFunctionFieldAction : hSubgroup q →* (drinfeldFunctionField q k ≃ₐ[k] drinfeldFunctionField q k) where
  toFun h := IsFractionRing.algEquivOfAlgEquiv (hAction q k h)
  map_one' := by
    apply AlgEquiv.ext
    intro x
    have key : ((IsFractionRing.algEquivOfAlgEquiv (hAction q k 1) :
          drinfeldFunctionField q k ≃ₐ[k] drinfeldFunctionField q k) :
            drinfeldFunctionField q k →+* drinfeldFunctionField q k) = RingHom.id _ := by
      apply IsLocalization.ringHom_ext (nonZeroDivisors (CoordRing q k))
      ext a
      simp [IsFractionRing.algEquivOfAlgEquiv_algebraMap]
    simpa using RingHom.congr_fun key x
  map_mul' g h := by
    apply AlgEquiv.ext
    intro x
    have key : ((IsFractionRing.algEquivOfAlgEquiv (hAction q k (g * h)) :
          drinfeldFunctionField q k ≃ₐ[k] drinfeldFunctionField q k) :
            drinfeldFunctionField q k →+* drinfeldFunctionField q k) =
        ((IsFractionRing.algEquivOfAlgEquiv (hAction q k g) :
          drinfeldFunctionField q k ≃ₐ[k] drinfeldFunctionField q k) :
            drinfeldFunctionField q k →+* drinfeldFunctionField q k).comp
          ((IsFractionRing.algEquivOfAlgEquiv (hAction q k h) :
            drinfeldFunctionField q k ≃ₐ[k] drinfeldFunctionField q k) :
              drinfeldFunctionField q k →+* drinfeldFunctionField q k) := by
      apply IsLocalization.ringHom_ext (nonZeroDivisors (CoordRing q k))
      ext a
      simp [IsFractionRing.algEquivOfAlgEquiv_algebraMap, map_mul]
    simpa using RingHom.congr_fun key x

theorem hFunctionFieldAction_algebraMap (h : hSubgroup q) (a : CoordRing q k) :
    hFunctionFieldAction q k h (algebraMap (CoordRing q k) (drinfeldFunctionField q k) a) =
      algebraMap (CoordRing q k) (drinfeldFunctionField q k) (hAction q k h a) :=
  IsFractionRing.algEquivOfAlgEquiv_algebraMap (hAction q k h) a

theorem hFunctionFieldAction_sl (g : Matrix.SpecialLinearGroup (Fin 2) (ZMod q)) :
    hFunctionFieldAction q k ⟨_, toGL_one_mem_hSubgroup q g⟩ =
      IsFractionRing.algEquivOfAlgEquiv (slAction q k g) := by
  rw [slAction_eq_hAction]
  rfl

theorem hFunctionFieldAction_mu (ζ : rootsOfUnity (q + 1) (GaloisField q 2)) :
    hFunctionFieldAction q k ⟨_, one_mem_hSubgroup_of_mem q ζ⟩ =
      IsFractionRing.algEquivOfAlgEquiv (muAction q k ζ) := by
  rw [muAction_eq_hAction]
  rfl

end DrinfeldCurve

end

Statements phrased using this module (30)