Module

DecompositionFieldLocalization.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.DecompositionFieldLocalization

31 declarations indexed from sourceView source ↗

Module documentation

Decomposition-field value and residue comparison

This file identifies the decomposition field with the literal intersection L ∩ K_v inside the algebraic localization L_w. It then records the canonical residue-field isomorphism and equality of absolute-value ranges in the nonarchimedean case.

Imports6

Imported by4

instance

proposition98CompletionBaseAlgebra

L41 ↗

HilbertRamification.proposition98CompletionBaseAlgebra

Source context 8 commands

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

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

Lean source · statement

instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion

instance

proposition98CompletionBaseSMul

L44 ↗

HilbertRamification.proposition98CompletionBaseSMul

Source context 9 commands

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

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

Lean source · statement

instance proposition98CompletionBaseSMul : SMul K w.1.Completion

instance

proposition98CompletionAlgebra

L47 ↗

HilbertRamification.proposition98CompletionAlgebra

Source context 10 commands

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

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

Lean source · statement

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

abbrev

localization

L50 ↗

HilbertRamification.localization

Source context 11 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section LocalizationGalois
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
local instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance proposition98CompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance proposition98CompletionAlgebra : 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

L53 ↗

HilbertRamification.toLocalization

Source context 11 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section LocalizationGalois
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
local instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance proposition98CompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance proposition98CompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2

Lean source · statement

abbrev toLocalization : L →+* localization vK w

instance

proposition98LocalizationBaseAlgebra

L56 ↗

HilbertRamification.proposition98LocalizationBaseAlgebra

Source context 11 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section LocalizationGalois
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
local instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance proposition98CompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance proposition98CompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2

Lean source · statement

instance proposition98LocalizationBaseAlgebra : Algebra K (localization vK w)

instance

proposition98LocalizationScalarTower

L60 ↗

HilbertRamification.proposition98LocalizationScalarTower

Source context 12 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section LocalizationGalois
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
local instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance proposition98CompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance proposition98CompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
local instance proposition98LocalizationBaseAlgebra : Algebra K (localization vK w) :=
  ((algebraMap vK.Completion (localization vK w)).comp
    (algebraMap K vK.Completion)).toAlgebra

Lean source · statement

instance proposition98LocalizationScalarTower :
    IsScalarTower K vK.Completion (localization vK w)

def

decompositionField_toLocalizationAlgHom

L68 ↗

HilbertRamification.decompositionField_toLocalizationAlgHom

Documentation

The dense copy of L in the localization, as a K-algebra embedding for the scalar tower K → K_v → L_w.

Source context 13 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section LocalizationGalois
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
local instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance proposition98CompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance proposition98CompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
local instance proposition98LocalizationBaseAlgebra : Algebra K (localization vK w) :=
  ((algebraMap vK.Completion (localization vK w)).comp
    (algebraMap K vK.Completion)).toAlgebra
local instance proposition98LocalizationScalarTower :
    IsScalarTower K vK.Completion (localization vK w) :=
  IsScalarTower.of_algebraMap_eq' (by
    ext x
    rfl)

Lean source · full declaration

def decompositionField_toLocalizationAlgHom :
    L →ₐ[K] localization vK w where
  __ := toLocalization vK w
  commutes' x := AbsoluteValue.toAlgebraicLocalization_algebraMap vK w.1 w.2 x

theorem

decompositionField_localization_adjoin_range_eq_top

L76 ↗

HilbertRamification.decompositionField_localization_adjoin_range_eq_top

Documentation

The localization is generated over K_v by the subtype-valued copy of L, not only by its ambient-completion representatives.

Source context 14 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section LocalizationGalois
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
local instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance proposition98CompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance proposition98CompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
local instance proposition98LocalizationBaseAlgebra : Algebra K (localization vK w) :=
  ((algebraMap vK.Completion (localization vK w)).comp
    (algebraMap K vK.Completion)).toAlgebra
local instance proposition98LocalizationScalarTower :
    IsScalarTower K vK.Completion (localization vK w) :=
  IsScalarTower.of_algebraMap_eq' (by
    ext x
    rfl)
