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 (L ≃ₐ[K] L)

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

Equations

• ValuationSubring.decompositionSubgroup K A = MulAction.stabilizer (L ≃ₐ[K] L) A

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.

Equations

• ValuationSubring.subMulAction K A = { carrier := ↑A, smul_mem' := ⋯ }

@[instance_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.

Equations

• ValuationSubring.decompositionSubgroupMulSemiringAction K A = { toMulAction := (ValuationSubring.subMulAction K A).mulAction, smul_zero := ⋯, smul_add := ⋯, smul_one := ⋯, smul_mul := ⋯ }

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.

Equations

• ValuationSubring.inertiaSubgroup K A = (MulSemiringAction.toRingAut (↥(ValuationSubring.decompositionSubgroup K A)) (IsLocalRing.ResidueField ↥A)).ker