Every ray class has a coprime integral ideal representative

Proved

TauCeti.GlobalNumberFields.idealClass_surjective

by riccardo.brasca · Sep 29, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theorytauceti-chebotarev

Let $K$ be a number field and $\mathfrak m=(\mathfrak m_0,\mathfrak m_\infty)$ a modulus, with nonzero integral ideal $\mathfrak m_0$ and a finite set $\mathfrak m_\infty$ of real places. Every ray class is represented by a nonzero integral ideal prime to the finite part:

\{I\subseteq\mathcal O_K:I\ne0,\ I+\mathfrak m_0=\mathcal O_K\} \twoheadrightarrow\operatorname{Cl}_{\mathfrak m}(K),\qquad I\longmapsto[I]_{\mathfrak m}.

This allows ray class arguments and counts to use integral ideals satisfying the modulus coprimality condition.

Source: the Tau Ceti contributors (Apache-2.0, commit 948fe4751b1fe528b6d580c522ca5d743d47f185).

Preamble

/- Transplanted from https://github.com/TauCetiProject/TauCeti at 948fe4751b1fe528b6d580c522ca5d743d47f185.
Original source copyright/license notices are retained below.
Generated exclusively from compiler declaration, command, and reference facts. -/
import Definitions.Def_TauCeti_NumberTheory_NumberField_Global_RayClass_Basic
import Definitions.Def_TauCeti_NumberTheory_NumberField_Global_RayClass_Integral
import Definitions.Def_TauCeti_NumberTheory_NumberField_Global_RayClass_Modulus
import Definitions.Def_TauCeti_NumberTheory_NumberField_Ideal_Away
import Definitions.Def_TauCeti_RingTheory_DedekindDomain_Factorization
import Definitions.Def_TauCeti_RingTheory_DedekindDomain_Ideal
import Mathlib.Algebra.Group.Subgroup.Ker
import Mathlib.Algebra.Order.Ring.Units
import Mathlib.Algebra.Ring.Int.Units
import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Data.Nat.Prime.Defs
import Mathlib.GroupTheory.Index
import Mathlib.GroupTheory.IndexNormal
import Mathlib.GroupTheory.Solvable
import Mathlib.GroupTheory.Subgroup.Center
import Mathlib.NumberTheory.NumberField.Basic
import Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
import Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
import Mathlib.RingTheory.ClassGroup.Basic
import Mathlib.RingTheory.DedekindDomain.AdicValuation
import Mathlib.RingTheory.DedekindDomain.Factorization
import Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
import Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing
import Mathlib.Tactic.Group

section
set_option autoImplicit true
/-
Copyright (c) 2026 The Tau Ceti contributors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Tau Ceti contributors
-/
/-!
# Integral representatives of ray classes

Every ray class of a modulus `𝔪` of a number field is the class of a nonzero *integral* ideal
prime to `𝔪`, and such an ideal has trivial class exactly when it is generated by an algebraic
integer congruent to one modulo `𝔪`, equivalently when it satisfies an integral equation
`I · (b) = (a)` whose two generators are congruent to one modulo `𝔪`.  The construction behind both
is that inside a nonzero ideal `D` comaximal with the finite part `𝔪₀` there is an algebraic
integer congruent to one modulo `𝔪₀` and positive at every real place (`exists_mem_isCongrOne`).
Its existence combines the comaximality, which supplies an element of `D` congruent to one, with
`NumberField.exists_isTotallyPositive_sub_mem`, which corrects the archimedean signs without
leaving the residue class modulo `D · 𝔪₀`.

Applying that construction to an integral ideal `I` prime to `𝔪` produces a principal ideal
`(α) = I · J` generated by an element congruent to one, so `J` is again prime to `𝔪` and the ray
class of `J` inverts the ray class of `I`.  The image of `idealClass 𝔪` is therefore a *subgroup*
of the ray class group, and since it contains the class of every prime not dividing `𝔪` it is
everything: this is the moving lemma, `idealClass_surjective`.

## Main results

* `TauCeti.GlobalNumberFields.exists_mem_isCongrOne`: an ideal comaximal with the finite part of
  `𝔪` contains a nonzero element whose image in `Kˣ` is congruent to one modulo `𝔪`.
* `TauCeti.GlobalNumberFields.exists_isCongrOne_span_eq_mul`: an integral ideal prime to `𝔪`
  divides a principal ideal whose generator is congruent to one modulo `𝔪`, with complementary
  ideal again prime to `𝔪`.
* `TauCeti.GlobalNumberFields.exists_idealClass_mul_eq_one`: the ray class of an integral ideal
  prime to `𝔪` is inverted by the ray class of another such ideal.
* `TauCeti.GlobalNumberFields.idealClass_surjective`: **the moving lemma**, that every ray class is
  the class of a nonzero integral ideal prime to the modulus.
* `TauCeti.GlobalNumberFields.idealClass_eq_one_iff_exists_generator`: the generator form of
  `idealClass_eq_one_iff`, with the generator kept inside `𝓞 K` and its two defining conditions
  spelled out.
* `TauCeti.GlobalNumberFields.idealClass_eq_one_iff_exists_integral`: the denominator-cleared form
  of `idealClass_eq_one_iff`, an equation `I · (b) = (a)` between integral ideals whose generators
  are congruent to one modulo `𝔪`.

## References

* J. Neukirch, *Algebraic Number Theory*, Chapter VI, §1.
* S. Lang, *Algebraic Number Theory*, Chapter VI, §1.
-/

 section

open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum NumberField
open scoped nonZeroDivisors NumberField

namespace TauCeti.GlobalNumberFields
end TauCeti.GlobalNumberFields
section TauCeti.GlobalNumberFields
open TauCeti TauCeti.GlobalNumberFields

variable {K : Type*} [Field K] [NumberField K]

/-! ### Generators congruent to one modulo a modulus -/







/-! ### The moving lemma -/

Formal statement

theorem TauCeti.GlobalNumberFields.idealClass_surjective (𝔪 : _root_.TauCeti.GlobalNumberFields.Modulus K) : _root_.Function.Surjective (_root_.TauCeti.GlobalNumberFields.idealClass 𝔪) := by sorry

Source

https://github.com/TauCetiProject/TauCeti/blob/948fe4751b1fe528b6d580c522ca5d743d47f185/TauCeti/NumberTheory/NumberField/Global/RayClass/Integral.lean#L151-L187

View graph