Module

LocalizationDensity.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.LocalizationDensity

21 declarations indexed from sourceView source ↗

Module documentation

Localization and decomposition comparison through density

For an infinite algebraic extension, the canonical L_w is the algebraic localization L K_v, not the whole metric completion. This file records the density consequences needed to transport inertia and ramification conditions between L and L_w. None of the results below assumes finite degree.

Imports14

Imported by3

theorem

algebraicLocalizationDensity_mem_nonunits_iff_abs_lt_one

L50 ↗

HilbertRamification.algebraicLocalizationDensity_mem_nonunits_iff_abs_lt_one

Documentation

For the valuation subring attached to a nonarchimedean absolute value, the ambient-field nonunits are exactly the open unit ball.

Source context 8 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section AbsoluteValuePrincipalUnits
variable {F : Type*} [Field F]

Lean source · statement

theorem algebraicLocalizationDensity_mem_nonunits_iff_abs_lt_one
    (a : AbsoluteValue F ℝ) (ha : LubinTate.Valuations.NonarchimedeanAbsoluteValue a)
    (x : F) :
    x ∈ (absoluteValueValuationSubring a ha).nonunits ↔
      a x < 1

theorem

algebraicLocalizationDensity_mem_principalUnitGroup_iff_abs_lt_one

L74 ↗

HilbertRamification.algebraicLocalizationDensity_mem_principalUnitGroup_iff_abs_lt_one

Documentation

Principal-unit membership in an absolute-value valuation subring is the strict-unit inequality |u - 1| < 1.

Source context 8 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section AbsoluteValuePrincipalUnits
variable {F : Type*} [Field F]

Lean source · statement

theorem algebraicLocalizationDensity_mem_principalUnitGroup_iff_abs_lt_one
    (a : AbsoluteValue F ℝ) (ha : LubinTate.Valuations.NonarchimedeanAbsoluteValue a)
    (x : Fˣ) :
    x ∈ (absoluteValueValuationSubring a ha).principalUnitGroup ↔
      a ((x : F) - 1) < 1

theorem

mem_inertiaGroup_iff_sub_mem_nonunits

L90 ↗

HilbertRamification.ValuationSubring.mem_inertiaGroup_iff_sub_mem_nonunits

Documentation

Inertia membership as the congruence sigma x = x modulo the maximal ideal for every integral element.

Source context 7 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
namespace ValuationSubring

Lean source · statement

theorem mem_inertiaGroup_iff_sub_mem_nonunits
    {F : Type*} {E : Type*} [Field F] [Field E] [Algebra F E]
    (A : _root_.ValuationSubring E) (sigma : decompositionGroup F A) :
    sigma ∈ inertiaGroup F A ↔
      ∀ x : A,
        ((sigma : E ≃ₐ[F] E) (x : E) - (x : E)) ∈ A.nonunits

instance

completionBaseAlgebra

L127 ↗

HilbertRamification.completionBaseAlgebra

Source context 9 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section Localization
variable (vK : AbsoluteValue K ℝ)
variable (w : AbsoluteValueExtension vK L)

Lean source · statement

instance completionBaseAlgebra : Algebra K w.1.Completion

instance

completionBaseSMul

L130 ↗

HilbertRamification.completionBaseSMul

Source context 10 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section Localization
variable (vK : AbsoluteValue K ℝ)
variable (w : AbsoluteValueExtension vK L)
local instance completionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1

Lean source · statement

instance completionBaseSMul : SMul K w.1.Completion

instance

completionAlgebra

L133 ↗

HilbertRamification.completionAlgebra

Source context 11 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section Localization
variable (vK : AbsoluteValue K ℝ)
variable (w : AbsoluteValueExtension vK L)
local instance completionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance completionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul

Lean source · statement

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

abbrev

localization

L136 ↗

HilbertRamification.localization

Source context 12 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section Localization
variable (vK : AbsoluteValue K ℝ)
variable (w : AbsoluteValueExtension vK L)
local instance completionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance completionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance completionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2

Lean source · statement

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

abbrev

toLocalization

L139 ↗

HilbertRamification.toLocalization

Source context 12 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section Localization
variable (vK : AbsoluteValue K ℝ)
variable (w : AbsoluteValueExtension vK L)
local instance completionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance completionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance completionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2

Lean source · statement

abbrev toLocalization : L →+* localization vK w

abbrev

localizationAbsoluteValue

L142 ↗

HilbertRamification.localizationAbsoluteValue

Source context 12 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section Localization
variable (vK : AbsoluteValue K ℝ)
variable (w : AbsoluteValueExtension vK L)
local instance completionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance completionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance completionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2

Lean source · statement

abbrev localizationAbsoluteValue :
    AbsoluteValue (localization vK w) ℝ

theorem

algebraicLocalizationDensity_localization_exists_close

L149 ↗

HilbertRamification.algebraicLocalizationDensity_localization_exists_close

Documentation

The dense copy of L approximates every element of the algebraic localization. This is the common source for residue and principal-unit transport in the localization and decomposition comparison.

