English
If P lies over p, stabilizer of P acts on the quotient extension by mapping each g to the induced A/p-algebra automorphism of B/P.
Русский
Если P лежит над p, стабилизатор P действует на расширение по частотам через автоморфизм A/p-алгебр B/P, индуцируемый каждым g.
LaTeX
$$$\text{stabilizerHom}: MulAction.stabilizer G P \to* (B/P) \cong_{A/p} (B/P)$$$
Lean4
/-- The action on an ideal corresponding to applying the action to every element.
This is available as an instance in the `Pointwise` locale. -/
protected def pointwiseMulSemiringAction {R : Type*} [CommRing R] [MulSemiringAction M R] :
MulSemiringAction M (Ideal R)
where
smul_one a := by simp only [Ideal.one_eq_top]; exact Ideal.map_top _
smul_mul a I J := Ideal.map_mul (MulSemiringAction.toRingHom _ _ a) I J
