Module

FinitePlaceTensorNormSubgroup.lean

Nyll.ClassFieldTheory.Definitions.GlobalClassFieldTheory.FinitePlaceTensorNormSubgroup

1 declaration indexed from sourceView source ↗

Module documentation

Finite-place tensor-norm subgroup

The local algebra of L / K at a finite place v is K_v ⊗[K] L. Its determinant norm on units defines a subgroup of K_vˣ. This definition retains the whole tensor algebra, including all factors above v; it does not choose a single completion of L.

Imports3

Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Mathlib.RingTheory.Norm.Basic
Mathlib.RingTheory.TensorProduct.Basic

Imported by6

def

finitePlaceTensorNormSubgroup

L31 ↗

ClassFieldTheory.finitePlaceTensorNormSubgroup

Documentation

The image of the determinant norm from the unit group of the finite-place tensor algebra K_v ⊗[K] L into K_vˣ.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u v

Lean source · statement

def finitePlaceTensorNormSubgroup
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [Algebra K L] [FiniteDimensional K L]
    (v : HeightOneSpectrum (𝓞 K)) :
    Subgroup (v.adicCompletion K)ˣ

Module documentation

Finite-place tensor-norm subgroup

Declarations

finitePlaceTensorNormSubgroup