NYLL
Module

ResidueAbsoluteDegree.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.ResidueAbsoluteDegree
21 declarations indexed from sourceView source ↗

Module documentation

Finite local reciprocity: the absolute residue degree map

For a finite field k, arithmetic Frobenius identifies the absolute Galois group of k with the profinite integers. This file proves the missing global statement from the compatible finite Frobenius coordinates:

  • every positive integer occurs as the degree of an actual finite Galois

intermediate field of AlgebraicClosure k;

  • those fields detect every finite coordinate of ℤ̂, hence the assembled

Frobenius map is injective;

  • its compact image is all of the absolute Galois group;
  • inversion gives the continuous degree map of the finite local reciprocity construction.
Imports4
Imported by3

Declarations

instance

finiteFieldRingCharPrime

L44 ↗
LocalClassFieldTheory.finiteFieldRingCharPrime
Source context 9 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
omit [Fintype k] in
Lean source · statement
instance finiteFieldRingCharPrime [Finite k] : Fact (ringChar k).Prime
instance

absoluteGaloisGroupT2

L47 ↗
LocalClassFieldTheory.absoluteGaloisGroupT2
Source context 8 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
Lean source · statement
instance absoluteGaloisGroupT2 :
    T2Space (Field.absoluteGaloisGroup k)
def

finiteResidueExtensionEmbedding

L54 ↗
LocalClassFieldTheory.finiteResidueExtensionEmbedding
Documentation

A chosen embedding of the degree-n finite extension of k into its algebraic closure.

Source context 8 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
Lean source · statement
def finiteResidueExtensionEmbedding (n : ℕ) [NeZero n] :
    FiniteField.Extension k (ringChar k) n →ₐ[k] AlgebraicClosure k
def

finiteResidueIntermediateField

L59 ↗
LocalClassFieldTheory.finiteResidueIntermediateField
Documentation

The image in AlgebraicClosure k of the chosen degree-n extension.

Source context 8 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
Lean source · statement
def finiteResidueIntermediateField (n : ℕ) [NeZero n] :
    IntermediateField k (AlgebraicClosure k)
def

finiteResidueExtensionEquivIntermediate

L66 ↗
LocalClassFieldTheory.finiteResidueExtensionEquivIntermediate
Documentation

The chosen degree-n extension is isomorphic to its image in the algebraic closure.

Source context 8 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
Lean source · statement
def finiteResidueExtensionEquivIntermediate (n : ℕ) [NeZero n] :
    FiniteField.Extension k (ringChar k) n ≃ₐ[k]
      finiteResidueIntermediateField k n
def

finiteResidueGaloisIntermediateField

L74 ↗
LocalClassFieldTheory.finiteResidueGaloisIntermediateField
Documentation

For every n > 0, an actual degree-n finite Galois intermediate field inside AlgebraicClosure k.

Source context 8 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
Lean source · full declaration
def finiteResidueGaloisIntermediateField (n : ℕ) [NeZero n] :
    FiniteGaloisIntermediateField k (AlgebraicClosure k) where
  toIntermediateField := finiteResidueIntermediateField k n
  finiteDimensional := Module.Finite.equiv
    (finiteResidueExtensionEquivIntermediate k n).toLinearEquiv
  isGalois := IsGalois.of_algEquiv
    (finiteResidueExtensionEquivIntermediate k n)
theorem

finrank_finiteResidueGaloisIntermediateField

L84 ↗
LocalClassFieldTheory.finrank_finiteResidueGaloisIntermediateField
Documentation

The canonical finite residue subextension of level n has degree n.

Source context 8 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
Lean source · statement
theorem finrank_finiteResidueGaloisIntermediateField (n : ℕ) [NeZero n] :
    Module.finrank k (finiteResidueGaloisIntermediateField k n) = n
theorem

residueAbsoluteFrobenius_algebraicClosure_injective

L94 ↗
LocalClassFieldTheory.residueAbsoluteFrobenius_algebraicClosure_injective
Documentation

Finite extensions of every degree detect all profinite coordinates, so the assembled Frobenius map on the algebraic closure is injective.

Source context 8 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
Lean source · statement
theorem residueAbsoluteFrobenius_algebraicClosure_injective :
    Function.Injective
      (residueAbsoluteFrobenius k (AlgebraicClosure k))
theorem

mem_range_algebraMap_iff_frobenius_fixed

L126 ↗
LocalClassFieldTheory.mem_range_algebraMap_iff_frobenius_fixed
Documentation

