Ramification groups

The decomposition subgroup and inertia subgroups.

TODO: Define higher ramification groups in lower numbering

@[reducible, inline]

abbrev ValuationSubring.decompositionSubgroup (K : Type u_1) {L : Type u_2} [Field K] [Field L] [Algebra K L] (A : ValuationSubring L) : Subgroup Gal(L/K)

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

def ValuationSubring.subMulAction (K : Type u_1) {L : Type u_2} [Field K] [Field L] [Algebra K L] (A : ValuationSubring L) : SubMulAction (↥(decompositionSubgroup K A)) L

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

@[implicit_reducible]

instance ValuationSubring.decompositionSubgroupMulSemiringAction (K : Type u_1) {L : Type u_2} [Field K] [Field L] [Algebra K L] (A : ValuationSubring L) : MulSemiringAction ↥(decompositionSubgroup K A) ↥A

The multiplicative action of the decomposition subgroup on A.

noncomputable def ValuationSubring.inertiaSubgroup (K : Type u_1) {L : Type u_2} [Field K] [Field L] [Algebra K L] (A : ValuationSubring L) : Subgroup ↥(decompositionSubgroup K A)

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.