Ramification groups

The decomposition subgroup and inertia subgroups.

TODO: Define higher ramification groups in lower numbering

@[reducible]

def 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 (↥(ValuationSubring.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' := (_ : ∀ (g : ↥(ValuationSubring.decompositionSubgroup K A)), ∀ x ∈ ↑A, g • x ∈ ↑A) }

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

The multiplicative action of the decomposition subgroup on A.

Equations

• One or more equations did not get rendered due to their size.

def ValuationSubring.inertiaSubgroup (K : Type u_1) {L : Type u_2} [Field K] [Field L] [Algebra K L] (A : ValuationSubring L) : Subgroup ↥(ValuationSubring.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 = MonoidHom.ker (MulSemiringAction.toRingAut (↥(ValuationSubring.decompositionSubgroup K A)) (LocalRing.ResidueField ↥A))