Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_NarrowRayClassGroup.lean

definition module

Narrow ray class groups, finiteness, and ray symbols

For a number field K and an ideal \mathfrak f \subseteq \mathcal O_K, the module works inside the group of units of the fractional ideals of \mathcal O_K in K. coprimeToModulus K 𝔣 is the subgroup of those invertible fractional ideals I with FractionalIdeal.count K v I = 0 at every height-one prime v of \mathcal O_K with v.\mathrm{asIdeal} \mid \mathfrak f; narrowRaySet K 𝔣 is the set of invertible fractional ideals of the shape (\alpha) for some \alpha \in \mathcal O_K with \alpha \neq 0, \alpha - 1 \in \mathfrak f, and \tau(\alpha) > 0 for every ring homomorphism \tau : K \to \mathbb R, and narrowRaySubgroup K 𝔣 is the subgroup it generates. NarrowRayClassGroup K 𝔣 is the quotient of coprimeToModulus K 𝔣 by the pullback of narrowRaySubgroup K 𝔣, with projection NarrowRayClassGroup.mk; membership criteria, a criterion for two classes to agree, the unit class of a prime not dividing \mathfrak f (primeUnit, primeClass), and the degenerate computation coprimeToModulus_top accompany it.

The finiteness theorem finite asserts that NarrowRayClassGroup K 𝔣 is finite whenever \mathfrak f \neq \bot. It is reached through raySet (the same condition without the positivity at real places), the subgroup rayClassSubgroup generated by the classes of its members β€” these classes square to 1 and are parametrised by sign vectors in (K \to_{+*} \mathbb R) \to \mathrm{Bool}, hence finitely many β€” the homomorphisms to ClassGroup (π“ž K) induced by I \mapsto [I], the finiteness of \mathcal O_K/\mathfrak f, and the predicate MovingLemma K 𝔣: every nonzero x_0 \in K whose principal fractional ideal has vanishing counts at the primes dividing \mathfrak f can be multiplied by some \beta \in \mathcal O_K, \beta \neq 0, \beta - 1 \in \mathfrak f, so as to become integral. movingLemma proves this predicate for \mathfrak f \neq \bot using the Dedekind approximation theorem.

Finally, for a commutative group M and f a function on height-one primes, raySymbol K f I is the finitary product \prod_v f(v)^{\mathrm{count}_v I}; it gives homomorphisms on the unit group, on coprimeToModulus K 𝔣, and on the nonzero ideals, sends primeUnit K v to f(v), and raySymbolDescend descends it to NarrowRayClassGroup K 𝔣 under the hypothesis that it kills every (\alpha) with \alpha \neq 0, \alpha - 1 \in \mathfrak f and \alpha positive at all real embeddings. A general group-theoretic lemma, that the subgroup generated by a finite set of involutions in a commutative group is finite, is proved here as well.

Relation to Mathlib

Mathlib supplies the ambient objects used here β€” fractional ideals and their unit group, the height-one spectrum with its count valuations, and ClassGroup β€” while the narrow ray class group at a modulus, its finiteness, the moving-lemma predicate and the ray symbol are the project's own constructions on top of them.

Where it is used

The module is background number theory: it supplies a finite abelian group of narrow ray classes modulo a nonzero ideal, together with a multiplicative symbol on ideals coprime to the modulus determined by arbitrary prescribed values at the primes and descending to the class group whenever it is trivial on the narrow ray. It is imported widely across the tree wherever characters of a number field specified prime by prime are needed.

References

  1. J. Neukirch, Algebraic Number Theory, Grundlehren der mathematischen Wissenschaften 322, Springer, 1999, Chapter VI
  2. S. Lang, Algebraic Number Theory, 2nd edition, Graduate Texts in Mathematics 110, Springer, 1994

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

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings β†—
import Mathlib.NumberTheory.NumberField.ClassNumber β†—
import Mathlib.RingTheory.DedekindDomain.Factorization β†—
import Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas β†—
import Mathlib.RingTheory.ClassGroup β†—
import Mathlib.LinearAlgebra.FreeModule.IdealQuotient β†—
import Mathlib.GroupTheory.QuotientGroup.Finite β†—
import Mathlib.Data.Fintype.Units β†—

open NumberField nonZeroDivisors IsDedekindDomain

noncomputable section

namespace Deep.NTSupply

section Involutions

