NYLL
Module

CyclotomicDegreeBound.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.CyclotomicDegreeBound
3 declarations indexed from sourceView source ↗

Module documentation

Cyclotomic degree bounds for inertia

An inertia group is bounded by the degree of its Galois extension. An embedding into a concrete cyclotomic field therefore bounds its cardinality by Euler's totient.

Imports3
Imported by2

Declarations

theorem

natCard_inertiaGroup_le_finrank

L27 ↗
HilbertRamification.natCard_inertiaGroup_le_finrank
Documentation

The inertia group of a finite Galois extension has cardinality at most the degree of the extension.

Source context 3 commands

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

noncomputable section
namespace HilbertRamification
open Polynomial
Lean source · statement
theorem natCard_inertiaGroup_le_finrank
    {K E : Type*} [Field K] [Field E] [Algebra K E]
    [FiniteDimensional K E] [IsGalois K E]
    (A : _root_.ValuationSubring E) :
    Nat.card
        (RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup K A) ≤
      Module.finrank K E
theorem

cyclotomicField_finrank_le_totient

L55 ↗
HilbertRamification.cyclotomicField_finrank_le_totient
Documentation

Over a characteristic-zero field, the concrete cyclotomic field of order m has degree at most φ(m).

Source context 3 commands

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

noncomputable section
namespace HilbertRamification
open Polynomial
Lean source · statement
theorem cyclotomicField_finrank_le_totient
    (K : Type*) [Field K] [CharZero K] (m : ℕ) (hm : 0 < m) :
    Module.finrank K (CyclotomicField m K) ≤ Nat.totient m
theorem

natCard_inertiaGroup_le_totient_of_cyclotomicEmbedding

L91 ↗
HilbertRamification.natCard_inertiaGroup_le_totient_of_cyclotomicEmbedding
Documentation

A concrete cyclotomic embedding bounds the inertia cardinality by the totient of its defining order.

Source context 3 commands

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

noncomputable section
namespace HilbertRamification
open Polynomial
Lean source · statement
theorem natCard_inertiaGroup_le_totient_of_cyclotomicEmbedding
    {K E : Type*} [Field K] [CharZero K] [Field E] [Algebra K E]
    [FiniteDimensional K E] [IsGalois K E]
    (A : _root_.ValuationSubring E) {m : ℕ} (hm : 0 < m)
    (i : E →ₐ[K] CyclotomicField m K) :
    Nat.card
        (RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup K A) ≤
      Nat.totient m

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.