Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_LanglandsTunnell_ArtinCoreCTM.lean

definition module

Ray-class vocabulary: relative norms, admissible moduli, adelic content

For number fields k \subseteq E the module first sets up the ideal-theoretic relative norm on the coprime-to-modulus groups. Here coprimeToModulus K 𝔣 is the subgroup of units of the group of fractional ideals of K whose v-adic count vanishes at every v \mid \mathfrak f. placeUnder' sends a height-one prime w of \mathcal O_E to the prime below it, modulusExt k E 𝔠 is the extended ideal \mathfrak c\mathcal O_E, and fracRelNormUnit is the ray symbol attached to w \mapsto \mathfrak p_w^{\,f(w/\mathfrak p_w)}, i.e. the multiplicative map sending a fractional ideal of E to the product of \mathfrak p_w^{f\cdot \mathrm{ord}_w}; relNormCTM is its restriction to a homomorphism \mathrm{coprimeToModulus}\,E\,(\mathfrak c\mathcal O_E) \to \mathrm{coprimeToModulus}\,k\,\mathfrak c. Adelically, placeOrd is the v-order of a finite idelic unit (minus the logarithm of its value), fadContentHom the induced content homomorphism to fractional-ideal units, projFin the projection of an adelic unit to its finite part, and placeOf/archRealProjTau/archSign record, for a real embedding \tau, the sign of the component of an adelic unit at the corresponding real place. The predicate IsAdjuster 𝔣 u Ξ± asserts that the finite part of u\alpha^{-1} has valuation 1 at every v \mid \mathfrak f and is congruent to 1 there with precision \exp(-n_v), n_v the multiplicity of v in \mathfrak f, and that u\alpha^{-1} is positive at every real embedding; unitIdeles K 𝔣 is the subgroup of adelic units satisfying these conditions outright. On the Galois side, resHom composes restriction of scalars with restriction to a normal subextension; admissibleExp K v = 4e_v(2)+2e_v(3)+1 and IsAdmissibleModulus K L 𝔣 requires \mathfrak f \neq 0 together with v^{\mathrm{admissibleExp}} \mid \mathfrak f at every v with nontrivial inertia in \mathrm{Gal}(L/K). normRaySubgroup is the join of the narrow ray subgroup with the image of relNormCTM, and FirstInequalityCTM/SecondInequalityCTM are the two divisibilities between \#\mathrm{Gal}(L/K) and the index of that subgroup. primeCarrier/primeCarriers name the classes of primes coprime to the modulus, coprimeToModulus_antitone/ctmInclusion the monotonicity in the modulus. Finally ArtinFieldCore packages, for a prime carrier i, an auxiliary tower E \subseteq N, E \subseteq \Theta = E(\zeta_q) with a multiple \mathfrak m of \mathfrak f, a prime v \nmid \mathfrak m representing i, a prime w of E above v of residue degree 1, admissibility and unramifiedness conditions away from \mathfrak m\mathcal O_E, and injectivity of resHom, with derived data Ip, Ni, Ο‰pi, Pi; ArtinPairCore does the same for two cores and a prescribed \sigma, carrying as a field the compatibility of the Artin symbol of L/K with the relative norm. IdeleFirstIneqData and IdeleFirstIneqDataAt assert the existence of an adelic norm homomorphism compatible with adjusters and with content, surjecting onto unitIdeles for admissible moduli, and whose image together with the principal ideles has index divisible by the degree.

Relation to Mathlib

Mathlib supplies the adele and finite adele rings, fractional ideals with their v-adic counts, infinite places and the arithmetic Frobenius; the ray-class layer used here (coprime-to-modulus and narrow ray subgroups, ray symbols, admissible moduli, the adelic content and adjuster predicates) is the project's own.

Where it is used

This is the class-field-theoretic vocabulary for the Langlands–Tunnell input to the proof: the two inequality predicates and the Artin-symbol cores are the data from which global reciprocity for abelian extensions of number fields is assembled, and that reciprocity underlies the construction of the Hecke characters used in Langlands–Tunnell, hence the modularity of the mod 3 representation attached to a Frey curve.

References

  1. J. Neukirch, Algebraic Number Theory, Grundlehren der mathematischen Wissenschaften 322, Springer, 1999, Ch. VI
  2. S. Lang, Algebraic Number Theory, 2nd ed., Graduate Texts in Mathematics 110, Springer, 1994
  3. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154

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

Imports

Imported by

Declarations

Source

import Definitions.Def_LanglandsTunnell_ArtinFrobenius
import Definitions.Def_M4aHerbrand_IdeleClassVocab

set_option autoImplicit false

noncomputable section

open Deep.NTSupply NumberField IsDedekindDomain WithZero
open scoped nonZeroDivisors IsMulCommutative Pointwise

namespace HeckeCharacter

section RelNorm

variable (k E : Type*) [Field k] [NumberField k] [Field E] [NumberField E] [Algebra k E]

