NYLL
Module

PadicValuationInertia.lean

Nyll.ClassFieldTheory.RamificationTheory.HilbertRamification.Dedekind.PadicValuationInertia
31 declarations indexed from sourceView source ↗

Module documentation

The global valuation/prime-ideal bridge in the global cyclotomic inertia argument

An extension w of the rational p-adic absolute value determines a valuation subring of a number field M. This file synchronizes that valuation subring with a concrete prime ideal of 𝓞 M, proves that the prime lies over (p), and identifies the valuation subring with the localization of 𝓞 M at that prime.

The final comparison sends ideal-theoretic inertia injectively to the valuation-subring inertia group. Thus the local cardinality bound furnished by the localization and decomposition comparison applies to the chosen global prime without an extra compatibility hypothesis.

Comparison of ideal inertia with valuation inertia

Imports8
Imported by2

Declarations

def

dedekindAtPrimeValuationSubring

L48 ↗
HilbertRamification.Dedekind.dedekindAtPrimeValuationSubring
Documentation

The localization of a Dedekind domain at a nonzero prime, realized inside its fraction field as a valuation subring. This construction belongs to the ideal/localization bridge; it is kept private here until that bridge is factored into prime-decomposition theory.

Source context 8 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
Lean source · statement
def dedekindAtPrimeValuationSubring
    (B : Type*) [CommRing B] [IsDedekindDomain B]
    {L : Type*} [Field L] [Algebra B L] [IsFractionRing B L]
    (P : Ideal B) [P.IsPrime] (hP : P ≠ ⊥) :
    _root_.ValuationSubring L
instance

dedekindAtPrimeValuationSubringAlgebra

L75 ↗
HilbertRamification.Dedekind.dedekindAtPrimeValuationSubringAlgebra
Documentation

The valuation-subring realization of a Dedekind localization carries its canonical algebra structure over the original domain.

Source context 8 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
Lean source · statement
instance dedekindAtPrimeValuationSubringAlgebra
    (B : Type*) [CommRing B] [IsDedekindDomain B]
    {L : Type*} [Field L] [Algebra B L] [IsFractionRing B L]
    (P : Ideal B) [P.IsPrime] (hP : P ≠ ⊥) :
    Algebra B (dedekindAtPrimeValuationSubring B (L := L) P hP)
instance

dedekindAtPrimeValuationSubringIsLocalization

L87 ↗
HilbertRamification.Dedekind.dedekindAtPrimeValuationSubringIsLocalization
Documentation

The valuation-subring realization is the localization away from the chosen prime.

Source context 8 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
Lean source · statement
instance dedekindAtPrimeValuationSubringIsLocalization
    (B : Type*) [CommRing B] [IsDedekindDomain B]
    {L : Type*} [Field L] [Algebra B L] [IsFractionRing B L]
    (P : Ideal B) [P.IsPrime] (hP : P ≠ ⊥) :
    IsLocalization P.primeCompl
      (dedekindAtPrimeValuationSubring B (L := L) P hP)
instance

dedekindAtPrimeValuationSubringIsDedekindDomain

L100 ↗
HilbertRamification.Dedekind.dedekindAtPrimeValuationSubringIsDedekindDomain
Documentation

A Dedekind localization realized as a valuation subring is again a Dedekind domain.

Source context 8 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
Lean source · statement
instance dedekindAtPrimeValuationSubringIsDedekindDomain
    (B : Type*) [CommRing B] [IsDedekindDomain B]
    {L : Type*} [Field L] [Algebra B L] [IsFractionRing B L]
    (P : Ideal B) [P.IsPrime] (hP : P ≠ ⊥) :
    IsDedekindDomain
      (dedekindAtPrimeValuationSubring B (L := L) P hP)
instance

dedekindAtPrimeValuationSubringKrullDimLE

L111 ↗
HilbertRamification.Dedekind.dedekindAtPrimeValuationSubringKrullDimLE
Documentation

