Elements that are norms at a place

For an extension L/K of number fields, an element x ∈ Kˣ is a local norm at a place of K when its image in the completion K_v is a norm from the local étale algebra K_v ⊗[K] L. Using the scalar extension, rather than one completion L_w above v, keeps every place of L above v: by TauCeti.mem_range_normUnits_adicCompletion_iff the local norms are the products of norms from all the completions L_w with w ∣ v. This file defines

• TauCeti.GlobalNumberFields.finiteLocalNormMap and TauCeti.GlobalNumberFields.infiniteLocalNormMap, the norm maps of these local étale algebras on units;
• TauCeti.GlobalNumberFields.IsFiniteLocalNorm, the local norm condition at a finite place;
• TauCeti.GlobalNumberFields.IsInfiniteLocalNorm, the local norm condition at an infinite place, on Mathlib's completion w.Completion;
• TauCeti.GlobalNumberFields.IsLocalNormEverywhere, the conjunction of both conditions at every finite and every infinite place.

Complex places are not dropped from IsLocalNormEverywhere; instead their condition is proved to be automatic (isInfiniteLocalNorm_of_isComplex), since every complex number is an [L : K]-th power.

Main results

• TauCeti.GlobalNumberFields.isFiniteLocalNorm_iff and TauCeti.GlobalNumberFields.isInfiniteLocalNorm_iff: the local norm conditions as products of norms from the completions of L above the place.

References

• J. S. Milne, Class Field Theory, v4.03, Chapter VII, §2.
• J. Neukirch, Algebraic Number Theory, Chapter VI, §2.

@[reducible, inline]

