Module

AlgebraicRamificationCharZero.lean

Nyll.EtaleFundamentalGroups.Inertia.AlgebraicRamificationCharZero

1 declaration indexed from sourceView source ↗

Module documentation

Wild inertia in residue characteristic zero

An element of the actual ramification subgroup restricts to ramification at every finite Galois layer. In residue characteristic zero those finite groups are trivial. Every field element belongs to a finite Galois layer, so the original automorphism is the identity.

This supplies the residue-characteristic-zero wild-inertia assertion of Stacks Project Tag 0BUA for valuation subrings, including infinite extensions. It does not require Henselianity, discreteness, or a perfect residue field.

Imports4

Imported by1

Nyll.EtaleFundamentalGroups.Inertia.All

theorem

ramificationGroup_eq_bot_of_isGalois_residueCharZero

L33 ↗

EtaleFundamentalGroups.Inertia.ramificationGroup_eq_bot_of_isGalois_residueCharZero

Documentation

Wild inertia is trivial in residue characteristic zero for a possibly infinite Galois extension and any chosen valuation subring upstairs.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
open RamificationTheory.HilbertRamification.ValuationSubring
universe u v

Lean source · statement

theorem ramificationGroup_eq_bot_of_isGalois_residueCharZero
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L] [IsGalois K L]
    (A : ValuationSubring L) [CharZero (IsLocalRing.ResidueField A)] :
    ramificationGroup K A = ⊥

Module documentation

Wild inertia in residue characteristic zero

Declarations

ramificationGroup_eq_bot_of_isGalois_residueCharZero