The action of a decomposition group on its valuation subring

For a valuation subring A of a field L and a subfield K, Mathlib's ValuationSubring.decompositionSubgroup K A acts on A by restricting its action on L. This file records that the restricted action is computed in L, and that it is faithful because L is the field of fractions of A.

Main results

• ValuationSubring.coe_decompositionSubgroup_smul: the action on A is the restriction of the action on L.
• ValuationSubring.decompositionSubgroup.ext: two elements of the decomposition group that agree on A are equal.
• ValuationSubring.instFaithfulSMulDecompositionSubgroup: the decomposition group acts faithfully on A.

@[simp]

theorem ValuationSubring.coe_decompositionSubgroup_smul {K : Type w} {L : Type w'} [Field K] [Field L] [Algebra K L] (A : ValuationSubring L) (g : ↥(decompositionSubgroup K A)) (x : ↥A) : ↑(g • x) = ↑g ↑x

The action of a decomposition group on its valuation subring is the restriction of its action on the fraction field.

theorem ValuationSubring.decompositionSubgroup.ext {K : Type w} {L : Type w'} [Field K] [Field L] [Algebra K L] (A : ValuationSubring L) {g h : ↥(decompositionSubgroup K A)} (hgh : ∀ (x : ↥A), ↑g ↑x = ↑h ↑x) : g = h

Two automorphisms in the decomposition group of a valuation subring that agree on the valuation subring are equal, because its ambient field is its field of fractions.

theorem ValuationSubring.decompositionSubgroup.ext_iff {K : Type w} {L : Type w'} [Field K] [Field L] [Algebra K L] {A : ValuationSubring L} {g h : ↥(decompositionSubgroup K A)} : g = h ↔ ∀ (x : ↥A), ↑g ↑x = ↑h ↑x

instance ValuationSubring.instFaithfulSMulDecompositionSubgroup {K : Type w} {L : Type w'} [Field K] [Field L] [Algebra K L] (A : ValuationSubring L) : FaithfulSMul ↥(decompositionSubgroup K A) ↥A

The decomposition group of a valuation subring acts faithfully on that subring.