The action of units on the mixed space

This file provides basic compatibility and measurability lemmas for the action of number-field units on the mixed space.

Main results

• TauCeti.NumberField.Units.unitSMul_comm: two unit actions commute;
• TauCeti.NumberField.Units.unitSMul_real_smul: the unit action commutes with real scalar multiplication;
• MeasurableConstSMul (𝓞 K)ˣ (mixedEmbedding.mixedSpace K): the action of a fixed unit is measurable, so Mathlib's measurable_const_smul applies;
• TauCeti.NumberField.Units.eq_one_of_unitSMul_mixedEmbedding_eq: a unit fixing the image of a nonzero element of K is the identity.

It also identifies the units of the mixed space itself:

• TauCeti.NumberField.mixedEmbedding.isUnit_iff_norm_ne_zero: a point of the mixed space is a unit exactly when its norm is nonzero.

theorem TauCeti.NumberField.Units.unitSMul_comm {K : Type u_1} [Field K] (u v : (NumberField.RingOfIntegers K)ˣ) (x : NumberField.mixedEmbedding.mixedSpace K) : u • v • x = v • u • x

The unit action on the mixed space is commutative: it is multiplication by the mixed embedding of a unit, and the mixed space is a commutative ring.

theorem TauCeti.NumberField.Units.unitSMul_real_smul {K : Type u_1} [Field K] (u : (NumberField.RingOfIntegers K)ˣ) (c : ℝ) (x : NumberField.mixedEmbedding.mixedSpace K) : u • c • x = c • u • x

The unit action on the mixed space commutes with the real scalar action.

instance TauCeti.NumberField.Units.instMeasurableConstSMulUnitsRingOfIntegersMixedSpaceOfNumberField_tauCeti {K : Type u_1} [Field K] [NumberField K] : MeasurableConstSMul (NumberField.RingOfIntegers K)ˣ (NumberField.mixedEmbedding.mixedSpace K)

The action of a fixed unit on the mixed space is measurable.

Stated as the MeasurableConstSMul instance rather than as a bare lemma, because that is what Mathlib's measure-theoretic API for group actions keys on: measurable_const_smul is then the equation, and measurePreserving_smul and the IsFundamentalDomain lemmas become available wherever the action is also measure-preserving.

theorem TauCeti.NumberField.Units.eq_one_of_unitSMul_mixedEmbedding_eq {K : Type u_1} [Field K] [NumberField K] {x : K} (hx : x ≠ 0) {u : (NumberField.RingOfIntegers K)ˣ} (h : u • (NumberField.mixedEmbedding K) x = (NumberField.mixedEmbedding K) x) : u = 1

The unit action on the mixed space is faithful away from zero. A unit fixing the image of a nonzero element of K is the identity.

theorem TauCeti.NumberField.mixedEmbedding.isUnit_iff_norm_ne_zero {K : Type u_1} [Field K] [NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K} : IsUnit x ↔ NumberField.mixedEmbedding.norm x ≠ 0

The units of the mixed space are its points of nonzero norm: a point is invertible exactly when none of its coordinates vanishes.