NYLL
Module

FiniteSubgroupResidueDegree.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.FiniteSubgroupResidueDegree
14 declarations indexed from sourceView source ↗

Module documentation

Finite local reciprocity: residue degree of a finite abstract field

This file compares the residue action used by localResidueDatum with the same residue action after changing the ground field to the fixed field of a closed subgroup. The comparison is made on the common selected residue field, so it also applies when the fixed field is not normal over the original local field.

Imports2
Imported by3

Declarations

def

localAbstractFixedResidueIntermediateField

L41 ↗
LocalClassFieldTheory.localAbstractFixedResidueIntermediateField
Documentation

The residue subfield inside the selected residue algebraic closure which is generated by the residue field attached to the fixed field of H.

We use adjoin rather than imposing a scalar-tower instance between the two intrinsic residue-action quotient presentations.

Source context 8 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology RamificationTheory ClassFormation
open 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
def localAbstractFixedResidueIntermediateField
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    IntermediateField
      (decompositionResidueField K (localSeparableValuationSubring K))
      (selectedResidueField (localSeparableValuationSubring K))
instance

localAbstractFixedResidueIntermediateFieldAlgebra

L57 ↗
LocalClassFieldTheory.localAbstractFixedResidueIntermediateFieldAlgebra
Documentation

The canonical scalar structure on the selected fixed residue field. Naming these instances keeps typeclass search from unfolding the fixed-field and residue-action constructions in finite-dimensionality statements.

Source context 8 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology RamificationTheory ClassFormation
open 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 localAbstractFixedResidueIntermediateFieldAlgebra
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    Algebra
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H)
instance

localAbstractFixedResidueIntermediateFieldSMul

L64 ↗
LocalClassFieldTheory.localAbstractFixedResidueIntermediateFieldSMul
Source context 9 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology RamificationTheory ClassFormation
open LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
/-- The canonical scalar structure on the selected fixed residue field.
Naming these instances keeps typeclass search from unfolding the fixed-field
and residue-action constructions in finite-dimensionality statements. -/
noncomputable local instance localAbstractFixedResidueIntermediateFieldAlgebra
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    Algebra
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  (localAbstractFixedResidueIntermediateField K H).algebra
Lean source · statement
instance localAbstractFixedResidueIntermediateFieldSMul
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    SMul
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H)
instance

localAbstractFixedResidueIntermediateFieldModule

L72 ↗
LocalClassFieldTheory.localAbstractFixedResidueIntermediateFieldModule
Source context 10 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology RamificationTheory ClassFormation
open LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
/-- The canonical scalar structure on the selected fixed residue field.
Naming these instances keeps typeclass search from unfolding the fixed-field
and residue-action constructions in finite-dimensionality statements. -/
noncomputable local instance localAbstractFixedResidueIntermediateFieldAlgebra
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    Algebra
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  (localAbstractFixedResidueIntermediateField K H).algebra
noncomputable local instance localAbstractFixedResidueIntermediateFieldSMul
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    SMul
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  @Algebra.toSMul _ _ _ _
    (localAbstractFixedResidueIntermediateFieldAlgebra K H)
Lean source · statement
instance localAbstractFixedResidueIntermediateFieldModule
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    Module
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H)
theorem

localAbstractFixedDecompositionGroup_eq_top

L83 ↗
LocalClassFieldTheory.localAbstractFixedDecompositionGroup_eq_top
Documentation

Every automorphism over the fixed field preserves the selected extension valuation. This is the base-change form of the full decomposition-group statement proved for K.

Source context 11 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology RamificationTheory ClassFormation
open LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
/-- The canonical scalar structure on the selected fixed residue field.
Naming these instances keeps typeclass search from unfolding the fixed-field
and residue-action constructions in finite-dimensionality statements. -/
noncomputable local instance localAbstractFixedResidueIntermediateFieldAlgebra
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    Algebra
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  (localAbstractFixedResidueIntermediateField K H).algebra
noncomputable local instance localAbstractFixedResidueIntermediateFieldSMul
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    SMul
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  @Algebra.toSMul _ _ _ _
    (localAbstractFixedResidueIntermediateFieldAlgebra K H)
noncomputable local instance localAbstractFixedResidueIntermediateFieldModule
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    Module
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  @Algebra.toModule _ _ _ _
    (localAbstractFixedResidueIntermediateFieldAlgebra K H)