noncomputable abbrev TauCeti.GlobalNumberFields.infiniteLocalNormMap (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [_hKL : FiniteDimensional K L] (w : NumberField.InfinitePlace K) : (TensorProduct K w.Completion L)ˣ →* w.Completionˣ

The norm map of the local étale algebra K_w ⊗[K] L at the infinite place w, on units, landing in Mathlib's completion K_w. Using the scalar extension, rather than one completion of L above w, retains every place of L above w.

def TauCeti.GlobalNumberFields.IsInfiniteLocalNorm (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (w : NumberField.InfinitePlace K) (x : Kˣ) : Prop

x ∈ Kˣ is a local norm at the infinite place w for a finite extension L/K: its image in Mathlib's completion K_w is the norm of a unit of the local étale algebra K_w ⊗[K] L.

@[reducible, inline]

noncomputable abbrev TauCeti.GlobalNumberFields.finiteLocalNormMap (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [NumberField K] [_hKL : FiniteDimensional K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : (TensorProduct K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) L)ˣ →* (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ

The norm map of the local étale algebra K_v ⊗[K] L at the finite place v, on units. Using the scalar extension, rather than one completion of L above v, retains every place of L above v.

def TauCeti.GlobalNumberFields.IsFiniteLocalNorm (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [NumberField K] [FiniteDimensional K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : Kˣ) : Prop

x ∈ Kˣ is a local norm at the finite place v for a finite extension L/K: its image in K_v is the norm of a unit of the local étale algebra K_v ⊗[K] L, which accounts for every place of L above v.

def TauCeti.GlobalNumberFields.IsLocalNormEverywhere (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [NumberField K] [FiniteDimensional K L] (x : Kˣ) : Prop

x ∈ Kˣ is a local norm everywhere for a finite extension L/K: it is a local norm at every finite place and at every infinite place of K, complex places included.

theorem TauCeti.GlobalNumberFields.isInfiniteLocalNorm_def {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (w : NumberField.InfinitePlace K) (x : Kˣ) : IsInfiniteLocalNorm K L w x ↔ (Units.map ↑(algebraMap K w.Completion)) x ∈ (infiniteLocalNormMap K L w).range

The defining characterization of IsInfiniteLocalNorm: membership in the range of infiniteLocalNormMap.

theorem TauCeti.GlobalNumberFields.isFiniteLocalNorm_def {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [NumberField K] [FiniteDimensional K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : Kˣ) : IsFiniteLocalNorm K L v x ↔ (Units.map ↑(algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v))) x ∈ (finiteLocalNormMap K L v).range

The defining characterization of IsFiniteLocalNorm: membership in the range of finiteLocalNormMap.

theorem TauCeti.GlobalNumberFields.isLocalNormEverywhere_def {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [NumberField K] [FiniteDimensional K L] (x : Kˣ) : IsLocalNormEverywhere K L x ↔ (∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), IsFiniteLocalNorm K L v x) ∧ ∀ (w : NumberField.InfinitePlace K), IsInfiniteLocalNorm K L w x

The defining characterization of IsLocalNormEverywhere: a local norm at every finite and every infinite place.

Closure under the group operations of Kˣ

@[simp]

theorem TauCeti.GlobalNumberFields.isInfiniteLocalNorm_one {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (w : NumberField.InfinitePlace K) : IsInfiniteLocalNorm K L w 1

1 is a local norm at every infinite place.

theorem TauCeti.GlobalNumberFields.IsInfiniteLocalNorm.mul {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] {w : NumberField.InfinitePlace K} {x y : Kˣ} (hx : IsInfiniteLocalNorm K L w x) (hy : IsInfiniteLocalNorm K L w y) : IsInfiniteLocalNorm K L w (x * y)

Local norms at an infinite place are closed under multiplication.

@[simp]

theorem TauCeti.GlobalNumberFields.isInfiniteLocalNorm_inv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] {w : NumberField.InfinitePlace K} {x : Kˣ} : IsInfiniteLocalNorm K L w x⁻¹ ↔ IsInfiniteLocalNorm K L w x

x⁻¹ is a local norm at an infinite place exactly when x is.

@[simp]

theorem TauCeti.GlobalNumberFields.isFiniteLocalNorm_one {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [NumberField K] [FiniteDimensional K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : IsFiniteLocalNorm K L v 1

1 is a local norm at every finite place.

theorem TauCeti.GlobalNumberFields.IsFiniteLocalNorm.mul {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [NumberField K] [FiniteDimensional K L] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} {x y : Kˣ} (hx : IsFiniteLocalNorm K L v x) (hy : IsFiniteLocalNorm K L v y) : IsFiniteLocalNorm K L v (x * y)

Local norms at a finite place are closed under multiplication.

@[simp]

theorem TauCeti.GlobalNumberFields.isFiniteLocalNorm_inv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [NumberField K] [FiniteDimensional K L] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} {x : Kˣ} : IsFiniteLocalNorm K L v x⁻¹ ↔ IsFiniteLocalNorm K L v x

x⁻¹ is a local norm at a finite place exactly when x is.

@[simp]

theorem TauCeti.GlobalNumberFields.isLocalNormEverywhere_one {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [NumberField K] [FiniteDimensional K L] : IsLocalNormEverywhere K L 1

1 is a local norm everywhere.

theorem TauCeti.GlobalNumberFields.IsLocalNormEverywhere.mul {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [NumberField K] [FiniteDimensional K L] {x y : Kˣ} (hx : IsLocalNormEverywhere K L x) (hy : IsLocalNormEverywhere K L y) : IsLocalNormEverywhere K L (x * y)

Local norms everywhere are closed under multiplication.

@[simp]

theorem TauCeti.GlobalNumberFields.isLocalNormEverywhere_inv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [NumberField K] [FiniteDimensional K L] {x : Kˣ} : IsLocalNormEverywhere K L x⁻¹ ↔ IsLocalNormEverywhere K L x

x⁻¹ is a local norm everywhere exactly when x is.

theorem TauCeti.GlobalNumberFields.isInfiniteLocalNorm_of_isComplex {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] {w : NumberField.InfinitePlace K} (hw : w.IsComplex) (x : Kˣ) : IsInfiniteLocalNorm K L w x

The local norm condition at a complex place is automatic. It is kept in IsLocalNormEverywhere rather than silently omitted, and this theorem discharges it.

theorem TauCeti.GlobalNumberFields.isFiniteLocalNorm_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : Kˣ) : IsFiniteLocalNorm K L v x ↔ ∃ (u : (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }) → (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)ˣ), ∏ᶠ (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }), (Algebra.normUnits (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (u w) = (Units.map ↑(algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v))) x

x is a local norm at the finite place v exactly when its image in K_v is a product of norms from the completions of L at the places above v.

theorem TauCeti.GlobalNumberFields.isInfiniteLocalNorm_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] (w : NumberField.InfinitePlace K) (x : Kˣ) : IsInfiniteLocalNorm K L w x ↔ ∃ (u : (w' : { w' : NumberField.InfinitePlace L // w'.LiesOver w }) → (↑w').Completionˣ), ∏ᶠ (w' : { w' : NumberField.InfinitePlace L // w'.LiesOver w }), (Algebra.normUnits w.Completion) (u w') = (Units.map ↑(algebraMap K w.Completion)) x

x is a local norm at the infinite place w exactly when its image in K_w is a product of norms from the completions of L at the places above w.