The unit logarithmic lattice in the sum-zero hyperplane

The weighted logarithms of the units of a number field form a full lattice in the hyperplane of functions on its infinite places whose coordinate sum is zero. Unlike a logarithmic embedding which omits a distinguished place, this presentation is compatible with field automorphisms: an automorphism permutes the logarithmic coordinates by its action on infinite places.

This is the archimedean part of the equivariant S-unit logarithmic lattice used to compute Herbrand quotients. We transfer the lattice property from Mathlib's NumberField.Units.unitLattice and use its torsion-kernel theorem, rather than proving Dirichlet's theorem again.

References

• J. S. Milne, Class Field Theory, Chapter VII, §4, the logarithmic unit lattice.

noncomputable def TauCeti.unitLogEmbedding (K : Type u_1) [Field K] [NumberField K] : Additive (NumberField.RingOfIntegers K)ˣ →+ ↥(singleParityCheckCode ℝ (NumberField.InfinitePlace K))

The weighted logarithm of a unit, retaining every infinite place. The product formula places its image in the sum-zero hyperplane singleParityCheckCode ℝ (InfinitePlace K).

@[simp]

theorem TauCeti.unitLogEmbedding_apply (K : Type u_1) [Field K] [NumberField K] (u : Additive (NumberField.RingOfIntegers K)ˣ) (w : NumberField.InfinitePlace K) : ↑((unitLogEmbedding K) u) w = ↑w.mult * Real.log (w ((algebraMap (NumberField.RingOfIntegers K) K) ↑(Additive.toMul u)))

The coordinate of the full logarithmic embedding at an infinite place.

@[simp]

theorem TauCeti.unitLogEmbedding_eq_zero_iff (K : Type u_1) [Field K] [NumberField K] (u : Additive (NumberField.RingOfIntegers K)ˣ) : (unitLogEmbedding K) u = 0 ↔ Additive.toMul u ∈ NumberField.Units.torsion K

The kernel of the full logarithmic embedding consists exactly of the roots of unity.

theorem TauCeti.unitLogEmbedding_ker (K : Type u_1) [Field K] [NumberField K] : (unitLogEmbedding K).ker = Subgroup.toAddSubgroup (NumberField.Units.torsion K)

The kernel of the full logarithmic embedding is the additive torsion subgroup of units.

noncomputable def TauCeti.fullUnitLattice (K : Type u_1) [Field K] [NumberField K] : Submodule ℤ ↥(singleParityCheckCode ℝ (NumberField.InfinitePlace K))

The unit logarithmic lattice, as an integral submodule of the sum-zero hyperplane.

@[simp]

theorem TauCeti.mem_fullUnitLattice (K : Type u_1) [Field K] [NumberField K] (x : ↥(singleParityCheckCode ℝ (NumberField.InfinitePlace K))) : x ∈ fullUnitLattice K ↔ ∃ (u : Additive (NumberField.RingOfIntegers K)ˣ), (unitLogEmbedding K) u = x

The full unit lattice is exactly the set of logarithmic images of units.

Comparison with Mathlib's coordinates transfers Dirichlet's lattice property and supplies the coordinate map used for the Euclidean covolume comparison in Log.Covolume. The distinguished place is not part of the full logarithmic embedding.

noncomputable def TauCeti.unitLogCoordinates (K : Type u_1) [Field K] [NumberField K] : ↥(singleParityCheckCode ℝ (NumberField.InfinitePlace K)) ≃ₗ[ℝ] NumberField.Units.dirichletUnitTheorem.logSpace K

Dropping the distinguished place identifies the sum-zero hyperplane with Mathlib's logarithmic coordinate space. Its inverse restores that coordinate using the product formula.

@[simp]

