Module

LocalizationRamificationGroups.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.LocalizationRamificationGroups

18 declarations indexed from sourceView source ↗

Module documentation

Localization of inertia and ramification groups

This file packages the decomposition-group equivalence of the localization and decomposition comparison as equivalences of the valuation-subring decomposition, inertia, and ramification groups. The difficult global-to-local implications use density of L in the algebraic localization, proved in RamificationTheory.HilbertRamification.LocalizationDensity.

Imports3

Imported by4

instance

irCompletionBaseAlgebra

L40 ↗

HilbertRamification.irCompletionBaseAlgebra

Source context 8 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
  [IsGalois K L]
section
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
  (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1)

Lean source · statement

instance irCompletionBaseAlgebra : Algebra K w.1.Completion

instance

irCompletionBaseSMul

L43 ↗

HilbertRamification.irCompletionBaseSMul

Source context 9 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
  [IsGalois K L]
section
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
  (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1)
local instance irCompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1

Lean source · statement

instance irCompletionBaseSMul : SMul K w.1.Completion

instance

irCompletionAlgebra

L46 ↗

HilbertRamification.irCompletionAlgebra

Source context 10 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
  [IsGalois K L]
section
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
  (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1)
local instance irCompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance irCompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul

Lean source · statement

instance irCompletionAlgebra : Algebra vK.Completion w.1.Completion

abbrev

localizationRamificationGroups_localization

L51 ↗

HilbertRamification.localizationRamificationGroups_localization

Documentation

The algebraic localization L K_v occurring in the localization and decomposition comparison.

Source context 11 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
  [IsGalois K L]
section
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
  (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1)
local instance irCompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance irCompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance irCompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2

Lean source · statement

abbrev localizationRamificationGroups_localization :
    IntermediateField vK.Completion w.1.Completion

abbrev

absoluteValueExtensionValuationSubring

L56 ↗

HilbertRamification.absoluteValueExtensionValuationSubring

Documentation

The valuation subring of L defined by w.

Source context 11 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
  [IsGalois K L]
section
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
  (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1)
local instance irCompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance irCompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance irCompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2

Lean source · statement

abbrev absoluteValueExtensionValuationSubring :
    _root_.ValuationSubring L

abbrev

algebraicLocalizationValuationSubring

L62 ↗

HilbertRamification.algebraicLocalizationValuationSubring

Documentation

The valuation subring of the algebraic localization defined by the extended absolute value.

Source context 11 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
  [IsGalois K L]
section
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
  (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1)
local instance irCompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance irCompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance irCompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2

Lean source · statement

abbrev algebraicLocalizationValuationSubring :
    _root_.ValuationSubring (localizationRamificationGroups_localization vK w)

theorem

mem_extensionValuationSubring_smul

L71 ↗

HilbertRamification.mem_extensionValuationSubring_smul

Source context 13 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
  [IsGalois K L]
section
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
  (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1)
local instance irCompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance irCompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance irCompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
include hvK
omit [IsGalois K L] in

Lean source · statement

theorem mem_extensionValuationSubring_smul
    (sigma : absoluteValueDecompositionGroup K w.1) :
    (sigma : L ≃ₐ[K] L) •
        absoluteValueExtensionValuationSubring vK w hw =
      absoluteValueExtensionValuationSubring vK w hw

def

localizationRamificationGroups_absoluteValueDecompositionGroupEquiv

L90 ↗

HilbertRamification.localizationRamificationGroups_absoluteValueDecompositionGroupEquiv

Documentation

The chosen-valuation decomposition group is the valuation-subring decomposition group attached to the same absolute value.

Source context 12 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
  [IsGalois K L]
section
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
  (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1)
local instance irCompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance irCompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance irCompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
include hvK

Lean source · full declaration

