Norms on completed multiplicative modules

For a finite extension L/K, the field norm induces a ℤ_p-linear map A(L) → A(K) on the inverse limits of the p-power class groups. Its value on the canonical class of a unit is the canonical class of its norm.

The completed norm is invariant under every K-automorphism of L, including on elements of A(L) that do not come from individual units. It therefore factors through Mathlib's coinvariants of the representation padicCompletionUnitsRepresentation p L K. This is the norm map whose cokernel enters the reciprocity description of a finite Galois layer.

The construction uses the algebraic inverse-limit carrier; it requires neither a topology on the fields nor a Galois hypothesis.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., VII §4, especially (7.4.4).

noncomputable def TauCeti.padicCompletionPowerClassNorm (p : ℕ) (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [_hfin : FiniteDimensional K L] (m : ℕ) : Lˣ ⧸ (powMonoidHom (p ^ m)).range →* Kˣ ⧸ (powMonoidHom (p ^ m)).range

The field norm on p^m-power classes for a finite extension L/K. Finiteness excludes the constant-one norm on infinite extensions.

@[simp]

theorem TauCeti.padicCompletionPowerClassNorm_mk (p : ℕ) (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (m : ℕ) (x : Lˣ) : (padicCompletionPowerClassNorm p K L m) ↑x = ↑((Algebra.normUnits K) x)

The norm on power classes sends the class of a unit to the class of its norm.

theorem TauCeti.padicCompletionPowerClassNorm_transition (p : ℕ) (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (m : ℕ) (x : Lˣ ⧸ (powMonoidHom (p ^ (m + 1))).range) : (padicCompletionTransition p K m) ((padicCompletionPowerClassNorm p K L (m + 1)) x) = (padicCompletionPowerClassNorm p K L m) ((padicCompletionTransition p L m) x)

The norm on power classes commutes with the completion's transition maps.

noncomputable def TauCeti.padicCompletionUnitsNorm (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] : Additive ↥(padicCompletionUnits p L) →ₗ[ℤ_[p]] Additive ↥(padicCompletionUnits p K)

The ℤ_p-linear norm A(L) → A(K) induced by the field norm at every finite level. Finiteness excludes the constant-one value of Mathlib's total norm on infinite extensions.

@[simp]

theorem TauCeti.padicCompletionUnitsNorm_apply (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (x : Additive ↥(padicCompletionUnits p L)) (m : ℕ) : ↑(Additive.toMul ((padicCompletionUnitsNorm p K L) x)) m = (padicCompletionPowerClassNorm p K L m) (↑(Additive.toMul x) m)

The completed norm is computed by the norm on each power-class coordinate.

@[simp]

theorem TauCeti.padicCompletionUnitsNorm_of (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (x : Lˣ) : (padicCompletionUnitsNorm p K L) (Additive.ofMul ((padicCompletionUnitsOf p L) x)) = Additive.ofMul ((padicCompletionUnitsOf p K) ((Algebra.normUnits K) x))

The norm of the canonical class of a unit is the canonical class of its norm.

@[simp]

theorem TauCeti.padicCompletionUnitsOf_norm_algEquiv (p : ℕ) (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] (σ : Gal(L/K)) (x : Lˣ) : (padicCompletionUnitsOf p K) ((Algebra.normUnits K) ((Units.map ↑↑σ) x)) = (padicCompletionUnitsOf p K) ((Algebra.normUnits K) x)

The canonical class of a norm is unchanged on replacing a unit by a Galois conjugate.

@[simp]

theorem TauCeti.padicCompletionUnitsNorm_aut (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (σ : Gal(L/K)) (x : ↥(padicCompletionUnits p L)) : (padicCompletionUnitsNorm p K L) (Additive.ofMul (((padicCompletionUnitsAut p L K) σ) x)) = (padicCompletionUnitsNorm p K L) (Additive.ofMul x)

The completed norm is invariant under the full K-automorphism action on A(L).

@[simp]

theorem TauCeti.padicCompletionUnitsNorm_smul (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (r : MonoidAlgebra ℤ_[p] Gal(L/K)) (x : Additive ↥(padicCompletionUnits p L)) : (padicCompletionUnitsNorm p K L) (r • x) = (MonoidAlgebra.augmentation ℤ_[p] Gal(L/K)) r • (padicCompletionUnitsNorm p K L) x

The group algebra acts through its augmentation after applying the completed norm. In particular the augmentation ideal annihilates the norm.

noncomputable def TauCeti.padicCompletionUnitsCoinvariantsNorm (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] : (padicCompletionUnitsRepresentation p L K).Coinvariants →ₗ[ℤ_[p]] Additive ↥(padicCompletionUnits p K)

The completed norm descends to the coinvariants of the Galois representation on A(L).

@[simp]

theorem TauCeti.padicCompletionUnitsCoinvariantsNorm_mk (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (x : Additive ↥(padicCompletionUnits p L)) : (padicCompletionUnitsCoinvariantsNorm p K L) ((Representation.Coinvariants.mk (padicCompletionUnitsRepresentation p L K)) x) = (padicCompletionUnitsNorm p K L) x

The norm on coinvariants recovers the completed norm on a representative.