Semilocal decomposition at infinite places

For an extension of number fields L/K and an infinite place v of K, scalar extension identifies v.Completion ⊗[K] L with the product of the completions at the places of L above v. The tensor product has the module topology over v.Completion, and the comparison is a continuous algebra equivalence. This is the local archimedean comparison used to assemble base change of infinite adele rings. Through it, the norm of L/K is the product of the local norms at the places above v (algebraMap_norm_eq_prod_norm_infiniteCompletion), which is the archimedean input to the norm map of adeles.

The map sends a ⊗ x to (a x)_w. Weak approximation makes its image dense, finite dimensionality makes that image closed, and the sum of local degrees proves injectivity. In particular, a complex place above a real place contributes dimension two, rather than one.

References

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

The completion algebra structures and local degrees are Mathlib's NumberField.LiesOver.completionMap and NumberField.InfinitePlace.inertiaDeg. The argument parallels TauCeti.semilocalEquiv, the finite-place decomposition.

noncomputable def TauCeti.GlobalNumberFields.infiniteSemilocalHom {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L] (v : NumberField.InfinitePlace K) : TensorProduct K v.Completion L →ₐ[v.Completion] (w : { w : NumberField.InfinitePlace L // w.LiesOver v }) → (↑w).Completion

The semilocal algebra map at an infinite place, with one component for each place above it.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.GlobalNumberFields.infiniteSemilocalHom_tmul {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : NumberField.InfinitePlace K} (a : v.Completion) (x : L) (w : { w : NumberField.InfinitePlace L // w.LiesOver v }) : (infiniteSemilocalHom L v) (a ⊗ₜ[K] x) w = (algebraMap v.Completion (↑w).Completion) a * (algebraMap L (↑w).Completion) x

The component formula determining the semilocal map.

theorem TauCeti.GlobalNumberFields.denseRange_algebraMap_pi_infinitePlaceLiesOver {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L] (v : NumberField.InfinitePlace K) [NumberField L] : DenseRange fun (x : L) (w : { w : NumberField.InfinitePlace L // w.LiesOver v }) => (algebraMap L (↑w).Completion) x

The field is dense in the product of its archimedean completions above a fixed place.

theorem TauCeti.GlobalNumberFields.sum_finrank_infiniteCompletion_eq_finrank {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L] (v : NumberField.InfinitePlace K) [NumberField K] [NumberField L] : ∑ w : { w : NumberField.InfinitePlace L // w.LiesOver v }, Module.finrank v.Completion (↑w).Completion = Module.finrank K L

The sum of the archimedean completed degrees above v is the global degree.

theorem TauCeti.GlobalNumberFields.infiniteSemilocalHom_surjective {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L] (v : NumberField.InfinitePlace K) [NumberField L] : Function.Surjective ⇑(infiniteSemilocalHom L v)

Every tuple of archimedean local elements above v comes from the scalar extension.

theorem TauCeti.GlobalNumberFields.infiniteSemilocalHom_injective {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L] (v : NumberField.InfinitePlace K) [NumberField K] [NumberField L] : Function.Injective ⇑(infiniteSemilocalHom L v)

The semilocal map is injective: the local degrees account for the whole scalar extension.

noncomputable def TauCeti.GlobalNumberFields.infiniteSemilocalEquiv {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L] (v : NumberField.InfinitePlace K) [NumberField K] [NumberField L] : TensorProduct K v.Completion L ≃ₐ[v.Completion] (w : { w : NumberField.InfinitePlace L // w.LiesOver v }) → (↑w).Completion

Scalar extension to an archimedean completion decomposes into the completions above it.

Equations

• TauCeti.GlobalNumberFields.infiniteSemilocalEquiv L v = AlgEquiv.ofBijective (TauCeti.GlobalNumberFields.infiniteSemilocalHom L v) ⋯

@[simp]

theorem TauCeti.GlobalNumberFields.infiniteSemilocalEquiv_tmul {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : NumberField.InfinitePlace K} [NumberField K] [NumberField L] (a : v.Completion) (x : L) (w : { w : NumberField.InfinitePlace L // w.LiesOver v }) : (infiniteSemilocalEquiv L v) (a ⊗ₜ[K] x) w = (algebraMap v.Completion (↑w).Completion) a * (algebraMap L (↑w).Completion) x

The semilocal equivalence has the prescribed formula on pure tensors.

theorem TauCeti.GlobalNumberFields.infiniteSemilocalEquiv_symm_algebraMap {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L] (v : NumberField.InfinitePlace K) [NumberField K] [NumberField L] (x : L) : ((infiniteSemilocalEquiv L v).symm fun (w : { w : NumberField.InfinitePlace L // w.LiesOver v }) => (algebraMap L (↑w).Completion) x) = 1 ⊗ₜ[K] x

The inverse algebraic comparison sends a diagonal field element to 1 ⊗ x.

theorem TauCeti.GlobalNumberFields.algebraMap_norm_eq_prod_norm_infiniteCompletion {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L] (v : NumberField.InfinitePlace K) [NumberField K] [NumberField L] (x : L) : (algebraMap K v.Completion) ((Algebra.norm K) x) = ∏ w : { w : NumberField.InfinitePlace L // w.LiesOver v }, (Algebra.norm v.Completion) ((algebraMap L (↑w).Completion) x)

The norm is the product of the archimedean local norms. For x ∈ L and an infinite place v of K, the image of N_{L/K}(x) in K_v is the product over the places w ∣ v of the norms N_{L_w/K_v}(x). This is the archimedean counterpart of TauCeti.algebraMap_norm_eq_prod_norm.

noncomputable def TauCeti.GlobalNumberFields.infiniteSemilocalContinuousEquiv {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L] (v : NumberField.InfinitePlace K) [NumberField K] [NumberField L] [TopologicalSpace (TensorProduct K v.Completion L)] [IsModuleTopology v.Completion (TensorProduct K v.Completion L)] : TensorProduct K v.Completion L ≃A[v.Completion] (w : { w : NumberField.InfinitePlace L // w.LiesOver v }) → (↑w).Completion

The archimedean semilocal comparison is topological when the tensor product carries the module topology over the base completion. Both it and its inverse are continuous.

Equations

• TauCeti.GlobalNumberFields.infiniteSemilocalContinuousEquiv L v = { toAlgEquiv := TauCeti.GlobalNumberFields.infiniteSemilocalEquiv L v, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem TauCeti.GlobalNumberFields.infiniteSemilocalContinuousEquiv_toAlgEquiv {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L] (v : NumberField.InfinitePlace K) [NumberField K] [NumberField L] [TopologicalSpace (TensorProduct K v.Completion L)] [IsModuleTopology v.Completion (TensorProduct K v.Completion L)] : (infiniteSemilocalContinuousEquiv L v).toAlgEquiv = infiniteSemilocalEquiv L v

Forgetting continuity recovers the algebraic semilocal comparison.

@[simp]

theorem TauCeti.GlobalNumberFields.infiniteSemilocalContinuousEquiv_tmul {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : NumberField.InfinitePlace K} [NumberField K] [NumberField L] [TopologicalSpace (TensorProduct K v.Completion L)] [IsModuleTopology v.Completion (TensorProduct K v.Completion L)] (a : v.Completion) (x : L) (w : { w : NumberField.InfinitePlace L // w.LiesOver v }) : (infiniteSemilocalContinuousEquiv L v) (a ⊗ₜ[K] x) w = (algebraMap v.Completion (↑w).Completion) a * (algebraMap L (↑w).Completion) x

The continuous semilocal comparison retains the component formula on pure tensors.

theorem TauCeti.GlobalNumberFields.infiniteSemilocalContinuousEquiv_symm_algebraMap {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : NumberField.InfinitePlace K} [NumberField K] [NumberField L] [TopologicalSpace (TensorProduct K v.Completion L)] [IsModuleTopology v.Completion (TensorProduct K v.Completion L)] (x : L) : ((infiniteSemilocalContinuousEquiv L v).symm fun (w : { w : NumberField.InfinitePlace L // w.LiesOver v }) => (algebraMap L (↑w).Completion) x) = 1 ⊗ₜ[K] x

The inverse comparison sends a diagonal field element to 1 ⊗ x.