NYLL
Module

LocalResidueDatum.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.LocalResidueDatum
24 declarations indexed from sourceView source ↗

Module documentation

Finite local reciprocity: the local residue degree datum

For a nonarchimedean local field K, this file makes the choices implicit in the construction explicit. The canonical local valuation is packaged as a complete DVF, Chevalley's theorem chooses an extension to AlgebraicClosure K, and that valuation is pulled back to SeparableClosure K. Finite-separable uniqueness shows that its decomposition subgroup is the whole Galois group. The residue field of the decomposition field is then identified with the finite residue field of K.

The remaining step is topological: the reduction action is shown continuous for the two Krull topologies and is composed with the intrinsic finite-field degree map from ResidueAlgebraicClosureDegree. The selected residue field is algebraically closed because its extension to the residue of AlgebraicClosure K is purely inseparable and the selected residue field is perfect over the finite base residue field.

The canonical complete discrete valuation and its absolute extension

Identification of the finite base residue field

Continuity of reduction and the local degree map

Imports4
Imported by9

Declarations

instance

localSeparableClosureAlgebra

L48 ↗
LocalClassFieldTheory.localSeparableClosureAlgebra
Source context 8 commands

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

namespace LocalClassFieldTheory
open ClassFormation
open ValuationTheory RamificationTheory LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
instance localSeparableClosureAlgebra :
    Algebra (SeparableClosure K) (AlgebraicClosure K)
instance

localSeparableClosureScalarTower

L52 ↗
LocalClassFieldTheory.localSeparableClosureScalarTower
Source context 9 commands

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

namespace LocalClassFieldTheory
open ClassFormation
open ValuationTheory RamificationTheory LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
local instance localSeparableClosureAlgebra :
    Algebra (SeparableClosure K) (AlgebraicClosure K) :=
  (separableClosure K (AlgebraicClosure K)).val.toRingHom.toAlgebra
Lean source · statement
instance localSeparableClosureScalarTower :
    IsScalarTower K (SeparableClosure K) (AlgebraicClosure K)
def

localAbsoluteValuationSubring

L60 ↗
LocalClassFieldTheory.localAbsoluteValuationSubring
Documentation

A Chevalley extension of the local valuation to the chosen algebraic closure. This is the valuation choice w | v made in the finite local reciprocity construction.

Source context 10 commands

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

namespace LocalClassFieldTheory
open ClassFormation
open ValuationTheory RamificationTheory LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
local instance localSeparableClosureAlgebra :
    Algebra (SeparableClosure K) (AlgebraicClosure K) :=
  (separableClosure K (AlgebraicClosure K)).val.toRingHom.toAlgebra
local instance localSeparableClosureScalarTower :
    IsScalarTower K (SeparableClosure K) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
Lean source · statement
def localAbsoluteValuationSubring :
    ValuationSubring (AlgebraicClosure K)
theorem

localAbsoluteValuationSubring_pullback

L68 ↗
LocalClassFieldTheory.localAbsoluteValuationSubring_pullback
Documentation

The chosen absolute valuation ring pulls back to the canonical valuation ring of K.

Source context 10 commands

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

namespace LocalClassFieldTheory
open ClassFormation
open ValuationTheory RamificationTheory LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
local instance localSeparableClosureAlgebra :
    Algebra (SeparableClosure K) (AlgebraicClosure K) :=
  (separableClosure K (AlgebraicClosure K)).val.toRingHom.toAlgebra
local instance localSeparableClosureScalarTower :
    IsScalarTower K (SeparableClosure K) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
Lean source · statement
theorem localAbsoluteValuationSubring_pullback (x : K) :
    algebraMap K (AlgebraicClosure K) x ∈
        localAbsoluteValuationSubring K ↔
      x ∈ (localCompleteDVF K).valuation.valuationSubring
instance

localAbsoluteValuationHasExtension

L78 ↗
LocalClassFieldTheory.localAbsoluteValuationHasExtension
Source context 10 commands

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

namespace LocalClassFieldTheory
open ClassFormation
open ValuationTheory RamificationTheory LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
local instance localSeparableClosureAlgebra :
    Algebra (SeparableClosure K) (AlgebraicClosure K) :=
  (separableClosure K (AlgebraicClosure K)).val.toRingHom.toAlgebra
local instance localSeparableClosureScalarTower :
    IsScalarTower K (SeparableClosure K) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
