Module

IdeleSupport.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Adele.IntegralTensorSupport.IdeleSupport

3 declarations indexed from sourceView source ↗

Module documentation

Finite support for integral relative ideles

This module combines coefficient support with the exceptional places of the local tensor decomposition, producing one finite set that controls integrality of a relative idele and its inverse.

Imports1

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Adele.IntegralTensorSupport.LocalTensorDecomposition

Imported by5

def

relativeIdeleLocalTensorDecompositionSupport

L36 ↗

Documentation

The single finite support controlling both coefficient integrality of a relative idele and the integral compatibility of the local tensor decomposition.

Source context 6 commands

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

open scoped NumberField TensorProduct NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]

Lean source · statement

def relativeIdeleLocalTensorDecompositionSupport
    (z : RelativeIdeleGroup K L) :
    Finset (HeightOneSpectrum (𝓞 K))

theorem

mem_relativeIdeleLocalTensorDecompositionSupport_iff

L48 ↗

Documentation

The support is exposed through this membership characterization.

Source context 6 commands

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

open scoped NumberField TensorProduct NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]

Lean source · statement

theorem mem_relativeIdeleLocalTensorDecompositionSupport_iff
    (z : RelativeIdeleGroup K L)
    (w : HeightOneSpectrum (𝓞 K)) :
    w ∈ relativeIdeleLocalTensorDecompositionSupport
        (K := K) (L := L) z ↔
      w ∈ relativeIdeleCoefficientSupport
          (K := K) (L := L) z ∨
        w ∈ integralTensorBadPlaces
          (K := K) (L := L)

theorem

relativeIdele_finiteComponent_localTensorDecompositionIntegralUnit_of_notMem

L62 ↗

Documentation

Outside one explicit finite support, the actual finite component of a relative idele and its inverse are units in every valuation-ring factor of the local tensor decomposition.

Source context 6 commands

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

open scoped NumberField TensorProduct NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]

Lean source · statement

theorem relativeIdele_finiteComponent_localTensorDecompositionIntegralUnit_of_notMem
    (z : RelativeIdeleGroup K L)
    (w : HeightOneSpectrum (𝓞 K))
    (hw : w ∉ relativeIdeleLocalTensorDecompositionSupport
      (K := K) (L := L) z) :
    RelativeLocalTensorDecompositionIntegralUnitAt
      (K := K) (L := L) w
      (RelativeIdeleGroup.finiteComponent
        (K := K) (L := L) w z)

Module documentation

Finite support for integral relative ideles

Declarations

relativeIdeleLocalTensorDecompositionSupport

mem_relativeIdeleLocalTensorDecompositionSupport_iff

relativeIdele_finiteComponent_localTensorDecompositionIntegralUnit_of_notMem