theorem TauCeti.unitLogCoordinates_apply (K : Type u_1) [Field K] [NumberField K] (x : ↥(singleParityCheckCode ℝ (NumberField.InfinitePlace K))) (w : { w : NumberField.InfinitePlace K // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }) : (unitLogCoordinates K) x w = ↑x ↑w

The logarithmic coordinate map retains each coordinate away from the distinguished place.

@[simp]

theorem TauCeti.unitLogCoordinates_symm_apply (K : Type u_1) [Field K] [NumberField K] (y : NumberField.Units.dirichletUnitTheorem.logSpace K) (w : NumberField.InfinitePlace K) : ↑((unitLogCoordinates K).symm y) w = (NumberField.Units.logSpaceExtend K) y w

The inverse coordinate map restores the distinguished coordinate as minus the sum of the others.

@[simp]

theorem TauCeti.unitLogCoordinates_embedding (K : Type u_1) [Field K] [NumberField K] (u : Additive (NumberField.RingOfIntegers K)ˣ) : (unitLogCoordinates K) ((unitLogEmbedding K) u) = (NumberField.Units.logEmbedding K) u

The full logarithmic embedding has Mathlib's logarithmic embedding as its coordinates.

theorem TauCeti.fullUnitLattice_eq_comap (K : Type u_1) [Field K] [NumberField K] : fullUnitLattice K = ZLattice.comap ℝ (NumberField.Units.unitLattice K) ↑↑(unitLogCoordinates K).toContinuousLinearEquiv

The full logarithmic lattice is the pullback of Mathlib's unit lattice under coordinates.

instance TauCeti.discreteTopology_fullUnitLattice (K : Type u_1) [Field K] [NumberField K] : DiscreteTopology ↥(fullUnitLattice K)

The unit logarithmic lattice is discrete.

instance TauCeti.isZLattice_fullUnitLattice (K : Type u_1) [Field K] [NumberField K] : IsZLattice ℝ (fullUnitLattice K)

Dirichlet's unit lattice theorem, with all places retained. The logarithmic image of the units is a full integral lattice in the sum-zero hyperplane.

theorem TauCeti.unitLogEmbedding_mapRingEquiv (K : Type u_1) [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] (e : K ≃+* L) (u : (NumberField.RingOfIntegers K)ˣ) (w : NumberField.InfinitePlace L) : ↑((unitLogEmbedding L) (Additive.ofMul ((Units.map ↑(NumberField.RingOfIntegers.mapRingEquiv e)) u))) w = ↑((unitLogEmbedding K) (Additive.ofMul u)) (w.comap ↑e)

Equivariance of the logarithmic embedding. Transporting a unit along a field isomorphism transports its coordinate at w to the coordinate at the pulled-back place.

def TauCeti.unitLogRepresentation (K : Type u_1) [Field K] [NumberField K] (k : Type u_2) [Field k] [Algebra k K] : Representation ℝ Gal(K/k) ↥(singleParityCheckCode ℝ (NumberField.InfinitePlace K))

The permutation representation on the logarithmic hyperplane: an automorphism acts by pullback along its inverse on infinite places.

@[simp]

theorem TauCeti.unitLogRepresentation_apply (K : Type u_1) [Field K] [NumberField K] (k : Type u_2) [Field k] [Algebra k K] (σ : Gal(K/k)) (x : ↥(singleParityCheckCode ℝ (NumberField.InfinitePlace K))) (w : NumberField.InfinitePlace K) : ↑(((unitLogRepresentation K k) σ) x) w = ↑x (σ⁻¹ • w)

The Galois action on logarithmic vectors is the permutation of their coordinates.

@[simp]

theorem TauCeti.unitLogRepresentation_embedding (K : Type u_1) [Field K] [NumberField K] (k : Type u_2) [Field k] [Algebra k K] (σ : Gal(K/k)) (u : (NumberField.RingOfIntegers K)ˣ) : ((unitLogRepresentation K k) σ) ((unitLogEmbedding K) (Additive.ofMul u)) = (unitLogEmbedding K) (Additive.ofMul ((Units.map ↑(NumberField.RingOfIntegers.mapRingEquiv σ.toRingEquiv)) u))

The full logarithmic embedding intertwines the action on units and the permutation representation on infinite places.

theorem TauCeti.unitLogRepresentation_mem_fullUnitLattice (K : Type u_1) [Field K] [NumberField K] (k : Type u_2) [Field k] [Algebra k K] (σ : Gal(K/k)) {x : ↥(singleParityCheckCode ℝ (NumberField.InfinitePlace K))} (hx : x ∈ fullUnitLattice K) : ((unitLogRepresentation K k) σ) x ∈ fullUnitLattice K

The full unit lattice is Galois-stable, so it is an integral lattice in the permutation representation on the logarithmic hyperplane.

noncomputable def TauCeti.fullUnitLatticeRepresentation (K : Type u_1) [Field K] [NumberField K] (k : Type u_2) [Field k] [Algebra k K] : Representation ℤ Gal(K/k) ↥(fullUnitLattice K)

The integral Galois representation on the full unit logarithmic lattice, obtained by restricting the permutation representation on the logarithmic hyperplane.

@[simp]

theorem TauCeti.fullUnitLatticeRepresentation_apply (K : Type u_1) [Field K] [NumberField K] (k : Type u_2) [Field k] [Algebra k K] (σ : Gal(K/k)) (x : ↥(fullUnitLattice K)) : ↑(((fullUnitLatticeRepresentation K k) σ) x) = ((unitLogRepresentation K k) σ) ↑x

The integral action on the full unit lattice agrees with the ambient permutation action.