NYLL
Module

FiniteResidueFrobenius.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.FiniteResidueFrobenius
18 declarations indexed from sourceView source ↗

Module documentation

Finite local reciprocity: finite residue Frobenius coordinates

The degree map used in local reciprocity comes from the arithmetic Frobenius on the algebraic closure of the finite residue field. This file constructs the finite-level source of that map: for every finite extension of a finite field, exponentiation of Frobenius identifies its Galois group with the appropriate cyclic quotient of ℤ̂.

No cyclic generator is chosen. The generator is the actual arithmetic Frobenius x ↦ x ^ #k, and the exponent map is obtained by factoring its integer powers through ZMod [L : k].

Imports4
Imported by3

Declarations

def

finiteResidueFrobeniusIntegerPowers

L40 ↗
LocalClassFieldTheory.finiteResidueFrobeniusIntegerPowers
Documentation

Integer powers of the arithmetic Frobenius, written additively.

Source context 5 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u v w
variable (k : Type u) (L : Type v)
  [Field k] [Fintype k] [Field L] [Finite L] [Algebra k L]
Lean source · statement
def finiteResidueFrobeniusIntegerPowers :
    ℤ →+ Additive (L ≃ₐ[k] L)
theorem

finiteResidueFrobeniusIntegerPowers_degree_eq_zero

L47 ↗
LocalClassFieldTheory.finiteResidueFrobeniusIntegerPowers_degree_eq_zero
Documentation

The order relation which lets integer Frobenius powers factor through ZMod [L : k].

Source context 5 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u v w
variable (k : Type u) (L : Type v)
  [Field k] [Fintype k] [Field L] [Finite L] [Algebra k L]
Lean source · statement
theorem finiteResidueFrobeniusIntegerPowers_degree_eq_zero :
    finiteResidueFrobeniusIntegerPowers k L (Module.finrank k L) = 0
def

finiteResidueFrobeniusExponentHom

L57 ↗
LocalClassFieldTheory.finiteResidueFrobeniusExponentHom
Documentation

The canonical finite-level exponent homomorphism Z/[L:k]Z → Gal(L/k), sending 1 to arithmetic Frobenius.

Source context 5 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u v w
variable (k : Type u) (L : Type v)
  [Field k] [Fintype k] [Field L] [Finite L] [Algebra k L]
Lean source · statement
def finiteResidueFrobeniusExponentHom :
    Multiplicative (ZMod (Module.finrank k L)) →* (L ≃ₐ[k] L)
theorem

finiteResidueFrobeniusExponentHom_intCast

L66 ↗
LocalClassFieldTheory.finiteResidueFrobeniusExponentHom_intCast
Documentation

An integer residue exponent maps to the corresponding power of Frobenius.

Source context 5 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u v w
variable (k : Type u) (L : Type v)
  [Field k] [Fintype k] [Field L] [Finite L] [Algebra k L]
Lean source · statement
theorem finiteResidueFrobeniusExponentHom_intCast (m : ℤ) :
    finiteResidueFrobeniusExponentHom k L
        (Multiplicative.ofAdd (m : ZMod (Module.finrank k L))) =
      (FiniteField.frobeniusAlgEquivOfAlgebraic k L) ^ m
theorem

finiteResidueFrobeniusExponentHom_one

L81 ↗
LocalClassFieldTheory.finiteResidueFrobeniusExponentHom_one
Documentation

Residue exponent one maps to the arithmetic Frobenius automorphism.

Source context 5 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u v w
variable (k : Type u) (L : Type v)
  [Field k] [Fintype k] [Field L] [Finite L] [Algebra k L]
Lean source · statement
theorem finiteResidueFrobeniusExponentHom_one :
    finiteResidueFrobeniusExponentHom k L
        (Multiplicative.ofAdd (1 : ZMod (Module.finrank k L))) =
      FiniteField.frobeniusAlgEquivOfAlgebraic k L
theorem

finiteResidueFrobeniusExponentHom_surjective

L89 ↗
LocalClassFieldTheory.finiteResidueFrobeniusExponentHom_surjective
Documentation

Every finite residue-field automorphism is a power of arithmetic Frobenius, so the canonical exponent homomorphism is onto.

Source context 5 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u v w
variable (k : Type u) (L : Type v)
  [Field k] [Fintype k] [Field L] [Finite L] [Algebra k L]
Lean source · statement
theorem finiteResidueFrobeniusExponentHom_surjective :
    Function.Surjective (finiteResidueFrobeniusExponentHom k L)
theorem

finiteResidueFrobeniusExponentHom_injective

L100 ↗
LocalClassFieldTheory.finiteResidueFrobeniusExponentHom_injective
Documentation

The finite-level Frobenius exponent homomorphism is injective.

Source context 5 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u v w
variable (k : Type u) (L : Type v)
  [Field k] [Fintype k] [Field L] [Finite L] [Algebra k L]
Lean source · statement
theorem finiteResidueFrobeniusExponentHom_injective :
    Function.Injective (finiteResidueFrobeniusExponentHom k L)
def

finiteResidueFrobeniusExponentEquiv

