NYLL
Module

GlobalCompositumValuedEmbedding.lean

Nyll.ClassFieldTheory.KroneckerWeber.GlobalCompositumValuedEmbedding
6 declarations indexed from sourceView source ↗

Module documentation

A valued global embedding of the auxiliary compositum

The left factor is embedded through its chosen localization. Consequently the pullback of the canonical absolute value on the common local cyclotomic target is exactly the chosen p-adic place. The corrected normal-compositum embedding preserves this exact left restriction.

Imports2
Imported by3

Declarations

def

kroneckerWeberGlobalLeftEmbeddingPreservesPadicPlace

L33 ↗
KroneckerWeber.kroneckerWeberGlobalLeftEmbeddingPreservesPadicPlace
Documentation

The value-preserving property for a global left-factor embedding. The finite-dimensional structure of the concrete cyclotomic target remains internal to this named proposition.

Source context 7 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
Lean source · statement
def kroneckerWeberGlobalLeftEmbeddingPreservesPadicPlace
    (p : Nat.Primes) [Fact p.1.Prime]
    (i : L →ₐ[ℚ]
      CyclotomicField (kroneckerWeberLocalCompositumOrder (L := L) p)
        ℚ_[p.1]) : Prop
def

kroneckerWeberGlobalValuedLeftEmbeddingProperty

L50 ↗
KroneckerWeber.kroneckerWeberGlobalValuedLeftEmbeddingProperty
Documentation

A global left-factor embedding which preserves the particular p-adic place used to choose the local exponent.

Source context 7 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
Lean source · statement
def kroneckerWeberGlobalValuedLeftEmbeddingProperty
    (p : Nat.Primes) : Prop
theorem

kroneckerWeberGlobalValuedLeftEmbedding

L60 ↗
KroneckerWeber.kroneckerWeberGlobalValuedLeftEmbedding
Documentation

The global field embeds into the common local cyclotomic target while preserving the chosen p-adic place.

Source context 7 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
Lean source · statement
theorem kroneckerWeberGlobalValuedLeftEmbedding
    (p : Nat.Primes) :
    kroneckerWeberGlobalValuedLeftEmbeddingProperty (L := L) p
structure

KroneckerWeberGlobalValuedCompositumEmbeddingData

L85 ↗
KroneckerWeber.KroneckerWeberGlobalValuedCompositumEmbeddingData
Documentation

A common-target compositum embedding whose restriction to L induces the chosen p-adic absolute value.

Source context 7 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
Lean source · full declaration
structure KroneckerWeberGlobalValuedCompositumEmbeddingData
    (p : Nat.Primes) [Fact p.1.Prime] where
  /-- The value-preserving embedding of the original global field. -/
  leftEmbedding :
    L →ₐ[ℚ]
      CyclotomicField (kroneckerWeberLocalCompositumOrder (L := L) p)
        ℚ_[p.1]
  /-- The embedding of the global compositum into the common local target. -/
  embedding :
    kroneckerWeberCompositumField L →ₐ[ℚ]
      CyclotomicField (kroneckerWeberLocalCompositumOrder (L := L) p)
        ℚ_[p.1]
  /-- The compositum embedding restricts to the chosen left-factor embedding. -/
  embedding_left : ∀ x : L,
    embedding (kroneckerWeberCompositumEmbeddingLeft (L := L) x) =
      leftEmbedding x
  /-- The left-factor embedding pulls back the canonical target absolute value
  to the chosen `p`-adic place. -/
  leftEmbedding_absoluteValue :
    kroneckerWeberGlobalLeftEmbeddingPreservesPadicPlace
      (L := L) p leftEmbedding
def

kroneckerWeberGlobalValuedCompositumEmbeddingData

L109 ↗
KroneckerWeber.kroneckerWeberGlobalValuedCompositumEmbeddingData
Documentation

The synchronized valued embeddings of the original field and its global cyclotomic compositum into the common local target.

Source context 7 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
Lean source · full declaration
def kroneckerWeberGlobalValuedCompositumEmbeddingData
    (p : Nat.Primes)
    (hp : p ∈ kroneckerWeberRamifiedPrimes (L := L)) :
    letI : Fact p.1.Prime := ⟨p.2⟩
    KroneckerWeberGlobalValuedCompositumEmbeddingData (L := L) p := by
  letI : Fact p.1.Prime := ⟨p.2⟩
  let hi := kroneckerWeberGlobalValuedLeftEmbedding (L := L) p
  let i := Classical.choose hi
  let hiAbs := Classical.choose_spec hi
  let j :
      CyclotomicField (kroneckerWeberConductorCandidate (L := L)) ℚ →ₐ[ℚ]
        CyclotomicField (kroneckerWeberLocalCompositumOrder (L := L) p)
          ℚ_[p.1] :=
    Classical.choice (kroneckerWeberGlobalRightEmbedding (L := L) p hp)
  let hex :=
    exists_finiteGaloisCompositumEmbeddingOfEmbeddings_left_eq
      ℚ L (CyclotomicField (kroneckerWeberConductorCandidate (L := L)) ℚ)
      (CyclotomicField (kroneckerWeberLocalCompositumOrder (L := L) p)
        ℚ_[p.1]) i j
  let g := Classical.choose hex
  let hg := Classical.choose_spec hex
  exact ⟨i, g, hg, hiAbs⟩
def

kroneckerWeberGlobalCompositumCyclotomicPadicExtension

L134 ↗
KroneckerWeber.kroneckerWeberGlobalCompositumCyclotomicPadicExtension
Documentation

The synchronized p-adic place on the global compositum, pulled back from the canonical absolute value on the common local cyclotomic target.

Source context 7 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
Lean source · statement
def kroneckerWeberGlobalCompositumCyclotomicPadicExtension
    (p : Nat.Primes) [Fact p.1.Prime]
    (hp : p ∈ kroneckerWeberRamifiedPrimes (L := L)) :
    AbsoluteValueExtension (Rat.AbsoluteValue.padic p.1)
      (kroneckerWeberCompositumField L)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.