Source context 12 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section Localization
variable (vK : AbsoluteValue K ℝ)
variable (w : AbsoluteValueExtension vK L)
local instance completionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance completionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance completionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2

Lean source · statement

theorem algebraicLocalizationDensity_localization_exists_close
    (z : localization vK w) {epsilon : ℝ} (hepsilon : 0 < epsilon) :
    ∃ x : L,
      localizationAbsoluteValue vK w (z - toLocalization vK w x) < epsilon

theorem

algebraicLocalizationDensity_localization_nonarchimedean

L164 ↗

HilbertRamification.algebraicLocalizationDensity_localization_nonarchimedean

Documentation

Nonarchimedeanness passes from w to the absolute value on L K_v. The bounded-natural-number definition makes this a direct consequence of the restriction formula on the dense copy of L.

Source context 12 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section Localization
variable (vK : AbsoluteValue K ℝ)
variable (w : AbsoluteValueExtension vK L)
local instance completionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance completionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance completionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2

Lean source · statement

theorem algebraicLocalizationDensity_localization_nonarchimedean
    (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1) :
    LubinTate.Valuations.NonarchimedeanAbsoluteValue (localizationAbsoluteValue vK w)

abbrev

extensionValuationSubring

L173 ↗

HilbertRamification.extensionValuationSubring

Source context 12 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section Localization
variable (vK : AbsoluteValue K ℝ)
variable (w : AbsoluteValueExtension vK L)
local instance completionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance completionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance completionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2

Lean source · statement

abbrev extensionValuationSubring
    (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1) :
    _root_.ValuationSubring L

abbrev

localizationValuationSubring

L178 ↗

HilbertRamification.localizationValuationSubring

Source context 12 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section Localization
variable (vK : AbsoluteValue K ℝ)
variable (w : AbsoluteValueExtension vK L)
local instance completionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance completionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance completionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2

Lean source · statement

abbrev localizationValuationSubring
    (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1) :
    _root_.ValuationSubring (localization vK w)

theorem

algebraicLocalizationDensity_localizationValuationSubring_comap

L188 ↗

HilbertRamification.algebraicLocalizationDensity_localizationValuationSubring_comap

Documentation

The valuation subring on L K_v pulls back to the valuation subring on L. This is the concrete valuation-ring square used by the conjugation and base-change law in the localization specialization.

Source context 12 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section Localization
variable (vK : AbsoluteValue K ℝ)
variable (w : AbsoluteValueExtension vK L)
local instance completionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance completionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance completionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2

Lean source · statement

theorem algebraicLocalizationDensity_localizationValuationSubring_comap
    (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1) :
    (localizationValuationSubring vK w hw).comap (toLocalization vK w) =
      extensionValuationSubring vK w hw

theorem

algebraicLocalizationDensity_localizationAbsoluteValue_algEquiv

L201 ↗

HilbertRamification.algebraicLocalizationDensity_localizationAbsoluteValue_algEquiv

Documentation

Every automorphism of the algebraic localization over K_v preserves its unique extended absolute value. This is the isometry source used when transporting strict congruences from the dense copy of L.

Source context 12 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section Localization
variable (vK : AbsoluteValue K ℝ)
variable (w : AbsoluteValueExtension vK L)
local instance completionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance completionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance completionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2

Lean source · statement

theorem algebraicLocalizationDensity_localizationAbsoluteValue_algEquiv
    [Algebra.IsAlgebraic K L]
    (hvK : vK.IsNontrivial)
    (tau : localization vK w ≃ₐ[vK.Completion] localization vK w)
    (z : localization vK w) :
    localizationAbsoluteValue vK w (tau z) =
      localizationAbsoluteValue vK w z

theorem

algebraicLocalizationDensity_localization_exists_residueRepresentative

L236 ↗

HilbertRamification.algebraicLocalizationDensity_localization_exists_residueRepresentative

Documentation

Every integral element of L K_v has the same residue as an integral element from L. The displayed strict inequality is the source form of surjectivity on residue fields and avoids choosing a quotient model.

Source context 12 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section Localization
variable (vK : AbsoluteValue K ℝ)
variable (w : AbsoluteValueExtension vK L)
local instance completionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance completionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance completionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2

Lean source · statement

theorem algebraicLocalizationDensity_localization_exists_residueRepresentative
    (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1)
    (z : localizationValuationSubring vK w hw) :
    ∃ x : extensionValuationSubring vK w hw,
      localizationAbsoluteValue vK w
          ((z : localization vK w) -
            toLocalization vK w (x : L)) < 1

theorem

algebraicLocalizationDensity_localization_mem_inertia_of_commutes

L280 ↗

HilbertRamification.algebraicLocalizationDensity_localization_mem_inertia_of_commutes

Documentation

The difficult direction of inertia transport in the localization and decomposition comparison. An automorphism of L K_v whose restriction is inertial on L is inertial on the whole localization. Density supplies an integral representative of each residue class.

Source context 12 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section Localization
variable (vK : AbsoluteValue K ℝ)
variable (w : AbsoluteValueExtension vK L)
local instance completionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance completionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance completionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2

