Integrality and torsion in the circle group

A rational number reduces to zero in ℚ/ℤ, realized as AddCircle (1 : ℚ), exactly when it lies in (1 : Submodule ℤ ℚ), the copy of ℤ inside ℚ. This bridges the two spellings of integrality used by the discriminant-form theory: vanishing in the circle group and membership in the unit ℤ-submodule.

For any period p in a division ring, the n-torsion of AddCircle p is generated by p / n whenever n is nonzero in that ring. Finiteness of the n-torsion only requires multiplication by n to be injective on the ambient additive group. For a nonzero period in characteristic zero and positive n, p / n has additive order exactly n; the torsion subgroup is therefore cyclic of order exactly n, and it is the only subgroup of that order. Consequently n ↦ (AddCircle p)[n] is an order embedding of the divisibility order on positive naturals into the subgroups of AddCircle p, and every finite subgroup is one of these.

Taking p = 1 over ℚ this is the classical description of the finite subgroups of ℚ/ℤ: for each n there is exactly one subgroup of order n, namely the cyclic group generated by the class of 1 / n. That statement is what normalizes a class-field-theoretic invariant map: an injective homomorphism from a finite group onto the n-torsion of ℚ/ℤ forces the group to be cyclic of order n with a distinguished generator, the one of invariant 1 / n.

Main declarations

• AddCircle.coe_eq_zero_iff_mem_one: vanishing in AddCircle (1 : ℚ) is membership in (1 : Submodule ℤ ℚ).
• AddCircle.zsmul_coe_eq_zero: an integer multiple of a rational number vanishes in AddCircle (1 : ℚ) once that multiple is an integer.
• AddCircle.coe_add_intCast: adding an integer does not change a class in AddCircle (1 : ℚ).
• AddCircle.intCast_floor_equivIco_add: the floor of the sum of two representatives in [0, 1) is their defect of additivity.
• AddCircle.torsionBy_eq_zmultiples: the n-torsion of AddCircle p is generated by the class of p / n.
• AddCircle.eq_zero_or_eq_coe_period_div_two: a point killed by 2 is 0 or the class of p / 2.
• AddCircle.addOrderOf_period_div_of_ne_zero: for a nonzero period and positive n, the class of p / n has additive order n.
• AddCircle.natCard_torsionBy: for positive n, the n-torsion of AddCircle p has exactly n elements.
• AddCircle.eq_torsionBy_of_natCard_eq: a subgroup of AddCircle p with n elements is the n-torsion; equivalently, AddCircle.exists_eq_torsionBy writes every finite subgroup as a torsion subgroup.
• AddCircle.torsionBy_le_torsionBy_iff and AddCircle.torsionBy_inj: the torsion subgroups are ordered by divisibility, and pairwise distinct.
• AddCircle.nsmul_coe_period_div and AddCircle.nsmul_coe_period_div_of_mul_eq: scaling the class of p / n by a divisor d of n gives the class of p / (n / d); when n is nonzero in 𝕜 these are the canonical generators of the n- and the n / d-torsion.
• AddCircle.natCard_eq_of_injective_of_range_eq_torsionBy, AddCircle.existsUnique_apply_eq_coe_period_div, AddCircle.exists_zsmul_eq_of_apply_eq_coe_period_div, AddCircle.isAddCyclic_of_injective_of_range_eq_torsionBy and AddCircle.zmodAddEquivOfInjectiveOfRangeEqTorsionBy: an injective homomorphism from a group onto the n-torsion makes that group cyclic of order n, with a unique element of invariant p / n as a distinguished generator.
• AddCircle.isAddTorsion_rat: a rational circle is a torsion group, so its torsion subgroups exhaust it (AddCircle.exists_mem_torsionBy_rat).
• ZMod.toRatAddCircle and ZMod.toRatAddCircle_range: the homomorphism from ℤ/n to ℚ/ℤ sending the class of an integer k to the class of k / n; for nonzero n, it is an injection onto the n-torsion, so every element killed by n lies in its image (ZMod.exists_toRatAddCircle_eq_of_nsmul_eq_zero).

References

• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §2: the invariant map of a class formation takes values in ℚ/ℤ, and on a layer of degree n its image is the unique subgroup of order n, in which the fundamental class is the element 1 / n.

theorem AddCircle.coe_eq_zero_iff_mem_one (q : ℚ) : ↑q = 0 ↔ q ∈ 1

A rational number reduces to zero in ℚ/ℤ exactly when it is an integer.

