Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_QExpReductionModL.lean

definition module

Reduction of q-expansion function fields and Jacobians modulo a place

Throughout: a field L over \mathbb{Q}, a valuation subring A\subseteq L, a ring homomorphism \pi\colon A\to k into a field k, an intermediate field F_0 of \mathbb{Q}((q))/\mathbb{Q} and an intermediate field \bar F of k((q))/k. Write F= laurentBaseChange L F₀ for the subfield of L((q)) generated over L by the coefficientwise images of F_0; places, their degrees (the K-finrank of the residue field), \operatorname{ord}, divisors as finitely supported \mathbb{Z}-valued functions on places, Divisor.principal, Divisor.degZero and Pic0 are the project's notions for a function field inside a Laurent series field.

IsLaurentPlaceReduction A π F₀ Fbar r, for r a map from places of F/L to places of \bar F/k, is the conjunction of: (i) (rP).\mathrm{deg}=P.\mathrm{deg} for every P; (ii) for every y\in A((q)) whose coefficientwise image in L((q)) lies in F and whose coefficientwise reduction \pi(y) lies in \bar F and is nonzero, and every divisor D with D(P)=\operatorname{ord}_P(y) for all P, the push-forward Finsupp.mapDomain r D satisfies (r_*D)(Q)=\operatorname{ord}_Q(\pi(y)) for all Q. laurentIntegralPrincipalDivisors is the set of divisors arising as divisors of such y, and LaurentPrincipalGeneratedByIntegral says that Divisor.principal for F/L is contained in the subgroup generated by that set. LaurentReductionInputs asserts the existence of an r satisfying (i)–(ii) together with this generation property (whose statement does not involve r).

Accompanying lemmas record that r_* preserves degrees of divisors, degree-zero divisors and, under the generation hypothesis, principal divisors; laurentReductionDiv, laurentReductionDegZero and laurentReductionPic0 are the resulting additive maps on divisors, on degree-zero divisors and on \mathrm{Pic}^0. laurentReduction A π F₀ Fbar is a total additive map \mathrm{Pic}^0(F/L)\to\mathrm{Pic}^0(\bar F/k): the descent attached to a chosen witness when LaurentReductionInputs holds, and the zero map otherwise, with the corresponding characterisations on classes and in the negative case.

Two uniqueness statements: if r_1,r_2 have equal push-forwards on all divisors of such integral y, the generation property holds, every place of F/L has degree 1 and \mathrm{Pic}^0(F/L) is divisible, then either r_1=r_2 or r_1 is constant; adding that principal divisors have degree 0 and that some principal divisor has nonzero push-forward under r_1 forces r_1=r_2.

The final section specialises to L=\overline{\mathbb{Q}}, \pi the residue map of A, F_0 the q-expansion function field qExpFunctionFieldC ℚ Γ of a subgroup \Gamma\le \mathrm{SL}_2(\mathbb{Z}) and \bar F the corresponding field over the residue field of A, yielding IsPlaceReductionQExpModL, ReductionInputsQExpModL, a chosen map of places placeReductionQExpModL satisfying the specification, and reductionQExpModL A Γ on \mathrm{Pic}^0; for \Gamma=\Gamma_1(M) this sends JOne M to JOneC M over the residue field.

Relation to Mathlib

Mathlib has no notion of reduction of a function field or of its divisor class group modulo a place; these predicates and maps are the project's own, built on its Place/Divisor/Pic0 for subfields of a Laurent series field, with Mathlib supplying LaurentSeries, ValuationSubring, IsLocalRing.residue and Finsupp.mapDomain.

Where it is used

The reduction map provides the comparison between the Jacobian of a modular curve over \overline{\mathbb{Q}}, as realised through q-expansion function fields, and its reduction at a place of \overline{\mathbb{Q}}, the setting in which torsion in J_1(M) and the associated Galois representations are studied. The conditions ReductionInputsQExpModL isolate, as named hypotheses, the good-reduction input needed for that comparison.

References

  1. H. Stichtenoth, Algebraic Function Fields and Codes, 2nd edition, Graduate Texts in Mathematics 254, Springer, 2009
  2. J.-I. Igusa, Kroneckerian model of fields of elliptic modular functions, American Journal of Mathematics 81 (1959), 561–577

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_X1

