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
def
valuation_subring.sub_mul_action
(K : Type u_1)
{L : Type u_2}
[field K]
[field L]
[algebra K L]
(A : valuation_subring L) :
The valuation subring A (considered as a subset of L)
is stable under the action of the decomposition group.
@[protected, instance]
def
valuation_subring.decomposition_subgroup_mul_semiring_action
(K : Type u_1)
{L : Type u_2}
[field K]
[field L]
[algebra K L]
(A : valuation_subring L) :
The multiplicative action of the decomposition subgroup on A.
Equations
- valuation_subring.decomposition_subgroup_mul_semiring_action K A = {to_distrib_mul_action := {to_mul_action := {to_has_smul := mul_action.to_has_smul (valuation_subring.sub_mul_action K A).mul_action, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}, smul_one := _, smul_mul := _}
def
valuation_subring.inertia_subgroup
(K : Type u_1)
{L : Type u_2}
[field K]
[field L]
[algebra K L]
(A : valuation_subring L) :
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.