The norm on unit groups

The norm Algebra.norm R : S →* R of an R-algebra is multiplicative, so it sends units to units. TauCeti.Algebra.normUnits packages that as a homomorphism Sˣ →* Rˣ. This is the form a statement about the norm of an invertible element wants: the value is a unit by construction, so no choice of proof that it is nonzero has to be carried alongside it.

No finiteness hypothesis is needed here, because Algebra.norm itself has none: it is the determinant of multiplication, which is 1 when S is not module-finite over R (Algebra.norm_eq_one_of_not_module_finite). A consumer that cares about the value — for instance the non-split torus of GL₂ in TauCeti/LinearAlgebra/Matrix/GeneralLinearGroup/NonSplitTorus.lean — supplies its own finiteness where the value is computed.

Main definitions

• TauCeti.Algebra.normUnits: the algebra norm read as a homomorphism Sˣ →* Rˣ.
• TauCeti.normGroup: the image of the norm on units in a finite field extension.

noncomputable def TauCeti.Algebra.normUnits (R : Type u_1) [CommRing R] {S : Type u_2} [Ring S] [Algebra R S] : Sˣ →* Rˣ

The norm as a homomorphism of unit groups. The norm of a unit is a unit, because the norm is multiplicative; this is Algebra.norm R read as a map Sˣ →* Rˣ.

Equations

• TauCeti.Algebra.normUnits R = Units.map (Algebra.norm R)

@[simp]

theorem TauCeti.Algebra.coe_normUnits (R : Type u_1) [CommRing R] {S : Type u_2} [Ring S] [Algebra R S] (x : Sˣ) : ↑((normUnits R) x) = (Algebra.norm R) ↑x

The value underlying TauCeti.Algebra.normUnits is the ordinary norm.

noncomputable def TauCeti.normGroup (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra K L] [_hfin : Module.Finite K L] : Subgroup Kˣ

The norm group N_{L/K}(Lˣ) of a finite field extension L/K: the image in Kˣ of the field norm on units, Algebra.normUnits K : Lˣ →* Kˣ. Finiteness is required because Algebra.norm K is identically 1 on an infinite extension.

Equations

• TauCeti.normGroup K L = (TauCeti.Algebra.normUnits K).range

@[simp]

theorem TauCeti.mem_normGroup_iff {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] [Module.Finite K L] {x : Kˣ} : x ∈ normGroup K L ↔ ∃ (y : Lˣ), (Algebra.norm K) ↑y = ↑x

An element of Kˣ lies in the norm group exactly when it is the norm of a unit of L.