set_option autoImplicit false

noncomputable section

open HahnSeries IntermediateField AlgebraicCurve

namespace ModularCurve

section Spec

variable {L : Type*} [Field L] [Algebra ℚ L] (A : ValuationSubring L)
variable {k : Type*} [Field k] (π : A →+* k)
variable (F₀ : IntermediateField ℚ (LaurentSeries ℚ)) (Fbar : IntermediateField k (LaurentSeries k))

def IsLaurentPlaceReduction (r : Place L (laurentBaseChange L F₀) → Place k Fbar) : Prop :=
  (∀ P, (r P).deg = P.deg) ∧
    ∀ (y : LaurentSeries A) (hy : coeffMap A.subtype y ∈ laurentBaseChange L F₀)
      (hyk : coeffMap π y ∈ Fbar), coeffMap π y ≠ 0 →
        ∀ D : Divisor L (laurentBaseChange L F₀),
          (∀ P, D P = P.ord (⟨coeffMap A.subtype y, hy⟩ : laurentBaseChange L F₀)) →
            ∀ Q, Finsupp.mapDomain r D Q = Q.ord (⟨coeffMap π y, hyk⟩ : Fbar)

def laurentIntegralPrincipalDivisors : Set (Divisor L (laurentBaseChange L F₀)) :=
  {D | ∃ (y : LaurentSeries A) (hy : coeffMap A.subtype y ∈ laurentBaseChange L F₀),
      coeffMap π y ∈ Fbar ∧ coeffMap π y ≠ 0 ∧
        ∀ P, D P = P.ord (⟨coeffMap A.subtype y, hy⟩ : laurentBaseChange L F₀)}

def LaurentPrincipalGeneratedByIntegral : Prop :=
  Divisor.principal (K := L) (F := laurentBaseChange L F₀) ≤
    AddSubgroup.closure (laurentIntegralPrincipalDivisors A π F₀ Fbar)

def LaurentReductionInputs : Prop :=
  ∃ r, IsLaurentPlaceReduction A π F₀ Fbar r ∧ LaurentPrincipalGeneratedByIntegral A π F₀ Fbar

end Spec

section SpecLemmas

variable {L : Type*} [Field L] [Algebra ℚ L] {A : ValuationSubring L}
variable {k : Type*} [Field k] {π : A →+* k}
variable {F₀ : IntermediateField ℚ (LaurentSeries ℚ)} {Fbar : IntermediateField k (LaurentSeries k)}
variable {r : Place L (laurentBaseChange L F₀) → Place k Fbar}

theorem IsLaurentPlaceReduction.deg_eq (hr : IsLaurentPlaceReduction A π F₀ Fbar r)
    (P : Place L (laurentBaseChange L F₀)) : (r P).deg = P.deg :=
  hr.1 P

theorem IsLaurentPlaceReduction.isPrincipal_mapDomain (hr : IsLaurentPlaceReduction A π F₀ Fbar r)
    {D : Divisor L (laurentBaseChange L F₀)} (hD : D ∈ laurentIntegralPrincipalDivisors A π F₀ Fbar) :
    Divisor.IsPrincipal (Finsupp.mapDomain r D) := by
  obtain ⟨y, hy, hyk, hne, hDy⟩ := hD
  refine ⟨⟨coeffMap π y, hyk⟩, fun h => hne (congrArg Subtype.val h), fun Q => ?_⟩
  exact hr.2 y hy hyk hne D hDy Q

theorem degree_mapDomain_of_laurent_deg_eq (hdeg : ∀ P, (r P).deg = P.deg)
    (D : Divisor L (laurentBaseChange L F₀)) :
    Divisor.degree (Finsupp.mapDomain r D) = Divisor.degree D := by
  induction D using Finsupp.induction with
  | zero => simp
  | single_add P n D _ _ ih =>
    rw [Finsupp.mapDomain_add, map_add, map_add, ih, Finsupp.mapDomain_single,
      Divisor.degree_single, Divisor.degree_single, hdeg]

