Module

PadicLocalization.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.PadicLocalization

5 declarations indexed from sourceView source ↗

Module documentation

Localizations at rational p-adic absolute values

This file collects the reusable algebra, finiteness, Galois, and nonarchimedean facts needed to compare a global algebraic localization with an extension of ℚ_[p].

Imports7

Imported by4

def

transportedAlgebraAlongRingEquiv

L30 ↗

HilbertRamification.transportedAlgebraAlongRingEquiv

Documentation

Transport an algebra structure across an equivalence of its base ring.

Source context 3 commands

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

noncomputable section
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations

Lean source · statement

def transportedAlgebraAlongRingEquiv
    {K K' E : Type*} [CommSemiring K] [CommSemiring K'] [CommSemiring E]
    [Algebra K E] (e : K ≃+* K') : Algebra K' E

theorem

transportedAlgebraAlongRingEquiv_algebraMap

L38 ↗

HilbertRamification.transportedAlgebraAlongRingEquiv_algebraMap

Documentation

The transported algebra map is the original algebra map precomposed with the inverse base-ring equivalence.

Source context 3 commands

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

noncomputable section
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations

Lean source · statement

theorem transportedAlgebraAlongRingEquiv_algebraMap
    {K K' E : Type*} [CommSemiring K] [CommSemiring K'] [CommSemiring E]
    [Algebra K E] (e : K ≃+* K') (x : K') :
    @algebraMap K' E _ _ (transportedAlgebraAlongRingEquiv e) x =
      algebraMap K E (e.symm x)

theorem

globalPadicLocalizationModuleFinite

L51 ↗

HilbertRamification.globalPadicLocalizationModuleFinite

Documentation

The localization of a finite global extension is finite over the completed base field.

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 · full declaration

theorem globalPadicLocalizationModuleFinite
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) L) :
    let vK := Rat.AbsoluteValue.padic p
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := ℚ) w.1
    letI : SMul ℚ w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    Module.Finite vK.Completion
      (AbsoluteValue.algebraicLocalization vK w.1 w.2) := by
  let vK := Rat.AbsoluteValue.padic p
  let hvK := padicAbsoluteValue_isNontrivial p
  let hK := AbsoluteValue.extensionCompletionAlgebra (K := ℚ) w.1
  let : SMul ℚ w.1.Completion := hK.toSMul
  let := AbsoluteValue.completionAlgebra vK w.1 w.2
  let E := AbsoluteValue.algebraicLocalization vK w.1 w.2
  let : Module.Finite vK.Completion w.1.Completion :=
    completionModuleFinite vK hvK w
  exact FiniteDimensional.of_injective E.val.toLinearMap E.val.injective

theorem

globalPadicLocalization_isAbelianGalois

L72 ↗

HilbertRamification.globalPadicLocalization_isAbelianGalois

Documentation

The localization of a finite abelian global extension is abelian Galois over the completed base.

Source context 6 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]
omit [FiniteDimensional ℚ L] in

Lean source · full declaration

theorem globalPadicLocalization_isAbelianGalois
    (w : AbsoluteValueExtension (Rat.AbsoluteValue.padic p) L) :
    let vK := Rat.AbsoluteValue.padic p
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := ℚ) w.1
    letI : SMul ℚ w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    IsAbelianGalois vK.Completion
      (AbsoluteValue.algebraicLocalization vK w.1 w.2) := by
  let vK := Rat.AbsoluteValue.padic p
  let hvK := padicAbsoluteValue_isNontrivial p
  let hK := AbsoluteValue.extensionCompletionAlgebra (K := ℚ) w.1
  let : SMul ℚ w.1.Completion := hK.toSMul
  let := AbsoluteValue.completionAlgebra vK w.1 w.2
  let E := AbsoluteValue.algebraicLocalization vK w.1 w.2
  let : IsGalois vK.Completion E :=
    algebraicLocalization_isGalois vK w
  let e := decompositionGroupEquivAlgebraicLocalizationAut vK hvK w
  exact
    { is_comm.comm := fun σ τ ↦ by
        apply e.symm.injective
        rw [map_mul, map_mul]
        apply Subtype.ext
        exact
          (inferInstance :
            IsMulCommutative (L ≃ₐ[ℚ] L)).is_comm.comm _ _
    }

theorem

rationalPadicAbsoluteValue_nonarchimedean

L101 ↗

HilbertRamification.rationalPadicAbsoluteValue_nonarchimedean

Documentation

The rational p-adic absolute value is nonarchimedean in the bounded natural-number sense used by the ramification API.

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 rationalPadicAbsoluteValue_nonarchimedean :
    LubinTate.Valuations.NonarchimedeanAbsoluteValue
      (Rat.AbsoluteValue.padic p)

Module documentation

Localizations at rational p-adic absolute values

Declarations

transportedAlgebraAlongRingEquiv

transportedAlgebraAlongRingEquiv_algebraMap

globalPadicLocalizationModuleFinite

globalPadicLocalization_isAbelianGalois

rationalPadicAbsoluteValue_nonarchimedean