Module

ArithmeticFrobeniusIsArithmetic.lean

Nyll.ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields.ArithmeticFrobeniusIsArithmetic

1 declaration indexed from sourceView source ↗

Module documentation

Arithmetic Frobenius satisfies the residue-field congruence

This statement exposes Mathlib's intrinsic arithmetic Frobenius, rather than an element named through a particular implementation of the global Artin map. It is therefore the precise bridge to IsArithFrobAt that downstream ramification arguments can use.

Imports1

Nyll.ClassFieldTheory.Definitions.FrobeniusAndHilbertClassFields.ArithmeticFrobeniusAt

Imported by1

Nyll.ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields.All

theorem

arithmeticFrobeniusAt_isArithFrobAt

L30 ↗

ClassFieldTheory.arithmeticFrobeniusAt_isArithFrobAt

Documentation

The chosen arithmetic Frobenius at w satisfies Mathlib's defining residue-field Frobenius congruence.

Source context 5 commands

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

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

Lean source · statement

theorem arithmeticFrobeniusAt_isArithFrobAt
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
    (w : HeightOneSpectrum (𝓞 L)) :
    IsArithFrobAt (𝓞 K) (arithmeticFrobeniusAt (K := K) w) w.asIdeal

Module documentation

Arithmetic Frobenius satisfies the residue-field congruence

Declarations

arithmeticFrobeniusAt_isArithFrobAt