theorem mapDomain_mem_degZero_of_laurent_deg_eq (hdeg : ∀ P, (r P).deg = P.deg)
    {D : Divisor L (laurentBaseChange L F₀)}
    (hD : D ∈ Divisor.degZero (K := L) (F := laurentBaseChange L F₀)) :
    Finsupp.mapDomain r D ∈ Divisor.degZero (K := k) (F := Fbar) := by
  rw [Divisor.mem_degZero] at hD ⊢
  rw [degree_mapDomain_of_laurent_deg_eq hdeg, hD]

theorem IsLaurentPlaceReduction.mapDomain_mem_principal (hr : IsLaurentPlaceReduction A π F₀ Fbar r)
    (hgen : LaurentPrincipalGeneratedByIntegral A π F₀ Fbar)
    {D : Divisor L (laurentBaseChange L F₀)}
    (hD : D ∈ Divisor.principal (K := L) (F := laurentBaseChange L F₀)) :
    Finsupp.mapDomain r D ∈ Divisor.principal (K := k) (F := Fbar) := by
  have hD' := hgen hD
  clear hD
  induction hD' using AddSubgroup.closure_induction with
  | mem E hE => exact hr.isPrincipal_mapDomain hE
  | zero => rw [Finsupp.mapDomain_zero]; exact AddSubgroup.zero_mem _
  | add E E' _ _ hE hE' => rw [Finsupp.mapDomain_add]; exact AddSubgroup.add_mem _ hE hE'
  | neg E _ hE =>
    rw [← Finsupp.mapDomain.addMonoidHom_apply, map_neg, Finsupp.mapDomain.addMonoidHom_apply]
    exact AddSubgroup.neg_mem _ hE

end SpecLemmas

section Descent

variable {L : Type*} [Field L] [Algebra ℚ L] {A : ValuationSubring L}
variable {k : Type*} [Field k] {π : A →+* k}
variable {F₀ : IntermediateField ℚ (LaurentSeries ℚ)} {Fbar : IntermediateField k (LaurentSeries k)}
variable (r : Place L (laurentBaseChange L F₀) → Place k Fbar)

def laurentReductionDiv : Divisor L (laurentBaseChange L F₀) →+ Divisor k Fbar :=
  Finsupp.mapDomain.addMonoidHom r

@[simp]
theorem laurentReductionDiv_apply (D : Divisor L (laurentBaseChange L F₀)) :
    laurentReductionDiv r D = Finsupp.mapDomain r D :=
  rfl

theorem laurentReductionDiv_single (P : Place L (laurentBaseChange L F₀)) (n : ℤ) :
    laurentReductionDiv r (Finsupp.single P n) = Finsupp.single (r P) n :=
  Finsupp.mapDomain_single

def laurentReductionDegZero (hdeg : ∀ P, (r P).deg = P.deg) :
    Divisor.degZero (K := L) (F := laurentBaseChange L F₀) →+ Divisor.degZero (K := k) (F := Fbar) :=
  ((laurentReductionDiv r).domRestrict _).codRestrict _
    fun D => mapDomain_mem_degZero_of_laurent_deg_eq hdeg D.2

@[simp]
theorem coe_laurentReductionDegZero (hdeg : ∀ P, (r P).deg = P.deg)
    (D : Divisor.degZero (K := L) (F := laurentBaseChange L F₀)) :
    (laurentReductionDegZero r hdeg D : Divisor k Fbar) =
      Finsupp.mapDomain r (D : Divisor L (laurentBaseChange L F₀)) :=
  rfl

def laurentReductionPic0 (hr : IsLaurentPlaceReduction A π F₀ Fbar r)
    (hgen : LaurentPrincipalGeneratedByIntegral A π F₀ Fbar) :
    Pic0 L (laurentBaseChange L F₀) →+ Pic0 k Fbar :=
  QuotientAddGroup.map _ _ (laurentReductionDegZero r hr.1) (by
    rintro ⟨D, hD0⟩ hD
    simp only [AddSubgroup.mem_addSubgroupOf] at hD ⊢
    exact hr.mapDomain_mem_principal hgen hD)

theorem laurentReductionPic0_mk (hr : IsLaurentPlaceReduction A π F₀ Fbar r)
    (hgen : LaurentPrincipalGeneratedByIntegral A π F₀ Fbar)
    (D : Divisor.degZero (K := L) (F := laurentBaseChange L F₀)) :
    laurentReductionPic0 r hr hgen (Pic0.mk D) = Pic0.mk (laurentReductionDegZero r hr.1 D) :=
  rfl