Lean source · statement
theorem localAbstractFixedDecompositionGroup_eq_top
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    decompositionGroup (abstractFixedField K (SeparableClosure K) H)
      (localSeparableValuationSubring K) = ⊤
theorem

localAbstractFixedResidueAction_apply

L102 ↗
LocalClassFieldTheory.localAbstractFixedResidueAction_apply
Documentation

Restricting the local residue action to H gives the same underlying automorphism of the selected residue field as applying the residue-action map over the fixed field of H.

Source context 11 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology RamificationTheory ClassFormation
open LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
/-- The canonical scalar structure on the selected fixed residue field.
Naming these instances keeps typeclass search from unfolding the fixed-field
and residue-action constructions in finite-dimensionality statements. -/
noncomputable local instance localAbstractFixedResidueIntermediateFieldAlgebra
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    Algebra
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  (localAbstractFixedResidueIntermediateField K H).algebra
noncomputable local instance localAbstractFixedResidueIntermediateFieldSMul
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    SMul
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  @Algebra.toSMul _ _ _ _
    (localAbstractFixedResidueIntermediateFieldAlgebra K H)
noncomputable local instance localAbstractFixedResidueIntermediateFieldModule
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    Module
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  @Algebra.toModule _ _ _ _
    (localAbstractFixedResidueIntermediateFieldAlgebra K H)
Lean source · statement
theorem localAbstractFixedResidueAction_apply
    (H : ClosedSubgroup (Gal(SeparableClosure K/K)))
    (sigma : H.toSubgroup)
    (x : selectedResidueField (localSeparableValuationSubring K)) :
    localSeparableResidueAlgAction K sigma.1 x =
      residueAlgActionOfEqTop
        (abstractFixedField K (SeparableClosure K) H)
        (localSeparableValuationSubring K)
        (localAbstractFixedDecompositionGroup_eq_top K H)
        (abstractSubgroupEquivGaloisGroup K (SeparableClosure K) H sigma) x
theorem

localAbstractFixedResidueAction_map_eq_fixingSubgroup

L128 ↗
LocalClassFieldTheory.localAbstractFixedResidueAction_map_eq_fixingSubgroup
Documentation

The image of H under the local residue action is exactly the subgroup fixing the residue subfield of its fixed field. The reverse inclusion is the surjectivity of the residue-action map after changing the base to that fixed field.

Source context 11 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology RamificationTheory ClassFormation
open LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
/-- The canonical scalar structure on the selected fixed residue field.
Naming these instances keeps typeclass search from unfolding the fixed-field
and residue-action constructions in finite-dimensionality statements. -/
noncomputable local instance localAbstractFixedResidueIntermediateFieldAlgebra
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    Algebra
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  (localAbstractFixedResidueIntermediateField K H).algebra
noncomputable local instance localAbstractFixedResidueIntermediateFieldSMul
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    SMul
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  @Algebra.toSMul _ _ _ _
    (localAbstractFixedResidueIntermediateFieldAlgebra K H)
noncomputable local instance localAbstractFixedResidueIntermediateFieldModule
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    Module
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  @Algebra.toModule _ _ _ _
    (localAbstractFixedResidueIntermediateFieldAlgebra K H)
Lean source · statement
theorem localAbstractFixedResidueAction_map_eq_fixingSubgroup
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    H.toSubgroup.map (localSeparableResidueAlgAction K).toMonoidHom =
      (localAbstractFixedResidueIntermediateField K H).fixingSubgroup
theorem

localAbstractFixedResidueAction_mem_fixingSubgroup

L214 ↗
LocalClassFieldTheory.localAbstractFixedResidueAction_mem_fixingSubgroup
Documentation

The residue action of an element of H fixes the finite residue subfield attached to the fixed field of H.

Source context 11 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology RamificationTheory ClassFormation
open LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
/-- The canonical scalar structure on the selected fixed residue field.
Naming these instances keeps typeclass search from unfolding the fixed-field
and residue-action constructions in finite-dimensionality statements. -/
noncomputable local instance localAbstractFixedResidueIntermediateFieldAlgebra
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    Algebra
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  (localAbstractFixedResidueIntermediateField K H).algebra
noncomputable local instance localAbstractFixedResidueIntermediateFieldSMul
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    SMul
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  @Algebra.toSMul _ _ _ _
    (localAbstractFixedResidueIntermediateFieldAlgebra K H)
