The finite-place completion tensor product

TheoremLocal degrees sum to the global degree#✓fully proved

Let \(L/K\) be an extension of number fields, \(v\) a finite place of \(K\) and \(K_v\) 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\), a \(K_v\)-algebra via the canonical map \(K_v \to L_w\). Then \(\sum_{w \mid v} [L_w : K_v] = [L : K]\).

theorem sum_finrank_adicCompletion_placesOver [Fintype (v.placesOver L)] :
    ∑ w : v.placesOver L,
      Module.finrank (v.adicCompletion K) (w.val.adicCompletion L) =
      Module.finrank K L
Sources
  • ATLAS N236, Theorem 11.23, parts (4) and (5) combined; used in N265.
Uses 3 · Used by 1
Statement usesFinite places lying over a finite place
Proof usesThe local degree is the product of ramification index and inertia degree · Places over a finite place correspond to primes over it
Used byDimension count for the base change to a finite completion

TheoremDimension count for the base change to a finite completion#✓fully proved

Let \(L/K\) be an extension of number fields, \(v\) a finite place of \(K\) and \(K_v\) 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\), a \(K_v\)-algebra via the canonical map \(K_v \to L_w\). Then \(K_v \otimes_K L\) and \(\prod_{w \mid v} L_w\) have the same dimension as \(K_v\)-vector spaces.

theorem finrank_completionTensorProduct_eq_pi :
    Module.finrank (v.adicCompletion K) (v.adicCompletion K ⊗[K] L) =
      Module.finrank (v.adicCompletion K)
        ((w : v.placesOver L) → w.val.adicCompletion L)
Uses 3 · Used by 1
Statement usesFinite places lying over a finite place
Proof usesPlaces over a finite place correspond to primes over it · Local degrees sum to the global degree
Used byThe canonical map to the product of completions is injective

TheoremThe canonical map to the product of completions is injective#✓fully proved

Let \(L/K\) be an extension of number fields, \(v\) a finite place of \(K\) and \(K_v\) 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\), a \(K_v\)-algebra via the canonical map \(K_v \to L_w\). The \(K_v\)-algebra map \(K_v \otimes_K L \to \prod_{w \mid v} L_w\) sending \(x \otimes y\) to \((x y)_w\), where \(x \in K_v\) and \(y \in L\) are mapped into each \(L_w\), is injective.

theorem completionTensorProductMap_injective :
    Function.Injective (completionTensorProductMap (K := K) (L := L) v)
Uses 4 · Used by 1
Statement usesThe completion tensor product map · Finite places lying over a finite place
Proof usesDimension count for the base change to a finite completion · Places over a finite place correspond to primes over it
Used byThe canonical map to the product of completions is bijective

TheoremThe canonical map to the product of completions is bijective#✓fully proved

Let \(L/K\) be an extension of number fields, \(v\) a finite place of \(K\) and \(K_v\) 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\), a \(K_v\)-algebra via the canonical map \(K_v \to L_w\). The \(K_v\)-algebra map \(K_v \otimes_K L \to \prod_{w \mid v} L_w\) sending \(x \otimes y\) to \((x y)_w\), where \(x \in K_v\) and \(y \in L\) are mapped into each \(L_w\), is bijective.

theorem completionTensorProductMap_bijective :
    Function.Bijective (completionTensorProductMap (K := K) (L := L) v)
Uses 4 · Used by 1
Statement usesThe completion tensor product map · Finite places lying over a finite place
Proof usesThe canonical map to the product of completions is injective · Places over a finite place correspond to primes over it
Used byBase change to a finite completion as a product of completions

DefinitionBase change to a finite completion as a product of completions#✓fully proved

Let \(L/K\) be an extension of number fields, \(v\) a finite place of \(K\) and \(K_v\) 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\), a \(K_v\)-algebra via the canonical map \(K_v \to L_w\). This is the isomorphism of \(K_v\)-algebras \(K_v \otimes_K L \cong \prod_{w \mid v} L_w\) sending \(x \otimes y\) to \((x y)_w\), where \(x \in K_v\) and \(y \in L\) are mapped into each \(L_w\).

noncomputable def completionTensorProductAlgEquiv :
    v.adicCompletion K ⊗[K] L ≃ₐ[v.adicCompletion K]
      ((w : v.placesOver L) → w.val.adicCompletion L) :=
  AlgEquiv.ofBijective (completionTensorProductMap (K := K) (L := L) v)
    (completionTensorProductMap_bijective (K := K) (L := L) v)
