NYLL
Module

LowerRamificationGroupZeroEqInertia.lean

Nyll.ClassFieldTheory.Theorems.HasseArf.LowerRamificationGroupZeroEqInertia
1 declaration indexed from sourceView source ↗

Module documentation

The zeroth lower group is the inertia group

Mathlib defines inertia through the action on the residue field. The valuation-subring definition of G₀ uses the equivalent condition that every difference σ • x - x belongs to the maximal ideal.

Imports1
Imported by1

Declarations

theorem

lowerRamificationGroup_zero_eq_inertiaSubgroup

L23 ↗
ClassFieldTheory.lowerRamificationGroup_zero_eq_inertiaSubgroup
Documentation

The zeroth lower ramification group agrees with Mathlib's inertia subgroup of the decomposition group.

Source context 2 commands

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

namespace ClassFieldTheory
universe u v
Lean source · statement
theorem lowerRamificationGroup_zero_eq_inertiaSubgroup
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (A : ValuationSubring L) :
    lowerRamificationGroup K A 0 = A.inertiaSubgroup K

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