Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_JLinePlaces.lean

definition module

The -line as a rational function field, with three places

Fix N\ge 1. Here \mathrm{jq} is the explicit Laurent series q^{-1}E_4^3\eta^{-24} over \mathbb{Q}, \mathbb{Q}\langle \mathrm{jq}\rangle the simple extension it generates inside \mathbb{Q}((q)), and modularFunctionField N the intermediate field \mathbb{Q}(\mathrm{jq},\ \mathrm{jq}(q^N)) generated by \mathrm{jq} and its N-fold q-substitution. The first group of declarations equips modularFunctionField N with the \mathbb{Q}\langle \mathrm{jq}\rangle-algebra structure coming from the inclusion ring homomorphism jAdjoinRingHom N (available as a reducible definition rather than a global instance), records that \mathbb{Q}\subset\mathbb{Q}\langle \mathrm{jq}\rangle\subset modularFunctionField N is a scalar tower, and states that the generator jGen of \mathbb{Q}\langle \mathrm{jq}\rangle maps to the Laurent series \mathrm{jq}.

The second group identifies the j-line with the rational function field. Since \mathrm{jq} is transcendental over \mathbb{Q}, Mathlib's algebra equivalence attached to a transcendental element is a bijection; jLineRingEquiv is the resulting ring isomorphism \mathbb{Q}(T)\xrightarrow{\sim}\mathbb{Q}\langle \mathrm{jq}\rangle, and it sends T to jGen.

Finally, three places of \mathbb{Q}\langle \mathrm{jq}\rangle over \mathbb{Q} are defined. In this development a place of F/K is a valuation subring of F which contains the image of K, is not all of F, and is a principal ideal ring (hence a discrete valuation ring). jLinePlace1728, jLinePlaceZero and jLinePlaceInfty are obtained by transporting along jLineRingEquiv, via the congruence operation on places (the valuation subring is pulled back along the inverse isomorphism), the place of \mathbb{Q}(T) attached to the height-one prime (T-1728), the place attached to (T), and the place of the degree valuation at infinity. A classical decidable-equality helper for \mathbb{Q}(T) is supplied, as the place at infinity is defined with such an assumption in scope.

Relation to Mathlib

The notion of a place used here — a valuation subring of F containing K, proper, and principal — is the project's own structure, as are the places of a rational function field at a point and at infinity; jLineRingEquiv repackages Mathlib's algebra equivalence K(T)\simeq K(x) for a transcendental x as a ring isomorphism.

Where it is used

These definitions set up the function-field language for the covering X_0(N)\to X(1): the tower \mathbb{Q}\subset\mathbb{Q}(j)\subset\mathbb{Q}(j(q),j(q^N)) lets one speak of restrictions of places, ramification indices and residue degrees for that cover, and the three distinguished places of the j-line at j=1728, j=0 and j=\infty are the base points at which the covering's behaviour is analysed.

References

  1. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Publications of the Mathematical Society of Japan 11, Princeton University Press, 1971
  2. H. Stichtenoth, Algebraic Function Fields and Codes, Graduate Texts in Mathematics 254, Springer, 2009

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

Imports

Theorems imported by this definition module

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_RouteBCoordRing
import Definitions.Def_AlgebraicCurve_RatFuncPlaces
import Definitions.Def_AlgebraicCurve_RatFuncPlaceInfty
import Theorems.Thm_ModularCurve_transcendental_jq

set_option autoImplicit false

noncomputable section

open IntermediateField AlgebraicCurve AlgebraicCurve.RationalFunctionField

namespace ModularCurve

section Tower

variable (N : ℕ) [NeZero N]

@[reducible] def jAdjoinAlgebra : Algebra ℚ⟮jq⟯ (modularFunctionField N) :=
  (jAdjoinRingHom N).toAlgebra

attribute [local instance] jAdjoinAlgebra

instance instIsScalarTowerJAdjoin :
    @IsScalarTower ℚ ℚ⟮jq⟯ (modularFunctionField N)
      Algebra.toSMul Algebra.toSMul Algebra.toSMul :=
  IsScalarTower.of_algebraMap_eq' (by apply RingHom.ext_rat)

theorem algebraMap_jGen_val : (algebraMap ℚ⟮jq⟯ (modularFunctionField N) jGen : LaurentSeries ℚ) = jq :=
  rfl

end Tower

attribute [local instance 2000] RatFunc.instAlgebraOfPolynomial

def jLineRingEquiv : RatFunc ℚ ≃+* ℚ⟮jq⟯ :=
  RingEquiv.ofBijective (RatFunc.algEquivOfTranscendental jq transcendental_jq)
    (EquivLike.bijective _)

theorem jLineRingEquiv_apply (f : RatFunc ℚ) :
    jLineRingEquiv f = RatFunc.algEquivOfTranscendental jq transcendental_jq f := rfl

theorem jLineRingEquiv_X : jLineRingEquiv RatFunc.X = jGen :=
  Subtype.ext (RatFunc.algEquivOfTranscendental_X jq transcendental_jq)

@[reducible] def instDecidableEqRatFuncRat : DecidableEq (RatFunc ℚ) := Classical.decEq _

attribute [local instance] instDecidableEqRatFuncRat

def jLinePlace1728 : Place ℚ ℚ⟮jq⟯ :=
  Place.congrRingEquiv jLineRingEquiv (RingHom.map_rat_algebraMap jLineRingEquiv.toRingHom)
    (placeOfPoint ℚ 1728)

def jLinePlaceZero : Place ℚ ℚ⟮jq⟯ :=
  Place.congrRingEquiv jLineRingEquiv (RingHom.map_rat_algebraMap jLineRingEquiv.toRingHom)
    (placeOfPoint ℚ 0)

def jLinePlaceInfty : Place ℚ ℚ⟮jq⟯ :=
  Place.congrRingEquiv jLineRingEquiv (RingHom.map_rat_algebraMap jLineRingEquiv.toRingHom)
    (placeInfty ℚ)

end ModularCurve

end

Statements phrased using this module (16)