Module

ArithmeticFrobeniusRestrictTower.lean

Nyll.ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields.ArithmeticFrobeniusRestrictTower

2 declarations indexed from sourceView source ↗

Module documentation

Arithmetic Frobenius in a finite abelian tower

At a prime unramified in the top field, restriction of arithmetic Frobenius to an intermediate field is arithmetic Frobenius at the prime below it.

Imports3

Imported by1

Nyll.ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields.All

theorem

arithmeticFinitePlacePrimeArtin_restrict_tower_of_globalArtin

L27 ↗

ClassFieldTheory.arithmeticFinitePlacePrimeArtin_restrict_tower_of_globalArtin

Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory
open NumberField IsDedekindDomain IdeleGroup
open GlobalClassFieldTheory.GlobalClassFields

Lean source · statement

theorem arithmeticFinitePlacePrimeArtin_restrict_tower_of_globalArtin
    (K E L : Type) [Field K] [Field E] [Field L]
    [NumberField K] [NumberField E] [NumberField L]
    [Algebra K E] [Algebra E L] [Algebra K L] [IsScalarTower K E L]
    [IsAbelianGalois K E] [IsAbelianGalois K L]
    (v : HeightOneSpectrum (𝓞 K)) :
    AlgEquiv.restrictNormalHom E
        (arithmeticFinitePlacePrimeArtin (K := K) (L := L) v) =
      arithmeticFinitePlacePrimeArtin (K := K) (L := E) v

theorem

arithmeticFrobeniusAt_restrict_tower

L48 ↗

ClassFieldTheory.arithmeticFrobeniusAt_restrict_tower

Documentation

In a finite abelian tower K ⊆ E ⊆ L, arithmetic Frobenius at an unramified prime of L restricts to arithmetic Frobenius at the specified prime of E below it.