The valuation-subring realization of a nonzero Dedekind localization has Krull dimension at most one.

Source context 8 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
Lean source · statement
instance dedekindAtPrimeValuationSubringKrullDimLE
    (B : Type*) [CommRing B] [IsDedekindDomain B]
    {L : Type*} [Field L] [Algebra B L] [IsFractionRing B L]
    (P : Ideal B) [P.IsPrime] (hP : P ≠ ⊥) :
    Ring.KrullDimLE 1
      (dedekindAtPrimeValuationSubring B (L := L) P hP)
abbrev

globalPadicExtensionValuationSubring

L121 ↗
HilbertRamification.Dedekind.globalPadicExtensionValuationSubring
Documentation

The nonarchimedean extension valuation ring attached to a global extension of the rational p-adic absolute value.

Source context 8 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
Lean source · statement
abbrev globalPadicExtensionValuationSubring
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) M) :
    _root_.ValuationSubring M
theorem

ringOfIntegers_mem_globalPadicExtensionValuationSubring

L134 ↗
HilbertRamification.Dedekind.ringOfIntegers_mem_globalPadicExtensionValuationSubring
Documentation

Every algebraic integer belongs to the valuation ring defined by w. This is the integrally-closed valuation-ring argument, rather than an additional boundedness assumption on algebraic integers.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
omit [IsAbelianGalois ℚ M] in
Lean source · statement
theorem ringOfIntegers_mem_globalPadicExtensionValuationSubring
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) M)
    (x : 𝓞 M) :
    (x : M) ∈ globalPadicExtensionValuationSubring p M w
def

globalPadicRingOfIntegersToExtensionValuationSubring

L147 ↗
HilbertRamification.Dedekind.globalPadicRingOfIntegersToExtensionValuationSubring
Documentation

The canonical inclusion 𝓞 M → A_w.

Source context 8 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
Lean source · statement
def globalPadicRingOfIntegersToExtensionValuationSubring
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) M) :
    𝓞 M →+* globalPadicExtensionValuationSubring p M w
theorem

globalPadicRingOfIntegersToExtensionValuationSubring_coe

L157 ↗
HilbertRamification.Dedekind.globalPadicRingOfIntegersToExtensionValuationSubring_coe
Documentation

The canonical map from 𝓞 M to the extension valuation ring agrees with the usual inclusion into M.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
omit [IsAbelianGalois ℚ M] in
Lean source · statement
theorem globalPadicRingOfIntegersToExtensionValuationSubring_coe
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) M)
    (x : 𝓞 M) :
    ((globalPadicRingOfIntegersToExtensionValuationSubring p M w x :
        globalPadicExtensionValuationSubring p M w) : M) = (x : M)
def

globalPadicPrimeIdeal

L165 ↗
HilbertRamification.Dedekind.globalPadicPrimeIdeal
Documentation

The prime ideal of 𝓞 M which is the center of w.

Source context 8 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
Lean source · statement
def globalPadicPrimeIdeal
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) M) :
    Ideal (𝓞 M)
theorem

mem_globalPadicPrimeIdeal_iff

L175 ↗
HilbertRamification.Dedekind.mem_globalPadicPrimeIdeal_iff
Documentation

Membership in the synchronized prime is the strict w-adic inequality.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
omit [IsAbelianGalois ℚ M] in
Lean source · statement
theorem mem_globalPadicPrimeIdeal_iff
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) M)
    (x : 𝓞 M) :
    x ∈ globalPadicPrimeIdeal p M w ↔ w.1 (x : M) < 1
theorem

globalPadicPrimeIdeal_isPrime

L192 ↗
HilbertRamification.Dedekind.globalPadicPrimeIdeal_isPrime
Documentation

The center of a valuation ring is prime.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
omit [IsAbelianGalois ℚ M] in
Lean source · statement
theorem globalPadicPrimeIdeal_isPrime
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) M) :
    (globalPadicPrimeIdeal p M w).IsPrime
