Norm equations in the local étale algebras

For a number-field extension L/K, the local norm is the norm of K_v ⊗[K] L. The semilocal comparisons identify its image with products of norms from all completions above the place, including split algebras and real and complex places.

Main results

• TauCeti.mem_range_normUnits_adicCompletion_iff and TauCeti.mem_range_normUnits_completion_iff: the local norm range as products of norms.
• TauCeti.exists_unit_preimages_of_isUnramifiedAt: a unit has integral unit preimages if one completion above the place is unramified.
• TauCeti.mem_range_normUnits_adicCompletion_of_finrank_eq_one: every element is a local norm if one completion above the place has degree one, and TauCeti.mem_range_normUnits_completion_of_finrank_eq_one is its infinite counterpart.
• TauCeti.pow_mem_range_normUnits_completion: at an infinite place every n-th power is a local norm once n kills Gal(L/K).
• TauCeti.mem_range_normUnits_completion_of_isComplex: at a complex place every unit is a local norm, for every finite extension L/K.

References

• J. Neukirch, Algebraic Number Theory, Chapter II, (8.4), and Chapter VI, §2.

The local decompositions are TauCeti.semilocalEquiv and TauCeti.GlobalNumberFields.infiniteSemilocalEquiv; unit-norm surjectivity is TauCeti.map_normUnits_unitFiltration.

theorem TauCeti.mem_range_normUnits_adicCompletion_iff (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (a : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ) : a ∈ (Algebra.normUnits (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).range ↔ ∃ (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) = a

A unit is a finite local norm exactly when it is a product of norms from the completions above the place. This includes split local algebras.

theorem TauCeti.mem_range_normUnits_completion_iff (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : NumberField.InfinitePlace K) (a : v.Completionˣ) : a ∈ (Algebra.normUnits v.Completion).range ↔ ∃ (u : (w : { w : NumberField.InfinitePlace L // w.LiesOver v }) → (↑w).Completionˣ), ∏ᶠ (w : { w : NumberField.InfinitePlace L // w.LiesOver v }), (Algebra.normUnits v.Completion) (u w) = a

A unit is an infinite local norm exactly when it is a product of norms from the completions above the place. Real and complex places are both retained.

theorem TauCeti.exists_unit_preimages_of_isUnramifiedAt (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (a : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ) (ha : Valued.v ↑a = 1) (hU : ∃ (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }), Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) (↑w).asIdeal) : ∃ (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) = a ∧ ∀ (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }), Valued.v ↑(u w) = 1

A unit of the base completion is a product of norms of integral units of the completions above it whenever at least one of those extensions is unramified.

theorem TauCeti.mem_range_normUnits_adicCompletion_of_finrank_eq_one (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (hv : ∃ (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }), Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w) = 1) (a : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ) : a ∈ (Algebra.normUnits (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).range

Local norms at a finite place of degree one. If some completion L_w of L above the finite place v has degree one over K_v, then every element of K_vˣ is a norm from the local étale algebra K_v ⊗[K] L.

theorem TauCeti.mem_range_normUnits_completion_of_finrank_eq_one (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : NumberField.InfinitePlace K) (hv : ∃ (w : { w : NumberField.InfinitePlace L // w.LiesOver v }), Module.finrank v.Completion (↑w).Completion = 1) (a : v.Completionˣ) : a ∈ (Algebra.normUnits v.Completion).range

Local norms at an infinite place of degree one. If some completion L_w of L above the infinite place v has degree one over K_v, then every element of K_vˣ is a norm from the local étale algebra K_v ⊗[K] L.

theorem TauCeti.pow_mem_range_normUnits_completion (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] {n : ℕ} (hn : Monoid.exponent Gal(L/K) ∣ n) (v : NumberField.InfinitePlace K) (a : v.Completionˣ) : a ^ n ∈ (Algebra.normUnits v.Completion).range

n-th powers are local norms at an infinite place. If n kills Gal(L/K), then every n-th power of K_vˣ is a norm from the local étale algebra K_v ⊗[K] L: the local degree [L_w : K_v] is the order of the decomposition group of w, a cyclic group of order 1 or 2, so it divides n, and a ^ [L_w : K_v] is the norm of a.

Complex places

theorem TauCeti.mem_range_normUnits_completion_of_isComplex {K : Type u_1} [Field K] (L : Type u_2) [Field L] [Algebra K L] [FiniteDimensional K L] {w : NumberField.InfinitePlace K} (hw : w.IsComplex) (a : w.Completionˣ) : a ∈ (Algebra.normUnits w.Completion).range

Every unit is a local norm at a complex place. At a complex place w of K every unit of K_w ≅ ℂ is the norm of a unit of the local étale algebra K_w ⊗[K] L: it is an [L : K]-th power, and the [L : K]-th power of b ∈ K_wˣ is the norm of b ⊗ 1.