Module

AbsoluteValueCoordinate.lean

Nyll.EtaleFundamentalGroups.Completions.Tensor.AbsoluteValueCoordinate

3 declarations indexed from sourceView source ↗

Module documentation

Selecting an absolute-value completion from a tensor component

For a finite separable field extension L / K, the completion tensor decomposition identifies L ⊗[K] K̂ with the finite product of the completions Lₓ over all exact extensions w of a fixed nontrivial absolute value on K.

This file proves that every maximal ideal of the tensor product is the kernel of one of the canonical coordinate maps. The coordinate is obtained from the prime-spectrum classification of a finite product; it is not supplied as an assumption.

Imports2

Mathlib.RingTheory.Spectrum.Prime.RingHom
Nyll.ValuedFieldTheory.Valuation.Completion.TensorProductDecomposition

Imported by1

Nyll.EtaleFundamentalGroups.Completions.Tensor.All

def

completionTensorAbsoluteValueCoordinateHom

L35 ↗

EtaleFundamentalGroups.completionTensorAbsoluteValueCoordinateHom

Documentation

The canonical map from the completion tensor product to the completion selected by an exact absolute-value extension.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped TensorProduct
open AlgebraicNumberTheory.Valuations
namespace EtaleFundamentalGroups
universe uK uL

Lean source · statement

def completionTensorAbsoluteValueCoordinateHom
    {K : Type uK} {L : Type uL}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L) :
    L ⊗[K] vK.Completion →+* w.1.Completion

theorem

completionTensorAbsoluteValueCoordinateHom_tmul

L54 ↗

EtaleFundamentalGroups.completionTensorAbsoluteValueCoordinateHom_tmul

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped TensorProduct
open AlgebraicNumberTheory.Valuations
namespace EtaleFundamentalGroups
universe uK uL

Lean source · full declaration

theorem completionTensorAbsoluteValueCoordinateHom_tmul
    {K : Type uK} {L : Type uL}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L) (a : L) (b : vK.Completion) :
    letI : Algebra vK.Completion w.1.Completion :=
      AbsoluteValue.completionAlgebra vK w.1 w.2
    completionTensorAbsoluteValueCoordinateHom vK hvK w (a ⊗ₜ[K] b) =
      AbsoluteValue.toCompletionAlgHom (K := K) w.1 a *
        algebraMap vK.Completion w.1.Completion b := by
  classical
  let := Algebra.TensorProduct.rightAlgebra
    (R := K) (A := L) (B := vK.Completion)
  let : ∀ u : AbsoluteValueExtension vK L,
      Algebra vK.Completion u.1.Completion :=
    fun u ↦ AbsoluteValue.completionAlgebra vK u.1 u.2
  exact completionTensorDecomposition_tmul_apply
    (K := K) (L := L) vK hvK a b w

theorem

exists_completionTensorAbsoluteValueCoordinate_ker_eq

L77 ↗

EtaleFundamentalGroups.exists_completionTensorAbsoluteValueCoordinate_ker_eq

Documentation

Every maximal tensor component is a canonical absolute-value completion coordinate. The chosen extension is produced from the finite-product prime spectrum, and the coordinate prime is zero because its ring is a field.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped TensorProduct
open AlgebraicNumberTheory.Valuations
namespace EtaleFundamentalGroups
universe uK uL

Lean source · statement

theorem exists_completionTensorAbsoluteValueCoordinate_ker_eq
    {K : Type uK} {L : Type uL}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (m : Ideal (L ⊗[K] vK.Completion)) [m.IsMaximal] :
    ∃ w : AbsoluteValueExtension vK L,
      RingHom.ker (completionTensorAbsoluteValueCoordinateHom vK hvK w) = m

Module documentation

Selecting an absolute-value completion from a tensor component

Declarations

completionTensorAbsoluteValueCoordinateHom

completionTensorAbsoluteValueCoordinateHom_tmul

exists_completionTensorAbsoluteValueCoordinate_ker_eq