Module

ArithmeticFrobeniusIndependentOfPrime.lean

Nyll.ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields.ArithmeticFrobeniusIndependentOfPrime

1 declaration indexed from sourceView source ↗

Module documentation

Independence of arithmetic Frobenius from the prime above

At an unramified prime of an abelian extension, all primes above the same finite base prime give the same canonical arithmetic Frobenius element. This is the equality, rather than merely conjugacy, needed to avoid choosing an upstairs prime.

Imports4

Nyll.ClassFieldTheory.Definitions.FrobeniusAndHilbertClassFields.ArithmeticFrobeniusAt
Mathlib.NumberTheory.RamificationInertia.Unramified
Mathlib.RingTheory.DedekindDomain.Factorization
Mathlib.RingTheory.Frobenius

Imported by2

theorem

arithmeticFrobeniusAt_eq_of_primesAbove

L32 ↗

ClassFieldTheory.arithmeticFrobeniusAt_eq_of_primesAbove

Documentation

At an unramified finite prime of an abelian extension, arithmetic Frobenius is independent of the chosen prime above the base prime.

Source context 5 commands

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

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

Lean source · statement

theorem arithmeticFrobeniusAt_eq_of_primesAbove
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
    (v : HeightOneSpectrum (𝓞 K))
    (w w' : HeightOneSpectrum (𝓞 L))
    (hw : w.asIdeal.LiesOver v.asIdeal)
    (hw' : w'.asIdeal.LiesOver v.asIdeal)
    (_hunram : Algebra.IsUnramifiedAt (𝓞 K) w.asIdeal) :
    arithmeticFrobeniusAt (K := K) w =
      arithmeticFrobeniusAt (K := K) w'

Module documentation

Independence of arithmetic Frobenius from the prime above

Declarations

arithmeticFrobeniusAt_eq_of_primesAbove