Residue separability under a group action #
If a group acts on an algebra while fixing its base, translation by a group element identifies the residue extension at an ideal with the residue extension at the translated ideal. Consequently separability of the residue extension is invariant under translation.
Thus separability at one prime suffices throughout its group orbit. The result assumes maximality only of the contraction, which makes the base of the residue extension a field; the upper ideal need not be maximal.
Main result #
Ideal.Quotient.isSeparable_smul: residue separability is preserved by translation.
theorem
Ideal.Quotient.isSeparable_smul
{A : Type u_1}
{B : Type u_2}
{G : Type u_3}
[CommRing A]
[CommRing B]
[Algebra A B]
[Group G]
[MulSemiringAction G B]
[SMulCommClass G A B]
(Q : Ideal B)
[(under A Q).IsMaximal]
(σ : G)
[Algebra.IsSeparable (A ⧸ under A Q) (B ⧸ Q)]
:
Residue separability is preserved when an ideal with maximal contraction is translated by a group action that fixes the base ring.