Module

ResidueDatum.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.ResidueDatum

4 declarations indexed from sourceView source ↗

Module documentation

Finite local reciprocity: the residue datum and its finite indices

The arithmetic-Frobenius degree on an algebraic closure of a finite field is packaged as the initial datum of the abstract class-formation framework. For every finite residue subextension, the image of its fixing subgroup is proved to be exactly n ℤ̂; consequently the abstract residue degree is the ordinary field degree. This is the finite-coordinate comparison needed in the local-field specialization.

Imports3

Imported by3

def

residueDatumIn

L37 ↗

LocalClassFieldTheory.residueDatumIn

Documentation

The abstract class-formation datum supplied by arithmetic Frobenius on the actual residue algebraic closure.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory
open ClassFormation
noncomputable section
variable (k Omega : Type)
  [Field k] [Fintype k] [Field Omega] [Algebra k Omega]
  [Algebra.IsAlgebraic k Omega] [IsAlgClosed Omega]

Lean source · full declaration

def residueDatumIn : DegreeData (Omega ≃ₐ[k] Omega) where
  degree := residueAbsoluteDegreeIn k Omega
  degree_surjective := (residueAbsoluteFrobeniusEquivIn k Omega).symm.surjective

theorem

mem_fixingSubgroup_iff_restrictNormalHom_eq_one

L42 ↗

LocalClassFieldTheory.mem_fixingSubgroup_iff_restrictNormalHom_eq_one

Source context 6 commands

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

namespace LocalClassFieldTheory
open RamificationTheory
open ClassFormation
noncomputable section
variable (k Omega : Type)
  [Field k] [Fintype k] [Field Omega] [Algebra k Omega]
  [Algebra.IsAlgebraic k Omega] [IsAlgClosed Omega]
omit [Fintype k] [Algebra.IsAlgebraic k Omega] [IsAlgClosed Omega] in

Lean source · statement

theorem mem_fixingSubgroup_iff_restrictNormalHom_eq_one
    (E : FiniteGaloisIntermediateField k Omega)
    (sigma : Omega ≃ₐ[k] Omega) :
    sigma ∈ E.toIntermediateField.fixingSubgroup ↔
      AlgEquiv.restrictNormalHom E sigma = 1

theorem

residueDatumIn_fieldImage_closedFixingSubgroup

L67 ↗

LocalClassFieldTheory.residueDatumIn_fieldImage_closedFixingSubgroup

Documentation

The degree image of the subgroup fixing a finite residue extension of degree n is exactly n ℤ̂.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory
open ClassFormation
noncomputable section
variable (k Omega : Type)
  [Field k] [Fintype k] [Field Omega] [Algebra k Omega]
  [Algebra.IsAlgebraic k Omega] [IsAlgClosed Omega]

Lean source · statement

theorem residueDatumIn_fieldImage_closedFixingSubgroup
    (E : FiniteGaloisIntermediateField k Omega) :
    (residueDatumIn k Omega).fieldImage
        (closedFixingSubgroup k Omega E) =
      (zHatMulNat (Module.finrank k E)).toAddMonoidHom.range.toSubgroup

theorem

residueDatumIn_fieldImage_index_closedFixingSubgroup

L112 ↗

LocalClassFieldTheory.Internal.residueDatumIn_fieldImage_index_closedFixingSubgroup

Documentation

Internal finite-coordinate calculation: the degree image of the fixing subgroup has natural index equal to the ordinary residue-field degree. Public residue-degree APIs use Cardinal or a finite residue-field bundle.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory
open ClassFormation
noncomputable section
variable (k Omega : Type)
  [Field k] [Fintype k] [Field Omega] [Algebra k Omega]
  [Algebra.IsAlgebraic k Omega] [IsAlgClosed Omega]

Lean source · statement

theorem Internal.residueDatumIn_fieldImage_index_closedFixingSubgroup
    (E : FiniteGaloisIntermediateField k Omega) :
    ((residueDatumIn k Omega).fieldImage
        (closedFixingSubgroup k Omega E)).index = Module.finrank k E

Module documentation

Finite local reciprocity: the residue datum and its finite indices

Declarations

residueDatumIn

mem_fixingSubgroup_iff_restrictNormalHom_eq_one

residueDatumIn_fieldImage_closedFixingSubgroup

residueDatumIn_fieldImage_index_closedFixingSubgroup