Module

ArithmeticFrobeniusEqOneIffSplitsCompletely.lean

Nyll.ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields.ArithmeticFrobeniusEqOneIffSplitsCompletely

1 declaration indexed from sourceView source ↗

Module documentation

Trivial arithmetic Frobenius and complete splitting

In a finite abelian extension, the Frobenius at an unramified prime is the identity exactly when the base prime splits completely. Complete splitting is expressed only with Mathlib's ramification indices and residue degrees.

Imports3

Imported by4

theorem

arithmeticFrobeniusAt_eq_one_iff_splitsCompletely

L31 ↗

ClassFieldTheory.arithmeticFrobeniusAt_eq_one_iff_splitsCompletely

Documentation

An unramified finite prime splits completely exactly when its arithmetic Frobenius is trivial.

Source context 5 commands

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

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

Lean source · statement

theorem arithmeticFrobeniusAt_eq_one_iff_splitsCompletely
    {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.IsUnramifiedIn (𝓞 L) v.asIdeal) :
    arithmeticFrobeniusAt (K := K) w = 1 ↔
      FinitePrimeSplitsCompletely K L v

Module documentation

Trivial arithmetic Frobenius and complete splitting

Declarations

arithmeticFrobeniusAt_eq_one_iff_splitsCompletely