This file provides the common algebraic norm map on unit groups. It is independent of any valuation or local-field structure, so valued-field and discrete-valuation APIs can share the same definition.
The algebra norm, restricted to unit groups.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]def normUnits : Lˣ →* KˣThe underlying field element of a unit norm is the algebra norm.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem normUnits_apply_coe (x : Lˣ) :
((normUnits K L x : Kˣ) : K) = Algebra.norm K (x : L)Field norms on unit groups are transitive in a tower.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory
noncomputable section
universe u v w
variable (K : Type u) (L : Type v)
variable [Field K] [Field L] [Algebra K L]theorem normUnits_tower
(K : Type u) (M : Type v) (L : Type w)
[Field K] [Field M] [Field L]
[Algebra K M] [Algebra M L] [Algebra K L]
[IsScalarTower K M L] [Module.Free M L] (x : Lˣ) :
normUnits K M (normUnits M L x) = normUnits K L x