theorem

int_mem_globalPadicPrimeIdeal_under_iff

L200 ↗
HilbertRamification.Dedekind.int_mem_globalPadicPrimeIdeal_under_iff
Documentation

On rational integers, membership in the center is divisibility by p.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
omit [IsAbelianGalois ℚ M] in
Lean source · statement
theorem int_mem_globalPadicPrimeIdeal_under_iff
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) M)
    (z : ℤ) :
    algebraMap ℤ (𝓞 M) z ∈ globalPadicPrimeIdeal p M w ↔
      (p : ℤ) ∣ z
theorem

globalPadicPrimeIdeal_under_eq_span

L217 ↗
HilbertRamification.Dedekind.globalPadicPrimeIdeal_under_eq_span
Documentation

The contraction of the synchronized prime to ℤ is the usual principal ideal (p).

Source context 9 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
omit [IsAbelianGalois ℚ M] in
Lean source · statement
theorem globalPadicPrimeIdeal_under_eq_span
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) M) :
    (globalPadicPrimeIdeal p M w).under ℤ =
      Ideal.span ({(p : ℤ)} : Set ℤ)
theorem

globalPadicPrimeIdeal_liesOver

L227 ↗
HilbertRamification.Dedekind.globalPadicPrimeIdeal_liesOver
Documentation

The synchronized prime lies over the rational height-one prime p.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
omit [IsAbelianGalois ℚ M] in
Lean source · statement
theorem globalPadicPrimeIdeal_liesOver
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) M) :
    (globalPadicPrimeIdeal p M w).LiesOver
      (rationalPrimeIdeal (⟨p, Fact.out⟩ : Nat.Primes))
theorem

globalPadicPrimeIdeal_ne_bot

L238 ↗
HilbertRamification.Dedekind.globalPadicPrimeIdeal_ne_bot
Documentation

The synchronized prime is nonzero.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
omit [IsAbelianGalois ℚ M] in
Lean source · statement
theorem globalPadicPrimeIdeal_ne_bot
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) M) :
    globalPadicPrimeIdeal p M w ≠ ⊥
theorem

globalPadicPrimeIdeal_isMaximal

L251 ↗
HilbertRamification.Dedekind.globalPadicPrimeIdeal_isMaximal
Documentation

In the Dedekind ring 𝓞 M, the synchronized nonzero prime is maximal.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
omit [IsAbelianGalois ℚ M] in
Lean source · statement
theorem globalPadicPrimeIdeal_isMaximal
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) M) :
    (globalPadicPrimeIdeal p M w).IsMaximal
instance

instIsPrimeGlobalPadicPrimeIdeal

L258 ↗
HilbertRamification.Dedekind.instIsPrimeGlobalPadicPrimeIdeal
Documentation

The center of a global p-adic place is a prime ideal.

Source context 8 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
Lean source · statement
instance instIsPrimeGlobalPadicPrimeIdeal
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) M) :
    (globalPadicPrimeIdeal p M w).IsPrime
instance

instIsMaximalGlobalPadicPrimeIdeal

L264 ↗
HilbertRamification.Dedekind.instIsMaximalGlobalPadicPrimeIdeal
Documentation

The center of a global p-adic place is a maximal ideal.

Source context 8 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
Lean source · statement
instance instIsMaximalGlobalPadicPrimeIdeal
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) M) :
    (globalPadicPrimeIdeal p M w).IsMaximal
instance

instLiesOverGlobalPadicPrimeIdeal

L271 ↗
HilbertRamification.Dedekind.instLiesOverGlobalPadicPrimeIdeal
Documentation

The center of a global p-adic place lies over the rational prime ideal generated by p.

Source context 8 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
Lean source · statement
instance instLiesOverGlobalPadicPrimeIdeal
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) M) :
    (globalPadicPrimeIdeal p M w).LiesOver
      (rationalPrimeIdeal ⟨p, Fact.out⟩)
def

globalPadicPrimeHeightOneSpectrum

