Ordinary units as S-units with no allowed finite denominators

For an extension of number fields L/K, the S-units with S = ∅ are the units of 𝓞 L. The identification respects the action of Aut(L/K), so it is an isomorphism of integral representations, rather than just an isomorphism of the underlying groups. In particular, their Herbrand quotients agree. This identifies the ordinary-unit term in the valuation sequence used to calculate the Herbrand quotient of S-units.

The underlying group identification is Set.unitEmptyEquivUnits; the action on integer units is Mathlib's Units.mulDistribMulActionRight applied to the action on the ring of integers.

Reference

• J. S. Milne, Class Field Theory, Chapter VII, §3 (the S-unit valuation sequence).

noncomputable def TauCeti.ClassFieldTheory.sUnitsEmptyIsoUnits {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : sUnitsRep L ∅ ≅ Rep.ofMulDistribMulAction Gal(L/K) (NumberField.RingOfIntegers L)ˣ

The S-units with no allowed finite denominators and the units of the ring of integers are canonically isomorphic as integral representations of Aut(L/K).

@[simp]

theorem TauCeti.ClassFieldTheory.algebraMap_sUnitsEmptyIsoUnits_hom_apply {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (u : ↑(sUnitsRep L ∅)) : (algebraMap (NumberField.RingOfIntegers L) L) ↑(Additive.toMul ((Rep.Hom.hom sUnitsEmptyIsoUnits.hom) u)) = ↑↑(Additive.toMul u)

The forward identification preserves the underlying element of the number field.

@[simp]

theorem TauCeti.ClassFieldTheory.coe_sUnitsEmptyIsoUnits_inv_apply {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (u : ↑(Rep.ofMulDistribMulAction Gal(L/K) (NumberField.RingOfIntegers L)ˣ)) : ↑(Additive.toMul ((Rep.Hom.hom sUnitsEmptyIsoUnits.inv) u)) = (Units.map ↑(algebraMap (NumberField.RingOfIntegers L) L)) (Additive.toMul u)

The inverse identification preserves the underlying element of the number field.

theorem TauCeti.ClassFieldTheory.herbrandQuotient_sUnitsRep_empty {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : TateCohomology.herbrandQuotient (sUnitsRep L ∅) = TateCohomology.herbrandQuotient (Rep.ofMulDistribMulAction Gal(L/K) (NumberField.RingOfIntegers L)ˣ)

The empty-set S-unit term in a Herbrand-quotient computation can be replaced by the ordinary units with their Galois action.