Module

Lattice.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Adele.IntegralTensorSupport.Lattice

39 declarations indexed from sourceView source ↗

Module documentation

Integral lattices in relative tensor coordinates

This module chooses a common integral scale for a field basis, constructs the associated integer lattice, and isolates the finite set of primes where its local integrality properties can fail.

Imports1

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Adele.IntegralTensorSupport.AbsoluteValue

Imported by7

theorem

exists_integral_relativeBasis_scale

L37 ↗

Documentation

One common nonzero integer scales every vector of the chosen K-basis into the ring of integers of L.

Source context 7 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]
omit [NumberField K] in

Lean source · statement

theorem exists_integral_relativeBasis_scale :
    ∃ d : ℤ, d ≠ 0 ∧
      ∀ i : RelativeAdeleBasisIndex (K := K) (L := L),
        IsIntegral ℤ
          (d • relativeExtensionBasis
            (K := K) (L := L) i)

def

chosenRelativeBasisIntegralScale

L62 ↗

Documentation

The chosen common integral scale.

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 chosenRelativeBasisIntegralScale : ℤ

theorem

chosenRelativeBasisIntegralScale_ne_zero

L69 ↗

Documentation

The chosen integral scale is nonzero.

Source context 7 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]
omit [NumberField K] in

Lean source · statement

theorem chosenRelativeBasisIntegralScale_ne_zero :
    chosenRelativeBasisIntegralScale (K := K) (L := L) ≠ 0

theorem

chosenRelativeBasisIntegralScale_isIntegral

L77 ↗

Documentation

The chosen integral scale is integral in the base field.

Source context 7 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]
omit [NumberField K] in

Lean source · statement

theorem chosenRelativeBasisIntegralScale_isIntegral
    (i : RelativeAdeleBasisIndex (K := K) (L := L)) :
    IsIntegral ℤ
      (chosenRelativeBasisIntegralScale (K := K) (L := L) •
        relativeExtensionBasis (K := K) (L := L) i)

def

relativeBasisIntegralScaleInK_ne_zero

L92 ↗

Documentation

The base-field coercion of the chosen integral scale is nonzero.

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 relativeBasisIntegralScaleInK_ne_zero :
    relativeBasisIntegralScaleInK (K := K) (L := L) ≠ 0

def

relativeBasisIntegralScaleUnit

L106 ↗

Documentation

The integral scale as a unit of K.

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 relativeBasisIntegralScaleUnit : Kˣ

def

scaledRelativeExtensionBasis_apply

L123 ↗

Documentation

Evaluation and integrality properties of the scaled relative basis.

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 scaledRelativeExtensionBasis_apply
    (i : RelativeAdeleBasisIndex (K := K) (L := L)) :
    scaledRelativeExtensionBasis (K := K) (L := L) i =
      relativeBasisIntegralScaleInK
          (K := K) (L := L) •
        relativeExtensionBasis (K := K) (L := L) i

theorem

scaledRelativeExtensionBasis_isIntegral

L134 ↗

Documentation

Every vector of the scaled relative basis is integral.

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 scaledRelativeExtensionBasis_isIntegral
    (i : RelativeAdeleBasisIndex (K := K) (L := L)) :
    IsIntegral ℤ
      (scaledRelativeExtensionBasis
        (K := K) (L := L) i)

theorem

scaledRelativeExtensionBasis_absoluteValue_le_one

L146 ↗

Documentation

Every scaled basis vector belongs to the valuation ring of every nonarchimedean extension of an absolute value of K.

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 scaledRelativeExtensionBasis_absoluteValue_le_one
    (vK : AbsoluteValue K ℝ)
    (hvK : IsNonarchimedean (vK : K → ℝ))
    (wL : AbsoluteValueExtension vK L)
    (i : RelativeAdeleBasisIndex (K := K) (L := L)) :
    wL.1
      (scaledRelativeExtensionBasis
        (K := K) (L := L) i) ≤ 1

def

scaledRelativeExtensionInteger

L162 ↗

Documentation

The scaled basis vector as an actual element of 𝓞 L.

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 scaledRelativeExtensionInteger
    (i : RelativeAdeleBasisIndex (K := K) (L := L)) :
    𝓞 L

theorem

scaledRelativeExtensionInteger_coe

L171 ↗

Documentation

The named scaled integer is the corresponding scaled basis vector.

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 scaledRelativeExtensionInteger_coe
    (i : RelativeAdeleBasisIndex (K := K) (L := L)) :
    (scaledRelativeExtensionInteger
        (K := K) (L := L) i : L) =
      scaledRelativeExtensionBasis (K := K) (L := L) i