noncomputable local instance localAbstractFixedResidueIntermediateFieldModule
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    Module
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  @Algebra.toModule _ _ _ _
    (localAbstractFixedResidueIntermediateFieldAlgebra K H)
Lean source · statement
theorem localAbstractFixedResidueAction_mem_fixingSubgroup
    (H : ClosedSubgroup (Gal(SeparableClosure K/K)))
    (sigma : H.toSubgroup) :
    localSeparableResidueAlgAction K sigma.1 ∈
      (localAbstractFixedResidueIntermediateField K H).fixingSubgroup
def

localAbstractFixedResidueActionOverIntermediateField

L225 ↗
LocalClassFieldTheory.localAbstractFixedResidueActionOverIntermediateField
Documentation

The residue action of H, with scalars restricted to the actual finite residue subfield selected by H inside the common residue algebraic closure.

Source context 11 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology RamificationTheory ClassFormation
open LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
/-- The canonical scalar structure on the selected fixed residue field.
Naming these instances keeps typeclass search from unfolding the fixed-field
and residue-action constructions in finite-dimensionality statements. -/
noncomputable local instance localAbstractFixedResidueIntermediateFieldAlgebra
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    Algebra
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  (localAbstractFixedResidueIntermediateField K H).algebra
noncomputable local instance localAbstractFixedResidueIntermediateFieldSMul
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    SMul
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  @Algebra.toSMul _ _ _ _
    (localAbstractFixedResidueIntermediateFieldAlgebra K H)
noncomputable local instance localAbstractFixedResidueIntermediateFieldModule
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    Module
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  @Algebra.toModule _ _ _ _
    (localAbstractFixedResidueIntermediateFieldAlgebra K H)
Lean source · statement
def localAbstractFixedResidueActionOverIntermediateField
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    H.toSubgroup →*
      (selectedResidueField (localSeparableValuationSubring K) ≃ₐ[
        localAbstractFixedResidueIntermediateField K H]
        selectedResidueField (localSeparableValuationSubring K))
theorem

localAbstractFixedResidueActionOverIntermediateField_apply

L246 ↗
LocalClassFieldTheory.localAbstractFixedResidueActionOverIntermediateField_apply
Documentation

Restricting residue scalars changes only the scalar-linearity proof, not the underlying automorphism of the selected residue field.

Source context 11 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology RamificationTheory ClassFormation
open LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
/-- The canonical scalar structure on the selected fixed residue field.
Naming these instances keeps typeclass search from unfolding the fixed-field
and residue-action constructions in finite-dimensionality statements. -/
noncomputable local instance localAbstractFixedResidueIntermediateFieldAlgebra
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    Algebra
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  (localAbstractFixedResidueIntermediateField K H).algebra
noncomputable local instance localAbstractFixedResidueIntermediateFieldSMul
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    SMul
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  @Algebra.toSMul _ _ _ _
    (localAbstractFixedResidueIntermediateFieldAlgebra K H)
noncomputable local instance localAbstractFixedResidueIntermediateFieldModule
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    Module
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  @Algebra.toModule _ _ _ _
    (localAbstractFixedResidueIntermediateFieldAlgebra K H)
Lean source · statement
theorem localAbstractFixedResidueActionOverIntermediateField_apply
    (H : ClosedSubgroup (Gal(SeparableClosure K/K)))
    (sigma : H.toSubgroup)
    (x : selectedResidueField (localSeparableValuationSubring K)) :
    localAbstractFixedResidueActionOverIntermediateField K H sigma x =
      localSeparableResidueAlgAction K sigma.1 x
theorem

localAbstractFixedResidueIntermediateField_finiteDimensional

L258 ↗
LocalClassFieldTheory.localAbstractFixedResidueIntermediateField_finiteDimensional
Documentation

A finite abstract field has a genuinely finite residue subfield inside the selected residue algebraic closure. Finiteness is deduced from the finite index of H: surjectivity of the absolute residue action makes the index of its image divide the index of H.

Source context 11 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology RamificationTheory ClassFormation
open LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
/-- The canonical scalar structure on the selected fixed residue field.
Naming these instances keeps typeclass search from unfolding the fixed-field
and residue-action constructions in finite-dimensionality statements. -/
noncomputable local instance localAbstractFixedResidueIntermediateFieldAlgebra
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    Algebra
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  (localAbstractFixedResidueIntermediateField K H).algebra
noncomputable local instance localAbstractFixedResidueIntermediateFieldSMul
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    SMul
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  @Algebra.toSMul _ _ _ _
    (localAbstractFixedResidueIntermediateFieldAlgebra K H)