theorem finite_closure_of_involutions {G : Type*} [CommGroup G] {S : Set G} (hS : S.Finite)
    (hsq : βˆ€ s ∈ S, s * s = 1) : ((Subgroup.closure S : Subgroup G) : Set G).Finite := by
  classical
  let F : Finset G := hS.toFinset
  let g : (F β†’ Bool) β†’ G := fun e => ∏ t ∈ F.attach, if e t then (t : G) else 1
  have hsqF : βˆ€ t : F, (t : G) * (t : G) = 1 := fun t => hsq t (hS.mem_toFinset.mp t.2)
  have key : βˆ€ (t : F) (b b' : Bool),
      (if b then (t : G) else 1) * (if b' then (t : G) else 1) = if (b != b') then (t : G) else 1 := by
    intro t b b'
    cases b <;> cases b' <;> simp [hsqF t]
  have hmul : βˆ€ e e' : F β†’ Bool, g e * g e' = g (fun t => e t != e' t) := by
    intro e e'
    rw [← Finset.prod_mul_distrib]
    exact Finset.prod_congr rfl fun t _ => key t (e t) (e' t)
  have hone : g (fun _ => false) = 1 := by simp [g]
  have hrange : (Set.range g).Finite := Set.finite_range g
  refine hrange.subset ?_
  intro x hx
  replace hx : x ∈ Subgroup.closure S := hx
  induction hx using Subgroup.closure_induction with
  | mem s hs =>
      refine ⟨fun t => decide ((t : G) = s), ?_⟩
      have hsF : s ∈ F := hS.mem_toFinset.mpr hs
      show (∏ t ∈ F.attach, if decide ((t : G) = s) then (t : G) else 1) = s
      rw [Finset.prod_eq_single ⟨s, hsF⟩]
      Β· simp
      Β· intro t _ ht
        have : ((t : G) = s) = False := by
          have : (t : G) β‰  s := fun h => ht (Subtype.ext h)
          exact eq_false this
        simp [this]
      Β· intro h
        exact absurd (Finset.mem_attach F ⟨s, hsF⟩) h
  | one => exact ⟨fun _ => false, hone⟩
  | mul a b ha hb iha ihb =>
      obtain ⟨e, rfl⟩ := iha
      obtain ⟨e', rfl⟩ := ihb
      exact ⟨fun t => e t != e' t, (hmul e e').symm⟩
  | inv a ha iha =>
      obtain ⟨e, rfl⟩ := iha
      have hself : g e * g e = 1 := by
        rw [hmul e e]
        have : (fun t : F => e t != e t) = fun _ => false := by
          funext t; simp
        rw [this, hone]
      exact ⟨e, (inv_eq_of_mul_eq_one_right hself).symm⟩

theorem finite_closure_of_involutions' {G : Type*} [CommGroup G] {S : Set G} (hS : S.Finite)
    (hsq : βˆ€ s ∈ S, s * s = 1) : Finite (Subgroup.closure S) :=
  (finite_closure_of_involutions hS hsq).to_subtype

end Involutions

section Carriers

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

def coprimeToModulus (𝔣 : Ideal (π“ž K)) : Subgroup (FractionalIdeal ((π“ž K)⁰) K)Λ£ where
  carrier := {I | βˆ€ v : HeightOneSpectrum (π“ž K), v.asIdeal ∣ 𝔣 β†’
    FractionalIdeal.count K v (I : FractionalIdeal ((π“ž K)⁰) K) = 0}
  mul_mem' := by
    intro I J hI hJ v hv
    have h : ((I * J : (FractionalIdeal ((π“ž K)⁰) K)Λ£) : FractionalIdeal ((π“ž K)⁰) K) =
        (I : FractionalIdeal ((π“ž K)⁰) K) * (J : FractionalIdeal ((π“ž K)⁰) K) := Units.val_mul I J
    rw [h, FractionalIdeal.count_mul K v I.ne_zero J.ne_zero, hI v hv, hJ v hv, add_zero]
  one_mem' := by
    intro v _
    rw [Units.val_one, FractionalIdeal.count_one]
  inv_mem' := by
    intro I hI v hv
    rw [Units.val_inv_eq_inv_val, FractionalIdeal.count_inv, hI v hv, neg_zero]

theorem mem_coprimeToModulus_iff {𝔣 : Ideal (π“ž K)} {I : (FractionalIdeal ((π“ž K)⁰) K)Λ£} :
    I ∈ coprimeToModulus K 𝔣 ↔ βˆ€ v : HeightOneSpectrum (π“ž K), v.asIdeal ∣ 𝔣 β†’
      FractionalIdeal.count K v (I : FractionalIdeal ((π“ž K)⁰) K) = 0 :=
  Iff.rfl

def narrowRaySet (𝔣 : Ideal (π“ž K)) : Set (FractionalIdeal ((π“ž K)⁰) K)Λ£ :=
  {I | βˆƒ Ξ± : π“ž K, Ξ± β‰  0 ∧ Ξ± - 1 ∈ 𝔣 ∧
    (βˆ€ Ο„ : K β†’+* ℝ, 0 < Ο„ (algebraMap (π“ž K) K Ξ±)) ∧
    (I : FractionalIdeal ((π“ž K)⁰) K) =
      ((Ideal.span {Ξ±} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K)}

theorem mem_narrowRaySet_iff {𝔣 : Ideal (π“ž K)} {I : (FractionalIdeal ((π“ž K)⁰) K)Λ£} :
    I ∈ narrowRaySet K 𝔣 ↔ βˆƒ Ξ± : π“ž K, Ξ± β‰  0 ∧ Ξ± - 1 ∈ 𝔣 ∧
      (βˆ€ Ο„ : K β†’+* ℝ, 0 < Ο„ (algebraMap (π“ž K) K Ξ±)) ∧
      (I : FractionalIdeal ((π“ž K)⁰) K) =
        ((Ideal.span {Ξ±} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K) :=
  Iff.rfl

def narrowRaySubgroup (𝔣 : Ideal (π“ž K)) : Subgroup (FractionalIdeal ((π“ž K)⁰) K)Λ£ :=
  Subgroup.closure (narrowRaySet K 𝔣)

theorem count_span_singleton_eq_zero_of_sub_one_mem {𝔣 : Ideal (π“ž K)} {Ξ± : π“ž K} (hΞ±0 : Ξ± β‰  0)
    (hΞ±1 : Ξ± - 1 ∈ 𝔣) {v : HeightOneSpectrum (π“ž K)} (hv : v.asIdeal ∣ 𝔣) :
    FractionalIdeal.count K v
      ((Ideal.span {Ξ±} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K) = 0 := by
  classical
  have hJ0 : (Ideal.span {Ξ±} : Ideal (π“ž K)) β‰  0 := by
    rw [Ne, Submodule.zero_eq_bot, Ideal.span_singleton_eq_bot]
    exact hΞ±0
  have hndvd : Β¬ v.asIdeal ∣ (Ideal.span {Ξ±} : Ideal (π“ž K)) := by
    intro hdvd
    have hαv : α ∈ v.asIdeal := Ideal.dvd_span_singleton.mp hdvd
    have hα1v : α - 1 ∈ v.asIdeal := Ideal.le_of_dvd hv hα1
    have h1 : (1 : π“ž K) ∈ v.asIdeal := by
      have := v.asIdeal.sub_mem hΞ±v hΞ±1v
      simpa using this
    exact v.isPrime.ne_top ((Ideal.eq_top_iff_one _).mpr h1)
  rw [FractionalIdeal.count_coe K v hJ0]
  have hc : (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {Ξ±} : Ideal (π“ž K))).factors
      = 0 := by
    by_contra h
    exact hndvd ((Associates.count_ne_zero_iff_dvd hJ0 v.irreducible).mp h)
  rw [hc, Nat.cast_zero]

theorem narrowRaySubgroup_le_coprimeToModulus (𝔣 : Ideal (π“ž K)) :
    narrowRaySubgroup K 𝔣 ≀ coprimeToModulus K 𝔣 := by
  rw [narrowRaySubgroup, Subgroup.closure_le]
  rintro I ⟨α, hα0, hα1, -, hI⟩
  rw [SetLike.mem_coe, mem_coprimeToModulus_iff]
  intro v hv
  rw [hI]
  exact count_span_singleton_eq_zero_of_sub_one_mem K hΞ±0 hΞ±1 hv

abbrev NarrowRayClassGroup (𝔣 : Ideal (π“ž K)) : Type _ :=
  β†₯(coprimeToModulus K 𝔣) β§Έ (narrowRaySubgroup K 𝔣).subgroupOf (coprimeToModulus K 𝔣)

def NarrowRayClassGroup.mk (𝔣 : Ideal (π“ž K)) :
    β†₯(coprimeToModulus K 𝔣) β†’* NarrowRayClassGroup K 𝔣 :=
  QuotientGroup.mk' _

theorem one_mem_narrowRaySet (𝔣 : Ideal (π“ž K)) :
    (1 : (FractionalIdeal ((π“ž K)⁰) K)Λ£) ∈ narrowRaySet K 𝔣 := by
  refine ⟨1, one_ne_zero, by simp, ?_, ?_⟩
  Β· intro Ο„
    rw [map_one, map_one]
    exact one_pos
  Β· rw [Units.val_one, Ideal.span_singleton_one, FractionalIdeal.coeIdeal_top]

end Carriers

section Symbol

variable (K : Type*) [Field K] [NumberField K] {M : Type*} [CommGroup M]

def raySymbol (f : HeightOneSpectrum (π“ž K) β†’ M) (I : FractionalIdeal ((π“ž K)⁰) K) : M :=
  ∏ᢠ v : HeightOneSpectrum (π“ž K), f v ^ FractionalIdeal.count K v I

theorem hasFiniteMulSupport_raySymbol_factors (f : HeightOneSpectrum (π“ž K) β†’ M)
    (I : FractionalIdeal ((π“ž K)⁰) K) :
    Function.HasFiniteMulSupport
      (fun v : HeightOneSpectrum (π“ž K) => f v ^ FractionalIdeal.count K v I) := by
  show (Function.mulSupport _).Finite
  refine (Filter.eventually_cofinite.mp (FractionalIdeal.finite_factors I)).subset ?_
  intro v hv
  simp only [Function.mem_mulSupport, ne_eq] at hv
  simp only [Set.mem_setOf_eq]
  intro h
  exact hv (by rw [h, zpow_zero])

theorem raySymbol_mul (f : HeightOneSpectrum (π“ž K) β†’ M) {I J : FractionalIdeal ((π“ž K)⁰) K}
    (hI : I β‰  0) (hJ : J β‰  0) :
    raySymbol K f (I * J) = raySymbol K f I * raySymbol K f J := by
  unfold raySymbol
  rw [← finprod_mul_distrib (hasFiniteMulSupport_raySymbol_factors K f I)
    (hasFiniteMulSupport_raySymbol_factors K f J)]
  refine finprod_congr fun v => ?_
  rw [FractionalIdeal.count_mul K v hI hJ, zpow_add]

def raySymbolUnitsHom (f : HeightOneSpectrum (π“ž K) β†’ M) : (FractionalIdeal ((π“ž K)⁰) K)Λ£ β†’* M where
  toFun I := raySymbol K f (I : FractionalIdeal ((π“ž K)⁰) K)
  map_one' := by simp [raySymbol, FractionalIdeal.count_one]
  map_mul' I J := by
    simp only [Units.val_mul]
    exact raySymbol_mul K f I.ne_zero J.ne_zero

def raySymbolHom (𝔣 : Ideal (π“ž K)) (f : HeightOneSpectrum (π“ž K) β†’ M) :
    β†₯(coprimeToModulus K 𝔣) β†’* M :=
  (raySymbolUnitsHom K f).comp (coprimeToModulus K 𝔣).subtype

theorem raySymbolHom_apply (𝔣 : Ideal (π“ž K)) (f : HeightOneSpectrum (π“ž K) β†’ M)
    (I : β†₯(coprimeToModulus K 𝔣)) :
    raySymbolHom K 𝔣 f I =
      raySymbol K f ((I : (FractionalIdeal ((π“ž K)⁰) K)Λ£) : FractionalIdeal ((π“ž K)⁰) K) :=
  rfl

end Symbol

section Finiteness

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

def raySet (𝔣 : Ideal (π“ž K)) : Set (FractionalIdeal ((π“ž K)⁰) K)Λ£ :=
  {I | βˆƒ Ξ± : π“ž K, Ξ± β‰  0 ∧ Ξ± - 1 ∈ 𝔣 ∧
    (I : FractionalIdeal ((π“ž K)⁰) K) =
      ((Ideal.span {Ξ±} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K)}

theorem narrowRaySet_subset_raySet (𝔣 : Ideal (π“ž K)) : narrowRaySet K 𝔣 βŠ† raySet K 𝔣 := by
  rintro I ⟨α, hα0, hα1, -, hI⟩
  exact ⟨α, hα0, hα1, hI⟩

theorem raySet_subset_coprimeToModulus (𝔣 : Ideal (π“ž K)) :
    raySet K 𝔣 βŠ† (coprimeToModulus K 𝔣 : Set (FractionalIdeal ((π“ž K)⁰) K)Λ£) := by
  rintro I ⟨α, hα0, hα1, hI⟩
  rw [SetLike.mem_coe, mem_coprimeToModulus_iff]
  intro v hv
  rw [hI]
  exact count_span_singleton_eq_zero_of_sub_one_mem K hΞ±0 hΞ±1 hv

def rayClasses (𝔣 : Ideal (π“ž K)) : Set (NarrowRayClassGroup K 𝔣) :=
  (NarrowRayClassGroup.mk K 𝔣) ''
    {y : β†₯(coprimeToModulus K 𝔣) | (y : (FractionalIdeal ((π“ž K)⁰) K)Λ£) ∈ raySet K 𝔣}

def rayClassSubgroup (𝔣 : Ideal (π“ž K)) : Subgroup (NarrowRayClassGroup K 𝔣) :=
  Subgroup.closure (rayClasses K 𝔣)

example (𝔣 : Ideal (π“ž K)) : CommGroup (NarrowRayClassGroup K 𝔣) := inferInstance

instance instNormalRayClassSubgroup (𝔣 : Ideal (π“ž K)) : (rayClassSubgroup K 𝔣).Normal :=
  ⟨fun n hn g => by rwa [mul_comm g n, mul_inv_cancel_right]⟩

theorem NarrowRayClassGroup.mk_eq_one_of_mem {𝔣 : Ideal (π“ž K)}
    {y : β†₯(coprimeToModulus K 𝔣)}
    (hy : (y : (FractionalIdeal ((π“ž K)⁰) K)Λ£) ∈ narrowRaySubgroup K 𝔣) :
    NarrowRayClassGroup.mk K 𝔣 y = 1 := by
  rw [NarrowRayClassGroup.mk, QuotientGroup.mk'_apply, QuotientGroup.eq_one_iff,
    Subgroup.mem_subgroupOf]
  exact hy

theorem NarrowRayClassGroup.mk_eq_mk_iff {𝔣 : Ideal (π“ž K)} {y y' : β†₯(coprimeToModulus K 𝔣)} :
    NarrowRayClassGroup.mk K 𝔣 y = NarrowRayClassGroup.mk K 𝔣 y' ↔
      ((y : (FractionalIdeal ((π“ž K)⁰) K)Λ£))⁻¹ * (y' : (FractionalIdeal ((π“ž K)⁰) K)Λ£) ∈
        narrowRaySubgroup K 𝔣 := by
  rw [NarrowRayClassGroup.mk, QuotientGroup.mk'_apply, QuotientGroup.mk'_apply, QuotientGroup.eq,
    Subgroup.mem_subgroupOf, Subgroup.coe_mul, Subgroup.coe_inv]

theorem rayClass_mul_self_eq_one {𝔣 : Ideal (π“ž K)} {g : NarrowRayClassGroup K 𝔣}
    (hg : g ∈ rayClasses K 𝔣) : g * g = 1 := by
  obtain ⟨y, ⟨α, hα0, hα1, hy⟩, rfl⟩ := hg
  rw [← map_mul]
  apply NarrowRayClassGroup.mk_eq_one_of_mem
  apply Subgroup.subset_closure

  have hΞ±' : (algebraMap (π“ž K) K) Ξ± β‰  0 :=
    (map_ne_zero_iff _ (IsFractionRing.injective (π“ž K) K)).mpr hΞ±0
  refine ⟨α * α, mul_ne_zero hα0 hα0, ?_, ?_, ?_⟩
  Β· have : Ξ± * Ξ± - 1 = (Ξ± + 1) * (Ξ± - 1) := by ring
    rw [this]
    exact Ideal.mul_mem_left _ _ hΞ±1
  Β· intro Ο„
    rw [map_mul, map_mul]
    exact mul_self_pos.mpr ((map_ne_zero Ο„).mpr hΞ±')
  Β· rw [Subgroup.coe_mul, Units.val_mul, hy, ← FractionalIdeal.coeIdeal_mul,
      Ideal.span_singleton_mul_span_singleton]

theorem mul_mem_narrowRaySet_of_sameSign {𝔣 : Ideal (π“ž K)}
    {y y' : β†₯(coprimeToModulus K 𝔣)} {Ξ± Ξ±' : π“ž K}
    (hΞ±0 : Ξ± β‰  0) (hΞ±1 : Ξ± - 1 ∈ 𝔣)
    (hy : ((y : (FractionalIdeal ((π“ž K)⁰) K)Λ£) : FractionalIdeal ((π“ž K)⁰) K) =
      ((Ideal.span {Ξ±} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K))
    (hΞ±0' : Ξ±' β‰  0) (hΞ±1' : Ξ±' - 1 ∈ 𝔣)
    (hy' : ((y' : (FractionalIdeal ((π“ž K)⁰) K)Λ£) : FractionalIdeal ((π“ž K)⁰) K) =
      ((Ideal.span {Ξ±'} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K))
    (hsgn : βˆ€ Ο„ : K β†’+* ℝ,
      (0 < Ο„ (algebraMap (π“ž K) K Ξ±)) ↔ (0 < Ο„ (algebraMap (π“ž K) K Ξ±'))) :
    ((y * y' : β†₯(coprimeToModulus K 𝔣)) : (FractionalIdeal ((π“ž K)⁰) K)Λ£) ∈
      narrowRaySet K 𝔣 := by
  have hΞ± : (algebraMap (π“ž K) K) Ξ± β‰  0 :=
    (map_ne_zero_iff _ (IsFractionRing.injective (π“ž K) K)).mpr hΞ±0
  have hΞ±'' : (algebraMap (π“ž K) K) Ξ±' β‰  0 :=
    (map_ne_zero_iff _ (IsFractionRing.injective (π“ž K) K)).mpr hΞ±0'
  refine ⟨α * α', mul_ne_zero hα0 hα0', ?_, ?_, ?_⟩
  Β· have : Ξ± * Ξ±' - 1 = Ξ± * (Ξ±' - 1) + (Ξ± - 1) := by ring
    rw [this]
    exact Ideal.add_mem _ (Ideal.mul_mem_left _ _ hΞ±1') hΞ±1
  Β· intro Ο„
    rw [map_mul, map_mul]
    rcases lt_or_gt_of_ne ((map_ne_zero Ο„).mpr hΞ±).symm with hpos | hneg
    Β· exact mul_pos hpos ((hsgn Ο„).mp hpos)
    Β· have hneg' : Ο„ (algebraMap (π“ž K) K Ξ±') < 0 := by
        rcases lt_or_gt_of_ne ((map_ne_zero Ο„).mpr hΞ±'').symm with hpos' | hneg'
        Β· exact absurd ((hsgn Ο„).mpr hpos') (not_lt.mpr hneg.le)
        Β· exact hneg'
      exact mul_pos_of_neg_of_neg hneg hneg'
  Β· rw [Subgroup.coe_mul, Units.val_mul, hy, hy', ← FractionalIdeal.coeIdeal_mul,
      Ideal.span_singleton_mul_span_singleton]

theorem NarrowRayClassGroup.mk_eq_of_sameSign {𝔣 : Ideal (π“ž K)}
    {y y' : β†₯(coprimeToModulus K 𝔣)} {Ξ± Ξ±' : π“ž K}
    (hΞ±0 : Ξ± β‰  0) (hΞ±1 : Ξ± - 1 ∈ 𝔣)
    (hy : ((y : (FractionalIdeal ((π“ž K)⁰) K)Λ£) : FractionalIdeal ((π“ž K)⁰) K) =
      ((Ideal.span {Ξ±} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K))
    (hΞ±0' : Ξ±' β‰  0) (hΞ±1' : Ξ±' - 1 ∈ 𝔣)
    (hy' : ((y' : (FractionalIdeal ((π“ž K)⁰) K)Λ£) : FractionalIdeal ((π“ž K)⁰) K) =
      ((Ideal.span {Ξ±'} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K))
    (hsgn : βˆ€ Ο„ : K β†’+* ℝ,
      (0 < Ο„ (algebraMap (π“ž K) K Ξ±)) ↔ (0 < Ο„ (algebraMap (π“ž K) K Ξ±'))) :
    NarrowRayClassGroup.mk K 𝔣 y = NarrowRayClassGroup.mk K 𝔣 y' := by
  rw [NarrowRayClassGroup.mk_eq_mk_iff]
  have h1 : ((y * y' : β†₯(coprimeToModulus K 𝔣)) : (FractionalIdeal ((π“ž K)⁰) K)Λ£) ∈
      narrowRaySubgroup K 𝔣 :=
    Subgroup.subset_closure (mul_mem_narrowRaySet_of_sameSign K hΞ±0 hΞ±1 hy hΞ±0' hΞ±1' hy' hsgn)
  have h2 : ((y * y : β†₯(coprimeToModulus K 𝔣)) : (FractionalIdeal ((π“ž K)⁰) K)Λ£) ∈
      narrowRaySubgroup K 𝔣 :=
    Subgroup.subset_closure (mul_mem_narrowRaySet_of_sameSign K hΞ±0 hΞ±1 hy hΞ±0 hΞ±1 hy
      (fun _ => Iff.rfl))
  rw [Subgroup.coe_mul] at h1 h2
  have e : ((y : (FractionalIdeal ((π“ž K)⁰) K)Λ£))⁻¹ * (y' : (FractionalIdeal ((π“ž K)⁰) K)Λ£) =
      (((y : (FractionalIdeal ((π“ž K)⁰) K)Λ£)) * (y : (FractionalIdeal ((π“ž K)⁰) K)Λ£))⁻¹ *
        (((y : (FractionalIdeal ((π“ž K)⁰) K)Λ£)) * (y' : (FractionalIdeal ((π“ž K)⁰) K)Λ£)) := by
    group
  rw [e]
  exact mul_mem (inv_mem h2) h1

theorem rayClasses_finite (𝔣 : Ideal (π“ž K)) : (rayClasses K 𝔣).Finite := by
  classical

  refine (Set.finite_range (fun s : (K β†’+* ℝ) β†’ Bool =>
    if h : βˆƒ (y : β†₯(coprimeToModulus K 𝔣)) (Ξ± : π“ž K), Ξ± β‰  0 ∧ Ξ± - 1 ∈ 𝔣 ∧
        ((y : (FractionalIdeal ((π“ž K)⁰) K)Λ£) : FractionalIdeal ((π“ž K)⁰) K) =
          ((Ideal.span {Ξ±} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K) ∧
        (fun Ο„ : K β†’+* ℝ => decide (0 < Ο„ (algebraMap (π“ž K) K Ξ±))) = s
    then NarrowRayClassGroup.mk K 𝔣 (Classical.choose h) else 1)).subset ?_
  rintro _ ⟨y, ⟨α, hα0, hα1, hy⟩, rfl⟩
  refine ⟨fun Ο„ : K β†’+* ℝ => decide (0 < Ο„ (algebraMap (π“ž K) K Ξ±)), ?_⟩
  have hex : βˆƒ (y : β†₯(coprimeToModulus K 𝔣)) (Ξ±' : π“ž K), Ξ±' β‰  0 ∧ Ξ±' - 1 ∈ 𝔣 ∧
      ((y : (FractionalIdeal ((π“ž K)⁰) K)Λ£) : FractionalIdeal ((π“ž K)⁰) K) =
        ((Ideal.span {Ξ±'} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K) ∧
      (fun Ο„ : K β†’+* ℝ => decide (0 < Ο„ (algebraMap (π“ž K) K Ξ±'))) =
        (fun Ο„ : K β†’+* ℝ => decide (0 < Ο„ (algebraMap (π“ž K) K Ξ±))) :=
    ⟨y, α, hα0, hα1, hy, rfl⟩
  simp only [dif_pos hex]
  obtain βŸ¨Ξ±β‚, hα₁0, hα₁1, hy₁, hsβ‚βŸ© := Classical.choose_spec hex
  apply NarrowRayClassGroup.mk_eq_of_sameSign K hα₁0 hα₁1 hy₁ hΞ±0 hΞ±1 hy
  intro Ο„
  have h : decide (0 < Ο„ (algebraMap (π“ž K) K α₁)) = decide (0 < Ο„ (algebraMap (π“ž K) K Ξ±)) :=
    congrFun hs₁ Ο„
  exact decide_eq_decide.mp h

theorem finite_rayClassSubgroup (𝔣 : Ideal (π“ž K)) : Finite (rayClassSubgroup K 𝔣) :=
  finite_closure_of_involutions' (rayClasses_finite K 𝔣)
    (fun _ hg => rayClass_mul_self_eq_one K hg)

def principalUnit (a : π“ž K) (ha : a β‰  0) : (FractionalIdeal ((π“ž K)⁰) K)Λ£ :=
  FractionalIdeal.mk0 K ⟨Ideal.span {a}, mem_nonZeroDivisors_of_ne_zero (by
    rw [Ne, Submodule.zero_eq_bot, Ideal.span_singleton_eq_bot]
    exact ha)⟩

theorem principalUnit_val (a : π“ž K) (ha : a β‰  0) :
    ((principalUnit K a ha : (FractionalIdeal ((π“ž K)⁰) K)Λ£) : FractionalIdeal ((π“ž K)⁰) K) =
      ((Ideal.span {a} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K) :=
  FractionalIdeal.coe_mk0 K _

def toClassGroup (𝔣 : Ideal (π“ž K)) : β†₯(coprimeToModulus K 𝔣) β†’* ClassGroup (π“ž K) :=
  (ClassGroup.mk (R := π“ž K) (K := K)).comp (coprimeToModulus K 𝔣).subtype

theorem classGroupMk_eq_one_of_principal {I : (FractionalIdeal ((π“ž K)⁰) K)Λ£} {Ξ± : π“ž K}
    (hI : (I : FractionalIdeal ((π“ž K)⁰) K) =
      ((Ideal.span {Ξ±} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K)) :
    ClassGroup.mk (R := π“ž K) (K := K) I = 1 := by
  rw [ClassGroup.mk_eq_one_iff, hI, FractionalIdeal.coeIdeal_span_singleton]
  exact (FractionalIdeal.isPrincipal_iff _).mpr ⟨algebraMap (π“ž K) K Ξ±, rfl⟩

theorem toClassGroup_eq_one_of_principal {𝔣 : Ideal (π“ž K)} {y : β†₯(coprimeToModulus K 𝔣)} {Ξ± : π“ž K}
    (hy : ((y : (FractionalIdeal ((π“ž K)⁰) K)Λ£) : FractionalIdeal ((π“ž K)⁰) K) =
      ((Ideal.span {Ξ±} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K)) :
    toClassGroup K 𝔣 y = 1 := by
  rw [toClassGroup, MonoidHom.coe_comp, Function.comp_apply, Subgroup.coe_subtype]
  exact classGroupMk_eq_one_of_principal K hy

theorem narrowRaySubgroupOf_le_ker (𝔣 : Ideal (π“ž K)) :
    (narrowRaySubgroup K 𝔣).subgroupOf (coprimeToModulus K 𝔣) ≀ (toClassGroup K 𝔣).ker := by
  intro y hy
  rw [Subgroup.mem_subgroupOf] at hy
  rw [MonoidHom.mem_ker]
  have hle : narrowRaySubgroup K 𝔣 ≀
      ((ClassGroup.mk (R := π“ž K) (K := K)) : (FractionalIdeal ((π“ž K)⁰) K)Λ£ β†’* ClassGroup (π“ž K)).ker := by
    rw [narrowRaySubgroup, Subgroup.closure_le]
    rintro I ⟨α, hα0, hα1, -, hI⟩
    rw [SetLike.mem_coe, MonoidHom.mem_ker]
    exact classGroupMk_eq_one_of_principal K hI
  exact MonoidHom.mem_ker.mp (hle hy)

def narrowRayClassGroupToClassGroup (𝔣 : Ideal (π“ž K)) :
    NarrowRayClassGroup K 𝔣 β†’* ClassGroup (π“ž K) :=
  QuotientGroup.lift ((narrowRaySubgroup K 𝔣).subgroupOf (coprimeToModulus K 𝔣))
    (toClassGroup K 𝔣) (narrowRaySubgroupOf_le_ker K 𝔣)

theorem narrowRayClassGroupToClassGroup_mk (𝔣 : Ideal (π“ž K)) (y : β†₯(coprimeToModulus K 𝔣)) :
    narrowRayClassGroupToClassGroup K 𝔣 (NarrowRayClassGroup.mk K 𝔣 y) = toClassGroup K 𝔣 y := by
  rw [NarrowRayClassGroup.mk, QuotientGroup.mk'_apply]
  exact QuotientGroup.lift_mk' _ (narrowRaySubgroupOf_le_ker K 𝔣) y

theorem rayClassSubgroup_le_ker (𝔣 : Ideal (π“ž K)) :
    rayClassSubgroup K 𝔣 ≀ (narrowRayClassGroupToClassGroup K 𝔣).ker := by
  rw [rayClassSubgroup, Subgroup.closure_le]
  rintro _ ⟨y, ⟨α, hα0, hα1, hy⟩, rfl⟩
  rw [SetLike.mem_coe, MonoidHom.mem_ker, narrowRayClassGroupToClassGroup_mk]
  exact toClassGroup_eq_one_of_principal K hy

def rayClassGroupToClassGroup (𝔣 : Ideal (π“ž K)) :
    NarrowRayClassGroup K 𝔣 β§Έ rayClassSubgroup K 𝔣 β†’* ClassGroup (π“ž K) :=
  QuotientGroup.lift (rayClassSubgroup K 𝔣) (narrowRayClassGroupToClassGroup K 𝔣)
    (rayClassSubgroup_le_ker K 𝔣)

theorem rayClassGroupToClassGroup_mk_mk (𝔣 : Ideal (π“ž K)) (y : β†₯(coprimeToModulus K 𝔣)) :
    rayClassGroupToClassGroup K 𝔣
      (QuotientGroup.mk (NarrowRayClassGroup.mk K 𝔣 y) :
        NarrowRayClassGroup K 𝔣 β§Έ rayClassSubgroup K 𝔣) = toClassGroup K 𝔣 y := by
  show (QuotientGroup.lift (rayClassSubgroup K 𝔣) (narrowRayClassGroupToClassGroup K 𝔣)
      (rayClassSubgroup_le_ker K 𝔣)) (QuotientGroup.mk (NarrowRayClassGroup.mk K 𝔣 y)) = _
  rw [QuotientGroup.lift_mk]
  exact narrowRayClassGroupToClassGroup_mk K 𝔣 y

def MovingLemma (𝔣 : Ideal (π“ž K)) : Prop :=
  βˆ€ xβ‚€ : K, xβ‚€ β‰  0 β†’
    (βˆ€ v : HeightOneSpectrum (π“ž K), v.asIdeal ∣ 𝔣 β†’
      FractionalIdeal.count K v (FractionalIdeal.spanSingleton ((π“ž K)⁰) xβ‚€) = 0) β†’
    βˆƒ Ξ² : π“ž K, Ξ² β‰  0 ∧ Ξ² - 1 ∈ 𝔣 ∧
      βˆƒ a : π“ž K, algebraMap (π“ž K) K a = algebraMap (π“ž K) K Ξ² * xβ‚€

theorem le_one_of_forall_count_nonneg {I : FractionalIdeal ((π“ž K)⁰) K} (hI : I β‰  0)
    (h : βˆ€ v : HeightOneSpectrum (π“ž K), 0 ≀ FractionalIdeal.count K v I) : I ≀ 1 := by
  classical
  rw [← FractionalIdeal.finprod_heightOneSpectrum_factorization' K hI]
  have hfin : (Function.mulSupport fun v : HeightOneSpectrum (π“ž K) =>
      (v.asIdeal : FractionalIdeal ((π“ž K)⁰) K) ^ FractionalIdeal.count K v I).Finite := by
    refine (Filter.eventually_cofinite.mp (FractionalIdeal.finite_factors I)).subset ?_
    intro v hv
    simp only [Function.mem_mulSupport, ne_eq] at hv
    simp only [Set.mem_setOf_eq]
    intro h0
    exact hv (by rw [h0, zpow_zero])
  rw [finprod_eq_prod_of_mulSupport_subset _ (s := hfin.toFinset)
    (by rw [Set.Finite.coe_toFinset])]
  apply Finset.prod_induction _ (fun x => x ≀ 1)
  Β· intro a b ha hb
    calc a * b ≀ a * 1 := by gcongr
      _ = a := mul_one a
      _ ≀ 1 := ha
  Β· exact le_rfl
  Β· intro v _
    obtain ⟨n, hn⟩ := Int.eq_ofNat_of_zero_le (h v)
    rw [hn, zpow_natCast, ← FractionalIdeal.coeIdeal_pow]
    exact FractionalIdeal.coeIdeal_le_one

theorem movingLemma {𝔣 : Ideal (π“ž K)} (h𝔣 : 𝔣 β‰  βŠ₯) : MovingLemma K 𝔣 := by
  classical
  intro xβ‚€ hxβ‚€ hcop
  by_cases htop : 𝔣 = ⊀
  Β·
    obtain ⟨n, s, hs, hns⟩ := IsFractionRing.div_surjective (A := π“ž K) xβ‚€
    have hs0 : s β‰  0 := nonZeroDivisors.ne_zero hs
    have hs0' : (algebraMap (π“ž K) K) s β‰  0 :=
      (map_ne_zero_iff _ (IsFractionRing.injective (π“ž K) K)).mpr hs0
    refine ⟨s, hs0, by rw [htop]; exact Submodule.mem_top, n, ?_⟩
    rw [← hns, mul_div_cancelβ‚€ _ hs0']
  Β·
    have h𝔣0 : (𝔣 : Ideal (π“ž K)) β‰  0 := by rwa [Ne, Submodule.zero_eq_bot]

    obtain ⟨T, hT⟩ : βˆƒ T : Finset (HeightOneSpectrum (π“ž K)), βˆ€ v, v ∈ T ↔ v.asIdeal ∣ 𝔣 :=
      ⟨(Ideal.finite_factors h𝔣0).toFinset, fun v => (Set.Finite.mem_toFinset _).trans Iff.rfl⟩

    have hWfin : {w : HeightOneSpectrum (π“ž K) |
        FractionalIdeal.count K w (FractionalIdeal.spanSingleton ((π“ž K)⁰) xβ‚€) < 0}.Finite := by
      refine (Filter.eventually_cofinite.mp
        (FractionalIdeal.finite_factors (FractionalIdeal.spanSingleton ((π“ž K)⁰) xβ‚€))).subset ?_
      intro w hw
      simp only [Set.mem_setOf_eq] at hw ⊒
      exact ne_of_lt hw
    obtain ⟨W, hW⟩ : βˆƒ W : Finset (HeightOneSpectrum (π“ž K)),
        βˆ€ w, w ∈ W ↔ FractionalIdeal.count K w (FractionalIdeal.spanSingleton ((π“ž K)⁰) xβ‚€) < 0 :=
      ⟨hWfin.toFinset, fun w => (Set.Finite.mem_toFinset _).trans Iff.rfl⟩

    obtain ⟨e, he⟩ : βˆƒ e : HeightOneSpectrum (π“ž K) β†’ β„•, βˆ€ v, e v =
        if v.asIdeal ∣ 𝔣 then (Associates.mk v.asIdeal).count (Associates.mk 𝔣).factors
        else (-(FractionalIdeal.count K v (FractionalIdeal.spanSingleton ((π“ž K)⁰) xβ‚€))).toNat :=
      ⟨_, fun v => rfl⟩

    obtain ⟨β, hβ⟩ := IsDedekindDomain.exists_forall_sub_mem_ideal
      (s := T βˆͺ W) (fun v => v.asIdeal) e
      (fun v _ => v.prime)
      (fun i _ j _ hij h => hij (by
        cases i; cases j; simpa using h))
      (fun v : β†₯(T βˆͺ W) => if v.1 ∈ T then (1 : π“ž K) else 0)

    have hΞ²T : βˆ€ v ∈ T, Ξ² - 1 ∈ v.asIdeal ^ e v := by
      intro v hvT
      have := hΞ² v (Finset.mem_union_left _ hvT)
      simpa [hvT] using this
    have hinf : (T.inf fun v => v.asIdeal ^ e v) = ∏ v ∈ T, v.asIdeal ^ e v :=
      IsDedekindDomain.HeightOneSpectrum.inf_pow_eq_prod T e id (fun i _ j _ hij => hij)
    have hprod : ∏ v ∈ T, v.asIdeal ^ e v = 𝔣 := by
      rw [← Ideal.finprod_heightOneSpectrum_factorization h𝔣0,
        finprod_eq_prod_of_mulSupport_subset _ (s := T) ?_]
      Β· refine Finset.prod_congr rfl fun v hv => ?_
        rw [he v, if_pos ((hT v).mp hv)]
        rfl
      Β· intro v hv
        rw [Function.mem_mulSupport] at hv
        rw [Finset.mem_coe, hT]
        by_contra hndvd
        apply hv
        have hcnt : (Associates.mk v.asIdeal).count (Associates.mk 𝔣).factors = 0 := by
          by_contra hne
          exact hndvd ((Associates.count_ne_zero_iff_dvd h𝔣0 v.irreducible).mp hne)
        show v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk 𝔣).factors = 1
        rw [hcnt, pow_zero]
    have hΞ²1 : Ξ² - 1 ∈ 𝔣 := by
      have hle : Ideal.span {Ξ² - 1} ≀ T.inf fun v => v.asIdeal ^ e v :=
        Finset.le_inf fun v hv => (Ideal.span_singleton_le_iff_mem _).mpr (hΞ²T v hv)
      have := hle (Ideal.mem_span_singleton_self _)
      rwa [hinf, hprod] at this

    obtain ⟨m, hm, hmπ”£βŸ© := Ideal.exists_le_maximal 𝔣 htop
    have hmbot : m β‰  βŠ₯ := by
      rintro rfl
      exact h𝔣 (le_bot_iff.mp hm𝔣)
    obtain ⟨vβ‚€, hvβ‚€βŸ© : βˆƒ vβ‚€ : HeightOneSpectrum (π“ž K), vβ‚€.asIdeal = m :=
      ⟨⟨m, hm.isPrime, hmbot⟩, rfl⟩
    have hvβ‚€T : vβ‚€ ∈ T := (hT vβ‚€).mpr (by rw [hvβ‚€]; exact Ideal.dvd_iff_le.mpr hm𝔣)
    have hevβ‚€ : e vβ‚€ β‰  0 := by
      rw [he vβ‚€, if_pos ((hT vβ‚€).mp hvβ‚€T)]
      exact (Associates.count_ne_zero_iff_dvd h𝔣0 vβ‚€.irreducible).mpr ((hT vβ‚€).mp hvβ‚€T)
    have hΞ²0 : Ξ² β‰  0 := by
      rintro rfl
      have h1 := hΞ²T vβ‚€ hvβ‚€T
      rw [zero_sub] at h1
      have h2 : (-1 : π“ž K) ∈ vβ‚€.asIdeal := Ideal.pow_le_self hevβ‚€ h1
      rw [hvβ‚€] at h2
      exact hm.ne_top ((Ideal.eq_top_iff_one _).mpr (by simpa using neg_mem_iff.mp h2))

    have hΞ²0' : (algebraMap (π“ž K) K) Ξ² β‰  0 :=
      (map_ne_zero_iff _ (IsFractionRing.injective (π“ž K) K)).mpr hΞ²0
    have hΞ²span : ((Ideal.span {Ξ²} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K) β‰  0 := by
      rw [Ne, FractionalIdeal.coeIdeal_eq_zero, Ideal.span_singleton_eq_bot]
      exact hΞ²0
    have hΞ²span0 : (Ideal.span {Ξ²} : Ideal (π“ž K)) β‰  0 := by
      rw [Ne, Submodule.zero_eq_bot, Ideal.span_singleton_eq_bot]
      exact hΞ²0
    have hx0' : FractionalIdeal.spanSingleton ((π“ž K)⁰) xβ‚€ β‰  0 := by
      rw [Ne, FractionalIdeal.spanSingleton_eq_zero_iff]
      exact hxβ‚€
    have hI0 : FractionalIdeal.spanSingleton ((π“ž K)⁰) (algebraMap (π“ž K) K Ξ² * xβ‚€) β‰  0 := by
      rw [Ne, FractionalIdeal.spanSingleton_eq_zero_iff]
      exact mul_ne_zero hΞ²0' hxβ‚€
    have hsplit : FractionalIdeal.spanSingleton ((π“ž K)⁰) (algebraMap (π“ž K) K Ξ² * xβ‚€) =
        ((Ideal.span {Ξ²} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K) *
          FractionalIdeal.spanSingleton ((π“ž K)⁰) xβ‚€ := by
      rw [FractionalIdeal.coeIdeal_span_singleton, FractionalIdeal.spanSingleton_mul_spanSingleton]
    have hnonneg : βˆ€ w : HeightOneSpectrum (π“ž K), 0 ≀ FractionalIdeal.count K w
        (FractionalIdeal.spanSingleton ((π“ž K)⁰) (algebraMap (π“ž K) K Ξ² * xβ‚€)) := by
      intro w
      rw [hsplit, FractionalIdeal.count_mul K w hΞ²span hx0']
      have hΞ²w : 0 ≀ FractionalIdeal.count K w
          ((Ideal.span {Ξ²} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K) :=
        FractionalIdeal.count_coe_nonneg K w _
      by_cases hwW : w ∈ W
      Β·
        have hwlt : FractionalIdeal.count K w (FractionalIdeal.spanSingleton ((π“ž K)⁰) xβ‚€) < 0 :=
          (hW w).mp hwW
        have hwT : w βˆ‰ T := by
          intro hwT
          have h0 := hcop w ((hT w).mp hwT)
          rw [h0] at hwlt
          exact lt_irrefl _ hwlt
        have hndvd : Β¬ w.asIdeal ∣ 𝔣 := by rwa [← hT]
        have hmem := hΞ² w (Finset.mem_union_right _ hwW)
        simp only [hwT, ite_false, sub_zero] at hmem

        have hew : (e w : β„€) = -(FractionalIdeal.count K w
            (FractionalIdeal.spanSingleton ((π“ž K)⁰) xβ‚€)) := by
          rw [he w, if_neg hndvd, Int.toNat_of_nonneg (by omega)]
        have hdvd : w.asIdeal ^ e w ∣ (Ideal.span {Ξ²} : Ideal (π“ž K)) :=
          (Ideal.dvd_span_singleton).mpr hmem
        have hle : e w ≀ (Associates.mk w.asIdeal).count
            (Associates.mk (Ideal.span {Ξ²} : Ideal (π“ž K))).factors := by
          rw [← Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero.mpr hΞ²span0)
            w.associates_irreducible, ← Associates.mk_pow]
          exact Associates.mk_dvd_mk.mpr hdvd
        have hcoe : FractionalIdeal.count K w
            ((Ideal.span {Ξ²} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K) =
              ((Associates.mk w.asIdeal).count
                (Associates.mk (Ideal.span {Ξ²} : Ideal (π“ž K))).factors : β„€) :=
          FractionalIdeal.count_coe K w hΞ²span0
        have hle' : (e w : β„€) ≀ FractionalIdeal.count K w
            ((Ideal.span {Ξ²} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K) := by
          rw [hcoe]
          exact_mod_cast hle
        omega
      Β·
        have hwge : 0 ≀ FractionalIdeal.count K w
            (FractionalIdeal.spanSingleton ((π“ž K)⁰) xβ‚€) := by
          by_contra hlt
          exact hwW ((hW w).mpr (lt_of_not_ge hlt))
        exact add_nonneg hΞ²w hwge

    have hle1 : FractionalIdeal.spanSingleton ((π“ž K)⁰) (algebraMap (π“ž K) K Ξ² * xβ‚€) ≀ 1 :=
      le_one_of_forall_count_nonneg K hI0 hnonneg
    have hmem1 : algebraMap (π“ž K) K Ξ² * xβ‚€ ∈
        (1 : FractionalIdeal ((π“ž K)⁰) K) :=
      hle1 (FractionalIdeal.mem_spanSingleton_self _ _)
    obtain ⟨a, ha⟩ := (FractionalIdeal.mem_one_iff _).mp hmem1
    exact ⟨β, hβ0, hβ1, a, ha⟩

theorem exists_mul_sub_one_mem_of_counts_zero {𝔣 : Ideal (π“ž K)} (h𝔣 : 𝔣 β‰  βŠ₯) {a : π“ž K}
    (ha : a β‰  0)
    (hcop : βˆ€ v : HeightOneSpectrum (π“ž K), v.asIdeal ∣ 𝔣 β†’
      FractionalIdeal.count K v ((Ideal.span {a} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K) = 0) :
    βˆƒ c : π“ž K, a * c - 1 ∈ 𝔣 := by
  classical

  have hsup : (Ideal.span {a} : Ideal (π“ž K)) βŠ” 𝔣 = ⊀ := by
    by_contra hne
    obtain ⟨m, hm, hle⟩ := Ideal.exists_le_maximal _ hne
    have hm𝔣 : 𝔣 ≀ m := le_trans le_sup_right hle
    have hma : (Ideal.span {a} : Ideal (π“ž K)) ≀ m := le_trans le_sup_left hle
    have hmbot : m β‰  βŠ₯ := by
      rintro rfl
      exact h𝔣 (le_bot_iff.mp hm𝔣)
    set v : HeightOneSpectrum (π“ž K) := ⟨m, hm.isPrime, hmbot⟩
    have hvdvd : v.asIdeal ∣ 𝔣 := (Ideal.dvd_iff_le.mpr hm𝔣)
    have hva : v.asIdeal ∣ (Ideal.span {a} : Ideal (π“ž K)) := (Ideal.dvd_iff_le.mpr hma)
    have hJ0 : (Ideal.span {a} : Ideal (π“ž K)) β‰  0 := by
      rw [Ne, Submodule.zero_eq_bot, Ideal.span_singleton_eq_bot]
      exact ha
    have hcnt := hcop v hvdvd
    rw [FractionalIdeal.count_coe K v hJ0] at hcnt
    have hz : (Associates.mk v.asIdeal).count
        (Associates.mk (Ideal.span {a} : Ideal (π“ž K))).factors = 0 := by
      exact_mod_cast hcnt
    exact ((Associates.count_ne_zero_iff_dvd hJ0 v.irreducible).mpr hva) hz

  have h1 : (1 : π“ž K) ∈ (Ideal.span {a} : Ideal (π“ž K)) βŠ” 𝔣 := by
    rw [hsup]; exact Submodule.mem_top
  obtain ⟨t, ht, f, hf, htf⟩ := Submodule.mem_sup.mp h1
  obtain ⟨c, rfl⟩ := Ideal.mem_span_singleton'.mp ht
  refine ⟨c, ?_⟩
  have : a * c - 1 = -f := by rw [mul_comm]; linear_combination htf
  rw [this]
  exact neg_mem_iff.mpr hf

theorem principalUnit_mem_coprimeToModulus {𝔣 : Ideal (π“ž K)} {Ξ² : π“ž K} (hΞ²0 : Ξ² β‰  0)
    (hΞ²1 : Ξ² - 1 ∈ 𝔣) : principalUnit K Ξ² hΞ²0 ∈ coprimeToModulus K 𝔣 := by
  rw [mem_coprimeToModulus_iff]
  intro v hv
  rw [principalUnit_val]
  exact count_span_singleton_eq_zero_of_sub_one_mem K hΞ²0 hΞ²1 hv

theorem mk_mk_eq_one_of_raySet {𝔣 : Ideal (π“ž K)} {z : β†₯(coprimeToModulus K 𝔣)}
    (hz : (z : (FractionalIdeal ((π“ž K)⁰) K)Λ£) ∈ raySet K 𝔣) :
    (QuotientGroup.mk (NarrowRayClassGroup.mk K 𝔣 z) :
      NarrowRayClassGroup K 𝔣 β§Έ rayClassSubgroup K 𝔣) = 1 := by
  rw [QuotientGroup.eq_one_iff]
  exact Subgroup.subset_closure ⟨z, hz, rfl⟩

private theorem exists_integral_ray_rep {𝔣 : Ideal (π“ž K)} (hmove : MovingLemma K 𝔣)
    (y : β†₯(coprimeToModulus K 𝔣)) (hprinc : toClassGroup K 𝔣 y = 1) :
    βˆƒ (a : π“ž K), a β‰  0 ∧ βˆƒ (ya : β†₯(coprimeToModulus K 𝔣)),
      ((ya : (FractionalIdeal ((π“ž K)⁰) K)Λ£) : FractionalIdeal ((π“ž K)⁰) K) =
        ((Ideal.span {a} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K) ∧
      (QuotientGroup.mk (NarrowRayClassGroup.mk K 𝔣 ya) :
        NarrowRayClassGroup K 𝔣 β§Έ rayClassSubgroup K 𝔣) =
      QuotientGroup.mk (NarrowRayClassGroup.mk K 𝔣 y) := by

  have hprinc' : ClassGroup.mk (R := π“ž K) (K := K)
      (y : (FractionalIdeal ((π“ž K)⁰) K)Λ£) = 1 := hprinc
  rw [ClassGroup.mk_eq_one_iff] at hprinc'
  obtain ⟨xβ‚€, hxβ‚€βŸ© := (FractionalIdeal.isPrincipal_iff _).mp hprinc'
  have hy0 : ((y : (FractionalIdeal ((π“ž K)⁰) K)Λ£) : FractionalIdeal ((π“ž K)⁰) K) β‰  0 :=
    Units.ne_zero _
  have hx0 : xβ‚€ β‰  0 := by
    intro h
    rw [h, FractionalIdeal.spanSingleton_zero] at hxβ‚€
    exact hy0 hxβ‚€

  have hcop : βˆ€ v : HeightOneSpectrum (π“ž K), v.asIdeal ∣ 𝔣 β†’
      FractionalIdeal.count K v (FractionalIdeal.spanSingleton ((π“ž K)⁰) xβ‚€) = 0 := by
    intro v hv
    rw [← hxβ‚€]
    exact (mem_coprimeToModulus_iff K).mp y.2 v hv
  obtain ⟨β, hΞ²0, hΞ²1, a, ha⟩ := hmove xβ‚€ hx0 hcop
  have hΞ²' : (algebraMap (π“ž K) K) Ξ² β‰  0 :=
    (map_ne_zero_iff _ (IsFractionRing.injective (π“ž K) K)).mpr hΞ²0
  have ha0 : a β‰  0 := by
    intro h
    rw [h, map_zero] at ha
    exact mul_ne_zero hΞ²' hx0 ha.symm

  refine ⟨a, ha0, ⟨principalUnit K Ξ² hΞ²0 * (y : (FractionalIdeal ((π“ž K)⁰) K)Λ£),
    mul_mem (principalUnit_mem_coprimeToModulus K hβ0 hβ1) y.2⟩, ?_, ?_⟩
  Β· rw [Units.val_mul, principalUnit_val, hxβ‚€, FractionalIdeal.coeIdeal_span_singleton,
      FractionalIdeal.coeIdeal_span_singleton, FractionalIdeal.spanSingleton_mul_spanSingleton, ha]
  Β· have hsplit : (⟨principalUnit K Ξ² hΞ²0 * (y : (FractionalIdeal ((π“ž K)⁰) K)Λ£),
        mul_mem (principalUnit_mem_coprimeToModulus K hβ0 hβ1) y.2⟩ :
          β†₯(coprimeToModulus K 𝔣)) =
        ⟨principalUnit K β hβ0, principalUnit_mem_coprimeToModulus K hβ0 hβ1⟩ * y := rfl
    rw [hsplit, map_mul, QuotientGroup.mk_mul,
      mk_mk_eq_one_of_raySet K ⟨β, hβ0, hβ1, principalUnit_val K β hβ0⟩, one_mul]

theorem mk_mk_eq_of_residue_eq {𝔣 : Ideal (π“ž K)} (h𝔣 : 𝔣 β‰  βŠ₯) (htop : 𝔣 β‰  ⊀)
    {a a' : π“ž K} (ha : a β‰  0) (ha' : a' β‰  0) (ya ya' : β†₯(coprimeToModulus K 𝔣))
    (hya : ((ya : (FractionalIdeal ((π“ž K)⁰) K)Λ£) : FractionalIdeal ((π“ž K)⁰) K) =
      ((Ideal.span {a} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K))
    (hya' : ((ya' : (FractionalIdeal ((π“ž K)⁰) K)Λ£) : FractionalIdeal ((π“ž K)⁰) K) =
      ((Ideal.span {a'} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K))
    (hres : Ideal.Quotient.mk 𝔣 a = Ideal.Quotient.mk 𝔣 a') :
    (QuotientGroup.mk (NarrowRayClassGroup.mk K 𝔣 ya) :
      NarrowRayClassGroup K 𝔣 β§Έ rayClassSubgroup K 𝔣) =
      QuotientGroup.mk (NarrowRayClassGroup.mk K 𝔣 ya') := by
  classical

  have hcopa : βˆ€ v : HeightOneSpectrum (π“ž K), v.asIdeal ∣ 𝔣 β†’
      FractionalIdeal.count K v ((Ideal.span {a} : Ideal (π“ž K)) :
        FractionalIdeal ((π“ž K)⁰) K) = 0 := by
    intro v hv
    rw [← hya]
    exact (mem_coprimeToModulus_iff K).mp ya.2 v hv
  obtain ⟨c, hac⟩ := exists_mul_sub_one_mem_of_counts_zero K h𝔣 ha hcopa
  have ha'a : a' - a ∈ 𝔣 := by
    have := (Ideal.Quotient.eq (I := 𝔣)).mp hres
    have h' : a' - a = -(a - a') := by ring
    rw [h']
    exact neg_mem_iff.mpr this
  have ha'c : a' * c - 1 ∈ 𝔣 := by
    have : a' * c - 1 = (a' - a) * c + (a * c - 1) := by ring
    rw [this]
    exact Ideal.add_mem _ (Ideal.mul_mem_right _ _ ha'a) hac
  have hc0 : c β‰  0 := by
    rintro rfl
    rw [mul_zero, zero_sub] at hac
    exact htop ((Ideal.eq_top_iff_one _).mpr (by simpa using neg_mem_iff.mp hac))

  have hac0 : a * c β‰  0 := mul_ne_zero ha hc0
  have hcopc : βˆ€ v : HeightOneSpectrum (π“ž K), v.asIdeal ∣ 𝔣 β†’
      FractionalIdeal.count K v ((Ideal.span {c} : Ideal (π“ž K)) :
        FractionalIdeal ((π“ž K)⁰) K) = 0 := by
    intro v hv
    have hprod : FractionalIdeal.count K v
        ((Ideal.span {a * c} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K) = 0 :=
      count_span_singleton_eq_zero_of_sub_one_mem K hac0 hac hv
    have hA : ((Ideal.span {a} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K) β‰  0 := by
      rw [Ne, FractionalIdeal.coeIdeal_eq_zero, Ideal.span_singleton_eq_bot]
      exact ha
    have hC : ((Ideal.span {c} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K) β‰  0 := by
      rw [Ne, FractionalIdeal.coeIdeal_eq_zero, Ideal.span_singleton_eq_bot]
      exact hc0
    rw [← Ideal.span_singleton_mul_span_singleton, FractionalIdeal.coeIdeal_mul,
      FractionalIdeal.count_mul K v hA hC, hcopa v hv, zero_add] at hprod
    exact hprod

  set yc : β†₯(coprimeToModulus K 𝔣) :=
    ⟨principalUnit K c hc0, (mem_coprimeToModulus_iff K).mpr (fun v hv => by
      rw [principalUnit_val]; exact hcopc v hv)⟩ with hyc
  have hvc : ((yc : (FractionalIdeal ((π“ž K)⁰) K)Λ£) : FractionalIdeal ((π“ž K)⁰) K) =
      ((Ideal.span {c} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K) := by
    rw [hyc]; exact principalUnit_val K c hc0
  have h1 : (QuotientGroup.mk (NarrowRayClassGroup.mk K 𝔣 (ya * yc)) :
      NarrowRayClassGroup K 𝔣 β§Έ rayClassSubgroup K 𝔣) = 1 := by
    apply mk_mk_eq_one_of_raySet
    refine ⟨a * c, hac0, hac, ?_⟩
    rw [Subgroup.coe_mul, Units.val_mul, hya, hvc, ← FractionalIdeal.coeIdeal_mul,
      Ideal.span_singleton_mul_span_singleton]
  have h2 : (QuotientGroup.mk (NarrowRayClassGroup.mk K 𝔣 (ya' * yc)) :
      NarrowRayClassGroup K 𝔣 β§Έ rayClassSubgroup K 𝔣) = 1 := by
    apply mk_mk_eq_one_of_raySet
    refine ⟨a' * c, mul_ne_zero ha' hc0, ha'c, ?_⟩
    rw [Subgroup.coe_mul, Units.val_mul, hya', hvc, ← FractionalIdeal.coeIdeal_mul,
      Ideal.span_singleton_mul_span_singleton]
  rw [map_mul, QuotientGroup.mk_mul] at h1 h2
  exact mul_right_cancel (h1.trans h2.symm)

private theorem finite_ker_rayClassGroupToClassGroup {𝔣 : Ideal (π“ž K)} (h𝔣 : 𝔣 β‰  βŠ₯)
    (hmove : MovingLemma K 𝔣) : Finite ((rayClassGroupToClassGroup K 𝔣).ker) := by
  classical
  haveI : Finite (π“ž K β§Έ 𝔣) := Ideal.finiteQuotientOfFreeOfNeBot 𝔣 h𝔣

  apply Set.Finite.to_subtype
  refine ((Set.finite_range (fun q : π“ž K β§Έ 𝔣 =>
    if h : βˆƒ (a : π“ž K) (ya : β†₯(coprimeToModulus K 𝔣)), a β‰  0 ∧
        ((ya : (FractionalIdeal ((π“ž K)⁰) K)Λ£) : FractionalIdeal ((π“ž K)⁰) K) =
          ((Ideal.span {a} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K) ∧
        Ideal.Quotient.mk 𝔣 a = q
    then (QuotientGroup.mk (NarrowRayClassGroup.mk K 𝔣 (Classical.choose (Classical.choose_spec h))) :
      NarrowRayClassGroup K 𝔣 β§Έ rayClassSubgroup K 𝔣)
    else 1)).union (Set.finite_singleton 1)).subset ?_
  intro x hx
  rw [SetLike.mem_coe, MonoidHom.mem_ker] at hx
  obtain ⟨x', rfl⟩ := QuotientGroup.mk_surjective x
  obtain ⟨y, rfl⟩ := QuotientGroup.mk_surjective x'
  replace hx : rayClassGroupToClassGroup K 𝔣
      (QuotientGroup.mk (NarrowRayClassGroup.mk K 𝔣 y)) = 1 := hx

  have hprinc : toClassGroup K 𝔣 y = 1 := by
    rw [← rayClassGroupToClassGroup_mk_mk]
    exact hx
  obtain ⟨a, ha, ya, hya, hcls⟩ := exists_integral_ray_rep K hmove y hprinc
  by_cases htop : 𝔣 = ⊀
  Β·
    right
    rw [Set.mem_singleton_iff]
    exact hcls.symm.trans
      (mk_mk_eq_one_of_raySet K ⟨a, ha, by rw [htop]; exact Submodule.mem_top, hya⟩)
  Β· left
    refine ⟨Ideal.Quotient.mk 𝔣 a, ?_⟩
    have hdite : βˆƒ (a' : π“ž K) (ya' : β†₯(coprimeToModulus K 𝔣)), a' β‰  0 ∧
        ((ya' : (FractionalIdeal ((π“ž K)⁰) K)Λ£) : FractionalIdeal ((π“ž K)⁰) K) =
          ((Ideal.span {a'} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K) ∧
        Ideal.Quotient.mk 𝔣 a' = Ideal.Quotient.mk 𝔣 a :=
      ⟨a, ya, ha, hya, rfl⟩
    simp only [dif_pos hdite]
    obtain ⟨ha₁, hya₁, hresβ‚βŸ© := Classical.choose_spec (Classical.choose_spec hdite)
    exact (mk_mk_eq_of_residue_eq K h𝔣 htop ha₁ ha
      (Classical.choose (Classical.choose_spec hdite)) ya hya₁ hya hres₁).trans hcls

private theorem finite_rayClassQuotient_of_movingLemma {𝔣 : Ideal (π“ž K)} (h𝔣 : 𝔣 β‰  βŠ₯)
    (hmove : MovingLemma K 𝔣) :
    Finite (NarrowRayClassGroup K 𝔣 β§Έ rayClassSubgroup K 𝔣) := by
  have h1 : Finite ((rayClassGroupToClassGroup K 𝔣).ker) :=
    finite_ker_rayClassGroupToClassGroup K h𝔣 hmove
  have h2 : Finite ((NarrowRayClassGroup K 𝔣 β§Έ rayClassSubgroup K 𝔣) β§Έ
      (rayClassGroupToClassGroup K 𝔣).ker) :=
    Finite.of_equiv _ (QuotientGroup.quotientKerEquivRange (rayClassGroupToClassGroup K 𝔣)).symm.toEquiv
  exact (finite_iff_subgroup_quotient (rayClassGroupToClassGroup K 𝔣).ker).mpr ⟨h1, h2⟩

private theorem finite_of_movingLemma {𝔣 : Ideal (π“ž K)} (h𝔣 : 𝔣 β‰  βŠ₯)
    (hmove : MovingLemma K 𝔣) : Finite (NarrowRayClassGroup K 𝔣) :=
  (finite_iff_subgroup_quotient (rayClassSubgroup K 𝔣)).mpr
    ⟨finite_rayClassSubgroup K 𝔣, finite_rayClassQuotient_of_movingLemma K h𝔣 hmove⟩

theorem finite {𝔣 : Ideal (π“ž K)} (h𝔣 : 𝔣 β‰  βŠ₯) : Finite (NarrowRayClassGroup K 𝔣) :=
  finite_of_movingLemma K h𝔣 (movingLemma K h𝔣)

end Finiteness

section Packaging

variable (K : Type*) [Field K] [NumberField K] {M : Type*} [CommGroup M]

def primeUnit (v : HeightOneSpectrum (π“ž K)) : (FractionalIdeal ((π“ž K)⁰) K)Λ£ :=
  FractionalIdeal.mk0 K ⟨v.asIdeal, mem_nonZeroDivisors_of_ne_zero (by
    rw [Ne, Submodule.zero_eq_bot]
    exact v.ne_bot)⟩

theorem primeUnit_val (v : HeightOneSpectrum (π“ž K)) :
    ((primeUnit K v : (FractionalIdeal ((π“ž K)⁰) K)Λ£) : FractionalIdeal ((π“ž K)⁰) K) =
      (v.asIdeal : FractionalIdeal ((π“ž K)⁰) K) :=
  FractionalIdeal.coe_mk0 K _

theorem primeUnit_mem_coprimeToModulus {𝔣 : Ideal (π“ž K)} {v : HeightOneSpectrum (π“ž K)}
    (hv : Β¬ v.asIdeal ∣ 𝔣) : primeUnit K v ∈ coprimeToModulus K 𝔣 := by
  rw [mem_coprimeToModulus_iff]
  intro w hw
  rw [primeUnit_val]
  exact FractionalIdeal.count_maximal_coprime K w (fun h => hv (h β–Έ hw))

def primeClass (𝔣 : Ideal (π“ž K)) (v : HeightOneSpectrum (π“ž K)) (hv : Β¬ v.asIdeal ∣ 𝔣) :
    NarrowRayClassGroup K 𝔣 :=
  NarrowRayClassGroup.mk K 𝔣 ⟨primeUnit K v, primeUnit_mem_coprimeToModulus K hv⟩

theorem raySymbol_primeUnit (f : HeightOneSpectrum (π“ž K) β†’ M) (v : HeightOneSpectrum (π“ž K)) :
    raySymbol K f ((primeUnit K v : (FractionalIdeal ((π“ž K)⁰) K)Λ£) :
      FractionalIdeal ((π“ž K)⁰) K) = f v := by
  rw [primeUnit_val, raySymbol, finprod_eq_single _ v]
  Β· rw [FractionalIdeal.count_self, zpow_one]
  Β· intro w hw
    rw [FractionalIdeal.count_maximal_coprime K w (Ne.symm hw), zpow_zero]

theorem raySymbolHom_prime (𝔣 : Ideal (π“ž K)) (f : HeightOneSpectrum (π“ž K) β†’ M)
    {v : HeightOneSpectrum (π“ž K)} (hv : Β¬ v.asIdeal ∣ 𝔣) :
    raySymbolHom K 𝔣 f ⟨primeUnit K v, primeUnit_mem_coprimeToModulus K hv⟩ = f v := by
  rw [raySymbolHom_apply]
  exact raySymbol_primeUnit K f v

theorem narrowRaySubgroupOf_le_ker_raySymbolHom {𝔣 : Ideal (π“ž K)}
    (f : HeightOneSpectrum (π“ž K) β†’ M)
    (hkill : βˆ€ Ξ± : π“ž K, Ξ± β‰  0 β†’ Ξ± - 1 ∈ 𝔣 β†’
      (βˆ€ Ο„ : K β†’+* ℝ, 0 < Ο„ (algebraMap (π“ž K) K Ξ±)) β†’
      raySymbol K f ((Ideal.span {Ξ±} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K) = 1) :
    (narrowRaySubgroup K 𝔣).subgroupOf (coprimeToModulus K 𝔣) ≀ (raySymbolHom K 𝔣 f).ker := by
  intro y hy
  rw [Subgroup.mem_subgroupOf] at hy
  rw [MonoidHom.mem_ker, raySymbolHom_apply]
  have hle : narrowRaySubgroup K 𝔣 ≀ (raySymbolUnitsHom K f).ker := by
    rw [narrowRaySubgroup, Subgroup.closure_le]
    rintro I ⟨α, hα0, hα1, hpos, hI⟩
    rw [SetLike.mem_coe, MonoidHom.mem_ker]
    show raySymbol K f (I : FractionalIdeal ((π“ž K)⁰) K) = 1
    rw [hI]
    exact hkill Ξ± hΞ±0 hΞ±1 hpos
  exact MonoidHom.mem_ker.mp (hle hy)

def raySymbolDescend {𝔣 : Ideal (π“ž K)} (f : HeightOneSpectrum (π“ž K) β†’ M)
    (hkill : βˆ€ Ξ± : π“ž K, Ξ± β‰  0 β†’ Ξ± - 1 ∈ 𝔣 β†’
      (βˆ€ Ο„ : K β†’+* ℝ, 0 < Ο„ (algebraMap (π“ž K) K Ξ±)) β†’
      raySymbol K f ((Ideal.span {Ξ±} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K) = 1) :
    NarrowRayClassGroup K 𝔣 β†’* M :=
  QuotientGroup.lift ((narrowRaySubgroup K 𝔣).subgroupOf (coprimeToModulus K 𝔣))
    (raySymbolHom K 𝔣 f) (narrowRaySubgroupOf_le_ker_raySymbolHom K f hkill)

theorem raySymbolDescend_mk {𝔣 : Ideal (π“ž K)} (f : HeightOneSpectrum (π“ž K) β†’ M)
    (hkill : βˆ€ Ξ± : π“ž K, Ξ± β‰  0 β†’ Ξ± - 1 ∈ 𝔣 β†’
      (βˆ€ Ο„ : K β†’+* ℝ, 0 < Ο„ (algebraMap (π“ž K) K Ξ±)) β†’
      raySymbol K f ((Ideal.span {Ξ±} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K) = 1)
    (y : β†₯(coprimeToModulus K 𝔣)) :
    raySymbolDescend K f hkill (NarrowRayClassGroup.mk K 𝔣 y) = raySymbolHom K 𝔣 f y := by
  rw [NarrowRayClassGroup.mk, QuotientGroup.mk'_apply]
  exact QuotientGroup.lift_mk' _ (narrowRaySubgroupOf_le_ker_raySymbolHom K f hkill) y

theorem raySymbolDescend_primeClass {𝔣 : Ideal (π“ž K)} (f : HeightOneSpectrum (π“ž K) β†’ M)
    (hkill : βˆ€ Ξ± : π“ž K, Ξ± β‰  0 β†’ Ξ± - 1 ∈ 𝔣 β†’
      (βˆ€ Ο„ : K β†’+* ℝ, 0 < Ο„ (algebraMap (π“ž K) K Ξ±)) β†’
      raySymbol K f ((Ideal.span {Ξ±} : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K) = 1)
    {v : HeightOneSpectrum (π“ž K)} (hv : Β¬ v.asIdeal ∣ 𝔣) :
    raySymbolDescend K f hkill (primeClass K 𝔣 v hv) = f v := by
  rw [primeClass, raySymbolDescend_mk]
  exact raySymbolHom_prime K 𝔣 f hv

def raySymbolIdealHom (f : HeightOneSpectrum (π“ž K) β†’ M) : β†₯(Ideal (π“ž K))⁰ β†’* M :=
  (raySymbolUnitsHom K f).comp (FractionalIdeal.mk0 K)

theorem raySymbolIdealHom_apply (f : HeightOneSpectrum (π“ž K) β†’ M) (I : β†₯(Ideal (π“ž K))⁰) :
    raySymbolIdealHom K f I =
      raySymbol K f ((I : Ideal (π“ž K)) : FractionalIdeal ((π“ž K)⁰) K) := by
  rw [raySymbolIdealHom, MonoidHom.comp_apply]
  show raySymbol K f ((FractionalIdeal.mk0 K I : (FractionalIdeal ((π“ž K)⁰) K)Λ£) :
    FractionalIdeal ((π“ž K)⁰) K) = _
  rw [FractionalIdeal.coe_mk0]

end Packaging

section Degenerate

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

theorem coprimeToModulus_top : coprimeToModulus K (⊀ : Ideal (π“ž K)) = ⊀ := by
  rw [eq_top_iff]
  intro I _
  rw [mem_coprimeToModulus_iff]
  intro v hv
  exact absurd (top_le_iff.mp (Ideal.dvd_iff_le.mp hv)) v.isPrime.ne_top

end Degenerate

#print axioms Deep.NTSupply.coprimeToModulus
#print axioms Deep.NTSupply.mem_coprimeToModulus_iff
#print axioms Deep.NTSupply.narrowRaySet
#print axioms Deep.NTSupply.narrowRaySubgroup
#print axioms Deep.NTSupply.narrowRaySubgroup_le_coprimeToModulus
#print axioms Deep.NTSupply.NarrowRayClassGroup
#print axioms Deep.NTSupply.NarrowRayClassGroup.mk
#print axioms Deep.NTSupply.one_mem_narrowRaySet
#print axioms Deep.NTSupply.raySymbol
#print axioms Deep.NTSupply.raySymbol_mul
#print axioms Deep.NTSupply.raySymbolHom
#print axioms Deep.NTSupply.raySymbolHom_prime
#print axioms Deep.NTSupply.raySymbolDescend
#print axioms Deep.NTSupply.raySymbolDescend_mk
#print axioms Deep.NTSupply.raySymbolDescend_primeClass
#print axioms Deep.NTSupply.raySymbolIdealHom
#print axioms Deep.NTSupply.primeUnit
#print axioms Deep.NTSupply.primeClass
#print axioms Deep.NTSupply.movingLemma
#print axioms Deep.NTSupply.finite
#print axioms Deep.NTSupply.coprimeToModulus_top
#print axioms Deep.NTSupply.finite_closure_of_involutions

end Deep.NTSupply

Statements phrased using this module (27)