Lean source · statement
instance localAbsoluteValuationHasExtension :
    (localCompleteDVF K).valuation.HasExtension
      (localAbsoluteValuationSubring K).valuation
def

localSeparableValuationSubring

L89 ↗
LocalClassFieldTheory.localSeparableValuationSubring
Documentation

The valuation ring on the separable closure used in finite local reciprocity. We choose it as the pullback of the auxiliary valuation ring on the algebraic closure.

Source context 10 commands

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

namespace LocalClassFieldTheory
open ClassFormation
open ValuationTheory RamificationTheory LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
local instance localSeparableClosureAlgebra :
    Algebra (SeparableClosure K) (AlgebraicClosure K) :=
  (separableClosure K (AlgebraicClosure K)).val.toRingHom.toAlgebra
local instance localSeparableClosureScalarTower :
    IsScalarTower K (SeparableClosure K) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
Lean source · statement
def localSeparableValuationSubring :
    ValuationSubring (SeparableClosure K)
theorem

localSeparableValuationSubring_pullback

L95 ↗
LocalClassFieldTheory.localSeparableValuationSubring_pullback
Documentation

Pulling the separable valuation subring back to K recovers the base valuation ring.

Source context 10 commands

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

namespace LocalClassFieldTheory
open ClassFormation
open ValuationTheory RamificationTheory LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
local instance localSeparableClosureAlgebra :
    Algebra (SeparableClosure K) (AlgebraicClosure K) :=
  (separableClosure K (AlgebraicClosure K)).val.toRingHom.toAlgebra
local instance localSeparableClosureScalarTower :
    IsScalarTower K (SeparableClosure K) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
Lean source · statement
theorem localSeparableValuationSubring_pullback (x : K) :
    algebraMap K (SeparableClosure K) x ∈
        localSeparableValuationSubring K ↔
      x ∈ (localCompleteDVF K).valuation.valuationSubring
instance

localSeparableValuationHasExtension

L107 ↗
LocalClassFieldTheory.localSeparableValuationHasExtension
Documentation

The valuation on the separable closure extends the base discrete valuation.

Source context 10 commands

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

namespace LocalClassFieldTheory
open ClassFormation
open ValuationTheory RamificationTheory LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
local instance localSeparableClosureAlgebra :
    Algebra (SeparableClosure K) (AlgebraicClosure K) :=
  (separableClosure K (AlgebraicClosure K)).val.toRingHom.toAlgebra
local instance localSeparableClosureScalarTower :
    IsScalarTower K (SeparableClosure K) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
Lean source · statement
instance localSeparableValuationHasExtension :
    (localCompleteDVF K).valuation.HasExtension
      (localSeparableValuationSubring K).valuation
theorem

localSeparableValuationSubring_eq_of_hasExtension

L118 ↗
LocalClassFieldTheory.localSeparableValuationSubring_eq_of_hasExtension
Documentation

The extension valuation on the separable closure is independent of the auxiliary Chevalley choice. Equality is checked at the finite separable field generated by one element and follows there from Henselian uniqueness.

Source context 10 commands

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

namespace LocalClassFieldTheory
open ClassFormation
open ValuationTheory RamificationTheory LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
local instance localSeparableClosureAlgebra :
    Algebra (SeparableClosure K) (AlgebraicClosure K) :=
  (separableClosure K (AlgebraicClosure K)).val.toRingHom.toAlgebra
local instance localSeparableClosureScalarTower :
    IsScalarTower K (SeparableClosure K) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
Lean source · statement
theorem localSeparableValuationSubring_eq_of_hasExtension
    (B : ValuationSubring (SeparableClosure K))
    [(localCompleteDVF K).valuation.HasExtension B.valuation] :
    localSeparableValuationSubring K = B
theorem

localSeparableDecompositionGroup_eq_top

L163 ↗
LocalClassFieldTheory.localSeparableDecompositionGroup_eq_top
Documentation

Every automorphism of the separable closure preserves the unique extension of the Henselian local valuation.

Source context 10 commands

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

namespace LocalClassFieldTheory
open ClassFormation
open ValuationTheory RamificationTheory LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
local instance localSeparableClosureAlgebra :
    Algebra (SeparableClosure K) (AlgebraicClosure K) :=
  (separableClosure K (AlgebraicClosure K)).val.toRingHom.toAlgebra
local instance localSeparableClosureScalarTower :
    IsScalarTower K (SeparableClosure K) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
Lean source · statement
theorem localSeparableDecompositionGroup_eq_top :
    decompositionGroup K (localSeparableValuationSubring K) = ⊤