omit [IsGalois K L] in

Lean source · statement

theorem decompositionField_localization_adjoin_range_eq_top :
    IntermediateField.adjoin vK.Completion
      (Set.range (toLocalization vK w)) = ⊤

theorem

decompositionField_toLocalization_isSeparable

L95 ↗

HilbertRamification.decompositionField_toLocalization_isSeparable

Documentation

Every generator coming from L is separable over K_v.

Source context 14 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section LocalizationGalois
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
local instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance proposition98CompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance proposition98CompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
local instance proposition98LocalizationBaseAlgebra : Algebra K (localization vK w) :=
  ((algebraMap vK.Completion (localization vK w)).comp
    (algebraMap K vK.Completion)).toAlgebra
local instance proposition98LocalizationScalarTower :
    IsScalarTower K vK.Completion (localization vK w) :=
  IsScalarTower.of_algebraMap_eq' (by
    ext x
    rfl)
omit hvK in

Lean source · statement

theorem decompositionField_toLocalization_isSeparable (x : L) :
    IsSeparable vK.Completion (toLocalization vK w x)

theorem

decompositionField_toLocalization_minpoly_splits

L107 ↗

HilbertRamification.decompositionField_toLocalization_minpoly_splits

Documentation

Every generator coming from L has its K_v-minimal polynomial split inside the localization.

Source context 14 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section LocalizationGalois
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
local instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance proposition98CompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance proposition98CompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
local instance proposition98LocalizationBaseAlgebra : Algebra K (localization vK w) :=
  ((algebraMap vK.Completion (localization vK w)).comp
    (algebraMap K vK.Completion)).toAlgebra
local instance proposition98LocalizationScalarTower :
    IsScalarTower K vK.Completion (localization vK w) :=
  IsScalarTower.of_algebraMap_eq' (by
    ext x
    rfl)
omit hvK in

Lean source · statement

theorem decompositionField_toLocalization_minpoly_splits (x : L) :
    ((minpoly vK.Completion (toLocalization vK w x)).map
      (algebraMap vK.Completion (localization vK w))).Splits

theorem

decompositionField_localization_normal

L138 ↗

HilbertRamification.decompositionField_localization_normal

Documentation

The algebraic localization of a Galois extension is normal over the completed base field, with no finite-degree hypothesis.

Source context 14 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section LocalizationGalois
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
local instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance proposition98CompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance proposition98CompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
local instance proposition98LocalizationBaseAlgebra : Algebra K (localization vK w) :=
  ((algebraMap vK.Completion (localization vK w)).comp
    (algebraMap K vK.Completion)).toAlgebra
local instance proposition98LocalizationScalarTower :
    IsScalarTower K vK.Completion (localization vK w) :=
  IsScalarTower.of_algebraMap_eq' (by
    ext x
    rfl)
omit hvK in

Lean source · statement

theorem decompositionField_localization_normal :
    Normal vK.Completion (localization vK w)

theorem

decompositionField_localization_separable

L159 ↗

HilbertRamification.decompositionField_localization_separable

Documentation

The algebraic localization of a Galois extension is separable over the completed base field, with no finite-degree hypothesis.

Source context 14 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section LocalizationGalois
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
local instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance proposition98CompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance proposition98CompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
local instance proposition98LocalizationBaseAlgebra : Algebra K (localization vK w) :=
  ((algebraMap vK.Completion (localization vK w)).comp
    (algebraMap K vK.Completion)).toAlgebra
local instance proposition98LocalizationScalarTower :
    IsScalarTower K vK.Completion (localization vK w) :=
  IsScalarTower.of_algebraMap_eq' (by
    ext x
    rfl)
omit hvK in

Lean source · statement

theorem decompositionField_localization_separable :
    Algebra.IsSeparable vK.Completion (localization vK w)

theorem

algebraicLocalization_isGalois

L180 ↗

HilbertRamification.algebraicLocalization_isGalois

Documentation

The algebraic localization of a Galois extension is Galois over K_v. This permits the fixed-field argument in infinite degree.