L278 ↗
HilbertRamification.Dedekind.globalPadicPrimeHeightOneSpectrum
Documentation

The height-one prime of 𝓞 M centered at w.

Source context 8 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
Lean source · statement
def globalPadicPrimeHeightOneSpectrum
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) M) :
    IsDedekindDomain.HeightOneSpectrum (𝓞 M)
abbrev

globalPadicPrimeLocalizationValuationSubring

L287 ↗
HilbertRamification.Dedekind.globalPadicPrimeLocalizationValuationSubring
Documentation

The ordinary localization of 𝓞 M at the prime centered at w, viewed as a valuation subring of M.

Source context 8 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
Lean source · statement
abbrev globalPadicPrimeLocalizationValuationSubring
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) M) :
    _root_.ValuationSubring M
theorem

globalPadicPrime_localizationValuationSubring_eq

L297 ↗
HilbertRamification.Dedekind.globalPadicPrime_localizationValuationSubring_eq
Documentation

The valuation ring defined by the absolute value w is exactly the ordinary localization of 𝓞 M at its center.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
omit [IsAbelianGalois ℚ M] in
Lean source · statement
theorem globalPadicPrime_localizationValuationSubring_eq
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) M) :
    globalPadicPrimeLocalizationValuationSubring p M w =
      globalPadicExtensionValuationSubring p M w
theorem

globalPadicPrimeCompl_smul_of_mem_inertia

L413 ↗
HilbertRamification.Dedekind.globalPadicPrimeCompl_smul_of_mem_inertia
Source context 9 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
omit [IsAbelianGalois ℚ M] in
Lean source · statement
theorem globalPadicPrimeCompl_smul_of_mem_inertia
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) M)
    (sigma : HilbertRamification.Dedekind.inertiaGroup
      (globalPadicPrimeIdeal p M w) (M ≃ₐ[ℚ] M))
    {s : 𝓞 M}
    (hs : s ∈ (globalPadicPrimeIdeal p M w).primeCompl) :
    (sigma : M ≃ₐ[ℚ] M) • s ∈
      (globalPadicPrimeIdeal p M w).primeCompl
theorem

globalPadicIdealInertia_maps_localization

L433 ↗
HilbertRamification.Dedekind.globalPadicIdealInertia_maps_localization
Documentation

An ideal-inertia automorphism preserves the localization of 𝓞 M at the synchronized prime.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
omit [IsAbelianGalois ℚ M] in
Lean source · statement
theorem globalPadicIdealInertia_maps_localization
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) M)
    (sigma : HilbertRamification.Dedekind.inertiaGroup
      (globalPadicPrimeIdeal p M w) (M ≃ₐ[ℚ] M))
    {x : M}
    (hx : x ∈
      globalPadicPrimeLocalizationValuationSubring p M w) :
    (sigma : M ≃ₐ[ℚ] M) x ∈
      globalPadicPrimeLocalizationValuationSubring p M w
def

globalPadicIdealInertiaToLocalizationDecomposition

L464 ↗
HilbertRamification.Dedekind.globalPadicIdealInertiaToLocalizationDecomposition
Documentation

Ideal inertia at the synchronized prime maps to the decomposition group of its localization.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
omit [IsAbelianGalois ℚ M] in
Lean source · statement
def globalPadicIdealInertiaToLocalizationDecomposition
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) M) :
    HilbertRamification.Dedekind.inertiaGroup
        (globalPadicPrimeIdeal p M w) (M ≃ₐ[ℚ] M) →
      RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup ℚ
        (globalPadicPrimeLocalizationValuationSubring p M w)
theorem

globalPadicIdealInertiaToLocalizationDecomposition_mem_maximalIdealInertia