def

localBaseValuationSubringEquivDecompositionField

L180 ↗
LocalClassFieldTheory.localBaseValuationSubringEquivDecompositionField
Documentation

When the decomposition subgroup is top, the valuation ring on the decomposition field is the original local valuation ring.

Source context 10 commands

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

namespace LocalClassFieldTheory
open ClassFormation
open ValuationTheory RamificationTheory LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
local instance localSeparableClosureAlgebra :
    Algebra (SeparableClosure K) (AlgebraicClosure K) :=
  (separableClosure K (AlgebraicClosure K)).val.toRingHom.toAlgebra
local instance localSeparableClosureScalarTower :
    IsScalarTower K (SeparableClosure K) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
Lean source · statement
def localBaseValuationSubringEquivDecompositionField :
    (localCompleteDVF K).valuationSubring ≃+*
      decompositionFieldValuationSubring K
        (localSeparableValuationSubring K)
def

localBaseResidueEquivDecompositionResidue

L227 ↗
LocalClassFieldTheory.localBaseResidueEquivDecompositionResidue
Documentation

The residue field in the residue-action exact sequence is canonically the finite residue field of the original local field.

Source context 10 commands

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

namespace LocalClassFieldTheory
open ClassFormation
open ValuationTheory RamificationTheory LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
local instance localSeparableClosureAlgebra :
    Algebra (SeparableClosure K) (AlgebraicClosure K) :=
  (separableClosure K (AlgebraicClosure K)).val.toRingHom.toAlgebra
local instance localSeparableClosureScalarTower :
    IsScalarTower K (SeparableClosure K) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
Lean source · statement
def localBaseResidueEquivDecompositionResidue :
    (localCompleteDVF K).residueField ≃+*
      decompositionResidueField K (localSeparableValuationSubring K)
theorem

localBaseResidueEquivDecompositionResidue_algebraMap

L239 ↗
LocalClassFieldTheory.localBaseResidueEquivDecompositionResidue_algebraMap
Documentation

Naturality of the base-residue comparison with the literal reduction map into the selected residue field. This is the scalar square used when transporting residue degrees from the residue-action presentation back to the canonical residue fields of local extensions.

Source context 10 commands

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

namespace LocalClassFieldTheory
open ClassFormation
open ValuationTheory RamificationTheory LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
local instance localSeparableClosureAlgebra :
    Algebra (SeparableClosure K) (AlgebraicClosure K) :=
  (separableClosure K (AlgebraicClosure K)).val.toRingHom.toAlgebra
local instance localSeparableClosureScalarTower :
    IsScalarTower K (SeparableClosure K) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
Lean source · statement
theorem localBaseResidueEquivDecompositionResidue_algebraMap
    (x : (localCompleteDVF K).valuationSubring) :
    algebraMap
        (decompositionResidueField K (localSeparableValuationSubring K))
        (selectedResidueField (localSeparableValuationSubring K))
        (localBaseResidueEquivDecompositionResidue K
          (IsLocalRing.residue (localCompleteDVF K).valuationSubring x)) =
      IsLocalRing.residue (localSeparableValuationSubring K)
        (⟨algebraMap K (SeparableClosure K) (x : K),
          (localSeparableValuationSubring_pullback K (x : K)).2
            x.property⟩ : localSeparableValuationSubring K)
instance

localDecompositionResidueFinite

L253 ↗
LocalClassFieldTheory.localDecompositionResidueFinite
Documentation

The residue field attached to the local decomposition datum is finite.

Source context 10 commands

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

namespace LocalClassFieldTheory
open ClassFormation
open ValuationTheory RamificationTheory LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
local instance localSeparableClosureAlgebra :
    Algebra (SeparableClosure K) (AlgebraicClosure K) :=
  (separableClosure K (AlgebraicClosure K)).val.toRingHom.toAlgebra
local instance localSeparableClosureScalarTower :
    IsScalarTower K (SeparableClosure K) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
Lean source · statement
instance localDecompositionResidueFinite :
    Finite (decompositionResidueField K
      (localSeparableValuationSubring K))
instance

localDecompositionResidueFintype

L263 ↗
LocalClassFieldTheory.localDecompositionResidueFintype
Documentation

The finite local decomposition residue field has a canonical finite enumeration.

Source context 10 commands

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

