mathlib3 documentation

ring_theory.valuation.ramification_group

Ramification groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The decomposition subgroup and inertia subgroups.

TODO: Define higher ramification groups in lower numbering

@[reducible]
def valuation_subring.decomposition_subgroup (K : Type u_1) {L : Type u_2} [field K] [field L] [algebra K L] (A : valuation_subring L) :

The decomposition subgroup defined as the stabilizer of the action on the type of all valuation subrings of the field.

Equations

The valuation subring A (considered as a subset of L) is stable under the action of the decomposition group.

Equations

The inertia subgroup defined as the kernel of the group homomorphism from the decomposition subgroup to the group of automorphisms of the residue field of A.

Equations