theorem AddCircle.zsmul_coe_eq_zero {k c : ℤ} {x : ℚ} (h : ↑k * x = ↑c) : k • ↑x = 0

The multiple k • x of a rational number vanishes in ℚ/ℤ as soon as it is the integer c.

This is the shape in which the torsion side conditions of the cyclic and Klein four presentations of a finite quadratic module arise: the witness c is supplied explicitly and the remaining arithmetic identity is a computation in ℚ.

theorem AddCircle.coe_add_intCast (x : ℚ) (n : ℤ) : ↑(x + ↑n) = ↑x

Adding an integer does not change a class in ℚ/ℤ. This is AddCircle.coe_add_period for an arbitrary integer multiple of the period 1.

theorem AddCircle.intCast_floor_equivIco_add (x y : AddCircle 1) : ↑⌊↑((equivIco 1 0) x) + ↑((equivIco 1 0) y)⌋ = ↑((equivIco 1 0) x) + ↑((equivIco 1 0) y) - ↑((equivIco 1 0) (x + y))

The floor of the sum of the representatives in [0, 1) of two points of ℚ/ℤ is the defect of additivity of the representatives.

theorem AddCircle.coe_intCast_div_natCast_eq_zero_iff {n : ℕ} (hn : n ≠ 0) (k : ℤ) : ↑(↑k / ↑n) = 0 ↔ ↑n ∣ k

A fraction with nonzero natural denominator vanishes in ℚ/ℤ exactly when the denominator divides the numerator.

theorem AddCircle.finite_torsionBy {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) {n : ℕ} (hn : IsSMulRegular 𝕜 n) : Finite ↥(AddSubgroup.torsionBy (AddCircle p) ↑n)

The n-torsion of AddCircle p is finite when multiplication by n is injective on 𝕜.

theorem AddCircle.coe_period_div_mem_torsionBy {𝕜 : Type u_1} [DivisionRing 𝕜] (p : 𝕜) {n : ℕ} : ↑(p / ↑n) ∈ AddSubgroup.torsionBy (AddCircle p) ↑n

The class of p / n is killed by n, including when n = 0 or p = 0.

theorem AddCircle.torsionBy_eq_zmultiples {𝕜 : Type u_1} [DivisionRing 𝕜] (p : 𝕜) {n : ℕ} (hn : ↑n ≠ 0) : AddSubgroup.torsionBy (AddCircle p) ↑n = AddSubgroup.zmultiples ↑(p / ↑n)

The n-torsion of AddCircle p is the cyclic subgroup generated by the class of p / n, whenever n is nonzero in 𝕜.

theorem AddCircle.exists_zsmul_eq_of_mem_torsionBy {𝕜 : Type u_1} [DivisionRing 𝕜] (p : 𝕜) {n : ℕ} (hn : ↑n ≠ 0) {u : AddCircle p} (hu : u ∈ AddSubgroup.torsionBy (AddCircle p) ↑n) : ∃ (k : ℤ), k • ↑(p / ↑n) = u

Every point killed by n is an integer multiple of the class of p / n, whenever n is nonzero in 𝕜.

theorem AddCircle.eq_zero_or_eq_coe_period_div_two {𝕜 : Type u_1} [DivisionRing 𝕜] (p : 𝕜) (h2 : 2 ≠ 0) {u : AddCircle p} (hu : 2 • u = 0) : u = 0 ∨ u = ↑(p / 2)

A point of AddCircle p killed by 2 is either 0 or the class of p / 2, whenever 2 is nonzero in 𝕜.

theorem AddCircle.isAddCyclic_torsionBy {𝕜 : Type u_1} [DivisionRing 𝕜] (p : 𝕜) {n : ℕ} (hn : ↑n ≠ 0) : IsAddCyclic ↥(AddSubgroup.torsionBy (AddCircle p) ↑n)

The n-torsion of AddCircle p is cyclic whenever n is nonzero in 𝕜.

theorem AddCircle.eq_torsionBy_of_natCard_eq {𝕜 : Type u_1} [DivisionRing 𝕜] (p : 𝕜) {n : ℕ} (hn : ↑n ≠ 0) {H : AddSubgroup (AddCircle p)} (hH : Nat.card ↥H = n) : H = AddSubgroup.torsionBy (AddCircle p) ↑n

A subgroup of AddCircle p with n elements is the n-torsion, whenever n is nonzero in 𝕜. For a nonzero period in characteristic zero this makes the n-torsion the only subgroup of order n.