L112 ↗
LocalClassFieldTheory.finiteResidueFrobeniusExponentEquiv
Documentation

Canonical finite-level Frobenius coordinates.

Source context 5 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u v w
variable (k : Type u) (L : Type v)
  [Field k] [Fintype k] [Field L] [Finite L] [Algebra k L]
Lean source · statement
def finiteResidueFrobeniusExponentEquiv :
    Multiplicative (ZMod (Module.finrank k L)) ≃* (L ≃ₐ[k] L)
theorem

finiteResidueFrobeniusExponentEquiv_apply

L120 ↗
LocalClassFieldTheory.finiteResidueFrobeniusExponentEquiv_apply
Documentation

The Frobenius exponent equivalence has the same underlying map as the exponent homomorphism.

Source context 5 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u v w
variable (k : Type u) (L : Type v)
  [Field k] [Fintype k] [Field L] [Finite L] [Algebra k L]
Lean source · statement
theorem finiteResidueFrobeniusExponentEquiv_apply (z) :
    finiteResidueFrobeniusExponentEquiv k L z =
      finiteResidueFrobeniusExponentHom k L z
theorem

finiteResidueFrobeniusExponentEquiv_one

L127 ↗
LocalClassFieldTheory.finiteResidueFrobeniusExponentEquiv_one
Documentation

The Frobenius exponent equivalence sends one to arithmetic Frobenius.

Source context 5 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u v w
variable (k : Type u) (L : Type v)
  [Field k] [Fintype k] [Field L] [Finite L] [Algebra k L]
Lean source · statement
theorem finiteResidueFrobeniusExponentEquiv_one :
    finiteResidueFrobeniusExponentEquiv k L
        (Multiplicative.ofAdd (1 : ZMod (Module.finrank k L))) =
      FiniteField.frobeniusAlgEquivOfAlgebraic k L
def

finiteResidueFrobeniusFromZHat

L135 ↗
LocalClassFieldTheory.finiteResidueFrobeniusFromZHat
Documentation

A profinite exponent acts on a finite residue extension through reduction modulo its degree.

Source context 5 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u v w
variable (k : Type u) (L : Type v)
  [Field k] [Fintype k] [Field L] [Finite L] [Algebra k L]
Lean source · full declaration
def finiteResidueFrobeniusFromZHat :
    ZHatMul →ₜ* (L ≃ₐ[k] L) where
  toFun z := finiteResidueFrobeniusExponentHom k L
    (Multiplicative.ofAdd
      (zHatReduction (Module.finrank k L) Module.finrank_pos z.toAdd))
  map_one' := by
    apply (finiteResidueFrobeniusExponentHom k L).map_one
  map_mul' x y := by
    apply (finiteResidueFrobeniusExponentHom k L).map_mul
  continuous_toFun := by
    apply continuous_of_discreteTopology.comp
    exact continuous_ofAdd.comp
      ((zHatReduction (Module.finrank k L) Module.finrank_pos).continuous_toFun.comp
        continuous_toAdd)
theorem

finiteResidueFrobeniusFromZHat_apply

L152 ↗
LocalClassFieldTheory.finiteResidueFrobeniusFromZHat_apply
Documentation

The profinite Frobenius map depends on reduction modulo the residue extension degree.

Source context 5 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u v w
variable (k : Type u) (L : Type v)
  [Field k] [Fintype k] [Field L] [Finite L] [Algebra k L]
Lean source · statement
theorem finiteResidueFrobeniusFromZHat_apply (z : ZHatMul) :
    finiteResidueFrobeniusFromZHat k L z =
      finiteResidueFrobeniusExponentHom k L
        (Multiplicative.ofAdd
          (zHatReduction (Module.finrank k L) Module.finrank_pos z.toAdd))
theorem

finiteResidueFrobeniusFromZHat_one

L161 ↗
LocalClassFieldTheory.finiteResidueFrobeniusFromZHat_one
Documentation

The distinguished profinite integer 1 acts as arithmetic Frobenius.

Source context 5 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u v w
variable (k : Type u) (L : Type v)
  [Field k] [Fintype k] [Field L] [Finite L] [Algebra k L]
Lean source · statement
theorem finiteResidueFrobeniusFromZHat_one :
    finiteResidueFrobeniusFromZHat k L
        (Multiplicative.ofAdd (1 : ZHat)) =
      FiniteField.frobeniusAlgEquivOfAlgebraic k L
theorem

finiteResidueFrobeniusFromZHat_surjective

L170 ↗
LocalClassFieldTheory.finiteResidueFrobeniusFromZHat_surjective
Documentation

Every automorphism of a finite residue extension is induced by a profinite Frobenius exponent.

Source context 5 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u v w
variable (k : Type u) (L : Type v)
  [Field k] [Fintype k] [Field L] [Finite L] [Algebra k L]
Lean source · statement
theorem finiteResidueFrobeniusFromZHat_surjective :
    Function.Surjective (finiteResidueFrobeniusFromZHat k L)
theorem

finiteResidueFrobeniusFromZHat_eq_one_iff

L186 ↗
LocalClassFieldTheory.finiteResidueFrobeniusFromZHat_eq_one_iff
Documentation

