SchemeTheory.stabilizerLocalizationInertiaMulEquiv
The actual local inertia and original ideal inertia are the same stabilizer elements, with only their canonical subgroup presentations changed.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
namespace SchemeTheory
universe u vLean source · full declaration
def stabilizerLocalizationInertiaMulEquiv
(B : Type u) [CommRing B] (G : Type v) [Group G] [MulSemiringAction G B]
(Q : Ideal B) [Q.IsPrime] :
(IsLocalRing.maximalIdeal (Localization.AtPrime Q)).inertia (MulAction.stabilizer G Q) ≃*
Q.inertia G where
toFun σ := ⟨σ.val.val,
(stabilizerLocalization_mem_inertia_iff B G Q σ.val).mp σ.property⟩
invFun σ :=
let d : MulAction.stabilizer G Q := ⟨σ.val, Q.inertia_le_stabilizer σ.property⟩
⟨d, (stabilizerLocalization_mem_inertia_iff B G Q d).mpr σ.property⟩
left_inv _ := Subtype.ext (Subtype.ext rfl)
right_inv _ := Subtype.ext rfl
map_mul' _ _ := Subtype.ext rfl