Source context 14 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section LocalizationGalois
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
local instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance proposition98CompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance proposition98CompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
local instance proposition98LocalizationBaseAlgebra : Algebra K (localization vK w) :=
  ((algebraMap vK.Completion (localization vK w)).comp
    (algebraMap K vK.Completion)).toAlgebra
local instance proposition98LocalizationScalarTower :
    IsScalarTower K vK.Completion (localization vK w) :=
  IsScalarTower.of_algebraMap_eq' (by
    ext x
    rfl)
omit hvK in

Lean source · statement

theorem algebraicLocalization_isGalois :
    IsGalois vK.Completion (localization vK w)

abbrev

decompositionField_completionImageSubfield

L187 ↗

HilbertRamification.decompositionField_completionImageSubfield

Documentation

The copy of K_v as an actual subfield of the algebraic localization.

Source context 13 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section LocalizationGalois
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
local instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance proposition98CompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance proposition98CompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
local instance proposition98LocalizationBaseAlgebra : Algebra K (localization vK w) :=
  ((algebraMap vK.Completion (localization vK w)).comp
    (algebraMap K vK.Completion)).toAlgebra
local instance proposition98LocalizationScalarTower :
    IsScalarTower K vK.Completion (localization vK w) :=
  IsScalarTower.of_algebraMap_eq' (by
    ext x
    rfl)

Lean source · statement

abbrev decompositionField_completionImageSubfield :
    Subfield (localization vK w)

theorem

decompositionField_decompositionField_eq_completionImage_comap

L196 ↗

HilbertRamification.decompositionField_decompositionField_eq_completionImage_comap

Documentation

The decomposition-field extension comparison, comap form: an element of L lies in the decomposition field exactly when its image in L_w belongs to the embedded copy of K_v.

Source context 14 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section LocalizationGalois
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
local instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance proposition98CompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance proposition98CompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
local instance proposition98LocalizationBaseAlgebra : Algebra K (localization vK w) :=
  ((algebraMap vK.Completion (localization vK w)).comp
    (algebraMap K vK.Completion)).toAlgebra
local instance proposition98LocalizationScalarTower :
    IsScalarTower K vK.Completion (localization vK w) :=
  IsScalarTower.of_algebraMap_eq' (by
    ext x
    rfl)
include hvK

Lean source · statement

theorem decompositionField_decompositionField_eq_completionImage_comap :
    (decompositionField_completionImageSubfield vK w).comap
        (toLocalization vK w) =
      (absoluteValueDecompositionField K w.1).toSubfield

theorem

decompositionField_decompositionField_image_eq_intersection

L235 ↗

HilbertRamification.decompositionField_decompositionField_image_eq_intersection

Documentation

The decomposition-field extension comparison, literal intersection form inside L_w: the image of Z_w is the infimum of the images of L and K_v.

Source context 14 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section LocalizationGalois
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
local instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance proposition98CompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance proposition98CompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
local instance proposition98LocalizationBaseAlgebra : Algebra K (localization vK w) :=
  ((algebraMap vK.Completion (localization vK w)).comp
    (algebraMap K vK.Completion)).toAlgebra
local instance proposition98LocalizationScalarTower :
    IsScalarTower K vK.Completion (localization vK w) :=
  IsScalarTower.of_algebraMap_eq' (by
    ext x
    rfl)
include hvK

Lean source · statement

theorem decompositionField_decompositionField_image_eq_intersection :
    (toLocalization vK w).fieldRange ⊓
        decompositionField_completionImageSubfield vK w =
      (absoluteValueDecompositionField K w.1).toSubfield.map
        (toLocalization vK w)

theorem

absoluteValueExtension_nonarchimedean_of_base

L259 ↗

HilbertRamification.absoluteValueExtension_nonarchimedean_of_base

Documentation

Nonarchimedeanness passes from the exact base valuation to its extension w; this uses only the bounded-natural-number definition.