namespace LocalClassFieldTheory
open ClassFormation
open ValuationTheory RamificationTheory LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
local instance localSeparableClosureAlgebra :
    Algebra (SeparableClosure K) (AlgebraicClosure K) :=
  (separableClosure K (AlgebraicClosure K)).val.toRingHom.toAlgebra
local instance localSeparableClosureScalarTower :
    IsScalarTower K (SeparableClosure K) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
Lean source · statement
instance localDecompositionResidueFintype :
    Fintype (decompositionResidueField K
      (localSeparableValuationSubring K))
instance

localSelectedResidueIsAlgClosed

L269 ↗
LocalClassFieldTheory.localSelectedResidueIsAlgClosed
Documentation

The selected residue field of the separable valuation is algebraically closed.

Source context 10 commands

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

namespace LocalClassFieldTheory
open ClassFormation
open ValuationTheory RamificationTheory LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
local instance localSeparableClosureAlgebra :
    Algebra (SeparableClosure K) (AlgebraicClosure K) :=
  (separableClosure K (AlgebraicClosure K)).val.toRingHom.toAlgebra
local instance localSeparableClosureScalarTower :
    IsScalarTower K (SeparableClosure K) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
Lean source · statement
instance localSelectedResidueIsAlgClosed :
    IsAlgClosed (selectedResidueField
      (localSeparableValuationSubring K))
def

localSelectedResidueLift

L307 ↗
LocalClassFieldTheory.localSelectedResidueLift
Documentation

A fixed representative in the chosen valuation ring of a residue class.

Source context 10 commands

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

namespace LocalClassFieldTheory
open ClassFormation
open ValuationTheory RamificationTheory LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
local instance localSeparableClosureAlgebra :
    Algebra (SeparableClosure K) (AlgebraicClosure K) :=
  (separableClosure K (AlgebraicClosure K)).val.toRingHom.toAlgebra
local instance localSeparableClosureScalarTower :
    IsScalarTower K (SeparableClosure K) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
Lean source · statement
def localSelectedResidueLift
    (x : selectedResidueField (localSeparableValuationSubring K)) :
    localSeparableValuationSubring K
theorem

localSelectedResidueLift_residue

L313 ↗
LocalClassFieldTheory.localSelectedResidueLift_residue
Source context 10 commands

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

namespace LocalClassFieldTheory
open ClassFormation
open ValuationTheory RamificationTheory LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
local instance localSeparableClosureAlgebra :
    Algebra (SeparableClosure K) (AlgebraicClosure K) :=
  (separableClosure K (AlgebraicClosure K)).val.toRingHom.toAlgebra
local instance localSeparableClosureScalarTower :
    IsScalarTower K (SeparableClosure K) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
Lean source · statement
theorem localSelectedResidueLift_residue
    (x : selectedResidueField (localSeparableValuationSubring K)) :
    IsLocalRing.residue (localSeparableValuationSubring K)
        (localSelectedResidueLift K x) = x
theorem

localSeparableResidueAlgAction_continuous

L323 ↗
LocalClassFieldTheory.localSeparableResidueAlgAction_continuous
Documentation

Reduction from the absolute Galois group to the absolute Galois group of the residue field is continuous for the Krull topologies. A finite residue subextension is controlled by adjoining to K one lift of each of its finitely many elements.

Source context 10 commands

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

namespace LocalClassFieldTheory
open ClassFormation
open ValuationTheory RamificationTheory LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
local instance localSeparableClosureAlgebra :
    Algebra (SeparableClosure K) (AlgebraicClosure K) :=
  (separableClosure K (AlgebraicClosure K)).val.toRingHom.toAlgebra
local instance localSeparableClosureScalarTower :
    IsScalarTower K (SeparableClosure K) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
Lean source · statement
theorem localSeparableResidueAlgAction_continuous :
    Continuous
      (residueAlgActionOfEqTop K
        (localSeparableValuationSubring K)
        (localSeparableDecompositionGroup_eq_top K))
def

localSeparableResidueAlgAction

L382 ↗
LocalClassFieldTheory.localSeparableResidueAlgAction
Documentation

The continuous residue action on the chosen residue algebraic closure.

Source context 10 commands

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

namespace LocalClassFieldTheory
open ClassFormation
open ValuationTheory RamificationTheory LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
local instance localSeparableClosureAlgebra :
    Algebra (SeparableClosure K) (AlgebraicClosure K) :=
  (separableClosure K (AlgebraicClosure K)).val.toRingHom.toAlgebra
local instance localSeparableClosureScalarTower :
    IsScalarTower K (SeparableClosure K) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