end Descent

section Total

variable {L : Type*} [Field L] [Algebra ℚ L] (A : ValuationSubring L)
variable {k : Type*} [Field k] (π : A →+* k)
variable (F₀ : IntermediateField ℚ (LaurentSeries ℚ)) (Fbar : IntermediateField k (LaurentSeries k))

open Classical in

def laurentReduction : Pic0 L (laurentBaseChange L F₀) →+ Pic0 k Fbar :=
  if h : LaurentReductionInputs A π F₀ Fbar then
    laurentReductionPic0 h.choose h.choose_spec.1 h.choose_spec.2
  else 0

variable {A π F₀ Fbar}

theorem laurentReduction_eq (h : LaurentReductionInputs A π F₀ Fbar) :
    laurentReduction A π F₀ Fbar = laurentReductionPic0 h.choose h.choose_spec.1 h.choose_spec.2 := by
  rw [laurentReduction, dif_pos h]

theorem laurentReduction_mk (h : LaurentReductionInputs A π F₀ Fbar)
    (D : Divisor.degZero (K := L) (F := laurentBaseChange L F₀)) :
    laurentReduction A π F₀ Fbar (Pic0.mk D) =
      Pic0.mk (laurentReductionDegZero h.choose h.choose_spec.1.1 D) := by
  rw [laurentReduction_eq h]
  rfl

theorem laurentReduction_of_not (h : ¬ LaurentReductionInputs A π F₀ Fbar) :
    laurentReduction A π F₀ Fbar = 0 := by
  rw [laurentReduction, dif_neg h]

end Total

section Uniqueness

variable {L : Type*} [Field L] [Algebra ℚ L] {A : ValuationSubring L}
variable {k : Type*} [Field k] {π : A →+* k}
variable {F₀ : IntermediateField ℚ (LaurentSeries ℚ)} {Fbar : IntermediateField k (LaurentSeries k)}

private theorem int_eq_zero_of_forall_dvd' {a : ℤ} (h : ∀ n : ℕ, n ≠ 0 → (n : ℤ) ∣ a) : a = 0 :=
  Int.eq_zero_of_dvd_of_natAbs_lt_natAbs (h (a.natAbs + 1) (Nat.succ_ne_zero _))
    (by rw [Int.natAbs_natCast]; exact Nat.lt_succ_self _)