def localizationRamificationGroups_absoluteValueDecompositionGroupEquiv :
    absoluteValueDecompositionGroup K w.1 ≃*
      RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup K
        (absoluteValueExtensionValuationSubring vK w hw) where
  toFun sigma :=
    ⟨(sigma : L ≃ₐ[K] L),
      mem_extensionValuationSubring_smul vK (hvK := hvK) w hw sigma⟩
  invFun sigma := by
    refine ⟨(sigma : L ≃ₐ[K] L), ?_⟩
    intro x
    rw [← algebraicLocalizationDensity_mem_nonunits_iff_abs_lt_one w.1 hw,
      ← algebraicLocalizationDensity_mem_nonunits_iff_abs_lt_one w.1 hw]
    rw [_root_.ValuationSubring.mem_nonunits_iff_or,
      _root_.ValuationSubring.mem_nonunits_iff_or]
    have hmem (y : L) :
        (sigma : L ≃ₐ[K] L) y ∈
            absoluteValueExtensionValuationSubring vK w hw ↔
          y ∈ absoluteValueExtensionValuationSubring vK w hw := by
      have h := congrArg
        (fun A : _root_.ValuationSubring L ↦
          (sigma : L ≃ₐ[K] L) y ∈ A) sigma.property
      have h' :
          (y ∈ absoluteValueExtensionValuationSubring vK w hw) =
            ((sigma : L ≃ₐ[K] L) y ∈
              absoluteValueExtensionValuationSubring vK w hw) := by
        simpa [_root_.ValuationSubring.mem_pointwise_smul_iff_inv_smul_mem,
          AlgEquiv.smul_def] using h
      exact Eq.to_iff h'.symm
    have hinv :
        ((sigma : L ≃ₐ[K] L) x)⁻¹ ∈
            absoluteValueExtensionValuationSubring vK w hw ↔
          x⁻¹ ∈ absoluteValueExtensionValuationSubring vK w hw := by
      simpa only [map_inv₀] using hmem x⁻¹
    constructor
    · rintro (hzero | hnot)
      · exact Or.inl ((sigma : L ≃ₐ[K] L).injective (by simpa using hzero))
      · exact Or.inr (fun hx ↦ hnot (hinv.mpr hx))
    · rintro (hzero | hnot)
      · subst x
        exact Or.inl (map_zero (sigma : L ≃ₐ[K] L))
      · exact Or.inr (fun hx ↦ hnot (hinv.mp hx))
  left_inv sigma := by
    apply Subtype.ext
    rfl
  right_inv sigma := by
    apply Subtype.ext
    rfl
  map_mul' sigma tau := by
    apply Subtype.ext
    rfl

theorem

local_mem_localizationValuationSubring_smul

L141 ↗

HilbertRamification.local_mem_localizationValuationSubring_smul

Source context 12 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
  [IsGalois K L]
section
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
  (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1)
local instance irCompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance irCompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance irCompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
include hvK

Lean source · statement

theorem local_mem_localizationValuationSubring_smul
    (tau : localizationRamificationGroups_localization vK w ≃ₐ[vK.Completion]
      localizationRamificationGroups_localization vK w) :
    tau • algebraicLocalizationValuationSubring vK w hw =
      algebraicLocalizationValuationSubring vK w hw

def

localizationRamificationGroups_localDecompositionGroupEquiv

L159 ↗

HilbertRamification.localizationRamificationGroups_localDecompositionGroupEquiv

Documentation

Every automorphism of the localization over K_v belongs to its valuation-subring decomposition group.

Source context 12 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
  [IsGalois K L]
section
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
  (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1)
local instance irCompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance irCompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance irCompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
include hvK

Lean source · full declaration

def localizationRamificationGroups_localDecompositionGroupEquiv :
    (localizationRamificationGroups_localization vK w ≃ₐ[vK.Completion]
      localizationRamificationGroups_localization vK w) ≃*
      RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup vK.Completion
        (algebraicLocalizationValuationSubring vK w hw) where
  toFun tau :=
    ⟨tau, local_mem_localizationValuationSubring_smul
      vK (hvK := hvK) w hw tau⟩
  invFun tau := tau
  left_inv tau := rfl
  right_inv tau := by
    apply Subtype.ext
    rfl
  map_mul' sigma tau := by
    apply Subtype.ext
    rfl

def

localizationRamificationGroups_valuationDecompositionGroupEquiv

L177 ↗

HilbertRamification.localizationRamificationGroups_valuationDecompositionGroupEquiv

Documentation

The localization and decomposition comparison for valuation-subring decomposition groups.

Source context 12 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
  [IsGalois K L]
section
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
  (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1)
local instance irCompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance irCompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance irCompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
include hvK

Lean source · statement

def localizationRamificationGroups_valuationDecompositionGroupEquiv :
    RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup K
        (absoluteValueExtensionValuationSubring vK w hw) ≃*
      RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup vK.Completion
        (algebraicLocalizationValuationSubring vK w hw)

theorem

localizationRamificationGroups_valuationDecompositionGroupEquiv_toLocalization

L188 ↗

HilbertRamification.localizationRamificationGroups_valuationDecompositionGroupEquiv_toLocalization

Source context 12 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
  [IsGalois K L]
section
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
  (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1)
local instance irCompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance irCompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance irCompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
include hvK

Lean source · statement

theorem localizationRamificationGroups_valuationDecompositionGroupEquiv_toLocalization
    (sigma : RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup K
      (absoluteValueExtensionValuationSubring vK w hw))
    (x : L) :
    (((localizationRamificationGroups_valuationDecompositionGroupEquiv
        vK (hvK := hvK) w hw sigma :
        RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup vK.Completion
          (algebraicLocalizationValuationSubring vK w hw)) :
        localizationRamificationGroups_localization vK w ≃ₐ[vK.Completion]
          localizationRamificationGroups_localization vK w)
      (AbsoluteValue.toAlgebraicLocalization vK w.1 w.2 x)) =
      AbsoluteValue.toAlgebraicLocalization vK w.1 w.2
        ((sigma : L ≃ₐ[K] L) x)