L485 ↗
HilbertRamification.Dedekind.globalPadicIdealInertiaToLocalizationDecomposition_mem_maximalIdealInertia
Source context 9 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
omit [IsAbelianGalois ℚ M] in
Lean source · statement
theorem
    globalPadicIdealInertiaToLocalizationDecomposition_mem_maximalIdealInertia
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) M)
    (sigma : HilbertRamification.Dedekind.inertiaGroup
      (globalPadicPrimeIdeal p M w) (M ≃ₐ[ℚ] M)) :
    globalPadicIdealInertiaToLocalizationDecomposition p M w sigma ∈
      (IsLocalRing.maximalIdeal
        (globalPadicPrimeLocalizationValuationSubring p M w)).toAddSubgroup.inertia
        (RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup ℚ
          (globalPadicPrimeLocalizationValuationSubring p M w))
theorem

globalPadicIdealInertiaToLocalizationDecomposition_mem_inertia

L553 ↗
HilbertRamification.Dedekind.globalPadicIdealInertiaToLocalizationDecomposition_mem_inertia
Source context 9 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
omit [IsAbelianGalois ℚ M] in
Lean source · statement
theorem
    globalPadicIdealInertiaToLocalizationDecomposition_mem_inertia
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) M)
    (sigma : HilbertRamification.Dedekind.inertiaGroup
      (globalPadicPrimeIdeal p M w) (M ≃ₐ[ℚ] M)) :
    globalPadicIdealInertiaToLocalizationDecomposition p M w sigma ∈
      RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup ℚ
        (globalPadicPrimeLocalizationValuationSubring p M w)
def

globalPadicIdealInertiaToLocalizationInertia

L574 ↗
HilbertRamification.Dedekind.globalPadicIdealInertiaToLocalizationInertia
Documentation

The canonical localization map from global ideal inertia to valuation inertia.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
omit [IsAbelianGalois ℚ M] in
Lean source · full declaration
def globalPadicIdealInertiaToLocalizationInertia
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) M) :
    HilbertRamification.Dedekind.inertiaGroup
        (globalPadicPrimeIdeal p M w) (M ≃ₐ[ℚ] M) →*
      RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup ℚ
        (globalPadicPrimeLocalizationValuationSubring p M w) where
  toFun sigma :=
    ⟨globalPadicIdealInertiaToLocalizationDecomposition p M w sigma,
      globalPadicIdealInertiaToLocalizationDecomposition_mem_inertia
        p M w sigma⟩
  map_one' := by
    apply Subtype.ext
    apply Subtype.ext
    rfl
  map_mul' _ _ := by
    apply Subtype.ext
    apply Subtype.ext
    rfl
theorem

globalPadicIdealInertiaToLocalizationInertia_injective

L596 ↗
HilbertRamification.Dedekind.globalPadicIdealInertiaToLocalizationInertia_injective
Documentation

The localization map is injective because it does not change the underlying ℚ-automorphism of M.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
omit [IsAbelianGalois ℚ M] in
Lean source · statement
theorem globalPadicIdealInertiaToLocalizationInertia_injective
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) M) :
    Function.Injective
      (globalPadicIdealInertiaToLocalizationInertia p M w)
theorem

globalPadicPrimeIdeal_inertia_natCard_le_valuationInertia

L612 ↗
HilbertRamification.Dedekind.globalPadicPrimeIdeal_inertia_natCard_le_valuationInertia
Documentation

The exact cardinal comparison needed in the global cyclotomic inertia argument: the ideal inertia group at the synchronized prime is no larger than the localization and decomposition comparison valuation inertia group attached to w.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory.Ramification
open scoped NumberField
variable (p : ℕ) [Fact p.Prime]
variable (M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
omit [IsAbelianGalois ℚ M] in
Lean source · statement
theorem globalPadicPrimeIdeal_inertia_natCard_le_valuationInertia
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) M) :
    Nat.card
        (HilbertRamification.Dedekind.inertiaGroup
          (globalPadicPrimeIdeal p M w) (M ≃ₐ[ℚ] M)) ≤
      Nat.card
        (RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup ℚ
          (globalPadicExtensionValuationSubring p M w))

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