Module

ResidueActionIndex.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.ResidueActionIndex

5 declarations indexed from sourceView source ↗

Module documentation

Finite local reciprocity: residue-action image indices

This file separates the two group-theoretic comparisons used by the local degree map. The residue-action exact-sequence theorem supplies the actual action of an absolute decomposition group on the selected residue algebraic closure. Once the decomposition group is all of the absolute Galois group, that action is surjective. If a finite-index subgroup has residue-action image equal to the fixing group of a finite residue subextension, its degree image has the ordinary residue-field index.

Imports2

Imported by3

def

toDecompositionGroupOfEqTop

L44 ↗

LocalClassFieldTheory.toDecompositionGroupOfEqTop

Documentation

View every ambient Galois automorphism as a decomposition-group element when the chosen extension valuation has full decomposition group. This is kept generic in the Galois ambient field: the ambient field is the separable closure, not the algebraic closure (the latter need not be Galois over an imperfect local field).

Source context 7 commands

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

namespace LocalClassFieldTheory
open RamificationTheory
open ClassFormation
noncomputable section
universe u v
open HilbertRamification.ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
  [IsGalois K L]

Lean source · full declaration

def toDecompositionGroupOfEqTop
    (A : _root_.ValuationSubring L)
    (hA : decompositionGroup K A = ⊤) :
    (L ≃ₐ[K] L) →* decompositionGroup K A where
  toFun sigma := ⟨sigma, by rw [hA]; exact Subgroup.mem_top sigma⟩
  map_one' := by ext; rfl
  map_mul' _ _ := by ext; rfl

theorem

toDecompositionGroupOfEqTop_coe

L54 ↗

LocalClassFieldTheory.toDecompositionGroupOfEqTop_coe

Documentation

States the theorem toDecompositionGroupOfEqTop_coe.

Source context 8 commands

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

namespace LocalClassFieldTheory
open RamificationTheory
open ClassFormation
noncomputable section
universe u v
open HilbertRamification.ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
  [IsGalois K L]
omit [IsGalois K L] in

Lean source · statement

theorem toDecompositionGroupOfEqTop_coe
    (A : _root_.ValuationSubring L)
    (hA : decompositionGroup K A = ⊤)
    (sigma : L ≃ₐ[K] L) :
    (toDecompositionGroupOfEqTop K A hA sigma : L ≃ₐ[K] L) = sigma

def

residueAlgActionOfEqTop

L63 ↗

LocalClassFieldTheory.residueAlgActionOfEqTop

Documentation

The residue action from the exact sequence, viewed on the whole Galois group when the chosen extension valuation has full decomposition group.

Source context 7 commands

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

namespace LocalClassFieldTheory
open RamificationTheory
open ClassFormation
noncomputable section
universe u v
open HilbertRamification.ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
  [IsGalois K L]

Lean source · statement

def residueAlgActionOfEqTop
    (A : _root_.ValuationSubring L)
    (hA : decompositionGroup K A = ⊤) :
    (L ≃ₐ[K] L) →*
      (selectedResidueField A ≃ₐ[decompositionResidueField K A]
        selectedResidueField A)

theorem

residueAlgActionOfEqTop_surjective

L73 ↗

LocalClassFieldTheory.residueAlgActionOfEqTop_surjective

Documentation

States the theorem residueAlgActionOfEqTop_surjective.

Source context 7 commands

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

namespace LocalClassFieldTheory
open RamificationTheory
open ClassFormation
noncomputable section
universe u v
open HilbertRamification.ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
  [IsGalois K L]

Lean source · statement

theorem residueAlgActionOfEqTop_surjective
    (A : _root_.ValuationSubring L)
    (hA : decompositionGroup K A = ⊤) :
    Function.Surjective (residueAlgActionOfEqTop K A hA)

theorem

residueDegreeImage_index_eq_finrank_of_map_eq_fixingSubgroup

L96 ↗

LocalClassFieldTheory.residueDegreeImage_index_eq_finrank_of_map_eq_fixingSubgroup

Documentation

Finite-subgroup coordinate/index comparison. If the residue action of a subgroup is precisely the subgroup fixing a finite residue field E, then the image of the composite degree map has index [E:k].

Source context 9 commands

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

namespace LocalClassFieldTheory
open RamificationTheory
open ClassFormation
noncomputable section
universe u v
open HilbertRamification.ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
  [IsGalois K L]
section FiniteImageIndex
variable (k Omega : Type)
  [Field k] [Fintype k] [Field Omega] [Algebra k Omega]
  [Algebra.IsAlgebraic k Omega] [IsAlgClosed Omega]

Lean source · statement

theorem residueDegreeImage_index_eq_finrank_of_map_eq_fixingSubgroup
    {G : Type*} [Group G]
    (rho : G →* (Omega ≃ₐ[k] Omega))
    (H : Subgroup G)
    (E : FiniteGaloisIntermediateField k Omega)
    (himage : H.map rho = E.toIntermediateField.fixingSubgroup) :
    (H.map ((residueAbsoluteDegreeIn k Omega).toMonoidHom.comp rho)).index =
      Module.finrank k E

Module documentation

Finite local reciprocity: residue-action image indices

Declarations

toDecompositionGroupOfEqTop

toDecompositionGroupOfEqTop_coe

residueAlgActionOfEqTop

residueAlgActionOfEqTop_surjective

residueDegreeImage_index_eq_finrank_of_map_eq_fixingSubgroup