theorem

localizationRamificationGroups_valuationDecompositionGroupEquiv_mem_inertia_iff

L209 ↗

HilbertRamification.localizationRamificationGroups_valuationDecompositionGroupEquiv_mem_inertia_iff

Documentation

The decomposition-group equivalence carries inertia precisely to inertia. The global-to-local implication is the residue-density argument; the converse is restriction along L → L K_v.

Source context 12 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
  [IsGalois K L]
section
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
  (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1)
local instance irCompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance irCompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance irCompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
include hvK

Lean source · statement

theorem localizationRamificationGroups_valuationDecompositionGroupEquiv_mem_inertia_iff
    (sigma : RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup K
      (absoluteValueExtensionValuationSubring vK w hw)) :
    localizationRamificationGroups_valuationDecompositionGroupEquiv
        vK (hvK := hvK) w hw sigma ∈
        RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup vK.Completion
          (algebraicLocalizationValuationSubring vK w hw) ↔
      sigma ∈ RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup K
        (absoluteValueExtensionValuationSubring vK w hw)

def

inertiaGroupEquivAlgebraicLocalization

L279 ↗

HilbertRamification.inertiaGroupEquivAlgebraicLocalization

Documentation

The localization and decomposition comparison for inertia groups.

Source context 12 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
  [IsGalois K L]
section
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
  (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1)
local instance irCompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance irCompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance irCompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
include hvK

Lean source · full declaration

def inertiaGroupEquivAlgebraicLocalization :
    RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup K
        (absoluteValueExtensionValuationSubring vK w hw) ≃*
      RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup vK.Completion
        (algebraicLocalizationValuationSubring vK w hw) where
  toFun sigma :=
    ⟨localizationRamificationGroups_valuationDecompositionGroupEquiv
        vK (hvK := hvK) w hw sigma,
      (localizationRamificationGroups_valuationDecompositionGroupEquiv_mem_inertia_iff
        vK hvK w hw sigma).mpr sigma.property⟩
  invFun tau := by
    let sigma := (localizationRamificationGroups_valuationDecompositionGroupEquiv
      vK (hvK := hvK) w hw).symm
        (tau : (open _root_.RamificationTheory.HilbertRamification.ValuationSubring in
          decompositionGroup vK.Completion
            (algebraicLocalizationValuationSubring vK w hw)))
    refine ⟨sigma, ?_⟩
    apply (localizationRamificationGroups_valuationDecompositionGroupEquiv_mem_inertia_iff
      vK hvK w hw sigma).mp
    simp [sigma, tau.property]
  left_inv sigma := by
    apply Subtype.ext
    exact (localizationRamificationGroups_valuationDecompositionGroupEquiv
      vK (hvK := hvK) w hw).symm_apply_apply sigma
  right_inv tau := by
    apply Subtype.ext
    exact (localizationRamificationGroups_valuationDecompositionGroupEquiv
      vK (hvK := hvK) w hw).apply_symm_apply tau
  map_mul' sigma tau := by
    apply Subtype.ext
    exact map_mul (localizationRamificationGroups_valuationDecompositionGroupEquiv
      vK (hvK := hvK) w hw)
        (sigma : RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup K
          (absoluteValueExtensionValuationSubring vK w hw))
        (tau : RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup K
          (absoluteValueExtensionValuationSubring vK w hw))

theorem

localizationRamificationGroups_inertiaGroupEquiv_toLocalization

L316 ↗

HilbertRamification.localizationRamificationGroups_inertiaGroupEquiv_toLocalization

Source context 12 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
  [IsGalois K L]
section
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
  (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1)
local instance irCompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance irCompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance irCompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
include hvK

Lean source · statement

theorem localizationRamificationGroups_inertiaGroupEquiv_toLocalization
    (sigma : RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup K
      (absoluteValueExtensionValuationSubring vK w hw))
    (x : L) :
    ((((inertiaGroupEquivAlgebraicLocalization vK hvK w hw sigma :
          RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup vK.Completion
            (algebraicLocalizationValuationSubring vK w hw)) :
          RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup vK.Completion
            (algebraicLocalizationValuationSubring vK w hw)) :
          localizationRamificationGroups_localization vK w ≃ₐ[vK.Completion]
            localizationRamificationGroups_localization vK w)
        (AbsoluteValue.toAlgebraicLocalization vK w.1 w.2 x)) =
      AbsoluteValue.toAlgebraicLocalization vK w.1 w.2
        (((sigma : RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup K
          (absoluteValueExtensionValuationSubring vK w hw)) :
            L ≃ₐ[K] L) x)