theorem IsLaurentPlaceReduction.eq_or_const_of_agree
    {r₁ r₂ : Place L (laurentBaseChange L F₀) → Place k Fbar}
    (hgen : LaurentPrincipalGeneratedByIntegral A π F₀ Fbar)
    (hagree : ∀ D ∈ laurentIntegralPrincipalDivisors A π F₀ Fbar,
      Finsupp.mapDomain r₁ D = Finsupp.mapDomain r₂ D)
    (hdeg : ∀ P : Place L (laurentBaseChange L F₀), P.deg = 1)
    (hdiv : ∀ n : ℕ, n ≠ 0 → ∀ x : Pic0 L (laurentBaseChange L F₀),
      ∃ y : Pic0 L (laurentBaseChange L F₀), n • y = x) :
    r₁ = r₂ ∨ ∀ P Q, r₁ P = r₁ Q := by
  classical

  set δ : Divisor L (laurentBaseChange L F₀) →+ Divisor k Fbar :=
    Finsupp.mapDomain.addMonoidHom r₁ - Finsupp.mapDomain.addMonoidHom r₂ with hδ
  have hδapp : ∀ D, δ D = Finsupp.mapDomain r₁ D - Finsupp.mapDomain r₂ D := fun D => rfl

  have hδprin : ∀ D ∈ Divisor.principal (K := L) (F := laurentBaseChange L F₀), δ D = 0 := by
    intro D hD
    have hD' := hgen hD
    clear hD
    induction hD' using AddSubgroup.closure_induction with
    | mem E hE => rw [hδapp, hagree E hE, sub_self]
    | zero => exact map_zero δ
    | add E E' _ _ hE hE' => rw [map_add, hE, hE', add_zero]
    | neg E _ hE => rw [map_neg, hE, neg_zero]

  have hδdeg0 : ∀ D ∈ Divisor.degZero (K := L) (F := laurentBaseChange L F₀), δ D = 0 := by
    intro D hD
    ext Q
    rw [Finsupp.zero_apply]
    refine int_eq_zero_of_forall_dvd' fun n hn => ?_
    obtain ⟨y, hy⟩ := hdiv n hn (Pic0.mk ⟨D, hD⟩)
    obtain ⟨E, rfl⟩ := Pic0.mk_surjective y

    have hmem : ((⟨D, hD⟩ : Divisor.degZero (K := L) (F := laurentBaseChange L F₀))
        - n • E : Divisor.degZero (K := L) (F := laurentBaseChange L F₀)) ∈
          (Divisor.principal (K := L) (F := laurentBaseChange L F₀)).addSubgroupOf
            (Divisor.degZero (K := L) (F := laurentBaseChange L F₀)) := by
      rw [← QuotientAddGroup.eq_iff_sub_mem, QuotientAddGroup.mk_nsmul]
      exact hy.symm
    rw [AddSubgroup.mem_addSubgroupOf, AddSubgroupClass.coe_sub, AddSubgroupClass.coe_nsmul] at hmem
    have h0 := hδprin _ hmem
    rw [map_sub, map_nsmul, sub_eq_zero] at h0
    refine ⟨δ (E : Divisor L (laurentBaseChange L F₀)) Q, ?_⟩
    rw [h0, Finsupp.smul_apply, nsmul_eq_mul]

  have hconst : ∀ P Q : Place L (laurentBaseChange L F₀),
      Finsupp.single (r₁ P) (1 : ℤ) - Finsupp.single (r₂ P) 1 =
        Finsupp.single (r₁ Q) 1 - Finsupp.single (r₂ Q) 1 := by
    intro P Q
    have hPQ : Finsupp.single P (1 : ℤ) - Finsupp.single Q 1 ∈
        Divisor.degZero (K := L) (F := laurentBaseChange L F₀) := by
      rw [Divisor.mem_degZero, map_sub, Divisor.degree_single, Divisor.degree_single, hdeg, hdeg, sub_self]
    have h := hδdeg0 _ hPQ
    rw [hδapp, Finsupp.mapDomain_sub, Finsupp.mapDomain_sub, Finsupp.mapDomain_single,
      Finsupp.mapDomain_single, Finsupp.mapDomain_single, Finsupp.mapDomain_single, sub_eq_zero] at h
    exact sub_eq_sub_iff_sub_eq_sub.mpr h

  rw [or_iff_not_imp_left]
  intro hne
  obtain ⟨P₀, hP₀⟩ : ∃ P₀, r₁ P₀ ≠ r₂ P₀ := by
    by_contra hall
    push Not at hall
    exact hne (funext hall)
  have hr₁const : ∀ Q, r₁ Q = r₁ P₀ := by
    intro Q
    have h := congrArg (fun E => E (r₁ P₀)) (hconst Q P₀)
    simp only [Finsupp.sub_apply, Finsupp.single_apply, if_neg (Ne.symm hP₀)] at h
    by_contra hQ
    rw [if_neg hQ] at h
    split_ifs at h <;> omega
  exact fun P Q => (hr₁const P).trans (hr₁const Q).symm

theorem IsLaurentPlaceReduction.eq_of_agree
    {r₁ r₂ : Place L (laurentBaseChange L F₀) → Place k Fbar}
    (hgen : LaurentPrincipalGeneratedByIntegral A π F₀ Fbar)
    (hagree : ∀ D ∈ laurentIntegralPrincipalDivisors A π F₀ Fbar,
      Finsupp.mapDomain r₁ D = Finsupp.mapDomain r₂ D)
    (hdeg : ∀ P : Place L (laurentBaseChange L F₀), P.deg = 1)
    (hprin0 : ∀ D ∈ Divisor.principal (K := L) (F := laurentBaseChange L F₀), Divisor.degree D = 0)
    (hdiv : ∀ n : ℕ, n ≠ 0 → ∀ x : Pic0 L (laurentBaseChange L F₀),
      ∃ y : Pic0 L (laurentBaseChange L F₀), n • y = x)
    (hnc : ∃ D ∈ Divisor.principal (K := L) (F := laurentBaseChange L F₀), Finsupp.mapDomain r₁ D ≠ 0) :
    r₁ = r₂ := by
  rcases IsLaurentPlaceReduction.eq_or_const_of_agree hgen hagree hdeg hdiv with h | hconst
  · exact h
  obtain ⟨D, hDprin, hDne⟩ := hnc
  obtain ⟨P₀⟩ : Nonempty (Place L (laurentBaseChange L F₀)) := by
    by_contra hempty
    rw [not_nonempty_iff] at hempty
    exact hDne (by rw [Subsingleton.elim D 0, Finsupp.mapDomain_zero])
  exfalso
  apply hDne
  have hmapconst : ∀ D : Divisor L (laurentBaseChange L F₀),
      Finsupp.mapDomain r₁ D = Finsupp.single (r₁ P₀) (Divisor.degree D) := by
    intro D
    induction D using Finsupp.induction with
    | zero => simp
    | single_add P n D _ _ ih =>
      rw [Finsupp.mapDomain_add, ih, Finsupp.mapDomain_single, hconst P P₀, map_add,
        Divisor.degree_single, hdeg, Nat.cast_one, mul_one, ← Finsupp.single_add, add_comm]
  rw [hmapconst D, hprin0 D hDprin, Finsupp.single_zero]

end Uniqueness

section CharL

set_option synthInstance.maxHeartbeats 400000

variable (A : ValuationSubring (AlgebraicClosure ℚ)) (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))