Lean source · full declaration
def localSeparableResidueAlgAction :
    Gal(SeparableClosure K / K) →ₜ*
      (selectedResidueField (localSeparableValuationSubring K) ≃ₐ[
        decompositionResidueField K (localSeparableValuationSubring K)]
          selectedResidueField (localSeparableValuationSubring K)) where
  toMonoidHom :=
    residueAlgActionOfEqTop K
      (localSeparableValuationSubring K)
      (localSeparableDecompositionGroup_eq_top K)
  continuous_toFun := localSeparableResidueAlgAction_continuous K
theorem

localSeparableResidueAlgAction_surjective

L394 ↗
LocalClassFieldTheory.localSeparableResidueAlgAction_surjective
Documentation

Every automorphism of the selected residue extension lifts to the separable Galois group.

Source context 10 commands

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

namespace LocalClassFieldTheory
open ClassFormation
open ValuationTheory RamificationTheory LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
local instance localSeparableClosureAlgebra :
    Algebra (SeparableClosure K) (AlgebraicClosure K) :=
  (separableClosure K (AlgebraicClosure K)).val.toRingHom.toAlgebra
local instance localSeparableClosureScalarTower :
    IsScalarTower K (SeparableClosure K) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
Lean source · statement
theorem localSeparableResidueAlgAction_surjective :
    Function.Surjective (localSeparableResidueAlgAction K)
def

localResidueDegree

L403 ↗
LocalClassFieldTheory.localResidueDegree
Documentation

Finite local reciprocity, local degree map. The residue Frobenius degree, defined directly on the separable-closure model used by the local reciprocity formalization.

Source context 10 commands

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

namespace LocalClassFieldTheory
open ClassFormation
open ValuationTheory RamificationTheory LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
local instance localSeparableClosureAlgebra :
    Algebra (SeparableClosure K) (AlgebraicClosure K) :=
  (separableClosure K (AlgebraicClosure K)).val.toRingHom.toAlgebra
local instance localSeparableClosureScalarTower :
    IsScalarTower K (SeparableClosure K) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
Lean source · full declaration
def localResidueDegree :
    Gal(SeparableClosure K / K) →ₜ* ZHatMul where
  toMonoidHom :=
    (residueAbsoluteDegreeIn
      (decompositionResidueField K (localSeparableValuationSubring K))
      (selectedResidueField (localSeparableValuationSubring K))).toMonoidHom.comp
        (localSeparableResidueAlgAction K).toMonoidHom
  continuous_toFun :=
    (residueAbsoluteDegreeIn
      (decompositionResidueField K (localSeparableValuationSubring K))
      (selectedResidueField
        (localSeparableValuationSubring K))).continuous_toFun.comp
      (localSeparableResidueAlgAction K).continuous_toFun
theorem

localResidueDegree_surjective

L418 ↗
LocalClassFieldTheory.localResidueDegree_surjective
Documentation

The local residue-degree map onto the profinite integers is surjective.

Source context 10 commands

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

namespace LocalClassFieldTheory
open ClassFormation
open ValuationTheory RamificationTheory LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
local instance localSeparableClosureAlgebra :
    Algebra (SeparableClosure K) (AlgebraicClosure K) :=
  (separableClosure K (AlgebraicClosure K)).val.toRingHom.toAlgebra
local instance localSeparableClosureScalarTower :
    IsScalarTower K (SeparableClosure K) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
Lean source · statement
theorem localResidueDegree_surjective :
    Function.Surjective (localResidueDegree K)
def

localResidueDatum

L438 ↗
LocalClassFieldTheory.localResidueDatum
Documentation

Finite local reciprocity. The actual abstract class-formation datum d : G_K -> ZHat furnished by the residue action of a local field.

Source context 10 commands

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

namespace LocalClassFieldTheory
open ClassFormation
open ValuationTheory RamificationTheory LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
local instance localSeparableClosureAlgebra :
    Algebra (SeparableClosure K) (AlgebraicClosure K) :=
  (separableClosure K (AlgebraicClosure K)).val.toRingHom.toAlgebra
local instance localSeparableClosureScalarTower :
    IsScalarTower K (SeparableClosure K) (AlgebraicClosure K) :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl
Lean source · full declaration
def localResidueDatum :
    DegreeData (Gal(SeparableClosure K / K)) where
  degree := localResidueDegree K
  degree_surjective := localResidueDegree_surjective K

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.