theorem

localizationRamificationGroups_inertiaGroupEquiv_mem_ramification_iff

L338 ↗

HilbertRamification.localizationRamificationGroups_inertiaGroupEquiv_mem_ramification_iff

Documentation

The inertia-group equivalence carries ramification precisely to ramification. The global-to-local implication uses density modulo principal units; the converse follows by restricting unit quotients.

Source context 12 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
  [IsGalois K L]
section
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
  (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1)
local instance irCompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance irCompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance irCompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
include hvK

Lean source · statement

theorem localizationRamificationGroups_inertiaGroupEquiv_mem_ramification_iff
    (sigma : RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup K
      (absoluteValueExtensionValuationSubring vK w hw)) :
    inertiaGroupEquivAlgebraicLocalization vK hvK w hw sigma ∈
        RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroup vK.Completion
          (algebraicLocalizationValuationSubring vK w hw) ↔
      sigma ∈ RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroup K
        (absoluteValueExtensionValuationSubring vK w hw)

def

localizationRamificationGroups_ramificationGroupEquiv

L421 ↗

HilbertRamification.localizationRamificationGroups_ramificationGroupEquiv

Documentation

The localization and decomposition comparison for ramification groups.

Source context 12 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
  [IsGalois K L]
section
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
  (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1)
local instance irCompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance irCompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance irCompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
include hvK

Lean source · full declaration

def localizationRamificationGroups_ramificationGroupEquiv :
    RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroup K
        (absoluteValueExtensionValuationSubring vK w hw) ≃*
      RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroup vK.Completion
        (algebraicLocalizationValuationSubring vK w hw) where
  toFun sigma :=
    ⟨inertiaGroupEquivAlgebraicLocalization vK hvK w hw sigma,
      (localizationRamificationGroups_inertiaGroupEquiv_mem_ramification_iff
        vK hvK w hw sigma).mpr sigma.property⟩
  invFun tau := by
    let sigma := (inertiaGroupEquivAlgebraicLocalization vK hvK w hw).symm
      (tau : RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup vK.Completion
        (algebraicLocalizationValuationSubring vK w hw))
    refine ⟨sigma, ?_⟩
    apply (localizationRamificationGroups_inertiaGroupEquiv_mem_ramification_iff
      vK hvK w hw sigma).mp
    simp [sigma, tau.property]
  left_inv sigma := by
    apply Subtype.ext
    exact (inertiaGroupEquivAlgebraicLocalization
      vK hvK w hw).symm_apply_apply sigma
  right_inv tau := by
    apply Subtype.ext
    exact (inertiaGroupEquivAlgebraicLocalization
      vK hvK w hw).apply_symm_apply tau
  map_mul' sigma tau := by
    apply Subtype.ext
    exact map_mul (inertiaGroupEquivAlgebraicLocalization vK hvK w hw)
      (sigma : RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup K
        (absoluteValueExtensionValuationSubring vK w hw))
      (tau : RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup K
        (absoluteValueExtensionValuationSubring vK w hw))

theorem

localizationRamificationGroups_ramificationGroupEquiv_toLocalization

L454 ↗

HilbertRamification.localizationRamificationGroups_ramificationGroupEquiv_toLocalization

Source context 12 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
  [IsGalois K L]
section
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
  (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1)
local instance irCompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance irCompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance irCompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
include hvK

Lean source · full declaration

theorem localizationRamificationGroups_ramificationGroupEquiv_toLocalization
    (sigma : RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroup K
      (absoluteValueExtensionValuationSubring vK w hw))
    (x : L) :
    ((show localizationRamificationGroups_localization vK w ≃ₐ[vK.Completion]
          localizationRamificationGroups_localization vK w from
        (((localizationRamificationGroups_ramificationGroupEquiv vK hvK w hw sigma :
            RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroup vK.Completion
              (algebraicLocalizationValuationSubring vK w hw)) :
            RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup vK.Completion
              (algebraicLocalizationValuationSubring vK w hw)) :
            RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup vK.Completion
              (algebraicLocalizationValuationSubring vK w hw)))
        (AbsoluteValue.toAlgebraicLocalization vK w.1 w.2 x)) =
      AbsoluteValue.toAlgebraicLocalization vK w.1 w.2
        ((show L ≃ₐ[K] L from
          ((sigma : RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup K
            (absoluteValueExtensionValuationSubring vK w hw)) :
            RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup K
              (absoluteValueExtensionValuationSubring vK w hw))) x) :=
  localizationRamificationGroups_inertiaGroupEquiv_toLocalization
    vK hvK w hw sigma x

Module documentation

Localization of inertia and ramification groups

Declarations