Module

RationalCyclotomicLocalization.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.RationalCyclotomicLocalization

18 declarations indexed from sourceView source ↗

Module documentation

Localized rational cyclotomic levels

This file identifies the algebraic localization of an actual finite rational cyclotomic level with a cyclotomic extension of the completed base. The primitive root is the image of a genuine primitive root in the global level under the canonical global-to-local map.

Imports3

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.NormApproximation.FinitePlaces
Nyll.GaloisCohomology.Kummer.Concrete.Cyclotomic.RationalCyclotomicField
Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Imported by2

def

rationalCyclotomicLevelPrimitiveRoot

L34 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicLevelPrimitiveRoot

Documentation

A genuine primitive root in the actual m-th rational cyclotomic level.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

def rationalCyclotomicLevelPrimitiveRoot
    (m : ℕ+) : KummerTheory.rationalCyclotomicLevel m

abbrev

rationalCyclotomicAdicAbsoluteValue

L44 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicAdicAbsoluteValue

Documentation

The finite adic absolute value of the rational base at v.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

abbrev rationalCyclotomicAdicAbsoluteValue
    (v : HeightOneSpectrum (𝓞 ℚ))

def

rationalCyclotomicChosenFinitePlaceExtension

L50 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicChosenFinitePlaceExtension

Documentation

The chosen extension of the rational finite-place absolute value to the actual m-th cyclotomic level.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

def rationalCyclotomicChosenFinitePlaceExtension
    (m : ℕ+) (v : HeightOneSpectrum (𝓞 ℚ)) :
    AbsoluteValueExtension
      (rationalCyclotomicAdicAbsoluteValue v)
      (KummerTheory.rationalCyclotomicLevel m)

instance

rationalCyclotomicCompletionAlgebra

L60 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicCompletionAlgebra

Documentation

The canonical algebra structure on the selected extension completion over the rational finite completion.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