def placeUnder' (w : HeightOneSpectrum (π“ž E)) : HeightOneSpectrum (π“ž k) :=
  ⟨w.asIdeal.under (π“ž k), inferInstance,
    fun h => w.ne_bot (Ideal.eq_bot_of_comap_eq_bot h)⟩

omit [NumberField k] [NumberField E] in
theorem placeUnder'_asIdeal (w : HeightOneSpectrum (π“ž E)) :
    (placeUnder' k E w).asIdeal = w.asIdeal.under (π“ž k) := rfl

abbrev modulusExt (𝔠 : Ideal (π“ž k)) : Ideal (π“ž E) := 𝔠.map (algebraMap (π“ž k) (π“ž E))

def fracRelNormUnit : (FractionalIdeal ((π“ž E)⁰) E)Λ£ β†’* (FractionalIdeal ((π“ž k)⁰) k)Λ£ :=
  raySymbolUnitsHom E (fun w =>
    primeUnit k (placeUnder' k E w) ^ ((placeUnder' k E w).asIdeal.inertiaDeg' w.asIdeal))

theorem placeUnder'_dvd_iff (𝔠 : Ideal (π“ž k)) (w : HeightOneSpectrum (π“ž E)) :
    (placeUnder' k E w).asIdeal ∣ 𝔠 ↔ w.asIdeal ∣ modulusExt k E 𝔠 := by
  rw [placeUnder'_asIdeal, modulusExt, Ideal.dvd_iff_le, Ideal.dvd_iff_le,
    Ideal.map_le_iff_le_comap]

def gcopNC2 (𝔠 : Ideal (π“ž k)) (w : HeightOneSpectrum (π“ž E)) : β†₯(coprimeToModulus k 𝔠) := by
  classical
  exact if h : Β¬ (placeUnder' k E w).asIdeal ∣ 𝔠
    then ⟨primeUnit k (placeUnder' k E w) ^ ((placeUnder' k E w).asIdeal.inertiaDeg' w.asIdeal),
      pow_mem (primeUnit_mem_coprimeToModulus k h) _⟩
    else 1

theorem coe_raySymbol_gcop_eq_fracRelNormUnit' {𝔠 : Ideal (π“ž k)}
    (Y : (FractionalIdeal ((π“ž E)⁰) E)Λ£) (hY : Y ∈ coprimeToModulus E (modulusExt k E 𝔠)) :
    ((raySymbol E (gcopNC2 k E 𝔠) (Y : FractionalIdeal ((π“ž E)⁰) E)
      : β†₯(coprimeToModulus k 𝔠)) : (FractionalIdeal ((π“ž k)⁰) k)Λ£)
      = fracRelNormUnit k E Y := by
  unfold raySymbol
  refine (MonoidHom.map_finprod ((coprimeToModulus k 𝔠).subtype)
    (hasFiniteMulSupport_raySymbol_factors E (gcopNC2 k E 𝔠) _)).trans ?_
  rw [show fracRelNormUnit k E Y
      = ∏ᢠ w, (primeUnit k (placeUnder' k E w)
            ^ ((placeUnder' k E w).asIdeal.inertiaDeg' w.asIdeal))
          ^ FractionalIdeal.count E w (Y : FractionalIdeal ((π“ž E)⁰) E) from rfl]
  refine finprod_congr (fun w => ?_)
  rw [map_zpow, Subgroup.coe_subtype]
  classical
  by_cases hw : (placeUnder' k E w).asIdeal ∣ 𝔠
  Β· have hct : FractionalIdeal.count E w (Y : FractionalIdeal ((π“ž E)⁰) E) = 0 :=
      (mem_coprimeToModulus_iff E).mp hY w ((placeUnder'_dvd_iff k E 𝔠 w).mp hw)
    rw [hct]; simp
  Β· simp only [gcopNC2]; rw [dif_pos hw]

theorem fracRelNormUnit_mem_coprimeToModulus {𝔠 : Ideal (π“ž k)}
    {Y : (FractionalIdeal ((π“ž E)⁰) E)Λ£} (hY : Y ∈ coprimeToModulus E (modulusExt k E 𝔠)) :
    fracRelNormUnit k E Y ∈ coprimeToModulus k 𝔠 :=
  coe_raySymbol_gcop_eq_fracRelNormUnit' k E Y hY β–Έ (raySymbol E (gcopNC2 k E 𝔠) _).2

def relNormCTM (𝔠 : Ideal (π“ž k)) :
    β†₯(coprimeToModulus E (modulusExt k E 𝔠)) β†’* β†₯(coprimeToModulus k 𝔠) :=
  ((fracRelNormUnit k E).comp (coprimeToModulus E (modulusExt k E 𝔠)).subtype).codRestrict
    (coprimeToModulus k 𝔠) (fun Y => fracRelNormUnit_mem_coprimeToModulus k E Y.2)

end RelNorm

section Content

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

theorem fad_one_apply (v : HeightOneSpectrum (π“ž K)) :
    ((1 : FiniteAdeleRing (π“ž K) K) v : v.adicCompletion K) = 1 := rfl

theorem fad_mul_apply (a b : FiniteAdeleRing (π“ž K) K) (v : HeightOneSpectrum (π“ž K)) :
    ((a * b : FiniteAdeleRing (π“ž K) K) v : v.adicCompletion K) = a v * b v := rfl

def placeOrd (u : (FiniteAdeleRing (π“ž K) K)Λ£) (v : HeightOneSpectrum (π“ž K)) : β„€ :=
  -WithZero.log (Valued.v ((u : FiniteAdeleRing (π“ž K) K) v))

theorem placeOrd_one (v : HeightOneSpectrum (π“ž K)) : placeOrd K 1 v = 0 := by
  unfold placeOrd
  rw [Units.val_one, fad_one_apply, map_one, WithZero.log_one, neg_zero]

theorem valued_ne_zero_of_unit (u : (FiniteAdeleRing (π“ž K) K)Λ£)
    (v : HeightOneSpectrum (π“ž K)) :
    Valued.v ((u : FiniteAdeleRing (π“ž K) K) v) β‰  0 := by
  rw [ne_eq, map_eq_zero]
  exact ((FiniteAdeleRing.isUnit_iff.mp u.isUnit).1 v)

theorem placeOrd_mul (u u' : (FiniteAdeleRing (π“ž K) K)Λ£) (v : HeightOneSpectrum (π“ž K)) :
    placeOrd K (u * u') v = placeOrd K u v + placeOrd K u' v := by
  unfold placeOrd
  rw [Units.val_mul, fad_mul_apply, map_mul,
    WithZero.log_mul (valued_ne_zero_of_unit K u v) (valued_ne_zero_of_unit K u' v),
    neg_add]

theorem placeOrd_eq_zero_iff (u : (FiniteAdeleRing (π“ž K) K)Λ£) (v : HeightOneSpectrum (π“ž K)) :
    placeOrd K u v = 0 ↔ Valued.v ((u : FiniteAdeleRing (π“ž K) K) v) = 1 := by
  unfold placeOrd
  rw [neg_eq_zero]
  constructor
  Β· intro hlog
    have h := WithZero.exp_log (x := Valued.v ((u : FiniteAdeleRing (π“ž K) K) v))
      (valued_ne_zero_of_unit K u v)
    rw [hlog, WithZero.exp_zero] at h
    exact h.symm
  Β· intro h; rw [h, WithZero.log_one]

theorem finite_support_placeOrd (u : (FiniteAdeleRing (π“ž K) K)Λ£) :
    (Function.support (placeOrd K u)).Finite := by
  have h := FiniteAdeleRing.unitsEquiv_finite_valued_eq_one (R := π“ž K) (K := K) u
  rw [Filter.eventually_cofinite] at h
  refine h.subset fun v hv => ?_
  rw [Function.mem_support] at hv
  rw [Set.mem_setOf_eq]
  intro hval
  exact hv ((placeOrd_eq_zero_iff K u v).mpr (by
    set_option backward.isDefEq.respectTransparency false in
    simpa [RestrictedProduct.unitsEquiv_apply] using hval))

def fadContentHom : (FiniteAdeleRing (π“ž K) K)Λ£ β†’* (FractionalIdeal ((π“ž K)⁰) K)Λ£ where
  toFun u := ∏ᢠ v : HeightOneSpectrum (π“ž K), (primeUnit K v) ^ (placeOrd K u v)
  map_one' := by simp [placeOrd_one]
  map_mul' u u' := by
    simp only [placeOrd_mul, zpow_add]
    exact finprod_mul_distrib
      ((finite_support_placeOrd K u).subset fun v hv => by
        simp only [Function.mem_mulSupport, ne_eq] at hv ⊒
        contrapose! hv; rw [Function.mem_support, not_not] at hv; simp [hv])
      ((finite_support_placeOrd K u').subset fun v hv => by
        simp only [Function.mem_mulSupport, ne_eq] at hv ⊒
        contrapose! hv; rw [Function.mem_support, not_not] at hv; simp [hv])

def projFin : (AdeleRing (π“ž K) K)Λ£ β†’* (FiniteAdeleRing (π“ž K) K)Λ£ :=
  (MonoidHom.snd (InfiniteAdeleRing K)Λ£ (FiniteAdeleRing (π“ž K) K)Λ£).comp
    MulEquiv.prodUnits.toMonoidHom

noncomputable def placeOf (Ο„ : K β†’+* ℝ) : InfinitePlace K :=
  InfinitePlace.mk (Complex.ofRealHom.comp Ο„)

omit [NumberField K] in

theorem isReal_compOfRealHom (Ο„ : K β†’+* ℝ) :
    ComplexEmbedding.IsReal (Complex.ofRealHom.comp Ο„) :=
  RingHom.ext fun x => Complex.conj_ofReal (Ο„ x)

omit [NumberField K] in
theorem isReal_placeOf (Ο„ : K β†’+* ℝ) : (placeOf K Ο„).IsReal :=
  ⟨_, isReal_compOfRealHom K Ο„, rfl⟩

open InfinitePlace.Completion in

noncomputable def archRealProjTau (Ο„ : K β†’+* ℝ) (u : (AdeleRing (π“ž K) K)Λ£) : ℝ :=
  ringEquivRealOfIsReal (isReal_placeOf K Ο„)
    (((u : AdeleRing (π“ž K) K).1 : InfiniteAdeleRing K) (placeOf K Ο„))

open InfinitePlace.Completion in
theorem archRealProjTau_mul (Ο„ : K β†’+* ℝ) (u u' : (AdeleRing (π“ž K) K)Λ£) :
    archRealProjTau K Ο„ (u * u') = archRealProjTau K Ο„ u * archRealProjTau K Ο„ u' := by
  unfold archRealProjTau
  rw [← map_mul]; rfl

open InfinitePlace.Completion in
theorem archRealProjTau_ne_zero (Ο„ : K β†’+* ℝ) (u : (AdeleRing (π“ž K) K)Λ£) :
    archRealProjTau K Ο„ u β‰  0 := by
  intro h
  have h1 : archRealProjTau K Ο„ u * archRealProjTau K Ο„ u⁻¹ = 1 := by
    rw [← archRealProjTau_mul, mul_inv_cancel]
    unfold archRealProjTau; rw [Units.val_one]
    exact (congrArg (ringEquivRealOfIsReal (isReal_placeOf K Ο„)) rfl).trans (map_one _)
  rw [h, zero_mul] at h1; exact zero_ne_one h1

def archSign (Ο„ : K β†’+* ℝ) (u : (AdeleRing (π“ž K) K)Λ£) : Prop :=
  0 < archRealProjTau K Ο„ u

open InfinitePlace.Completion in

theorem archSign_of_fst_eq_one (Ο„ : K β†’+* ℝ) {u : (AdeleRing (π“ž K) K)Λ£}
    (huarch : (u : AdeleRing (π“ž K) K).1 = 1) : archSign K Ο„ u := by
  show (0:ℝ) < ringEquivRealOfIsReal (isReal_placeOf K Ο„) _
  rw [huarch, show ((1 : InfiniteAdeleRing K) (placeOf K Ο„)) = 1 from rfl, map_one]
  exact one_pos

theorem archSign_mul (Ο„ : K β†’+* ℝ) (u u' : (AdeleRing (π“ž K) K)Λ£) :
    archSign K Ο„ (u * u') ↔ (archSign K Ο„ u ↔ archSign K Ο„ u') := by
  unfold archSign; rw [archRealProjTau_mul]
  constructor
  Β· intro hmul
    rcases mul_pos_iff.mp hmul with ⟨h1, h2⟩ | ⟨h1, h2⟩
    Β· exact iff_of_true h1 h2
    Β· exact iff_of_false h1.not_gt h2.not_gt
  Β· intro hiff
    rcases (archRealProjTau_ne_zero K Ο„ u).lt_or_gt with h1 | h1
    Β· have h2 := (not_iff_not.mpr hiff).mp h1.not_gt
      exact mul_pos_of_neg_of_neg h1 ((archRealProjTau_ne_zero K Ο„ u').lt_or_gt.resolve_right h2)
    Β· exact mul_pos h1 (hiff.mp h1)

theorem archSign_one (Ο„ : K β†’+* ℝ) : archSign K Ο„ 1 :=
  archSign_of_fst_eq_one K Ο„ rfl

theorem archSign_inv (Ο„ : K β†’+* ℝ) (u : (AdeleRing (π“ž K) K)Λ£) :
    archSign K Ο„ u⁻¹ ↔ archSign K Ο„ u := by
  have h := archSign_mul K Ο„ u u⁻¹
  rw [mul_inv_cancel, iff_true_intro (archSign_one K Ο„), true_iff] at h
  exact h.symm

theorem unit_cong_mul {v : HeightOneSpectrum (π“ž K)} {Ξ΅ : ℀ᡐ⁰} {a b : v.adicCompletion K}
    (hva : Valued.v a = 1) (hca : Valued.v (a - 1) ≀ Ξ΅)
    (hvb : Valued.v b = 1) (hcb : Valued.v (b - 1) ≀ Ξ΅) :
    Valued.v (a * b) = 1 ∧ Valued.v (a * b - 1) ≀ Ξ΅ := by
  refine ⟨by rw [map_mul, hva, hvb, one_mul], ?_⟩
  have heq : a * b - 1 = a * (b - 1) + (a - 1) := by ring
  calc Valued.v (a * b - 1) = Valued.v (a * (b - 1) + (a - 1)) := by rw [heq]
    _ ≀ max (Valued.v (a * (b - 1))) (Valued.v (a - 1)) := Valuation.map_add _ _ _
    _ ≀ Ξ΅ := by
        rw [map_mul, hva, one_mul]
        exact max_le hcb hca

theorem unit_cong_div {v : HeightOneSpectrum (π“ž K)} {Ξ΅ : ℀ᡐ⁰} {a b : v.adicCompletion K}
    (hca : Valued.v (a - 1) ≀ Ξ΅)
    (hvb : Valued.v b = 1) (hcb : Valued.v (b - 1) ≀ Ξ΅) :
    Valued.v (a * b⁻¹ - 1) ≀ Ξ΅ := by
  have hb0 : b β‰  0 := fun h => by simp [h] at hvb
  have heq : a * b⁻¹ - 1 = (a - b) * b⁻¹ := by field_simp
  rw [heq, map_mul, map_invβ‚€, hvb, inv_one, mul_one]
  calc Valued.v (a - b) = Valued.v ((a - 1) - (b - 1)) := by ring_nf
    _ ≀ max (Valued.v (a - 1)) (Valued.v (b - 1)) := Valuation.map_sub _ _ _
    _ ≀ Ξ΅ := max_le hca hcb

theorem fad_units_inv_apply (X : (FiniteAdeleRing (π“ž K) K)Λ£)
    (v : HeightOneSpectrum (π“ž K)) :
    (((X⁻¹ : (FiniteAdeleRing (π“ž K) K)Λ£) : FiniteAdeleRing (π“ž K) K) v)
      = (((X : (FiniteAdeleRing (π“ž K) K)Λ£) : FiniteAdeleRing (π“ž K) K) v)⁻¹ := by
  refine eq_inv_of_mul_eq_one_right ?_
  rw [← fad_mul_apply, ← Units.val_mul, mul_inv_cancel, Units.val_one, fad_one_apply]

structure IsAdjuster (𝔣 : Ideal (π“ž K)) (u : (AdeleRing (π“ž K) K)Λ£) (Ξ± : KΛ£) : Prop where
  cong : βˆ€ v : HeightOneSpectrum (π“ž K), v.asIdeal ∣ 𝔣 β†’
    Valued.v ((((u * (Units.map (algebraMap K (AdeleRing (π“ž K) K)) Ξ±)⁻¹ :
        (AdeleRing (π“ž K) K)Λ£) : AdeleRing (π“ž K) K).2 : FiniteAdeleRing (π“ž K) K) v) = 1 ∧
    Valued.v ((((u * (Units.map (algebraMap K (AdeleRing (π“ž K) K)) Ξ±)⁻¹ :
        (AdeleRing (π“ž K) K)Λ£) : AdeleRing (π“ž K) K).2 : FiniteAdeleRing (π“ž K) K) v - 1)
      ≀ WithZero.exp (-((Associates.mk v.asIdeal).count (Associates.mk 𝔣).factors : β„€))
  sign : βˆ€ Ο„ : K β†’+* ℝ,
    archSign K Ο„ (u * (Units.map (algebraMap K (AdeleRing (π“ž K) K)) Ξ±)⁻¹)

end Content

end HeckeCharacter

namespace LanglandsTunnell.P2.Artin

open NumberField IsDedekindDomain Deep.NTSupply HeckeCharacter WithZero

section Carriers

variable (K : Type*) [Field K] [NumberField K] (𝔣 : Ideal (π“ž K))

def primeCarrier (v : HeightOneSpectrum (π“ž K)) (hv : Β¬ v.asIdeal ∣ 𝔣) : β†₯(coprimeToModulus K 𝔣) :=
  ⟨primeUnit K v, primeUnit_mem_coprimeToModulus K hv⟩

def primeCarriers : Set β†₯(coprimeToModulus K 𝔣) :=
  {x | βˆƒ (v : HeightOneSpectrum (π“ž K)) (hv : Β¬ v.asIdeal ∣ 𝔣), x = primeCarrier K 𝔣 v hv}

end Carriers

section Inclusion

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

theorem coprimeToModulus_antitone {𝔣 π”ͺ : Ideal (π“ž K)} (h : 𝔣 ∣ π”ͺ) : coprimeToModulus K π”ͺ ≀ coprimeToModulus K 𝔣 :=
  fun _ hx v hv => hx v (dvd_trans hv h)

noncomputable def ctmInclusion {𝔣 π”ͺ : Ideal (π“ž K)} (h : 𝔣 ∣ π”ͺ) : β†₯(coprimeToModulus K π”ͺ) β†’* β†₯(coprimeToModulus K 𝔣) :=
  Subgroup.inclusion (coprimeToModulus_antitone K h)

end Inclusion

section Tower

variable (K M E N : Type*) [Field K] [NumberField K] [Field M] [NumberField M] [Field E]
  [NumberField E] [Field N] [NumberField N]
  [Algebra K M] [Algebra K E] [Algebra K N] [Algebra M N] [Algebra E N] [IsScalarTower K M N]
  [IsScalarTower K E N] [IsGalois K M] [IsGalois E N]

def resHom : (N ≃ₐ[E] N) β†’* (M ≃ₐ[K] M) :=
  (AlgEquiv.restrictNormalHom M).comp
    { toFun := fun Οƒ => Οƒ.restrictScalars K
      map_one' := AlgEquiv.ext fun _ => rfl
      map_mul' := fun _ _ => AlgEquiv.ext fun _ => rfl }

end Tower

section Admissible

variable (K L : Type*) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L]
  [IsGalois K L]

def admissibleExp (v : HeightOneSpectrum (π“ž K)) : β„• :=
  4 * Ideal.ramificationIdx' (Ideal.span {(2 : β„€)}) v.asIdeal + 2 * Ideal.ramificationIdx' (Ideal.span {(3 : β„€)}) v.asIdeal + 1

def IsAdmissibleModulus (𝔣 : Ideal (π“ž K)) : Prop :=
  𝔣 β‰  βŠ₯ ∧ βˆ€ v : HeightOneSpectrum (π“ž K), (primeAbove K L v).inertia (L ≃ₐ[K] L) β‰  βŠ₯ β†’ v.asIdeal ^ admissibleExp K v ∣ 𝔣

end Admissible

section DefN

variable (K L : Type*) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L]

def normRaySubgroup (𝔣 : Ideal (π“ž K)) : Subgroup β†₯(coprimeToModulus K 𝔣) :=
  (narrowRaySubgroup K 𝔣).subgroupOf (coprimeToModulus K 𝔣)
    βŠ” (HeckeCharacter.relNormCTM K L 𝔣).range

end DefN

section Pincer

variable (K L : Type*) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L]
  [IsGalois K L] [IsMulCommutative (L ≃ₐ[K] L)]

def SecondInequalityCTM (𝔣 : Ideal (π“ž K)) : Prop :=
  (normRaySubgroup K L 𝔣).index ∣ Nat.card (L ≃ₐ[K] L)

def FirstInequalityCTM (𝔣 : Ideal (π“ž K)) : Prop :=
  Nat.card (L ≃ₐ[K] L) ∣ (normRaySubgroup K L 𝔣).index

end Pincer

section UnitIdeles

variable (K : Type*) [Field K] [NumberField K] (𝔣 : Ideal (π“ž K))

def unitIdeles : Subgroup (AdeleRing (π“ž K) K)Λ£ where
  carrier := {u | (βˆ€ v : HeightOneSpectrum (π“ž K), Valued.v (((projFin K u : (FiniteAdeleRing (π“ž K) K)Λ£) : FiniteAdeleRing (π“ž K) K) v) = 1) ∧
    (βˆ€ v : HeightOneSpectrum (π“ž K), v.asIdeal ∣ 𝔣 β†’
      Valued.v (((projFin K u : (FiniteAdeleRing (π“ž K) K)Λ£) : FiniteAdeleRing (π“ž K) K) v - 1) ≀ exp (-((Associates.mk v.asIdeal).count (Associates.mk 𝔣).factors : β„€))) ∧
    βˆ€ Ο„ : K β†’+* ℝ, archSign K Ο„ u}
  one_mem' := ⟨fun v => by rw [map_one, Units.val_one, fad_one_apply, map_one],
    fun v _ => by rw [map_one, Units.val_one, fad_one_apply, sub_self, map_zero]; exact zero_le', fun Ο„ => archSign_one K Ο„βŸ©
  mul_mem' {u u'} hu hu' := by
    refine ⟨fun v => ?_, fun v hv => ?_, fun Ο„ => (archSign_mul K Ο„ u u').mpr (iff_of_true (hu.2.2 Ο„) (hu'.2.2 Ο„))⟩
    Β· rw [map_mul, Units.val_mul, fad_mul_apply, map_mul, hu.1 v, hu'.1 v, one_mul]
    Β· rw [map_mul, Units.val_mul, fad_mul_apply]
      exact (unit_cong_mul K (hu.1 v) (hu.2.1 v hv) (hu'.1 v) (hu'.2.1 v hv)).2
  inv_mem' {u} hu := by
    refine ⟨fun v => ?_, fun v hv => ?_, fun Ο„ => (archSign_inv K Ο„ u).mpr (hu.2.2 Ο„)⟩
    Β· rw [map_inv, fad_units_inv_apply, map_invβ‚€, hu.1 v, inv_one]
    Β· rw [map_inv, fad_units_inv_apply]
      have h := unit_cong_div K (a := (1 : v.adicCompletion K)) (by rw [sub_self, map_zero]; exact zero_le') (hu.1 v) (hu.2.1 v hv)
      rwa [one_mul] at h

end UnitIdeles

structure ArtinFieldCore (K L : Type*) [Field K] [NumberField K] [Field L] [NumberField L]
    [Algebra K L] [IsGalois K L] [IsMulCommutative (L ≃ₐ[K] L)]
    (𝔣 : Ideal (π“ž K)) (i : β†₯(primeCarriers K 𝔣)) where
  E : Type*
  N : Type*
  Θ : Type*
  [instFE : Field E]
  [instNFE : NumberField E]
  [instFN : Field N]
  [instNFN : NumberField N]
  [instFΘ : Field Θ]
  [instNFΘ : NumberField Θ]
  [instAKE : Algebra K E]
  [instAKN : Algebra K N]
  [instAEN : Algebra E N]
  [instALN : Algebra L N]
  [instAEΘ : Algebra E Θ]
  [instANΘ : Algebra N Θ]
  [instSTKEN : IsScalarTower K E N]
  [instSTKLN : IsScalarTower K L N]
  [instSTENΘ : IsScalarTower E N Θ]
  [instGEN : IsGalois E N]
  [instGEΘ : IsGalois E Θ]
  [instCN : IsMulCommutative (N ≃ₐ[E] N)]
  [instCΘ : IsMulCommutative (Θ ≃ₐ[E] Θ)]
  π”ͺ : Ideal (π“ž K)
  hπ”ͺ : 𝔣 ∣ π”ͺ
  v : HeightOneSpectrum (π“ž K)
  hvπ”ͺ : Β¬ v.asIdeal ∣ π”ͺ
  hvi : primeCarrier K 𝔣 v (fun hv => hvπ”ͺ (dvd_trans hv hπ”ͺ)) = (i : β†₯(coprimeToModulus K 𝔣))
  w : HeightOneSpectrum (π“ž E)
  hw : Β¬ w.asIdeal ∣ modulusExt K E π”ͺ
  hwv : w.asIdeal.under (π“ž K) = v.asIdeal
  hf : v.asIdeal.inertiaDeg' w.asIdeal = 1
  q : β„•
  [instNZq : NeZero q]
  ΢ : Θ
  hΞΆ : IsPrimitiveRoot ΞΆ q
  htop : (IntermediateField.adjoin E {΢} : IntermediateField E Θ) = ⊀
  hqπ”ͺ : Ideal.span {(q : π“ž E)} ∣ modulusExt K E π”ͺ
  hunr : βˆ€ v' : HeightOneSpectrum (π“ž E), Β¬ v'.asIdeal ∣ modulusExt K E π”ͺ β†’
    ((primeAbove E Θ v').under (π“ž N)).inertia (N ≃ₐ[E] N) = βŠ₯
  hadm : IsAdmissibleModulus E N (modulusExt K E π”ͺ)
  hI_E : βˆ€ w' : HeightOneSpectrum (π“ž E), Β¬ w'.asIdeal ∣ modulusExt K E π”ͺ β†’
    ((primeAbove E N w').under (π“ž L)).inertia (L ≃ₐ[K] L) = βŠ₯
  hresInj : Function.Injective (resHom K L E N)

attribute [instance] ArtinFieldCore.instFE ArtinFieldCore.instNFE ArtinFieldCore.instFN
  ArtinFieldCore.instNFN ArtinFieldCore.instFΘ ArtinFieldCore.instNFΘ ArtinFieldCore.instAKE
  ArtinFieldCore.instAKN ArtinFieldCore.instAEN ArtinFieldCore.instALN ArtinFieldCore.instAEΘ
  ArtinFieldCore.instANΘ ArtinFieldCore.instSTKEN ArtinFieldCore.instSTKLN
  ArtinFieldCore.instSTENΘ ArtinFieldCore.instGEN ArtinFieldCore.instGEΘ ArtinFieldCore.instCN
  ArtinFieldCore.instCΘ ArtinFieldCore.instNZq

section PerICore

set_option maxSynthPendingDepth 3

variable {K L : Type*} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L]
  [IsGalois K L] [IsMulCommutative (L ≃ₐ[K] L)] {𝔣 : Ideal (π“ž K)} {i : β†₯(primeCarriers K 𝔣)}
  (c : ArtinFieldCore K L 𝔣 i)

def ArtinFieldCore.Ip : Type _ := β†₯(coprimeToModulus c.E (modulusExt K c.E c.π”ͺ))

instance : CommGroup c.Ip := inferInstanceAs (CommGroup β†₯(coprimeToModulus c.E (modulusExt K c.E c.π”ͺ)))

def ArtinFieldCore.Ni : c.Ip β†’* β†₯(coprimeToModulus K 𝔣) :=
  (ctmInclusion K c.hπ”ͺ).comp (relNormCTM K c.E c.π”ͺ)

def ArtinFieldCore.Ο‰pi : c.Ip β†’* (L ≃ₐ[K] L) :=
  (resHom K L c.E c.N).comp (artinSymbol c.E c.N (modulusExt K c.E c.π”ͺ))

def ArtinFieldCore.Pi : c.Ip := ⟨primeUnit c.E c.w, primeUnit_mem_coprimeToModulus c.E c.hw⟩

end PerICore

structure ArtinPairCore (K L : Type*) [Field K] [NumberField K] [Field L] [NumberField L]
    [Algebra K L] [IsGalois K L] [IsMulCommutative (L ≃ₐ[K] L)]
    (𝔣 : Ideal (π“ž K)) (Οƒ : L ≃ₐ[K] L) {i j : β†₯(primeCarriers K 𝔣)}
    (ci : ArtinFieldCore K L 𝔣 i) (cj : ArtinFieldCore K L 𝔣 j) where
  E'' : Type*
  N'' : Type*
  [instFE : Field E'']
  [instNFE : NumberField E'']
  [instFN : Field N'']
  [instNFN : NumberField N'']
  [instAKE : Algebra K E'']
  [instAKN : Algebra K N'']
  [instAiE : Algebra ci.E E'']
  [instAjE : Algebra cj.E E'']
  [instSTKiE : IsScalarTower K ci.E E'']
  [instSTKjE : IsScalarTower K cj.E E'']
  [instAEN : Algebra E'' N'']
  [instALN : Algebra L N'']
  [instSTKEN : IsScalarTower K E'' N'']
  [instSTKLN : IsScalarTower K L N'']
  [instGEN : IsGalois E'' N'']
  [instCN : IsMulCommutative (N'' ≃ₐ[E''] N'')]
  π”ͺ'' : Ideal (π“ž K)
  h'' : 𝔣 ∣ π”ͺ''
  hi'' : ci.π”ͺ ∣ π”ͺ''
  hj'' : cj.π”ͺ ∣ π”ͺ''
  hadm'' : IsAdmissibleModulus E'' N'' (modulusExt K E'' π”ͺ'')
  hcompat'' : βˆ€ B : β†₯(coprimeToModulus E'' (modulusExt K E'' π”ͺ'')),
    artinSymbol K L 𝔣 (ctmInclusion K h'' (relNormCTM K E'' π”ͺ'' B))
      = resHom K L E'' N'' (artinSymbol E'' N'' (modulusExt K E'' π”ͺ'') B)
  hΟƒ'' : Οƒ ∈ (resHom K L E'' N'').range
  hresInj'' : Function.Injective (resHom K L E'' N'')

attribute [instance] ArtinPairCore.instFE ArtinPairCore.instNFE ArtinPairCore.instFN ArtinPairCore.instNFN
  ArtinPairCore.instAKE ArtinPairCore.instAKN ArtinPairCore.instAiE ArtinPairCore.instAjE ArtinPairCore.instSTKiE
  ArtinPairCore.instSTKjE ArtinPairCore.instAEN ArtinPairCore.instALN ArtinPairCore.instSTKEN ArtinPairCore.instSTKLN
  ArtinPairCore.instGEN ArtinPairCore.instCN

section IdeleData

variable (K M : Type*) [Field K] [NumberField K] [Field M] [NumberField M] [Algebra K M]
  [IsGalois K M] [IsMulCommutative (M ≃ₐ[K] M)]

def IdeleFirstIneqData (F : IntermediateField K M) (𝔣 : Ideal (π“ž K)) : Prop :=
  βˆƒ Nrm : (AdeleRing (π“ž F) F)Λ£ β†’* (AdeleRing (π“ž K) K)Λ£,
    (βˆ€ {u : (AdeleRing (π“ž F) F)Λ£} {Ξ± : (F)Λ£},
      IsAdjuster F (modulusExt K F 𝔣) u Ξ± β†’ IsAdjuster K 𝔣 (Nrm u) (Units.map (Algebra.norm K) Ξ±)) ∧
    (βˆ€ u : (AdeleRing (π“ž F) F)Λ£,
      fadContentHom K (projFin K (Nrm u)) = fracRelNormUnit K F (fadContentHom F (projFin F u))) ∧
    (IsAdmissibleModulus K F 𝔣 β†’ unitIdeles K 𝔣 ≀ Nrm.range) ∧
    Module.finrank K F ∣ (M4aHerbrand.principalIdeles (π“ž K) K βŠ” Nrm.range).index

end IdeleData

section IdeleDataTop

variable (K M : Type*) [Field K] [NumberField K] [Field M] [NumberField M] [Algebra K M]

def IdeleFirstIneqDataAt (𝔣 : Ideal (π“ž K)) : Prop :=
  βˆƒ Nrm : (AdeleRing (π“ž M) M)Λ£ β†’* (AdeleRing (π“ž K) K)Λ£,
    (βˆ€ {u : (AdeleRing (π“ž M) M)Λ£} {Ξ± : MΛ£},
      IsAdjuster M (modulusExt K M 𝔣) u Ξ± β†’ IsAdjuster K 𝔣 (Nrm u) (Units.map (Algebra.norm K) Ξ±)) ∧
    (βˆ€ u : (AdeleRing (π“ž M) M)Λ£,
      fadContentHom K (projFin K (Nrm u)) = fracRelNormUnit K M (fadContentHom M (projFin M u))) ∧
    (IsAdmissibleModulus K M 𝔣 β†’ unitIdeles K 𝔣 ≀ Nrm.range) ∧
    Module.finrank K M ∣ (M4aHerbrand.principalIdeles (π“ž K) K βŠ” Nrm.range).index

end IdeleDataTop

end LanglandsTunnell.P2.Artin

Statements phrased using this module (72)