Module

ArithmeticFrobeniusAt.lean

Nyll.ClassFieldTheory.Definitions.FrobeniusAndHilbertClassFields.ArithmeticFrobeniusAt

1 declaration indexed from sourceView source ↗

Module documentation

Arithmetic Frobenius at a finite prime

Imports4

Mathlib.FieldTheory.Galois.Abelian
Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Mathlib.NumberTheory.RamificationInertia.Galois
Mathlib.RingTheory.Frobenius

Imported by13

def

arithmeticFrobeniusAt

L29 ↗

ClassFieldTheory.arithmeticFrobeniusAt

Documentation

Mathlib's chosen arithmetic Frobenius lift at a finite prime of the extension field. At a ramified prime such a lift need not be unique.

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

def arithmeticFrobeniusAt
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
    (w : HeightOneSpectrum (𝓞 L)) : L ≃ₐ[K] L

Module documentation

Arithmetic Frobenius at a finite prime

Declarations

arithmeticFrobeniusAt