Source context 16 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section LocalizationGalois
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
local instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance proposition98CompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance proposition98CompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
local instance proposition98LocalizationBaseAlgebra : Algebra K (localization vK w) :=
  ((algebraMap vK.Completion (localization vK w)).comp
    (algebraMap K vK.Completion)).toAlgebra
local instance proposition98LocalizationScalarTower :
    IsScalarTower K vK.Completion (localization vK w) :=
  IsScalarTower.of_algebraMap_eq' (by
    ext x
    rfl)
include hvK
omit hvK
omit [IsGalois K L] in

Lean source · statement

theorem absoluteValueExtension_nonarchimedean_of_base
    (hv : LubinTate.Valuations.NonarchimedeanAbsoluteValue vK) :
    LubinTate.Valuations.NonarchimedeanAbsoluteValue w.1

theorem

decompositionField_decompositionField_nonarchimedean

L269 ↗

HilbertRamification.decompositionField_decompositionField_nonarchimedean

Documentation

Nonarchimedeanness also passes to the restriction of w to Z_w.

Source context 16 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section LocalizationGalois
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
local instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance proposition98CompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance proposition98CompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
local instance proposition98LocalizationBaseAlgebra : Algebra K (localization vK w) :=
  ((algebraMap vK.Completion (localization vK w)).comp
    (algebraMap K vK.Completion)).toAlgebra
local instance proposition98LocalizationScalarTower :
    IsScalarTower K vK.Completion (localization vK w) :=
  IsScalarTower.of_algebraMap_eq' (by
    ext x
    rfl)
include hvK
omit hvK
omit [IsGalois K L] in

Lean source · statement

theorem decompositionField_decompositionField_nonarchimedean
    (hv : LubinTate.Valuations.NonarchimedeanAbsoluteValue vK) :
    LubinTate.Valuations.NonarchimedeanAbsoluteValue
      (AlgebraicNumberTheory.Valuations.absoluteValueRestrictIntermediateField w.1
        (absoluteValueDecompositionField K w.1))

theorem

decompositionField_completion_nonarchimedean

L278 ↗

HilbertRamification.decompositionField_completion_nonarchimedean

Documentation

The norm absolute value on K_v is nonarchimedean whenever v is.

Source context 15 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section LocalizationGalois
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
local instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance proposition98CompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance proposition98CompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
local instance proposition98LocalizationBaseAlgebra : Algebra K (localization vK w) :=
  ((algebraMap vK.Completion (localization vK w)).comp
    (algebraMap K vK.Completion)).toAlgebra
local instance proposition98LocalizationScalarTower :
    IsScalarTower K vK.Completion (localization vK w) :=
  IsScalarTower.of_algebraMap_eq' (by
    ext x
    rfl)
include hvK
omit hvK

Lean source · statement

theorem decompositionField_completion_nonarchimedean
    (hv : LubinTate.Valuations.NonarchimedeanAbsoluteValue vK) :
    LubinTate.Valuations.NonarchimedeanAbsoluteValue
      (AbsoluteValue.completionAbsoluteValue vK)

theorem

decompositionField_completionAbsoluteValue_range_eq

L290 ↗

HilbertRamification.decompositionField_completionAbsoluteValue_range_eq

Documentation

Completion does not enlarge the range of a nonarchimedean absolute value. This provides the value-group equality used in the decomposition-field extension comparison.

Source context 15 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section LocalizationGalois
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
local instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance proposition98CompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance proposition98CompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
local instance proposition98LocalizationBaseAlgebra : Algebra K (localization vK w) :=
  ((algebraMap vK.Completion (localization vK w)).comp
    (algebraMap K vK.Completion)).toAlgebra
local instance proposition98LocalizationScalarTower :
    IsScalarTower K vK.Completion (localization vK w) :=
  IsScalarTower.of_algebraMap_eq' (by
    ext x
    rfl)
include hvK
omit hvK

Lean source · statement

theorem decompositionField_completionAbsoluteValue_range_eq
    (hv : LubinTate.Valuations.NonarchimedeanAbsoluteValue vK) :
    Set.range (AbsoluteValue.completionAbsoluteValue vK) = Set.range vK

theorem

