English
If P lies over p, the stabilizer of P acts on the extension (B∕P) over (A∕p) by A∕p-algebra automorphisms, given by σ induced from the action.
Русский
Если P лежит над p, стабилизатор P действует на расширение (B∕P) над (A∕p) через автоморфизмы A∕p-алгебр, индуцируемые действием σ.
LaTeX
$$$\text{stabilizerHom}: \mathrm{MulAction.stabilizer}\, G\, P \to \; (B/P) \cong_{A/p} (B/P)$$$
Lean4
/-- If `P` lies over `p`, then the stabilizer of `P` acts on the extension `(B ⧸ P) / (A ⧸ p)`. -/
def stabilizerHom : MulAction.stabilizer G P →* ((B ⧸ P) ≃ₐ[A ⧸ p] (B ⧸ P))
where
toFun g := algEquivOfEqMap p (MulSemiringAction.toAlgEquiv A B g) g.2.symm
map_one' := by
ext ⟨x⟩
exact congrArg (Ideal.Quotient.mk P) (one_smul G x)
map_mul' g
h := by
ext ⟨x⟩
exact congrArg (Ideal.Quotient.mk P) (mul_smul g h x)
