Norm and trace in the semilocal decomposition

The semilocal decomposition transports the norm and trace of a number-field extension to the finite family of completed extensions above a finite place. The generic determinant, trace, and finite-product calculations live in TauCeti.RingTheory.NormTrace.Pi. The scalar-extension identities are from TauCeti.RingTheory.NormTrace.BaseChange.

Main results

• TauCeti.norm_eq_prod_norm_semilocalEquiv: the norm in the local étale algebra.
• TauCeti.algebraMap_norm_eq_prod_norm: the norm of x ∈ L is the product of its local norms.
• TauCeti.trace_eq_sum_trace_semilocalEquiv: the trace of K_v ⊗[K] L over K_v is the sum of the traces of its semilocal components.
• TauCeti.algebraMap_trace_eq_sum_trace: the trace of x ∈ L is the sum of its local traces.
• TauCeti.trace_semilocalEquiv_symm_single_mul: the trace pairing of one semilocal component with a global element is its local trace pairing.
• TauCeti.trace_integralSemilocalToField_tmul_mul: the trace pairing of an integral pure tensor with a global element commutes with extension to the completed field.

References

• J. Neukirch, Algebraic Number Theory, Chapter II, (8.4).

theorem TauCeti.trace_integralSemilocalToField_tmul_mul {K : Type u} [Field K] [NumberField K] (L : Type v) [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (a : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (x : NumberField.RingOfIntegers L) (d : L) : (Algebra.trace (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (TensorProduct K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) L)) ((integralSemilocalToField L v) (a ⊗ₜ[NumberField.RingOfIntegers K] x) * 1 ⊗ₜ[K] d) = ↑a * (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ((Algebra.trace K L) (↑x * d))

The trace of a pure integral tensor paired with a global element is a scalar extension of the global trace pairing.

theorem TauCeti.norm_eq_prod_norm_semilocalEquiv {K : Type u} [Field K] [NumberField K] (L : Type v) [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (ξ : TensorProduct K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) L) : (Algebra.norm (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ξ = ∏ w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }, (Algebra.norm (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ((semilocalEquiv L v) ξ w)

The norm of the local étale algebra is the product of the norms of its semilocal components.

theorem TauCeti.algebraMap_norm_eq_prod_norm {K : Type u} [Field K] [NumberField K] (L : Type v) [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : L) : (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ((Algebra.norm K) x) = ∏ w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }, (Algebra.norm (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ((algebraMap L (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) x)

The norm of a number-field element is the product of its norms in the completions above v.

@[simp]

theorem TauCeti.trace_eq_sum_trace_semilocalEquiv {K : Type u} [Field K] [NumberField K] (L : Type v) [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (ξ : TensorProduct K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) L) : (Algebra.trace (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (TensorProduct K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) L)) ξ = ∑ w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }, (Algebra.trace (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) ((semilocalEquiv L v) ξ w)

The trace of the semilocal algebra K_v ⊗[K] L over K_v is the sum of the traces of the components of the semilocal decomposition.

theorem TauCeti.trace_semilocalEquiv_symm_single_mul {K : Type u} [Field K] [NumberField K] (L : Type v) [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] (z : IsDedekindDomain.HeightOneSpectrum.adicCompletion L w) (x : L) : (Algebra.trace (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (TensorProduct K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) L)) ((semilocalEquiv L v).symm (Pi.single ⟨w, ⋯⟩ z) * 1 ⊗ₜ[K] x) = (Algebra.trace (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)) (z * (algebraMap L (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)) x)

An element of L_w, placed in the w-component of K_v ⊗[K] L, has the same trace pairing with a global element as in L_w.

theorem TauCeti.algebraMap_trace_eq_sum_trace {K : Type u} [Field K] [NumberField K] (L : Type v) [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : L) : (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ((Algebra.trace K L) x) = ∑ w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }, (Algebra.trace (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) ((algebraMap L (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) x)

The trace of a number-field element is the sum of its traces in the completions above v.