feat(ring_theory/valuation/valuation_subring): Add `valuation_subring…

….inertia_subgroup` (#17086)

The decomposition and inertia subgroups.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Michail Karatarakis <40603357+mkaratarakis@users.noreply.github.com>

src/ring_theory/ideal/local_ring.lean

@@ -389,6 +389,17 @@ is the residue field of `R`. -/
   map_mul' := λ e₁ e₂, map_equiv_trans e₂ e₁,
   map_one' := map_equiv_refl }
 
+section mul_semiring_action
+variables (G : Type*) [group G] [mul_semiring_action G R]
+
+/-- If `G` acts on `R` as a `mul_semiring_action`, then it also acts on `residue_field R`. -/
+instance : mul_semiring_action G (local_ring.residue_field R) :=
+mul_semiring_action.comp_hom _ $ map_aut.comp (mul_semiring_action.to_ring_aut G R)
+
+@[simp] lemma residue_smul (g : G) (r : R) : residue R (g • r) = g • residue R r := rfl
+
+end mul_semiring_action
+
 end residue_field
 
 lemma ker_eq_maximal_ideal [field K] (φ : R →+* K) (hφ : function.surjective φ) :

src/ring_theory/valuation/ramification_group.lean

@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2022 Michail Karatarakis. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michail Karatarakis
+-/
+import ring_theory.ideal.local_ring
+import ring_theory.valuation.valuation_subring
+
+/-!
+# Ramification groups
+
+The decomposition subgroup and inertia subgroups.
+
+TODO: Define higher ramification groups in lower numbering
+-/
+
+namespace valuation_subring
+
+open_locale pointwise
+
+variables (K : Type*) {L : Type*} [field K] [field L] [algebra K L]
+
+/-- The decomposition subgroup defined as the stabilizer of the action
+on the type of all valuation subrings of the field. -/
+@[reducible] def decomposition_subgroup (A : valuation_subring L) :
+  subgroup (L ≃ₐ[K] L) :=
+mul_action.stabilizer (L ≃ₐ[K] L) A
+
+/-- The valuation subring `A` (considered as a subset of `L`)
+is stable under the action of the decomposition group. -/
+def sub_mul_action (A : valuation_subring L) :
+  sub_mul_action (A.decomposition_subgroup K) L :=
+{ carrier := A,
+  smul_mem' := λ g l h, set.mem_of_mem_of_subset (set.smul_mem_smul_set h) g.prop.le }
+
+/-- The multiplicative action of the decomposition subgroup on `A`. -/
+instance decomposition_subgroup_mul_semiring_action (A : valuation_subring L) :
+  mul_semiring_action (A.decomposition_subgroup K) A :=
+{ smul_add :=  λ g k l, subtype.ext $ smul_add g k l,
+  smul_zero := λ g, subtype.ext $ smul_zero g,
+  smul_one := λ g, subtype.ext $ smul_one g,
+  smul_mul := λ g k l, subtype.ext $ smul_mul' g k l,
+   ..(sub_mul_action.mul_action (A.sub_mul_action K)) }
+
+/-- 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`. -/
+def inertia_subgroup (A : valuation_subring L) :
+  subgroup (A.decomposition_subgroup K) :=
+monoid_hom.ker $
+  mul_semiring_action.to_ring_aut (A.decomposition_subgroup K) (local_ring.residue_field A)
+
+end valuation_subring