decompositionField_decompositionField_valueRange_eq

L300 ↗

HilbertRamification.decompositionField_decompositionField_valueRange_eq

Documentation

The decomposition-field extension comparison, value-group form: w|Z_w and v have literally the same range in ℝ.

Source context 16 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section LocalizationGalois
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
local instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance proposition98CompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance proposition98CompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
local instance proposition98LocalizationBaseAlgebra : Algebra K (localization vK w) :=
  ((algebraMap vK.Completion (localization vK w)).comp
    (algebraMap K vK.Completion)).toAlgebra
local instance proposition98LocalizationScalarTower :
    IsScalarTower K vK.Completion (localization vK w) :=
  IsScalarTower.of_algebraMap_eq' (by
    ext x
    rfl)
include hvK
omit hvK
include hvK

Lean source · statement

theorem decompositionField_decompositionField_valueRange_eq
    (hv : LubinTate.Valuations.NonarchimedeanAbsoluteValue vK) :
    Set.range
        (AlgebraicNumberTheory.Valuations.absoluteValueRestrictIntermediateField w.1
          (absoluteValueDecompositionField K w.1)) =
      Set.range vK

abbrev

decompositionField_baseValuationSubring

L336 ↗

HilbertRamification.decompositionField_baseValuationSubring

Documentation

The valuation subring of the nonarchimedean base absolute value.

Source context 17 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section LocalizationGalois
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
local instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance proposition98CompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance proposition98CompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
local instance proposition98LocalizationBaseAlgebra : Algebra K (localization vK w) :=
  ((algebraMap vK.Completion (localization vK w)).comp
    (algebraMap K vK.Completion)).toAlgebra
local instance proposition98LocalizationScalarTower :
    IsScalarTower K vK.Completion (localization vK w) :=
  IsScalarTower.of_algebraMap_eq' (by
    ext x
    rfl)
include hvK
omit hvK
include hvK
omit hvK

Lean source · statement

abbrev decompositionField_baseValuationSubring
    (hv : LubinTate.Valuations.NonarchimedeanAbsoluteValue vK) :
    _root_.ValuationSubring K

abbrev

decompositionField_decompositionFieldValuationSubring

L342 ↗

HilbertRamification.decompositionField_decompositionFieldValuationSubring

Documentation

The valuation subring of w|Z_w.

Source context 17 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section LocalizationGalois
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
local instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance proposition98CompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance proposition98CompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
local instance proposition98LocalizationBaseAlgebra : Algebra K (localization vK w) :=
  ((algebraMap vK.Completion (localization vK w)).comp
    (algebraMap K vK.Completion)).toAlgebra
local instance proposition98LocalizationScalarTower :
    IsScalarTower K vK.Completion (localization vK w) :=
  IsScalarTower.of_algebraMap_eq' (by
    ext x
    rfl)
include hvK
omit hvK
include hvK
omit hvK

Lean source · statement

abbrev decompositionField_decompositionFieldValuationSubring
    (hv : LubinTate.Valuations.NonarchimedeanAbsoluteValue vK) :
    _root_.ValuationSubring (absoluteValueDecompositionField K w.1)

def

decompositionField_decompositionField_integerMap

L352 ↗

HilbertRamification.decompositionField_decompositionField_integerMap

Documentation

The canonical local homomorphism between the two valuation subrings in the decomposition-field extension comparison.

Source context 17 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section LocalizationGalois
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
local instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance proposition98CompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance proposition98CompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
local instance proposition98LocalizationBaseAlgebra : Algebra K (localization vK w) :=
  ((algebraMap vK.Completion (localization vK w)).comp
    (algebraMap K vK.Completion)).toAlgebra
local instance proposition98LocalizationScalarTower :
    IsScalarTower K vK.Completion (localization vK w) :=
  IsScalarTower.of_algebraMap_eq' (by
    ext x
    rfl)
include hvK
omit hvK
include hvK
omit hvK

Lean source · statement