abbrev IsPlaceReductionQExpModL
    (r : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (qExpFunctionFieldC ℚ Γ)) →
      Place (IsLocalRing.ResidueField A) (qExpFunctionFieldC (IsLocalRing.ResidueField A) Γ)) : Prop :=
  IsLaurentPlaceReduction A (IsLocalRing.residue A) (qExpFunctionFieldC ℚ Γ)
    (qExpFunctionFieldC (IsLocalRing.ResidueField A) Γ) r

abbrev ReductionInputsQExpModL : Prop :=
  LaurentReductionInputs A (IsLocalRing.residue A) (qExpFunctionFieldC ℚ Γ)
    (qExpFunctionFieldC (IsLocalRing.ResidueField A) Γ)

variable {A Γ} in

def placeReductionQExpModL (h : ReductionInputsQExpModL A Γ) :
    Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (qExpFunctionFieldC ℚ Γ)) →
      Place (IsLocalRing.ResidueField A) (qExpFunctionFieldC (IsLocalRing.ResidueField A) Γ) :=
  h.choose

variable {A Γ} in
theorem isPlaceReductionQExpModL_placeReductionQExpModL (h : ReductionInputsQExpModL A Γ) :
    IsPlaceReductionQExpModL A Γ (placeReductionQExpModL h) :=
  h.choose_spec.1

abbrev reductionQExpModL :
    Pic0 (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (qExpFunctionFieldC ℚ Γ)) →+
      Pic0 (IsLocalRing.ResidueField A) (qExpFunctionFieldC (IsLocalRing.ResidueField A) Γ) :=
  laurentReduction A (IsLocalRing.residue A) (qExpFunctionFieldC ℚ Γ)
    (qExpFunctionFieldC (IsLocalRing.ResidueField A) Γ)

variable {A Γ} in
theorem reductionQExpModL_mk (h : ReductionInputsQExpModL A Γ)
    (D : Divisor.degZero (K := AlgebraicClosure ℚ)
      (F := laurentBaseChange (AlgebraicClosure ℚ) (qExpFunctionFieldC ℚ Γ))) :
    reductionQExpModL A Γ (Pic0.mk D) =
      Pic0.mk (laurentReductionDegZero (placeReductionQExpModL h)
        (isPlaceReductionQExpModL_placeReductionQExpModL h).1 D) :=
  laurentReduction_mk h D

variable {A Γ} in
theorem reductionQExpModL_of_not (h : ¬ ReductionInputsQExpModL A Γ) : reductionQExpModL A Γ = 0 :=
  laurentReduction_of_not h

example (M : ℕ) (z : JOne M) : JOneC M (IsLocalRing.ResidueField A) :=
  reductionQExpModL A (CongruenceSubgroup.Gamma1 M) z

end CharL

end ModularCurve

end

Statements phrased using this module (39)