theorem AddCircle.exists_eq_torsionBy {𝕜 : Type u_1} [DivisionRing 𝕜] [CharZero 𝕜] (p : 𝕜) {H : AddSubgroup (AddCircle p)} [Finite ↥H] : ∃ (n : ℕ), 0 < n ∧ H = AddSubgroup.torsionBy (AddCircle p) ↑n

Every finite subgroup of AddCircle p is a torsion subgroup.

theorem AddCircle.addOrderOf_period_div_of_ne_zero {𝕜 : Type u_1} [DivisionRing 𝕜] [CharZero 𝕜] (p : 𝕜) [NeZero p] {n : ℕ} (hn : 0 < n) : addOrderOf ↑(p / ↑n) = n

For a nonzero period, the class of p / n has additive order exactly n when n is positive. This generalizes Mathlib's AddCircle.addOrderOf_period_div, which assumes a positive period in a linearly ordered field.

theorem AddCircle.natCard_torsionBy {𝕜 : Type u_1} [DivisionRing 𝕜] [CharZero 𝕜] (p : 𝕜) [NeZero p] {n : ℕ} (hn : 0 < n) : Nat.card ↥(AddSubgroup.torsionBy (AddCircle p) ↑n) = n

The n-torsion of AddCircle p has exactly n elements.

theorem AddCircle.torsionBy_le_torsionBy_iff {𝕜 : Type u_1} [DivisionRing 𝕜] [CharZero 𝕜] (p : 𝕜) [NeZero p] {m n : ℕ} (hm : 0 < m) (hn : 0 < n) : AddSubgroup.torsionBy (AddCircle p) ↑m ≤ AddSubgroup.torsionBy (AddCircle p) ↑n ↔ m ∣ n

The torsion subgroups of AddCircle p are ordered by divisibility.

theorem AddCircle.torsionBy_inj {𝕜 : Type u_1} [DivisionRing 𝕜] [CharZero 𝕜] (p : 𝕜) [NeZero p] {m n : ℕ} (hm : 0 < m) (hn : 0 < n) : AddSubgroup.torsionBy (AddCircle p) ↑m = AddSubgroup.torsionBy (AddCircle p) ↑n ↔ m = n

Distinct positive orders give distinct torsion subgroups of AddCircle p.

@[simp]

theorem AddCircle.nsmul_coe_period_div {𝕜 : Type u_1} [DivisionRing 𝕜] (p : 𝕜) {n d : ℕ} (hd : d ∣ n) : d • ↑(p / ↑n) = ↑(p / ↑(n / d))

Scaling the class of p / n by a divisor d of n gives the class of p / (n / d). For n nonzero in 𝕜 these two classes are the canonical generators of the n-torsion and of the n / d-torsion; when n vanishes in 𝕜 both sides are 0.

For p = 1 over ℚ this reads d • (1 / n) = 1 / (n / d), the arithmetic behind the way restriction rescales a class-field-theoretic invariant.

theorem AddCircle.nsmul_coe_period_div_of_mul_eq {𝕜 : Type u_1} [DivisionRing 𝕜] (p : 𝕜) {a b d : ℕ} (h : a * d = b) (hd : 0 < d) : d • ↑(p / ↑b) = ↑(p / ↑a)

If a * d = b with d positive, scaling the class of p / b by d gives the class of p / a.

Groups normalized by an invariant map

An invariant map on a group H is an injective homomorphism f : H →+ AddCircle p whose image is the n-torsion. For n nonzero in the division ring, H is cyclic and the element of invariant p / n is a distinguished generator. For a nonzero period in characteristic zero, H has order exactly n. Over ℚ with p = 1 this is the normalization that produces the fundamental class of a class formation from its invariant map.

theorem AddCircle.natCard_eq_of_injective_of_range_eq_torsionBy {n : ℕ} {H : Type u_1} {𝕜 : Type u_2} [DivisionRing 𝕜] [CharZero 𝕜] (p : 𝕜) [NeZero p] {f : H → AddCircle p} (hn : 0 < n) (hf : Function.Injective f) (hr : Set.range f = ↑(AddSubgroup.torsionBy (AddCircle p) ↑n)) : Nat.card H = n

A type with an injective map onto the n-torsion has exactly n elements.

