Orbits of the congruence roots of unity on the ray integer set

Two points of rayIntegerSet 𝔪 lie in the same orbit of the congruence roots of unity exactly when some unit congruent to one modulo 𝔪 carries one to the other. So orbits of the small group unitsCongruenceTorsion 𝔪 on the domain are the traces of the large group unitsCongruenceSubgroup 𝔪 acting on the whole space: the large group identifies no two points of the domain that the small group does not already identify. Together with exists_unitsCongruenceSubgroup_smul_mem_rayFundamentalDomain, which moves each point of nonzero norm in posRegion 𝔪 into the domain, that is the sense in which the domain is fundamental for the large group modulo the small one.

For the trivial modulus the large group is all of (𝓞 K)ˣ, translation by it is associatedness in (𝓞 K)⁰, and the statement is Mathlib's integerSetToAssociates_eq_iff, whose left-hand side reads the orbit off in Associates (𝓞 K)⁰. Mathlib has no such quotient type for a proper subgroup of the units, so this file states the orbit relation directly.

Main results

• TauCeti.GlobalNumberFields.exists_mem_unitsCongruenceTorsion_smul_iff: the orbit relation for any two points of the domain;
• TauCeti.GlobalNumberFields.exists_unitsCongruenceTorsion_smul_iff: the same on rayIntegerSet 𝔪, which is the form the count consumes.

theorem TauCeti.GlobalNumberFields.exists_mem_unitsCongruenceTorsion_smul_iff {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {a b : NumberField.mixedEmbedding.mixedSpace K} (ha : a ∈ rayFundamentalDomain 𝔪) (hb : b ∈ rayFundamentalDomain 𝔪) : (∃ ζ ∈ unitsCongruenceTorsion 𝔪, ζ • a = b) ↔ ∃ u ∈ unitsCongruenceSubgroup 𝔪, u • a = b

The orbit relation, for any two points of the domain. A congruence unit carrying one point of rayFundamentalDomain 𝔪 to another is automatically a root of unity, so the two subgroups have the same orbits on the domain. Only membership of the domain is needed; the points need not be images of algebraic integers.

theorem TauCeti.GlobalNumberFields.exists_unitsCongruenceTorsion_smul_iff {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} (a b : ↑(rayIntegerSet 𝔪)) : (∃ (ζ : ↥(unitsCongruenceTorsion 𝔪)), ζ • a = b) ↔ ∃ u ∈ unitsCongruenceSubgroup 𝔪, u • ↑a = ↑b

The orbit relation on the ray integer set. Two points of rayIntegerSet 𝔪 lie in one orbit of the congruence roots of unity exactly when some unit congruent to one modulo 𝔪 carries one to the other in the mixed space. Since mixedEmbedding is injective and multiplicative, that is the same as their algebraic integers differing by such a unit, which is the form the ray class count consumes.