def

ringOfIntegersToFieldLinearMap

L195 ↗

Documentation

The canonical 𝓞 K-linear inclusion 𝓞 L → L.

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 ringOfIntegersToFieldLinearMap :
    𝓞 L →ₗ[𝓞 K] L

theorem

scaledRelativeIntegerLattice_map_toField

L201 ↗

Documentation

Mapping the integral lattice into L gives the field-valued lattice spanned by the scaled basis.

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 scaledRelativeIntegerLattice_map_toField :
    (scaledRelativeIntegerLattice
      (K := K) (L := L)).map
        (ringOfIntegersToFieldLinearMap
          (K := K) (L := L)) =
      scaledRelativeFieldLattice
        (K := K) (L := L)

theorem

ringOfIntegersToFieldLinearMap_injective

L219 ↗

Documentation

The inclusion 𝓞 L → L used above is injective.

Source context 7 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]
omit [NumberField K] [NumberField L] [FiniteDimensional K L] in

Lean source · statement

theorem ringOfIntegersToFieldLinearMap_injective :
    Function.Injective
      (ringOfIntegersToFieldLinearMap
        (K := K) (L := L))

theorem

exists_nonZeroDivisor_smul_mem_scaledRelativeIntegerLattice

L230 ↗

Documentation

Every algebraic integer becomes a member of the scaled lattice after multiplication by some non-zero-divisor of 𝓞 K. This is the direct denominator-clearing statement behind torsion of the lattice quotient.

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 exists_nonZeroDivisor_smul_mem_scaledRelativeIntegerLattice
    (x : 𝓞 L) :
    ∃ d : nonZeroDivisors (𝓞 K),
      (d : 𝓞 K) • x ∈
        scaledRelativeIntegerLattice
          (K := K) (L := L)

abbrev

ScaledRelativeIntegerLatticeQuotient

L275 ↗

Documentation

The finite quotient measuring the index of the scaled basis lattice in 𝓞 L.

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

abbrev ScaledRelativeIntegerLatticeQuotient

instance

scaledRelativeIntegerLatticeQuotientFinite

L281 ↗

Documentation

The lattice quotient is finitely generated over 𝓞 K.

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

instance
    scaledRelativeIntegerLatticeQuotientFinite :
    Module.Finite (𝓞 K)
      (ScaledRelativeIntegerLatticeQuotient
        (K := K) (L := L))

theorem

scaledRelativeIntegerLatticeQuotient_isTorsion

L291 ↗

Documentation

The lattice quotient is torsion.

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 scaledRelativeIntegerLatticeQuotient_isTorsion :
    Module.IsTorsion (𝓞 K)
      (ScaledRelativeIntegerLatticeQuotient
        (K := K) (L := L))

def

chosenScaledRelativeIntegerLatticeAnnihilatorData

L312 ↗

Documentation

A chosen nonzero element of the annihilator of the finite lattice quotient.

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 chosenScaledRelativeIntegerLatticeAnnihilatorData :
    { r : 𝓞 K //
      r ∈
          (⊤ : Submodule (𝓞 K)
            (ScaledRelativeIntegerLatticeQuotient
              (K := K) (L := L))).annihilator ∧
        r ∈ nonZeroDivisors (𝓞 K) }

def

scaledRelativeIntegerLatticeAnnihilator

L329 ↗

Documentation

The chosen annihilator element in 𝓞 K.

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 scaledRelativeIntegerLatticeAnnihilator :
    𝓞 K

theorem

scaledRelativeIntegerLatticeAnnihilator_mem

L335 ↗

Documentation

The selected annihilator element lies in the annihilator ideal.

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 scaledRelativeIntegerLatticeAnnihilator_mem :
    scaledRelativeIntegerLatticeAnnihilator
        (K := K) (L := L) ∈
      (⊤ : Submodule (𝓞 K)
        (ScaledRelativeIntegerLatticeQuotient
          (K := K) (L := L))).annihilator

theorem

scaledRelativeIntegerLatticeAnnihilator_ne_zero

L345 ↗

Documentation

The selected annihilator element is nonzero.

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 scaledRelativeIntegerLatticeAnnihilator_ne_zero :
    scaledRelativeIntegerLatticeAnnihilator
      (K := K) (L := L) ≠ 0

theorem

scaledRelativeIntegerLatticeAnnihilator_smul_mem

L354 ↗

Documentation