In an algebraic closure of a finite field, the fixed points of arithmetic Frobenius are exactly the elements of the base field.

Source context 8 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
Lean source · statement
theorem mem_range_algebraMap_iff_frobenius_fixed
    (x : AlgebraicClosure k) :
    x ∈ Set.range (algebraMap k (AlgebraicClosure k)) ↔
      FiniteField.frobeniusAlgEquivOfAlgebraic k (AlgebraicClosure k) x = x
def

residueAbsoluteFrobeniusRange

L153 ↗
LocalClassFieldTheory.residueAbsoluteFrobeniusRange
Documentation

The compact image of the assembled Frobenius map, as a closed subgroup of the absolute Galois group.

Source context 8 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
Lean source · full declaration
def residueAbsoluteFrobeniusRange :
    ClosedSubgroup (AlgebraicClosure k ≃ₐ[k] AlgebraicClosure k) where
  toSubgroup :=
    (residueAbsoluteFrobenius k (AlgebraicClosure k)).toMonoidHom.range
  isClosed' := by
    change IsClosed
      (Set.range (residueAbsoluteFrobenius k (AlgebraicClosure k)))
    exact (isCompact_range
      (residueAbsoluteFrobenius k
        (AlgebraicClosure k)).continuous_toFun).isClosed
theorem

fixedField_residueAbsoluteFrobeniusRange

L166 ↗
LocalClassFieldTheory.fixedField_residueAbsoluteFrobeniusRange
Documentation

The compact Frobenius image fixes no elements beyond the base finite field.

Source context 8 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
Lean source · statement
theorem fixedField_residueAbsoluteFrobeniusRange :
    IntermediateField.fixedField
        (residueAbsoluteFrobeniusRange k).toSubgroup = ⊥
theorem

residueAbsoluteFrobeniusRange_eq_top

L188 ↗
LocalClassFieldTheory.residueAbsoluteFrobeniusRange_eq_top
Documentation

The closed Frobenius image is the whole absolute Galois group.

Source context 8 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
Lean source · statement
theorem residueAbsoluteFrobeniusRange_eq_top :
    (residueAbsoluteFrobeniusRange k).toSubgroup = ⊤
theorem

residueAbsoluteFrobenius_algebraicClosure_surjective

L198 ↗
LocalClassFieldTheory.residueAbsoluteFrobenius_algebraicClosure_surjective
Documentation

The assembled Frobenius map onto the absolute Galois group of a finite field is surjective.

Source context 8 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
Lean source · statement
theorem residueAbsoluteFrobenius_algebraicClosure_surjective :
    Function.Surjective
      (residueAbsoluteFrobenius k (AlgebraicClosure k))
theorem

residueAbsoluteFrobenius_algebraicClosure_bijective

L209 ↗
LocalClassFieldTheory.residueAbsoluteFrobenius_algebraicClosure_bijective
Documentation

The Frobenius parameter map is a bijection for the algebraic closure of a finite field.

Source context 8 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
Lean source · statement
theorem residueAbsoluteFrobenius_algebraicClosure_bijective :
    Function.Bijective
      (residueAbsoluteFrobenius k (AlgebraicClosure k))
def

residueAbsoluteFrobeniusMulEquiv

L217 ↗
LocalClassFieldTheory.residueAbsoluteFrobeniusMulEquiv
Documentation

The underlying multiplicative equivalence between profinite integers and the absolute Galois group of a finite field.

Source context 8 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
Lean source · statement
def residueAbsoluteFrobeniusMulEquiv :
    ZHatMul ≃* Field.absoluteGaloisGroup k
def

residueAbsoluteFrobeniusEquiv

L225 ↗
LocalClassFieldTheory.residueAbsoluteFrobeniusEquiv
Documentation

Arithmetic Frobenius gives a topological group equivalence ℤ̂ ≃ Gal(k̄/k).

Source context 8 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
Lean source · full declaration
def residueAbsoluteFrobeniusEquiv :
    ZHatMul ≃ₜ* Field.absoluteGaloisGroup k where
  toMulEquiv := residueAbsoluteFrobeniusMulEquiv k
  continuous_toFun :=
    (residueAbsoluteFrobenius k
      (AlgebraicClosure k)).continuous_toFun
  continuous_invFun :=
    Continuous.continuous_symm_of_equiv_compact_to_t2
      (f := (residueAbsoluteFrobeniusMulEquiv k).toEquiv)
      (residueAbsoluteFrobenius k
        (AlgebraicClosure k)).continuous_toFun
