Finite-place completion tensor product maps

DefinitionComponent at a place of the completion tensor product map#✓fully proved

Let \(L/K\) be an extension of number fields, let \(v\) be a finite place of \(K\), given as a height-one prime of the ring of integers \(\mathcal{O}_K\), let \(K_v\) be the completion of \(K\) at \(v\), and let \(w\) be a finite place of \(L\) lying over \(v\), with completion \(L_w\). Let \(\iota_w : K_v \to L_w\) be the continuous ring homomorphism extending \(K \to L\). This is the \(K_v\)-algebra homomorphism \(K_v \otimes_K L \to L_w\) sending \(x \otimes y\) to \(\iota_w(x)\, y\), where \(y \in L\) is viewed in \(L_w\).

noncomputable def completionTensorProductComponent (w : v.placesOver L) :
    v.adicCompletion K ⊗[K] L →ₐ[v.adicCompletion K] w.val.adicCompletion L :=
  Algebra.TensorProduct.lift (Algebra.algHom _ _ _) (Algebra.algHom K L _)
    (fun _ _ => mul_comm _ _)

Uses 1 · Used by 1

Statement usesFinite places lying over a finite place

Used byThe completion tensor product map

DefinitionThe completion tensor product map#✓fully proved

Let \(L/K\) be an extension of number fields, let \(v\) be a finite place of \(K\), given as a height-one prime of the ring of integers \(\mathcal{O}_K\), and let \(K_v\) be the completion of \(K\) at \(v\). For each finite place \(w\) of \(L\) lying over \(v\), let \(L_w\) be the completion of \(L\) at \(w\) and \(\iota_w : K_v \to L_w\) the continuous ring homomorphism extending \(K \to L\). This is the \(K_v\)-algebra homomorphism \(K_v \otimes_K L \to \prod_{w \mid v} L_w\) sending \(x \otimes y\) to \((\iota_w(x)\, y)_w\), where \(y \in L\) is viewed in each \(L_w\) and the product runs over the finite places of \(L\) lying over \(v\).

noncomputable def completionTensorProductMap :
    v.adicCompletion K ⊗[K] L →ₐ[v.adicCompletion K]
      ((w : v.placesOver L) → w.val.adicCompletion L) :=
  AlgHom.pi (fun w => completionTensorProductComponent v w)

Uses 2 · Used by 3

Statement usesComponent at a place of the completion tensor product map · Finite places lying over a finite place

Used byBase change to a finite completion as a product of completions · The canonical map to the product of completions is bijective · The canonical map to the product of completions is injective

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.