theorem AddCircle.existsUnique_apply_eq_coe_period_div {n : ℕ} {H : Type u_1} {𝕜 : Type u_2} [DivisionRing 𝕜] (p : 𝕜) {f : H → AddCircle p} (hf : Function.Injective f) (hr : Set.range f = ↑(AddSubgroup.torsionBy (AddCircle p) ↑n)) : ∃! u : H, f u = ↑(p / ↑n)

An injective map onto the n-torsion has a unique preimage of the class of p / n.

theorem AddCircle.exists_zsmul_eq_of_apply_eq_coe_period_div {n : ℕ} {H : Type u_1} {𝕜 : Type u_2} [DivisionRing 𝕜] (p : 𝕜) [AddGroup H] {f : H →+ AddCircle p} (hn : ↑n ≠ 0) (hf : Function.Injective ⇑f) (hr : Set.range ⇑f = ↑(AddSubgroup.torsionBy (AddCircle p) ↑n)) {u : H} (hu : f u = ↑(p / ↑n)) (x : H) : ∃ (k : ℤ), k • u = x

The element of invariant p / n generates a group carrying an invariant map onto the n-torsion, whenever n is nonzero in 𝕜.

theorem AddCircle.isAddCyclic_of_injective_of_range_eq_torsionBy {n : ℕ} {H : Type u_1} {𝕜 : Type u_2} [DivisionRing 𝕜] (p : 𝕜) [AddGroup H] {f : H →+ AddCircle p} (hn : ↑n ≠ 0) (hf : Function.Injective ⇑f) (hr : Set.range ⇑f = ↑(AddSubgroup.torsionBy (AddCircle p) ↑n)) : IsAddCyclic H

A group with an invariant map onto the n-torsion is cyclic whenever n is nonzero in 𝕜.

noncomputable def AddCircle.zmodAddEquivOfInjectiveOfRangeEqTorsionBy {n : ℕ} {H : Type u_1} {𝕜 : Type u_2} [DivisionRing 𝕜] [CharZero 𝕜] (p : 𝕜) [NeZero p] [AddGroup H] {f : H →+ AddCircle p} (hn : 0 < n) (hf : Function.Injective ⇑f) (hr : Set.range ⇑f = ↑(AddSubgroup.torsionBy (AddCircle p) ↑n)) {u : H} (hu : f u = ↑(p / ↑n)) : ZMod n ≃+ H

A group with an invariant map onto the n-torsion is ZMod n, by an isomorphism sending 1 to the element u of invariant p / n.

Equations

• AddCircle.zmodAddEquivOfInjectiveOfRangeEqTorsionBy p hn hf hr hu = zmodAddEquivOfGenerator ⋯ ⋯

@[simp]

theorem AddCircle.zmodAddEquivOfInjectiveOfRangeEqTorsionBy_apply_intCast {n : ℕ} {H : Type u_1} {𝕜 : Type u_2} [DivisionRing 𝕜] [CharZero 𝕜] (p : 𝕜) [NeZero p] [AddGroup H] {f : H →+ AddCircle p} (hn : 0 < n) (hf : Function.Injective ⇑f) (hr : Set.range ⇑f = ↑(AddSubgroup.torsionBy (AddCircle p) ↑n)) {u : H} (hu : f u = ↑(p / ↑n)) (i : ℤ) : (zmodAddEquivOfInjectiveOfRangeEqTorsionBy p hn hf hr hu) ↑i = i • u

The isomorphism AddCircle.zmodAddEquivOfInjectiveOfRangeEqTorsionBy sends the class of an integer i to the multiple i • u of the element u of invariant p / n.

@[simp]

theorem AddCircle.zmodAddEquivOfInjectiveOfRangeEqTorsionBy_symm_apply_zsmul {n : ℕ} {H : Type u_1} {𝕜 : Type u_2} [DivisionRing 𝕜] [CharZero 𝕜] (p : 𝕜) [NeZero p] [AddGroup H] {f : H →+ AddCircle p} (hn : 0 < n) (hf : Function.Injective ⇑f) (hr : Set.range ⇑f = ↑(AddSubgroup.torsionBy (AddCircle p) ↑n)) {u : H} (hu : f u = ↑(p / ↑n)) (i : ℤ) : (zmodAddEquivOfInjectiveOfRangeEqTorsionBy p hn hf hr hu).symm (i • u) = ↑i

The inverse of AddCircle.zmodAddEquivOfInjectiveOfRangeEqTorsionBy sends the multiple i • u of the element u of invariant p / n to the class of the integer i.

@[simp]

