English
The inertia subgroup of a valuation subring A is defined as the kernel of the natural group homomorphism from the decomposition subgroup to the automorphism group of the residue field κ_A of A. Equivalently, it consists of those elements of the decomposition subgroup that act trivially on the residue field.
Русский
Инерционная подгруппа A — это ядро естественной гомоморфной группы от подгруппы разложения к группе автоморфизмов остаточного поля κ_A; другими словами, это те элементы подгруппы разложения, которые действуют тривиально на остаточное поле.
LaTeX
$$$\operatorname{InertiaSubgroup}(A) = \ker\bigl( \varphi: A.\mathrm{decompositionSubgroup}(K) \to \mathrm{Aut}(\kappa_A) \bigr),\; \kappa_A = \mathrm{ResidueField}(A).$$$
Lean4
/-- 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`. -/
noncomputable def inertiaSubgroup (A : ValuationSubring L) : Subgroup (A.decompositionSubgroup K) :=
MonoidHom.ker <| MulSemiringAction.toRingAut (A.decompositionSubgroup K) (IsLocalRing.ResidueField A)