def decompositionField_decompositionField_integerMap
    (hv : LubinTate.Valuations.NonarchimedeanAbsoluteValue vK) :
    decompositionField_baseValuationSubring vK hv →+*
      decompositionField_decompositionFieldValuationSubring vK w hv

theorem

decompositionField_decompositionField_integerMap_apply

L368 ↗

HilbertRamification.decompositionField_decompositionField_integerMap_apply

Source context 18 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section LocalizationGalois
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
local instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance proposition98CompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance proposition98CompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
local instance proposition98LocalizationBaseAlgebra : Algebra K (localization vK w) :=
  ((algebraMap vK.Completion (localization vK w)).comp
    (algebraMap K vK.Completion)).toAlgebra
local instance proposition98LocalizationScalarTower :
    IsScalarTower K vK.Completion (localization vK w) :=
  IsScalarTower.of_algebraMap_eq' (by
    ext x
    rfl)
include hvK
omit hvK
include hvK
omit hvK
omit [IsGalois K L] in

Lean source · statement

theorem decompositionField_decompositionField_integerMap_apply
    (hv : LubinTate.Valuations.NonarchimedeanAbsoluteValue vK)
    (x : decompositionField_baseValuationSubring vK hv) :
    ((decompositionField_decompositionField_integerMap vK w hv x :
        decompositionField_decompositionFieldValuationSubring vK w hv) :
      absoluteValueDecompositionField K w.1) =
      algebraMap K (absoluteValueDecompositionField K w.1) (x : K)

instance

decompositionField_decompositionField_integerMap_isLocalHom

L378 ↗

HilbertRamification.decompositionField_decompositionField_integerMap_isLocalHom

Documentation

The valuation-ring map in the decomposition-field extension comparison is local.

Source context 17 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section LocalizationGalois
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
local instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance proposition98CompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance proposition98CompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
local instance proposition98LocalizationBaseAlgebra : Algebra K (localization vK w) :=
  ((algebraMap vK.Completion (localization vK w)).comp
    (algebraMap K vK.Completion)).toAlgebra
local instance proposition98LocalizationScalarTower :
    IsScalarTower K vK.Completion (localization vK w) :=
  IsScalarTower.of_algebraMap_eq' (by
    ext x
    rfl)
include hvK
omit hvK
include hvK
omit hvK

Lean source · full declaration

instance decompositionField_decompositionField_integerMap_isLocalHom
    (hv : LubinTate.Valuations.NonarchimedeanAbsoluteValue vK) :
    IsLocalHom (decompositionField_decompositionField_integerMap vK w hv) where
  map_nonunit x hx := by
    rw [← IsLocalRing.notMem_maximalIdeal] at hx ⊢
    intro hxmax
    apply hx
    have hxabs : vK (x : K) < 1 :=
      (absoluteValueValuationSubring_mem_maximalIdeal_iff_abs_lt_one
        vK hv x).mp hxmax
    rw [absoluteValueValuationSubring_mem_maximalIdeal_iff_abs_lt_one]
    rw [decompositionField_decompositionField_integerMap_apply]
    change w.1 (algebraMap
      (absoluteValueDecompositionField K w.1) L
      (algebraMap K (absoluteValueDecompositionField K w.1) (x : K))) < 1
    rw [← IsScalarTower.algebraMap_apply K
      (absoluteValueDecompositionField K w.1) L, w.2]
    exact hxabs

def

decompositionField_decompositionField_residueMap

L398 ↗

HilbertRamification.decompositionField_decompositionField_residueMap

Documentation

The induced canonical map of actual residue fields.

Source context 17 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section LocalizationGalois
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
local instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance proposition98CompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance proposition98CompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
local instance proposition98LocalizationBaseAlgebra : Algebra K (localization vK w) :=
  ((algebraMap vK.Completion (localization vK w)).comp
    (algebraMap K vK.Completion)).toAlgebra
local instance proposition98LocalizationScalarTower :
    IsScalarTower K vK.Completion (localization vK w) :=
  IsScalarTower.of_algebraMap_eq' (by
    ext x
    rfl)
include hvK
omit hvK
include hvK
omit hvK

Lean source · statement