The chosen annihilator uniformly carries all of 𝓞 L into the scaled basis lattice.

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 scaledRelativeIntegerLatticeAnnihilator_smul_mem
    (x : 𝓞 L) :
    scaledRelativeIntegerLatticeAnnihilator
          (K := K) (L := L) • x ∈
      scaledRelativeIntegerLattice
        (K := K) (L := L)

def

relativeBasisIntegralScaleInRingOfIntegers

L373 ↗

Documentation

The original integral scaling factor, now viewed in 𝓞 K.

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 relativeBasisIntegralScaleInRingOfIntegers :
    𝓞 K

theorem

relativeBasisIntegralScaleInRingOfIntegers_ne_zero

L379 ↗

Documentation

The integral scale remains nonzero in the ring of integers.

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 relativeBasisIntegralScaleInRingOfIntegers_ne_zero :
    relativeBasisIntegralScaleInRingOfIntegers
      (K := K) (L := L) ≠ 0

def

integralTensorControlElement

L395 ↗

Documentation

One nonzero element controlling both the initial basis scaling and the finite index of the resulting lattice.

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 integralTensorControlElement :
    𝓞 K

theorem

integralTensorControlElement_ne_zero

L403 ↗

Documentation

The tensor control element is nonzero.

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 integralTensorControlElement_ne_zero :
    integralTensorControlElement
      (K := K) (L := L) ≠ 0

def

integralTensorControlIdeal

L413 ↗

Documentation

The nonzero principal ideal defining the bad primes.

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 integralTensorControlIdeal :
    Ideal (𝓞 K)

theorem

integralTensorControlIdeal_ne_bot

L419 ↗

Documentation

The tensor control ideal is nontrivial.

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 integralTensorControlIdeal_ne_bot :
    integralTensorControlIdeal
      (K := K) (L := L) ≠ ⊥

def

integralTensorBadPlaces

L429 ↗

Documentation

The actual finite set of primes at which either the basis scaling or the lattice index can fail to be invertible.

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 integralTensorBadPlaces :
    Finset (HeightOneSpectrum (𝓞 K))

theorem

mem_integralTensorBadPlaces_iff

L437 ↗

Documentation

Membership in the finite bad-place set is ideal membership.

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_integralTensorBadPlaces_iff
    (w : HeightOneSpectrum (𝓞 K)) :
    w ∈ integralTensorBadPlaces
        (K := K) (L := L) ↔
      w.asIdeal ∣
        integralTensorControlIdeal
          (K := K) (L := L)

theorem

integralTensorControlElement_not_mem_of_notMem

L451 ↗

Documentation

Outside the bad set the common control element is not in the corresponding height-one prime.

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 integralTensorControlElement_not_mem_of_notMem
    (w : HeightOneSpectrum (𝓞 K))
    (hw : w ∉ integralTensorBadPlaces
      (K := K) (L := L)) :
    integralTensorControlElement
        (K := K) (L := L) ∉ w.asIdeal

theorem

scaledRelativeIntegerLatticeAnnihilator_not_mem_of_notMem

L465 ↗

Documentation

The annihilator alone is invertible away from the bad set.

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 scaledRelativeIntegerLatticeAnnihilator_not_mem_of_notMem
    (w : HeightOneSpectrum (𝓞 K))
    (hw : w ∉ integralTensorBadPlaces
      (K := K) (L := L)) :
    scaledRelativeIntegerLatticeAnnihilator
        (K := K) (L := L) ∉ w.asIdeal

theorem

relativeBasisIntegralScale_not_mem_of_notMem

L481 ↗

Documentation

The initial integer scale is also invertible away from the bad set.

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 relativeBasisIntegralScale_not_mem_of_notMem
    (w : HeightOneSpectrum (𝓞 K))
    (hw : w ∉ integralTensorBadPlaces
      (K := K) (L := L)) :
    relativeBasisIntegralScaleInRingOfIntegers
        (K := K) (L := L) ∉ w.asIdeal

theorem

relativeExtensionBasis_absoluteValue_le_one_of_notMem

L498 ↗

Documentation

Away from the bad set, the original (unscaled) relative basis is integral for every extension of the corresponding finite absolute value to L.

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 relativeExtensionBasis_absoluteValue_le_one_of_notMem
    (w : HeightOneSpectrum (𝓞 K))
    (hw : w ∉ integralTensorBadPlaces
      (K := K) (L := L))
    (wL : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K w) L)
    (i : RelativeAdeleBasisIndex (K := K) (L := L)) :
    wL.1
      (relativeExtensionBasis
        (K := K) (L := L) i) ≤ 1

Module documentation

Integral lattices in relative tensor coordinates

Declarations