theorem AddCircle.zmodAddEquivOfInjectiveOfRangeEqTorsionBy_apply_one {n : ℕ} {H : Type u_1} {𝕜 : Type u_2} [DivisionRing 𝕜] [CharZero 𝕜] (p : 𝕜) [NeZero p] [AddGroup H] {f : H →+ AddCircle p} (hn : 0 < n) (hf : Function.Injective ⇑f) (hr : Set.range ⇑f = ↑(AddSubgroup.torsionBy (AddCircle p) ↑n)) {u : H} (hu : f u = ↑(p / ↑n)) : (zmodAddEquivOfInjectiveOfRangeEqTorsionBy p hn hf hr hu) 1 = u

The isomorphism AddCircle.zmodAddEquivOfInjectiveOfRangeEqTorsionBy sends 1 : ZMod n to the element u of invariant p / n.

theorem AddCircle.isOfFinAddOrder_rat {p : ℚ} [hp : Fact (0 < p)] (u : AddCircle p) : IsOfFinAddOrder u

Every element of a rational circle ℚ ⧸ pℤ has finite additive order: the class of r is killed by the denominator of r / p.

theorem AddCircle.isAddTorsion_rat {p : ℚ} [hp : Fact (0 < p)] : IsAddTorsion (AddCircle p)

A rational circle ℚ ⧸ pℤ is a torsion group.

theorem AddCircle.exists_mem_torsionBy_rat {p : ℚ} [hp : Fact (0 < p)] (u : AddCircle p) : ∃ (n : ℕ), 0 < n ∧ u ∈ AddSubgroup.torsionBy (AddCircle p) ↑n

The torsion subgroups exhaust a rational circle: every element lies in (ℚ ⧸ pℤ)[n] for some positive n. Together with AddCircle.eq_torsionBy_of_natCard_eq this describes ℚ/ℤ as the union of its unique subgroups of each finite order, a family directed by divisibility rather than by the order on ℕ (AddCircle.torsionBy_le_torsionBy_iff).

def ZMod.toRatAddCircle (n : ℕ) : ZMod n →+ AddCircle 1

The homomorphism from ℤ/n to ℚ/ℤ sending the class of an integer k to the class of k / n. For nonzero n, it is an injection onto the n-torsion; for n = 0, it is the zero map.

Mathlib's ZMod.toAddCircle is this map into the real circle ℝ/ℤ. Discriminant forms and character modules take rational values, so the rational circle is the target used here.

Equations

• ZMod.toRatAddCircle n = (ZMod.lift n) ⟨(zmultiplesHom (AddCircle 1)) ↑(1 / ↑n), ⋯⟩

@[simp]

theorem ZMod.toRatAddCircle_intCast (n : ℕ) (k : ℤ) : (toRatAddCircle n) ↑k = ↑(↑k / ↑n)

The class of an integer maps to the class of that integer divided by n.

@[simp]

theorem ZMod.toRatAddCircle_natCast (n k : ℕ) : (toRatAddCircle n) ↑k = ↑(↑k / ↑n)

The class of a natural number maps to the class of that number divided by n.

theorem ZMod.toRatAddCircle_apply (n : ℕ) [NeZero n] (x : ZMod n) : (toRatAddCircle n) x = ↑(↑x.val / ↑n)

The value of ZMod.toRatAddCircle on the canonical representative of a residue class.

@[simp]

theorem ZMod.toRatAddCircle_eq_zero (n : ℕ) [NeZero n] {x : ZMod n} : (toRatAddCircle n) x = 0 ↔ x = 0

Only the zero residue has integral image in ℚ/ℤ.

theorem ZMod.toRatAddCircle_injective (n : ℕ) [NeZero n] : Function.Injective ⇑(toRatAddCircle n)

For a nonzero modulus the rational-circle character of ℤ/n is injective.

theorem ZMod.toRatAddCircle_range (n : ℕ) [NeZero n] : (toRatAddCircle n).range = AddSubgroup.torsionBy (AddCircle 1) ↑n

For a nonzero modulus, the image of the rational-circle character of ℤ/n is exactly the n-torsion of ℚ/ℤ.

theorem ZMod.exists_toRatAddCircle_eq_of_nsmul_eq_zero (n : ℕ) [NeZero n] {v : AddCircle 1} (hv : n • v = 0) : ∃ (a : ZMod n), (toRatAddCircle n) a = v

For a nonzero modulus, every element of ℚ/ℤ killed by n is the image of a residue class under the rational-circle character of ℤ/n.