noncomputable local instance localAbstractFixedResidueIntermediateFieldModule
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    Module
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  @Algebra.toModule _ _ _ _
    (localAbstractFixedResidueIntermediateFieldAlgebra K H)
Lean source · statement
theorem localAbstractFixedResidueIntermediateField_finiteDimensional
    (H : ClosedSubgroup (Gal(SeparableClosure K/K)))
    [Finite
      ((baseField (Gal(SeparableClosure K/K))).toSubgroup ⧸
        extensionSubgroup
          (baseField (Gal(SeparableClosure K/K))) H
          (le_baseField H))] :
    FiniteDimensional
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H)
def

localAbstractFixedResidueFiniteGaloisIntermediateField

L302 ↗
LocalClassFieldTheory.localAbstractFixedResidueFiniteGaloisIntermediateField
Documentation

The finite residue subfield, packaged in the form used by the intrinsic finite-field residue datum.

Source context 11 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology RamificationTheory ClassFormation
open LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
/-- The canonical scalar structure on the selected fixed residue field.
Naming these instances keeps typeclass search from unfolding the fixed-field
and residue-action constructions in finite-dimensionality statements. -/
noncomputable local instance localAbstractFixedResidueIntermediateFieldAlgebra
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    Algebra
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  (localAbstractFixedResidueIntermediateField K H).algebra
noncomputable local instance localAbstractFixedResidueIntermediateFieldSMul
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    SMul
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  @Algebra.toSMul _ _ _ _
    (localAbstractFixedResidueIntermediateFieldAlgebra K H)
noncomputable local instance localAbstractFixedResidueIntermediateFieldModule
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    Module
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  @Algebra.toModule _ _ _ _
    (localAbstractFixedResidueIntermediateFieldAlgebra K H)
Lean source · statement
def localAbstractFixedResidueFiniteGaloisIntermediateField
    (H : ClosedSubgroup (Gal(SeparableClosure K/K)))
    [Finite
      ((baseField (Gal(SeparableClosure K/K))).toSubgroup ⧸
        extensionSubgroup
          (baseField (Gal(SeparableClosure K/K))) H
          (le_baseField H))] :
    FiniteGaloisIntermediateField
      (decompositionResidueField K (localSeparableValuationSubring K))
      (selectedResidueField (localSeparableValuationSubring K))
theorem

localResidueDatum_residueDegree_eq_selectedResidueFinrank

L336 ↗
LocalClassFieldTheory.localResidueDatum_residueDegree_eq_selectedResidueFinrank
Documentation

Finite local reciprocity, finite-field index form. The residue degree attached by localResidueDatum to a finite abstract field is the degree of the actual residue subfield selected by the residue action.

Source context 11 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology RamificationTheory ClassFormation
open LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
/-- The canonical scalar structure on the selected fixed residue field.
Naming these instances keeps typeclass search from unfolding the fixed-field
and residue-action constructions in finite-dimensionality statements. -/
noncomputable local instance localAbstractFixedResidueIntermediateFieldAlgebra
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    Algebra
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  (localAbstractFixedResidueIntermediateField K H).algebra
noncomputable local instance localAbstractFixedResidueIntermediateFieldSMul
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    SMul
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  @Algebra.toSMul _ _ _ _
    (localAbstractFixedResidueIntermediateFieldAlgebra K H)
noncomputable local instance localAbstractFixedResidueIntermediateFieldModule
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    Module
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  @Algebra.toModule _ _ _ _
    (localAbstractFixedResidueIntermediateFieldAlgebra K H)
Lean source · statement
theorem localResidueDatum_residueDegree_eq_selectedResidueFinrank
    (H : FiniteAbstractField (Gal(SeparableClosure K/K))) :
    (H.residueDegree (localResidueDatum K) : ℕ) =
      Module.finrank
        (decompositionResidueField K (localSeparableValuationSubring K))
        (localAbstractFixedResidueIntermediateField K H.field)
theorem

localResidueDatum_normalizedDegree_eq_residueAbsoluteDegreeIn

L394 ↗
LocalClassFieldTheory.localResidueDatum_normalizedDegree_eq_residueAbsoluteDegreeIn
Documentation

Finite local reciprocity, pointwise fixed-field degree comparison. The normalized degree on a finite abstract field is the ordinary intrinsic absolute residue degree after changing the finite residue base to the residue subfield selected by that fixed field.