instance rationalCyclotomicCompletionAlgebra
    (m : ℕ+) (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra (rationalCyclotomicAdicAbsoluteValue v).Completion
      (rationalCyclotomicChosenFinitePlaceExtension m v).1.Completion

abbrev

rationalCyclotomicLocalizedCompletion

L70 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicLocalizedCompletion

Documentation

The actual algebraic localization of the rational cyclotomic level at v.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

abbrev rationalCyclotomicLocalizedCompletion
    (m : ℕ+) (v : HeightOneSpectrum (𝓞 ℚ))

instance

rationalCyclotomicLocalizedCompletionFinite

L77 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicLocalizedCompletionFinite

Documentation

The selected rational cyclotomic localization is finite over the finite completion.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

instance rationalCyclotomicLocalizedCompletionFinite
    (m : ℕ+) (v : HeightOneSpectrum (𝓞 ℚ)) :
    FiniteDimensional (rationalCyclotomicAdicAbsoluteValue v).Completion
      (rationalCyclotomicLocalizedCompletion m v)

instance

rationalCyclotomicLocalizedCompletionIsAlgebraic

L87 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicLocalizedCompletionIsAlgebraic

Documentation

The selected rational cyclotomic localization is algebraic over the finite completion.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

instance rationalCyclotomicLocalizedCompletionIsAlgebraic
    (m : ℕ+) (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra.IsAlgebraic (rationalCyclotomicAdicAbsoluteValue v).Completion
      (rationalCyclotomicLocalizedCompletion m v)

theorem

rationalCyclotomicLevelPrimitiveRoot_isPrimitiveRoot

L98 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicLevelPrimitiveRoot_isPrimitiveRoot

Documentation

The selected root in the actual rational cyclotomic level is primitive of order m.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

theorem rationalCyclotomicLevelPrimitiveRoot_isPrimitiveRoot
    (m : ℕ+) :
    IsPrimitiveRoot (rationalCyclotomicLevelPrimitiveRoot m)
      (m : ℕ)

theorem

rationalCyclotomicLocalizedCompletion_charZero

L111 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicLocalizedCompletion_charZero

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section RationalGlobalToLocalized

Lean source · statement

theorem rationalCyclotomicLocalizedCompletion_charZero
    (m : ℕ+) (v : HeightOneSpectrum (𝓞 ℚ)) :
    CharZero (rationalCyclotomicLocalizedCompletion m v)

def

rationalCyclotomicGlobalToLocalizedAlgHom

L125 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicGlobalToLocalizedAlgHom

Documentation

The actual global-to-local embedding of the selected rational cyclotomic level, regarded as a rational algebra homomorphism.

Source context 9 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section RationalGlobalToLocalized
attribute [local instance] rationalCyclotomicLocalizedCompletion_charZero

Lean source · statement

def rationalCyclotomicGlobalToLocalizedAlgHom
    (m : ℕ+) (v : HeightOneSpectrum (𝓞 ℚ)) :
    KummerTheory.rationalCyclotomicLevel m →ₐ[ℚ]
      rationalCyclotomicLocalizedCompletion m v

theorem

rationalCyclotomicGlobalToLocalizedAlgHom_apply

L137 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicGlobalToLocalizedAlgHom_apply

Documentation

The named rational algebra homomorphism has the canonical global-to-local ring homomorphism as its underlying map.

Source context 9 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section RationalGlobalToLocalized
attribute [local instance] rationalCyclotomicLocalizedCompletion_charZero

Lean source · statement

theorem rationalCyclotomicGlobalToLocalizedAlgHom_apply
    (m : ℕ+) (v : HeightOneSpectrum (𝓞 ℚ))
    (x : KummerTheory.rationalCyclotomicLevel m) :
    rationalCyclotomicGlobalToLocalizedAlgHom m v x =
      AbsoluteValue.toAlgebraicLocalization
        (rationalCyclotomicAdicAbsoluteValue v)
        (rationalCyclotomicChosenFinitePlaceExtension m v).1
        (rationalCyclotomicChosenFinitePlaceExtension m v).2 x

def

rationalCyclotomicLocalizedPrimitiveRoot

L149 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicLocalizedPrimitiveRoot

Documentation

The image of the selected global primitive root in the algebraic localization at v.

Source context 9 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section RationalGlobalToLocalized
attribute [local instance] rationalCyclotomicLocalizedCompletion_charZero

Lean source · statement

def rationalCyclotomicLocalizedPrimitiveRoot
    (m : ℕ+) (v : HeightOneSpectrum (𝓞 ℚ)) :
    rationalCyclotomicLocalizedCompletion m v

theorem

rationalCyclotomicGlobalToLocalizedAlgHom_primitiveRoot

L161 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicGlobalToLocalizedAlgHom_primitiveRoot

Documentation

The selected localized root is the actual global-to-local image of the selected global primitive root.

Source context 9 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section RationalGlobalToLocalized
attribute [local instance] rationalCyclotomicLocalizedCompletion_charZero

Lean source · statement

theorem rationalCyclotomicGlobalToLocalizedAlgHom_primitiveRoot
    (m : ℕ+) (v : HeightOneSpectrum (𝓞 ℚ)) :
    rationalCyclotomicGlobalToLocalizedAlgHom m v
        (rationalCyclotomicLevelPrimitiveRoot m) =
      rationalCyclotomicLocalizedPrimitiveRoot m v

theorem

rationalCyclotomicLocalizedPrimitiveRoot_isPrimitiveRoot

L170 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicLocalizedPrimitiveRoot_isPrimitiveRoot

Documentation

The localized global root remains primitive because the canonical global-to-local homomorphism is injective.

Source context 9 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
section RationalGlobalToLocalized
attribute [local instance] rationalCyclotomicLocalizedCompletion_charZero

Lean source · statement

theorem rationalCyclotomicLocalizedPrimitiveRoot_isPrimitiveRoot
    (m : ℕ+) (v : HeightOneSpectrum (𝓞 ℚ)) :
    IsPrimitiveRoot
      (rationalCyclotomicLocalizedPrimitiveRoot m v) (m : ℕ)

theorem

rationalCyclotomicLevelPrimitiveRoot_adjoin_eq_top

L182 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicLevelPrimitiveRoot_adjoin_eq_top

Documentation

The selected primitive root generates the actual rational cyclotomic level over ℚ.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

theorem rationalCyclotomicLevelPrimitiveRoot_adjoin_eq_top
    (m : ℕ+) :
    IntermediateField.adjoin ℚ
        ({rationalCyclotomicLevelPrimitiveRoot m} :
          Set (KummerTheory.rationalCyclotomicLevel m)) =
      ⊤

theorem

rationalCyclotomicLocalizedPrimitiveRoot_adjoin_eq_top

L199 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicLocalizedPrimitiveRoot_adjoin_eq_top

Documentation

The localized primitive root generates the whole algebraic localization over the completed rational field.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

theorem
    rationalCyclotomicLocalizedPrimitiveRoot_adjoin_eq_top
    (m : ℕ+) (v : HeightOneSpectrum (𝓞 ℚ)) :
    IntermediateField.adjoin
        (rationalCyclotomicAdicAbsoluteValue v).Completion
        {rationalCyclotomicLocalizedPrimitiveRoot m v} =
      ⊤

theorem

rationalCyclotomicLocalizedPrimitiveRoot_algebraAdjoin_eq_top

L228 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicLocalizedPrimitiveRoot_algebraAdjoin_eq_top

Documentation

The localized primitive root generates the same top subalgebra as its intermediate-field closure. This avoids reducing the two adjoin constructions.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

theorem rationalCyclotomicLocalizedPrimitiveRoot_algebraAdjoin_eq_top
    (m : ℕ+) (v : HeightOneSpectrum (𝓞 ℚ)) :
    Algebra.adjoin (rationalCyclotomicAdicAbsoluteValue v).Completion
      ({rationalCyclotomicLocalizedPrimitiveRoot m v} :
        Set (rationalCyclotomicLocalizedCompletion m v)) = ⊤

theorem

rationalCyclotomicLevel_localizedCompletion_isCyclotomicExtension

L246 ↗

GlobalClassFieldTheory.Reciprocity.rationalCyclotomicLevel_localizedCompletion_isCyclotomicExtension

Documentation

The algebraic localization of the actual m-th rational cyclotomic level is itself a cyclotomic extension of the completed rational field.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity

Lean source · statement

theorem rationalCyclotomicLevel_localizedCompletion_isCyclotomicExtension
    (m : ℕ+) (v : HeightOneSpectrum (𝓞 ℚ)) :
    IsCyclotomicExtension {(m : ℕ)}
      (rationalCyclotomicAdicAbsoluteValue v).Completion
      (rationalCyclotomicLocalizedCompletion m v)

Module documentation

Localized rational cyclotomic levels

Declarations