def decompositionField_decompositionField_residueMap
    (hv : LubinTate.Valuations.NonarchimedeanAbsoluteValue vK) :
    IsLocalRing.ResidueField (decompositionField_baseValuationSubring vK hv) →+*
      IsLocalRing.ResidueField
        (decompositionField_decompositionFieldValuationSubring vK w hv)

theorem

decompositionField_decompositionField_residueMap_surjective

L411 ↗

HilbertRamification.decompositionField_decompositionField_residueMap_surjective

Documentation

The canonical residue-field map in the decomposition-field extension comparison is surjective. The proof chooses a representative in K_v, then approximates it modulo the maximal ideal by an element of K.

Source context 18 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section LocalizationGalois
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
local instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance proposition98CompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance proposition98CompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
local instance proposition98LocalizationBaseAlgebra : Algebra K (localization vK w) :=
  ((algebraMap vK.Completion (localization vK w)).comp
    (algebraMap K vK.Completion)).toAlgebra
local instance proposition98LocalizationScalarTower :
    IsScalarTower K vK.Completion (localization vK w) :=
  IsScalarTower.of_algebraMap_eq' (by
    ext x
    rfl)
include hvK
omit hvK
include hvK
omit hvK
include hvK

Lean source · statement

theorem decompositionField_decompositionField_residueMap_surjective
    (hv : LubinTate.Valuations.NonarchimedeanAbsoluteValue vK) :
    Function.Surjective
      (decompositionField_decompositionField_residueMap vK w hv)

def

decompositionField_decompositionField_residueFieldEquiv

L499 ↗

HilbertRamification.decompositionField_decompositionField_residueFieldEquiv

Documentation

The decomposition-field extension comparison, residue-field form: the canonical residue map is an isomorphism of the actual residue fields.

Source context 18 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section LocalizationGalois
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
local instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance proposition98CompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance proposition98CompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
local instance proposition98LocalizationBaseAlgebra : Algebra K (localization vK w) :=
  ((algebraMap vK.Completion (localization vK w)).comp
    (algebraMap K vK.Completion)).toAlgebra
local instance proposition98LocalizationScalarTower :
    IsScalarTower K vK.Completion (localization vK w) :=
  IsScalarTower.of_algebraMap_eq' (by
    ext x
    rfl)
include hvK
omit hvK
include hvK
omit hvK
include hvK

Lean source · statement

def decompositionField_decompositionField_residueFieldEquiv
    (hv : LubinTate.Valuations.NonarchimedeanAbsoluteValue vK) :
    IsLocalRing.ResidueField (decompositionField_baseValuationSubring vK hv) ≃+*
      IsLocalRing.ResidueField
        (decompositionField_decompositionFieldValuationSubring vK w hv)

theorem

decompositionField_decompositionField_residueFieldEquiv_apply

L508 ↗

HilbertRamification.decompositionField_decompositionField_residueFieldEquiv_apply

Source context 18 commands

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

noncomputable section
universe u v
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
section LocalizationGalois
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
  (w : AbsoluteValueExtension vK L)
local instance proposition98CompletionBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance proposition98CompletionBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance proposition98CompletionAlgebra : Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
local instance proposition98LocalizationBaseAlgebra : Algebra K (localization vK w) :=
  ((algebraMap vK.Completion (localization vK w)).comp
    (algebraMap K vK.Completion)).toAlgebra
local instance proposition98LocalizationScalarTower :
    IsScalarTower K vK.Completion (localization vK w) :=
  IsScalarTower.of_algebraMap_eq' (by
    ext x
    rfl)
include hvK
omit hvK
include hvK
omit hvK
include hvK

Lean source · statement

theorem decompositionField_decompositionField_residueFieldEquiv_apply
    (hv : LubinTate.Valuations.NonarchimedeanAbsoluteValue vK)
    (x : IsLocalRing.ResidueField
      (decompositionField_baseValuationSubring vK hv)) :
    decompositionField_decompositionField_residueFieldEquiv vK hvK w hv x =
      decompositionField_decompositionField_residueMap vK w hv x

Module documentation

Decomposition-field value and residue comparison

Declarations