NYLL
Module

AlgebraicInertiaCharZero.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.AlgebraicInertiaCharZero
1 declaration indexed from sourceView source ↗

Module documentation

Inertia in residue characteristic zero over an algebraic Galois extension

Every field element lies in its actual finite Galois normal closure. Pullback restricts inertia to that layer, and the comap valuation subring has residue characteristic zero. Finite inertia is commutative there, and the defining restriction formula gives commutativity on each element of the original field. No Henselianity, discreteness, or finite-residue hypothesis is used.

Imports5
Imported by1

Declarations

theorem

inertiaGroup_isMulCommutative_of_isGalois_residueCharZero

L30 ↗
RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup_isMulCommutative_of_isGalois_residueCharZero
Documentation

Inertia is commutative for any algebraic Galois extension in residue characteristic zero, using the specified valuation subring upstairs.

Source context 2 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
universe u v
Lean source · statement
theorem inertiaGroup_isMulCommutative_of_isGalois_residueCharZero
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L] [IsGalois K L]
    (A : _root_.ValuationSubring L) [CharZero (IsLocalRing.ResidueField A)] :
    IsMulCommutative (inertiaGroup K A)

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