Maximal ideals under the pointwise action #
A group acting on a ring by ring automorphisms permutes its maximal ideals: the translate
g • I is the preimage of I under the ring automorphism g⁻¹. This is the maximal-ideal
companion of Mathlib's Ideal.IsPrime.smul.
Main results #
Ideal.IsMaximal.smul: the translate of a maximal ideal is maximal.
instance
Ideal.IsMaximal.smul
{M : Type u_1}
{R : Type u_2}
[Group M]
[Semiring R]
[MulSemiringAction M R]
{I : Ideal R}
[I.IsMaximal]
(g : M)
:
Translates of maximal ideals are maximal. The translate g • I is the preimage of I
under a ring automorphism, so it is maximal whenever I is.