Sources
  • ATLAS N236, Theorem 11.23(5), with the tensor factors swapped; used later in N265.
Uses 3 · Used by 2
Statement usesThe completion tensor product map · The canonical map to the product of completions is bijective · Finite places lying over a finite place
Used byTensor product decomposition at a finite place · Coordinate law for the tensor product decomposition

DefinitionTensor product decomposition at a finite place#✓fully proved

Let \(L/K\) be an extension of number fields, \(v\) a finite place of \(K\) and \(K_v\) 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\), a \(K_v\)-algebra via the canonical map \(K_v \to L_w\), and make \(L \otimes_K K_v\) a \(K_v\)-algebra through its second factor. This is the isomorphism of \(K_v\)-algebras \(L \otimes_K K_v \cong \prod_{w \mid v} L_w\) sending \(y \otimes x\) to \((y x)_w\), where \(y \in L\) and \(x \in K_v\) are mapped into each \(L_w\).

noncomputable def completionTensorProductRightAlgEquiv :
    L ⊗[K] v.adicCompletion K ≃ₐ[v.adicCompletion K]
      ((w : v.placesOver L) → w.val.adicCompletion L) :=
  (Algebra.TensorProduct.commRight K (v.adicCompletion K) L).symm.trans
    (completionTensorProductAlgEquiv (K := K) (L := L) v)
Sources
  • ATLAS N265, Theorem 13.5, the finite-place \(K_v\)-algebra form for number fields.
Uses 2 · Used by 4
Statement usesBase change to a finite completion as a product of completions · Finite places lying over a finite place
Used byGlobal norm as a product of local norms · Global trace as a sum of local traces · Coordinate law for the tensor product decomposition · Tensor product decomposition at a finite place over the base field

TheoremCoordinate law for the tensor product decomposition#✓fully proved

Let \(L/K\) be an extension of number fields, \(v\) a finite place of \(K\) and \(K_v\) 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\), a \(K_v\)-algebra via the canonical map \(K_v \to L_w\), and make \(L \otimes_K K_v\) a \(K_v\)-algebra through its second factor. Consider the isomorphism of \(K_v\)-algebras \(L \otimes_K K_v \cong \prod_{w \mid v} L_w\) sending \(a \otimes b\) to \((a b)_w\), where \(a \in L\) and \(b \in K_v\) are mapped into each \(L_w\). For every \(y \in L\) and every finite place \(w\) of \(L\) lying over \(v\), the \(w\)-coordinate of the image of \(y \otimes 1\) is the image of \(y\) in \(L_w\).

@[simp]
theorem completionTensorProductRightAlgEquiv_tmul_one (y : L)
    (w : v.placesOver L) :
    completionTensorProductRightAlgEquiv (K := K) (L := L) v
      (y ⊗ₜ[K] (1 : v.adicCompletion K)) w =
      algebraMap L (w.val.adicCompletion L) y
Sources
  • ATLAS N265, Theorem 13.5, the coordinate law for pure tensors.
Uses 3 · Used by 2
Statement usesTensor product decomposition at a finite place · Finite places lying over a finite place
Proof usesBase change to a finite completion as a product of completions
Used byGlobal norm as a product of local norms · Global trace as a sum of local traces

TheoremTensor product decomposition at a finite place over the base field#✓fully proved

Let \(L/K\) be an extension of number fields, \(v\) a finite place of \(K\) and \(K_v\) 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\). There exists an isomorphism of \(K\)-algebras \(L \otimes_K K_v \cong \prod_{w \mid v} L_w\).

It is obtained by restricting scalars from \(K_v\) to \(K\) in the isomorphism of \(K_v\)-algebras \(L \otimes_K K_v \cong \prod_{w \mid v} L_w\) sending \(y \otimes x\) to \((y x)_w\), where \(y \in L\) and \(x \in K_v\) are mapped into each \(L_w\), \(L_w\) is a \(K_v\)-algebra via the canonical map \(K_v \to L_w\), and \(L \otimes_K K_v\) is a \(K_v\)-algebra through its second factor.

theorem completionTensorProductRightAlgEquiv_K :
    Nonempty (L ⊗[K] v.adicCompletion K ≃ₐ[K]
      ((w : v.placesOver L) → w.val.adicCompletion L))
Uses 2
Statement usesFinite places lying over a finite place
Proof usesTensor product decomposition at a finite place
8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.