NYLL
Module

PadicLocalizationCanonicalValuation.lean

Nyll.ClassFieldTheory.RamificationTheory.HilbertRamification.PadicLocalizationCanonicalValuation
4 declarations indexed from sourceView source ↗

Module documentation

The valuation on the p-adic localization in the global cyclotomic inertia argument

The localization constructed in is transported from the absolute value completion of ℚ to the concrete field ℚ_p. Uniqueness of the absolute-value extension identifies its valuation ring with the canonical norm-formula valuation ring used in the unramified cyclotomic extension theorem.

Imports14
Imported by4

Declarations

def

globalPadicLocalizationCanonicalAbsoluteValueProperty

L43 ↗
HilbertRamification.globalPadicLocalizationCanonicalAbsoluteValueProperty
Documentation

The absolute-value comparison statement for the raw algebraic localization, with the transported ℚ_p structure kept internal.

Source context 5 commands

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

noncomputable section
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable (p : ℕ) [Fact p.Prime]
variable (L : Type) [Field L] [Algebra ℚ L]
  [FiniteDimensional ℚ L] [IsAbelianGalois ℚ L]
Lean source · statement
def globalPadicLocalizationCanonicalAbsoluteValueProperty
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) L) : Prop
theorem

globalPadicLocalizationAbsoluteValue_eq_canonical

L70 ↗
HilbertRamification.globalPadicLocalizationAbsoluteValue_eq_canonical
Documentation

The algebraic-localization absolute value is exactly the canonical norm-formula absolute value on its transported finite ℚ_p-extension.

Source context 5 commands

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

noncomputable section
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable (p : ℕ) [Fact p.Prime]
variable (L : Type) [Field L] [Algebra ℚ L]
  [FiniteDimensional ℚ L] [IsAbelianGalois ℚ L]
Lean source · statement
theorem globalPadicLocalizationAbsoluteValue_eq_canonical
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) L) :
    globalPadicLocalizationCanonicalAbsoluteValueProperty p L w
def

globalPadicLocalizationCanonicalValuationProperty

L136 ↗
HilbertRamification.globalPadicLocalizationCanonicalValuationProperty
Documentation

The valuation-ring comparison statement for the raw algebraic localization, with all transported local instances kept internal.

Source context 5 commands

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

noncomputable section
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable (p : ℕ) [Fact p.Prime]
variable (L : Type) [Field L] [Algebra ℚ L]
  [FiniteDimensional ℚ L] [IsAbelianGalois ℚ L]
Lean source · statement
def globalPadicLocalizationCanonicalValuationProperty
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) L) : Prop
theorem

globalPadicLocalizationValuationSubring_eq_canonical

L168 ↗
HilbertRamification.globalPadicLocalizationValuationSubring_eq_canonical
Documentation

The algebraic-localization valuation ring is the canonical valuation ring on the transported finite extension of ℚ_p.

Source context 5 commands

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

noncomputable section
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable (p : ℕ) [Fact p.Prime]
variable (L : Type) [Field L] [Algebra ℚ L]
  [FiniteDimensional ℚ L] [IsAbelianGalois ℚ L]
Lean source · statement
theorem globalPadicLocalizationValuationSubring_eq_canonical
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) L) :
    globalPadicLocalizationCanonicalValuationProperty p L w

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