Lean source · statement

theorem algebraicLocalizationDensity_localization_mem_inertia_of_commutes
    [Algebra.IsAlgebraic K L]
    (hvK : vK.IsNontrivial)
    (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1)
    (tau : RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup vK.Completion
      (localizationValuationSubring vK w hw))
    (sigma : RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup K
      (extensionValuationSubring vK w hw))
    (hcomm : ∀ x : L,
      ((tau : localization vK w ≃ₐ[vK.Completion] localization vK w)
          (toLocalization vK w x)) =
        toLocalization vK w
          ((sigma : L ≃ₐ[K] L) x))
    (hsigma : sigma ∈ RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup K
      (extensionValuationSubring vK w hw)) :
    tau ∈ RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup vK.Completion
      (localizationValuationSubring vK w hw)

theorem

algebraicLocalizationDensity_localization_exists_principalUnitRepresentative_abs

L354 ↗

HilbertRamification.algebraicLocalizationDensity_localization_exists_principalUnitRepresentative_abs

Documentation

Every nonzero element of L K_v is congruent modulo principal units to an element from Lˣ. The equality of absolute values is included because it is the value-group transport used in the ramification argument.

Source context 12 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section Localization
variable (vK : AbsoluteValue K ℝ)
variable (w : AbsoluteValueExtension vK L)
local instance completionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance completionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance completionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2

Lean source · statement

theorem algebraicLocalizationDensity_localization_exists_principalUnitRepresentative_abs
    (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1)
    (z : (localization vK w)ˣ) :
    ∃ x : Lˣ,
      localizationAbsoluteValue vK w
          (toLocalization vK w (x : L)) =
        localizationAbsoluteValue vK w (z : localization vK w) ∧
      localizationAbsoluteValue vK w
          ((z : localization vK w) /
            toLocalization vK w (x : L) - 1) < 1

theorem

algebraicLocalizationDensity_localization_exists_principalUnitRepresentative

L409 ↗

HilbertRamification.algebraicLocalizationDensity_localization_exists_principalUnitRepresentative

Documentation

Quotient formulation of the preceding approximation: the natural map Lˣ / U_L¹ → (L K_v)ˣ / U_{L K_v}¹ is surjective on representatives.

Source context 12 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section Localization
variable (vK : AbsoluteValue K ℝ)
variable (w : AbsoluteValueExtension vK L)
local instance completionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance completionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance completionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2

Lean source · statement

theorem algebraicLocalizationDensity_localization_exists_principalUnitRepresentative
    (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1)
    (z : (localization vK w)ˣ) :
    ∃ x : Lˣ,
      z / Units.map (toLocalization vK w) x ∈
        (localizationValuationSubring vK w hw).principalUnitGroup

theorem

algebraicLocalizationDensity_localization_principalUnit_map

L424 ↗

HilbertRamification.algebraicLocalizationDensity_localization_principalUnit_map

Documentation

The dense embedding L → L K_v sends global principal units to local principal units.

Source context 12 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section Localization
variable (vK : AbsoluteValue K ℝ)
variable (w : AbsoluteValueExtension vK L)
local instance completionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance completionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance completionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2

Lean source · statement

theorem algebraicLocalizationDensity_localization_principalUnit_map
    (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1)
    (x : Lˣ)
    (hx : x ∈ (extensionValuationSubring vK w hw).principalUnitGroup) :
    Units.map (toLocalization vK w) x ∈
      (localizationValuationSubring vK w hw).principalUnitGroup

theorem

algebraicLocalizationDensity_localization_mem_ramification_of_commutes

L450 ↗

HilbertRamification.algebraicLocalizationDensity_localization_mem_ramification_of_commutes

Documentation

The difficult direction of ramification transport in the localization and decomposition comparison. Once the restrictions commute, an automorphism ramified-trivially on every global multiplicative class is ramified-trivially on every local class. Surjectivity modulo principal units is the essential density input.

Source context 12 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section Localization
variable (vK : AbsoluteValue K ℝ)
variable (w : AbsoluteValueExtension vK L)
local instance completionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance completionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance completionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2

Lean source · statement

theorem algebraicLocalizationDensity_localization_mem_ramification_of_commutes
    [Algebra.IsAlgebraic K L]
    (hvK : vK.IsNontrivial)
    (hw : LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1)
    (tau : RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup vK.Completion
      (localizationValuationSubring vK w hw))
    (sigma : RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup K
      (extensionValuationSubring vK w hw))
    (hcomm : ∀ x : L,
      (((tau : RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup
        vK.Completion
          (localizationValuationSubring vK w hw)) :
            localization vK w ≃ₐ[vK.Completion] localization vK w)
          (toLocalization vK w x)) =
        toLocalization vK w
          ((((sigma : RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup K
            (extensionValuationSubring vK w hw)) : L ≃ₐ[K] L) x)))
    (hsigma : sigma ∈ RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroup K
      (extensionValuationSubring vK w hw)) :
    tau ∈ RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroup vK.Completion
      (localizationValuationSubring vK w hw)

Module documentation

Localization and decomposition comparison through density

Declarations