Module

Padic.lean

Nyll.ValuedFieldTheory.Valuation.Completion.Padic

11 declarations indexed from sourceView source ↗

Module documentation

The `p`-adic completion used in the global cyclotomic argument

the completion construction constructs localizations using the absolute-value completion v.Completion, whereas the local Kronecker--Weber local cyclotomic theorem is stated over mathlib's concrete field ℚ_[p]. For the rational p-adic absolute value these are canonically isomorphic. This file packages that comparison without adding any hypothesis to the global theorem.

Imports3

Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.Completion
Mathlib.NumberTheory.Ostrowski
Mathlib.NumberTheory.Padics.PadicNumbers

Imported by2

theorem

padicAbsoluteValue_isNontrivial

L29 ↗

AlgebraicNumberTheory.Valuations.padicAbsoluteValue_isNontrivial

Documentation

The rational p-adic absolute value is nontrivial.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory.Valuations
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem padicAbsoluteValue_isNontrivial :
    (Rat.AbsoluteValue.padic p).IsNontrivial

def

padicAbsoluteValueBaseMap

L38 ↗

AlgebraicNumberTheory.Valuations.padicAbsoluteValueBaseMap

Documentation

The dense isometric embedding of rational numbers, equipped with their p-adic absolute value, into the concrete field ℚ_[p].

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory.Valuations
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

def padicAbsoluteValueBaseMap :
    WithAbs (Rat.AbsoluteValue.padic p) →+* ℚ_[p]

theorem

padicAbsoluteValueBaseMap_norm

L44 ↗

AlgebraicNumberTheory.Valuations.padicAbsoluteValueBaseMap_norm

Documentation

The dense rational embedding preserves the p-adic norm.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory.Valuations
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem padicAbsoluteValueBaseMap_norm
    (x : WithAbs (Rat.AbsoluteValue.padic p)) :
    ‖padicAbsoluteValueBaseMap p x‖ = ‖x‖

theorem

padicAbsoluteValueBaseMap_isometry

L53 ↗

AlgebraicNumberTheory.Valuations.padicAbsoluteValueBaseMap_isometry

Documentation

The preceding rational embedding is an isometry.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory.Valuations
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem padicAbsoluteValueBaseMap_isometry :
    Isometry (padicAbsoluteValueBaseMap p)

def

padicAbsoluteValueCompletionRingHom

L60 ↗

AlgebraicNumberTheory.Valuations.padicAbsoluteValueCompletionRingHom

Documentation

The canonical ring homomorphism from the absolute-value completion of ℚ at p to the concrete p-adic field.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory.Valuations
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

def padicAbsoluteValueCompletionRingHom :
    (Rat.AbsoluteValue.padic p).Completion →+* ℚ_[p]

theorem

padicAbsoluteValueCompletionRingHom_coe

L69 ↗

AlgebraicNumberTheory.Valuations.padicAbsoluteValueCompletionRingHom_coe

Documentation

On the dense rational subring, the completed map agrees with the original p-adic embedding.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory.Valuations
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem padicAbsoluteValueCompletionRingHom_coe
    (x : WithAbs (Rat.AbsoluteValue.padic p)) :
    padicAbsoluteValueCompletionRingHom p
        (x : (Rat.AbsoluteValue.padic p).Completion) =
      padicAbsoluteValueBaseMap p x

theorem

padicAbsoluteValueCompletionRingHom_isometry

L79 ↗

AlgebraicNumberTheory.Valuations.padicAbsoluteValueCompletionRingHom_isometry

Documentation

The completed map remains an isometry.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory.Valuations
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem padicAbsoluteValueCompletionRingHom_isometry :
    Isometry (padicAbsoluteValueCompletionRingHom p)

theorem

padicAbsoluteValueCompletionRingHom_surjective

L85 ↗

AlgebraicNumberTheory.Valuations.padicAbsoluteValueCompletionRingHom_surjective

Documentation

The completed map is surjective because its closed range contains the dense copy of ℚ in ℚ_[p].

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory.Valuations
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem padicAbsoluteValueCompletionRingHom_surjective :
    Function.Surjective (padicAbsoluteValueCompletionRingHom p)

def

padicAbsoluteValueCompletionRingEquiv

L109 ↗

AlgebraicNumberTheory.Valuations.padicAbsoluteValueCompletionRingEquiv

Documentation

The absolute-value completion of ℚ at p is the concrete p-adic field.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory.Valuations
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

def padicAbsoluteValueCompletionRingEquiv :
    (Rat.AbsoluteValue.padic p).Completion ≃+* ℚ_[p]

def

padicAbsoluteValueCompletionAlgEquiv

L117 ↗

AlgebraicNumberTheory.Valuations.padicAbsoluteValueCompletionAlgEquiv

Documentation

The same comparison as a ℚ-algebra equivalence, in the form needed to transport the global cyclotomic local extension to the local cyclotomic theorem.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory.Valuations
variable (p : ℕ) [Fact p.Prime]

Lean source · full declaration

def padicAbsoluteValueCompletionAlgEquiv :
    (Rat.AbsoluteValue.padic p).Completion ≃ₐ[ℚ] ℚ_[p] where
  __ := padicAbsoluteValueCompletionRingEquiv p
  commutes' q := by
    change padicAbsoluteValueCompletionRingHom p
        (((WithAbs.equiv (Rat.AbsoluteValue.padic p)).symm q :
          WithAbs (Rat.AbsoluteValue.padic p)) :
            (Rat.AbsoluteValue.padic p).Completion) = (q : ℚ_[p])
    rw [padicAbsoluteValueCompletionRingHom_coe]
    rfl

theorem

padicAbsoluteValueCompletionAlgEquiv_coe

L131 ↗

AlgebraicNumberTheory.Valuations.padicAbsoluteValueCompletionAlgEquiv_coe

Documentation

On the dense rational subring, the completion algebra equivalence agrees with the original p-adic embedding.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory.Valuations
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem padicAbsoluteValueCompletionAlgEquiv_coe
    (x : WithAbs (Rat.AbsoluteValue.padic p)) :
    padicAbsoluteValueCompletionAlgEquiv p
        (x : (Rat.AbsoluteValue.padic p).Completion) =
      padicAbsoluteValueBaseMap p x

Module documentation

The p-adic completion used in the global cyclotomic argument

Declarations

The `p`-adic completion used in the global cyclotomic argument