A profinite exponent acts trivially on a finite residue extension exactly when it is zero modulo the extension degree.

Source context 5 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u v w
variable (k : Type u) (L : Type v)
  [Field k] [Fintype k] [Field L] [Finite L] [Algebra k L]
Lean source · statement
theorem finiteResidueFrobeniusFromZHat_eq_one_iff (z : ZHatMul) :
    finiteResidueFrobeniusFromZHat k L z = 1 ↔
      zHatReduction (Module.finrank k L) Module.finrank_pos z.toAdd = 0
theorem

restrictNormalHom_finiteResidueFrobenius

L212 ↗
LocalClassFieldTheory.restrictNormalHom_finiteResidueFrobenius
Documentation

Arithmetic Frobenius commutes with restriction in a tower of finite extensions of a finite field.

Source context 7 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u v w
variable (k : Type u) (L : Type v)
  [Field k] [Fintype k] [Field L] [Finite L] [Algebra k L]
section Tower
variable {E : Type v} {F : Type w}
  [Field E] [Finite E] [Field F] [Finite F]
  [Algebra k E] [Algebra k F] [Algebra E F]
  [IsScalarTower k E F] [Normal k E]
Lean source · statement
theorem restrictNormalHom_finiteResidueFrobenius :
    AlgEquiv.restrictNormalHom E
        (FiniteField.frobeniusAlgEquivOfAlgebraic k F) =
      FiniteField.frobeniusAlgEquivOfAlgebraic k E
theorem

restrictNormalHom_finiteResidueFrobeniusExponentHom

L235 ↗
LocalClassFieldTheory.restrictNormalHom_finiteResidueFrobeniusExponentHom
Documentation

The finite Frobenius exponent coordinates commute with restriction. The exponent on the smaller field is obtained by the canonical reduction Z/[F:k]Z → Z/[E:k]Z.

Source context 7 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u v w
variable (k : Type u) (L : Type v)
  [Field k] [Fintype k] [Field L] [Finite L] [Algebra k L]
section Tower
variable {E : Type v} {F : Type w}
  [Field E] [Finite E] [Field F] [Finite F]
  [Algebra k E] [Algebra k F] [Algebra E F]
  [IsScalarTower k E F] [Normal k E]
Lean source · full declaration
theorem restrictNormalHom_finiteResidueFrobeniusExponentHom
    (z : Multiplicative (ZMod (Module.finrank k F))) :
    AlgEquiv.restrictNormalHom E
        (finiteResidueFrobeniusExponentHom k F z) =
      finiteResidueFrobeniusExponentHom k E
        (Multiplicative.ofAdd
          (ZMod.castHom
            (show Module.finrank k E ∣ Module.finrank k F from
              ⟨Module.finrank E F,
                (Module.finrank_mul_finrank k E F).symm⟩)
            (ZMod (Module.finrank k E)) z.toAdd)) := by
  rcases ZMod.intCast_surjective z.toAdd with ⟨m, hm⟩
  have hz : z = Multiplicative.ofAdd
      (m : ZMod (Module.finrank k F)) := by
    apply Multiplicative.ext
    exact hm.symm
  subst z
  apply AlgEquiv.ext
  intro x
  rw [finiteResidueFrobeniusExponentHom_intCast]
  simp only [toAdd_ofAdd]
  have hred :
      ZMod.castHom
          (show Module.finrank k E ∣ Module.finrank k F from
            ⟨Module.finrank E F,
              (Module.finrank_mul_finrank k E F).symm⟩)
          (ZMod (Module.finrank k E))
          (m : ZMod (Module.finrank k F)) =
        (m : ZMod (Module.finrank k E)) := by
    exact map_intCast _ m
  rw [hred, finiteResidueFrobeniusExponentHom_intCast]
  have hfrob := restrictNormalHom_finiteResidueFrobenius
    (k := k) (E := E) (F := F)
  have hpow := congrArg (fun sigma : E ≃ₐ[k] E => sigma ^ m) hfrob
  rw [map_zpow]
  exact DFunLike.congr_fun hpow x
theorem

restrictNormalHom_finiteResidueFrobeniusFromZHat

L274 ↗
LocalClassFieldTheory.restrictNormalHom_finiteResidueFrobeniusFromZHat
Documentation

The actions of ℤ̂ on finite residue extensions commute with restriction in finite towers.

Source context 7 commands

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

namespace LocalClassFieldTheory
open ClassFormation
noncomputable section
universe u v w
variable (k : Type u) (L : Type v)
  [Field k] [Fintype k] [Field L] [Finite L] [Algebra k L]
section Tower
variable {E : Type v} {F : Type w}
  [Field E] [Finite E] [Field F] [Finite F]
  [Algebra k E] [Algebra k F] [Algebra E F]
  [IsScalarTower k E F] [Normal k E]
Lean source · statement
theorem restrictNormalHom_finiteResidueFrobeniusFromZHat (z : ZHatMul) :
    AlgEquiv.restrictNormalHom E
        (finiteResidueFrobeniusFromZHat k F z) =
      finiteResidueFrobeniusFromZHat k E z

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