def

residueAbsoluteDegree

L240 ↗
LocalClassFieldTheory.residueAbsoluteDegree
Documentation

Finite local reciprocity, absolute residue degree. The inverse of arithmetic Frobenius coordinates, as a continuous surjective homomorphism Gal(k̄/k) → ℤ̂.

Source context 8 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
Lean source · statement
def residueAbsoluteDegree :
    Field.absoluteGaloisGroup k →ₜ* ZHatMul
theorem

residueAbsoluteDegree_frobenius

L247 ↗
LocalClassFieldTheory.residueAbsoluteDegree_frobenius
Documentation

The degree map is normalized by sending arithmetic Frobenius to 1.

Source context 8 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
Lean source · statement
theorem residueAbsoluteDegree_frobenius :
    residueAbsoluteDegree k
        (FiniteField.frobeniusAlgEquivOfAlgebraic k (AlgebraicClosure k)) =
      Multiplicative.ofAdd (1 : ZHat)
theorem

finiteResidueFrobeniusIntermediate_residueAbsoluteDegree

L266 ↗
LocalClassFieldTheory.finiteResidueFrobeniusIntermediate_residueAbsoluteDegree
Documentation

On every finite Galois residue subextension, the absolute degree of an automorphism is exactly its canonical Frobenius exponent. This is the finite-coordinate compatibility needed when the residue degree map is pulled back to the absolute Galois group of a local field.

Source context 8 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
Lean source · statement
theorem finiteResidueFrobeniusIntermediate_residueAbsoluteDegree
    (sigma : Field.absoluteGaloisGroup k)
    (E : FiniteGaloisIntermediateField k (AlgebraicClosure k)) :
    finiteResidueFrobeniusIntermediate k (AlgebraicClosure k) E
        (residueAbsoluteDegree k sigma) =
      AlgEquiv.restrictNormalHom E sigma
theorem

finiteResidueFrobeniusExponentHom_degree_coordinate

L289 ↗
LocalClassFieldTheory.finiteResidueFrobeniusExponentHom_degree_coordinate
Documentation

Coordinate form of finiteResidueFrobeniusIntermediate_residueAbsoluteDegree: reducing the absolute degree modulo [E:k] and exponentiating arithmetic Frobenius gives the actual restriction of the automorphism to E.

Source context 8 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
Lean source · full declaration
theorem finiteResidueFrobeniusExponentHom_degree_coordinate
    (sigma : Field.absoluteGaloisGroup k)
    (E : FiniteGaloisIntermediateField k (AlgebraicClosure k)) :
    letI : Finite E := Module.finite_of_finite k
    finiteResidueFrobeniusExponentHom k E
        (Multiplicative.ofAdd
          (zHatReduction (Module.finrank k E) Module.finrank_pos
            (residueAbsoluteDegree k sigma).toAdd)) =
      AlgEquiv.restrictNormalHom E sigma := by
  let : Finite E := Module.finite_of_finite k
  exact finiteResidueFrobeniusIntermediate_residueAbsoluteDegree k sigma E
theorem

finiteResidueFrobeniusExponentEquiv_symm_restrict

L303 ↗
LocalClassFieldTheory.finiteResidueFrobeniusExponentEquiv_symm_restrict
Documentation

Equivalently, the inverse finite Frobenius coordinate of a restriction is the reduction of the absolute degree modulo the residue extension degree.

Source context 8 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u
open CategoryTheory Opposite
open FiniteGaloisIntermediateField ProfiniteGrp
open Polynomial
variable (k : Type u) [Field k] [Fintype k]
Lean source · full declaration
theorem finiteResidueFrobeniusExponentEquiv_symm_restrict
    (sigma : Field.absoluteGaloisGroup k)
    (E : FiniteGaloisIntermediateField k (AlgebraicClosure k)) :
    letI : Finite E := Module.finite_of_finite k
    (finiteResidueFrobeniusExponentEquiv k E).symm
        (AlgEquiv.restrictNormalHom E sigma) =
      Multiplicative.ofAdd
        (zHatReduction (Module.finrank k E) Module.finrank_pos
          (residueAbsoluteDegree k sigma).toAdd) := by
  let : Finite E := Module.finite_of_finite k
  apply (finiteResidueFrobeniusExponentEquiv k E).injective
  rw [(finiteResidueFrobeniusExponentEquiv k E).apply_symm_apply]
  exact (finiteResidueFrobeniusExponentHom_degree_coordinate k sigma E).symm

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