Module

FiniteResidueFinrankTransfer.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.FiniteResidueFinrankTransfer

4 declarations indexed from sourceView source ↗

Module documentation

Finite local reciprocity: comparison of the two finite residue-field models

The residue-action exact sequence presents the residue field of a finite fixed field intrinsically, inside the selected residue algebraic closure. The norm formula uses the literal residue field of the spectral valuation on that fixed field. This file compares those presentations by the uniqueness of the finite extension valuation.

The finite fixed-field comparison

Imports4

Imported by7

def

valuationSubringEquivDecompositionFieldOfEqTop

L39 ↗

LocalClassFieldTheory.valuationSubringEquivDecompositionFieldOfEqTop

Documentation

If the decomposition group of an ambient valuation ring is the whole Galois group, its decomposition-field valuation ring is canonically equivalent to the given valuation ring on the ground field.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology RamificationTheory ClassFormation
open LocalFieldTheory ValuationTheory
noncomputable section
open scoped ValuativeRel
open HilbertRamification.ValuationSubring
universe u v

Lean source · statement

def valuationSubringEquivDecompositionFieldOfEqTop
    {F : Type u} {Omega : Type v} [Field F] [Field Omega] [Algebra F Omega]
    [IsGalois F Omega]
    (A : ValuationSubring Omega) (C : ValuationSubring F)
    (hC : A.comap (algebraMap F Omega) = C)
    (hA : decompositionGroup F A = ⊤) :
    C ≃+* decompositionFieldValuationSubring F A

def

residueFieldEquivDecompositionResidueOfEqTop

L92 ↗

LocalClassFieldTheory.residueFieldEquivDecompositionResidueOfEqTop

Documentation

The corresponding equivalence between literal and intrinsic residue fields.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology RamificationTheory ClassFormation
open LocalFieldTheory ValuationTheory
noncomputable section
open scoped ValuativeRel
open HilbertRamification.ValuationSubring
universe u v

Lean source · statement

def residueFieldEquivDecompositionResidueOfEqTop
    {F : Type u} {Omega : Type v} [Field F] [Field Omega] [Algebra F Omega]
    [IsGalois F Omega]
    (A : ValuationSubring Omega) (C : ValuationSubring F)
    (hC : A.comap (algebraMap F Omega) = C)
    (hA : decompositionGroup F A = ⊤) :
    IsLocalRing.ResidueField C ≃+* decompositionResidueField F A

theorem

residueFieldEquivDecompositionResidueOfEqTop_algebraMap

L105 ↗

LocalClassFieldTheory.residueFieldEquivDecompositionResidueOfEqTop_algebraMap

Documentation

Naturality of the preceding residue equivalence with reduction into the selected residue field.

Source context 7 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology RamificationTheory ClassFormation
open LocalFieldTheory ValuationTheory
noncomputable section
open scoped ValuativeRel
open HilbertRamification.ValuationSubring
universe u v

Lean source · full declaration

theorem residueFieldEquivDecompositionResidueOfEqTop_algebraMap
    {F : Type u} {Omega : Type v} [Field F] [Field Omega] [Algebra F Omega]
    [IsGalois F Omega]
    (A : ValuationSubring Omega) (C : ValuationSubring F)
    (hC : A.comap (algebraMap F Omega) = C)
    (hA : decompositionGroup F A = ⊤) (x : C) :
    algebraMap (decompositionResidueField F A) (selectedResidueField A)
        (residueFieldEquivDecompositionResidueOfEqTop A C hC hA
          (IsLocalRing.residue C x)) =
      IsLocalRing.residue A
        (⟨algebraMap F Omega (x : F), by
          have hx : (x : F) ∈ A.comap (algebraMap F Omega) := by
            rw [hC]
            exact x.property
          exact hx⟩ : A) := by
  rfl

theorem

localResidueDatum_residueDegree_eq_residueFinrank

L131 ↗

LocalClassFieldTheory.localResidueDatum_residueDegree_eq_residueFinrank

Documentation

Finite local reciprocity, residue-degree comparison. For an arbitrary finite closed subgroup field (not necessarily normal over K), the residue degree defined by the absolute residue action is the degree of the literal residue field of the unique finite extension valuation.

Source context 8 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology RamificationTheory ClassFormation
open LocalFieldTheory ValuationTheory
noncomputable section
open scoped ValuativeRel
open HilbertRamification.ValuationSubring
universe u v
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · statement

theorem localResidueDatum_residueDegree_eq_residueFinrank
    (H : FiniteAbstractField (Gal(SeparableClosure K/K)))
    [FiniteDimensional K
      (abstractFixedField K (SeparableClosure K) H.field)]
    [ValuativeRel (abstractFixedField K (SeparableClosure K) H.field)]
    [TopologicalSpace (abstractFixedField K (SeparableClosure K) H.field)]
    [IsNonarchimedeanLocalField
      (abstractFixedField K (SeparableClosure K) H.field)]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation
        (abstractFixedField K (SeparableClosure K) H.field))] :
    (H.residueDegree (localResidueDatum K) : ℕ) =
      @Module.finrank 𝓀[K]
        𝓀[abstractFixedField K (SeparableClosure K) H.field] _ _
          (IsLocalRing.ResidueField.instModule
            (R := 𝒪[K])
            (S := 𝒪[abstractFixedField K (SeparableClosure K) H.field]))

Module documentation

Finite local reciprocity: comparison of the two finite residue-field models

The finite fixed-field comparison

Declarations

valuationSubringEquivDecompositionFieldOfEqTop

residueFieldEquivDecompositionResidueOfEqTop

residueFieldEquivDecompositionResidueOfEqTop_algebraMap

localResidueDatum_residueDegree_eq_residueFinrank