Module

ArithmeticFrobeniusOrder.lean

Nyll.ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields.ArithmeticFrobeniusOrder

1 declaration indexed from sourceView source ↗

Module documentation

Order of arithmetic Frobenius at an unramified prime

For a prime w of L above v of K, unramifiedness kills the inertia subgroup. The arithmetic Frobenius therefore has order equal to the residue degree at w.

Imports4

Nyll.ClassFieldTheory.Definitions.FrobeniusAndHilbertClassFields.ArithmeticFrobeniusAt
Mathlib.FieldTheory.Finite.Basic
Mathlib.NumberTheory.RamificationInertia.Unramified
Mathlib.RingTheory.Frobenius

Imported by3

theorem

orderOf_arithmeticFrobeniusAt_eq_inertiaDegree

L33 ↗

ClassFieldTheory.orderOf_arithmeticFrobeniusAt_eq_inertiaDegree

Documentation

At an unramified prime, the order of arithmetic Frobenius is the inertia (residue) degree.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory
open NumberField IsDedekindDomain
open scoped Pointwise
universe u v

Lean source · statement

theorem orderOf_arithmeticFrobeniusAt_eq_inertiaDegree
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
    (v : HeightOneSpectrum (𝓞 K))
    (w : HeightOneSpectrum (𝓞 L))
    (hw : w.asIdeal.LiesOver v.asIdeal)
    (hunram : Algebra.IsUnramifiedAt (𝓞 K) w.asIdeal) :
    orderOf (arithmeticFrobeniusAt (K := K) w) =
      w.asIdeal.inertiaDeg (𝓞 K)

Module documentation

Order of arithmetic Frobenius at an unramified prime

Declarations

orderOf_arithmeticFrobeniusAt_eq_inertiaDegree