Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_HpoolLevelRing.lean

definition module

Integral chart ring of , its localisations and level quotients

Throughout, p is a prime and F = modularFunctionFieldFull p is the subfield of \mathbb{Q}((q)) generated over \mathbb{Q} by the q-expansions j(q^d) for the positive divisors d \mid p, with j = IgusaScheme.jFull p the element of F given by the q-expansion of the modular invariant.

Three types are introduced. First, Afin p is the chart algebra AlgebraicCurve.TwoChartIntegralModel.chartAlgFin ℤ F j regarded as a type: by the definition of chartAlg, it consists of those x \in F that are integral over \mathbb{Z}[j] = Algebra.adjoin ℤ {j}, i.e. the integral closure of \mathbb{Z}[j] in F; it is recorded as a commutative domain and a \mathbb{Z}-algebra. Secondly, for an integer f, AfinAway p f is the localisation of Afin p away from the image of f, written A[1/f]; besides its A- and \mathbb{Z}-algebra structures it is given an algebra structure over Localization.Away f = \mathbb{Z}[1/f], induced by functoriality of localisation from \mathbb{Z} \to A, and the lemma algebraMap_awayMap_algebraMap states that the composite \mathbb{Z} \to \mathbb{Z}[1/f] \to A[1/f] is the structure map \mathbb{Z} \to A[1/f]. Thirdly, for u \in A and an integer polynomial g \in \mathbb{Z}[T], levelRing p f u g is the quotient of A[1/f] by the principal ideal generated by g evaluated at the image of u in A[1/f], together with its commutative-ring structure and its algebra structures over A[1/f] and over \mathbb{Z}[1/f].

Nothing is asserted beyond the compatibility lemma above and the auxiliary observation that a prime is non-zero; the parameters u and g are arbitrary, so the constructions are generic in (p,f,u,g).

Relation to Mathlib

The types themselves are Mathlib's Localization.Away and quotient by a principal ideal applied to the project's chart algebra AlgebraicCurve.TwoChartIntegralModel.chartAlgFin; Mathlib has no notion of the modular function field or of this integral chart algebra.

Where it is used

These rings are the common coordinate rings for the affine schemes \operatorname{Spec} of such quotients used in later modules that study the two-chart integral model of X_0(p): fixing one \mathbb{Z}[1/f]-algebra structure here lets finiteness, étaleness and component statements about those schemes be formulated over the same base.

References

  1. J.-I. Igusa, Kroneckerian model of fields of elliptic modular functions, American Journal of Mathematics 81 (1959), 561–577
  2. P. Deligne and M. Rapoport, Les schémas de modules de courbes elliptiques, in: Modular Functions of One Variable II, Lecture Notes in Mathematics 349, Springer, 1973, 143–316

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_X0
import Definitions.Def_ModularCurve_IgusaScheme
import Definitions.Def_AlgebraicCurve_TwoChartIntegralModel

set_option autoImplicit false

noncomputable section

namespace ModularCurve

namespace HpoolLevelRing

variable (p : ℕ) [Fact p.Prime]

theorem neZero_of_fact_prime : NeZero p := ⟨(Fact.out : p.Prime).ne_zero⟩

attribute [local instance] neZero_of_fact_prime

abbrev Afin : Type :=
  ↥(AlgebraicCurve.TwoChartIntegralModel.chartAlgFin ℤ ↥(modularFunctionFieldFull p) (IgusaScheme.jFull p))

set_option synthInstance.maxHeartbeats 200000 in
instance instCommRingAfin : CommRing (Afin p) := inferInstance

set_option synthInstance.maxHeartbeats 200000 in
instance instIsDomainAfin : IsDomain (Afin p) := inferInstance

set_option synthInstance.maxHeartbeats 200000 in
instance instAlgebraIntAfin : Algebra ℤ (Afin p) := inferInstance

set_option synthInstance.maxHeartbeats 200000 in
instance instModuleAfinSelf : Module (Afin p) (Afin p) := Semiring.toModule

abbrev AfinAway (f : ℤ) : Type :=
  Localization.Away (algebraMap ℤ (Afin p) f)

set_option synthInstance.maxHeartbeats 200000 in
instance instCommRingAfinAway (f : ℤ) : CommRing (AfinAway p f) := inferInstance

set_option synthInstance.maxHeartbeats 200000 in
instance instAlgebraAfinAfinAway (f : ℤ) : Algebra (Afin p) (AfinAway p f) := inferInstance

set_option synthInstance.maxHeartbeats 200000 in
instance instAlgebraIntAfinAway (f : ℤ) : Algebra ℤ (AfinAway p f) := inferInstance

set_option synthInstance.maxHeartbeats 200000 in
instance instSMulAfinAfinAway (f : ℤ) : SMul (Afin p) (AfinAway p f) := Algebra.toSMul

set_option synthInstance.maxHeartbeats 200000 in
instance instModuleAfinAfinAway (f : ℤ) : Module (Afin p) (AfinAway p f) := Algebra.toModule

set_option synthInstance.maxHeartbeats 200000 in

instance algebraAway (f : ℤ) : Algebra (Localization.Away f) (AfinAway p f) :=
  (Localization.awayMap (algebraMap ℤ (Afin p)) f).toAlgebra

set_option synthInstance.maxHeartbeats 200000 in
instance instSMulAway (f : ℤ) : SMul (Localization.Away f) (AfinAway p f) := Algebra.toSMul

set_option synthInstance.maxHeartbeats 200000 in
instance instModuleAway (f : ℤ) : Module (Localization.Away f) (AfinAway p f) := Algebra.toModule

set_option synthInstance.maxHeartbeats 200000 in

theorem algebraMap_awayMap_algebraMap (f : ℤ) (x : ℤ) :
    algebraMap (Localization.Away f) (AfinAway p f) (algebraMap ℤ (Localization.Away f) x) =
      algebraMap ℤ (AfinAway p f) x :=
  RingHom.congr_fun (Subsingleton.elim ((algebraMap (Localization.Away f) (AfinAway p f)).comp
    (algebraMap ℤ (Localization.Away f))) (algebraMap ℤ (AfinAway p f))) x

abbrev levelRing (f : ℤ) (u : Afin p) (g : Polynomial ℤ) : Type :=
  AfinAway p f ⧸ Ideal.span {Polynomial.aeval (algebraMap (Afin p) (AfinAway p f) u) g}

set_option synthInstance.maxHeartbeats 200000 in
instance instCommRingLevelRing (f : ℤ) (u : Afin p) (g : Polynomial ℤ) : CommRing (levelRing p f u g) := inferInstance

set_option synthInstance.maxHeartbeats 200000 in
instance instAlgebraLevelRing (f : ℤ) (u : Afin p) (g : Polynomial ℤ) :
    Algebra (Localization.Away f) (levelRing p f u g) := inferInstance

set_option synthInstance.maxHeartbeats 200000 in
instance instSMulLevelRing (f : ℤ) (u : Afin p) (g : Polynomial ℤ) :
    SMul (Localization.Away f) (levelRing p f u g) := Algebra.toSMul

set_option synthInstance.maxHeartbeats 200000 in
instance instModuleLevelRing (f : ℤ) (u : Afin p) (g : Polynomial ℤ) :
    Module (Localization.Away f) (levelRing p f u g) := Algebra.toModule

set_option synthInstance.maxHeartbeats 200000 in
instance instAlgebraAfinAwayLevelRing (f : ℤ) (u : Afin p) (g : Polynomial ℤ) :
    Algebra (AfinAway p f) (levelRing p f u g) := inferInstance

end HpoolLevelRing

end ModularCurve

end

Statements phrased using this module (19)