Source context 11 commands

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

namespace LocalClassFieldTheory
open CyclicCohomology RamificationTheory ClassFormation
open LocalFieldTheory
noncomputable section
open scoped Pointwise ValuativeRel
open HilbertRamification.ValuationSubring
open Field.absoluteGaloisGroup
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
/-- The canonical scalar structure on the selected fixed residue field.
Naming these instances keeps typeclass search from unfolding the fixed-field
and residue-action constructions in finite-dimensionality statements. -/
noncomputable local instance localAbstractFixedResidueIntermediateFieldAlgebra
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    Algebra
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  (localAbstractFixedResidueIntermediateField K H).algebra
noncomputable local instance localAbstractFixedResidueIntermediateFieldSMul
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    SMul
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  @Algebra.toSMul _ _ _ _
    (localAbstractFixedResidueIntermediateFieldAlgebra K H)
noncomputable local instance localAbstractFixedResidueIntermediateFieldModule
    (H : ClosedSubgroup (Gal(SeparableClosure K/K))) :
    Module
      (decompositionResidueField K (localSeparableValuationSubring K))
      (localAbstractFixedResidueIntermediateField K H) :=
  @Algebra.toModule _ _ _ _
    (localAbstractFixedResidueIntermediateFieldAlgebra K H)
Lean source · full declaration
theorem localResidueDatum_normalizedDegree_eq_residueAbsoluteDegreeIn
    (H : FiniteAbstractField (Gal(SeparableClosure K/K)))
    (sigma : H.field.toSubgroup) :
    let F := localAbstractFixedResidueIntermediateField K H.field
    letI : Algebra
        (decompositionResidueField K (localSeparableValuationSubring K))
        F := F.algebra
    letI : Module
        (decompositionResidueField K (localSeparableValuationSubring K))
        F := Algebra.toModule
    letI : FiniteDimensional
        (decompositionResidueField K (localSeparableValuationSubring K))
        F :=
      localAbstractFixedResidueIntermediateField_finiteDimensional K H.field
    letI : Finite F := Module.finite_of_finite
      (decompositionResidueField K (localSeparableValuationSubring K))
    letI : Fintype F := Fintype.ofFinite F
    (localResidueDatum K).normalizedDegree
        (H.toFiniteResidueAbstractField (localResidueDatum K)) sigma =
      residueAbsoluteDegreeIn F
        (selectedResidueField (localSeparableValuationSubring K))
        (localAbstractFixedResidueActionOverIntermediateField
          K H.field sigma) := by
  let A := localSeparableValuationSubring K
  let k := decompositionResidueField K A
  let Omega := selectedResidueField A
  let F := localAbstractFixedResidueIntermediateField K H.field
  let : Algebra k F := F.algebra
  let : FiniteDimensional k F :=
    localAbstractFixedResidueIntermediateField_finiteDimensional K H.field
  let : Finite F := Module.finite_of_finite k
  let : Fintype F := Fintype.ofFinite F
  let HF := H.toFiniteResidueAbstractField (localResidueDatum K)
  let tau : Omega ≃ₐ[F] Omega :=
    localAbstractFixedResidueActionOverIntermediateField K H.field sigma
  have htau :
      tau.restrictScalars k =
        localSeparableResidueAlgAction K sigma.1 := by
    apply AlgEquiv.ext
    intro x
    rfl
  have hbase :=
    residueAbsoluteDegreeIn_restrictScalars k Omega F tau
  rw [htau] at hbase
  have hdegree :
      (HF.residueDegree : ℕ) =
        Module.finrank k F :=
    localResidueDatum_residueDegree_eq_selectedResidueFinrank K H
  apply Multiplicative.ext
  apply zHatMulNat_injective
    HF.residueDegree.property
  change
    (HF.residueDegree : ℕ) •
        ((localResidueDatum K).normalizedDegree HF sigma).toAdd =
      (HF.residueDegree : ℕ) •
        (residueAbsoluteDegreeIn F Omega tau).toAdd
  rw [(localResidueDatum K).residueDegree_nsmul_normalizedDegree HF,
    hdegree]
  change
    (residueAbsoluteDegreeIn k Omega
      (localSeparableResidueAlgAction K sigma.1)).toAdd =
        Module.finrank k F •
          (residueAbsoluteDegreeIn F Omega tau).toAdd
  exact congrArg Multiplicative.toAdd hbase

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