The maximal-ideal filtration is invariant under ring automorphisms #
A group acting on a local ring by ring automorphisms acts by surjective local homomorphisms, so it fixes the maximal ideal and every one of its powers. This file records that invariance, both as an equality of ideals for the pointwise action and in the membership form its consumers use.
Main results #
TauCeti.IsLocalRing.smul_maximalIdeal_pow: the pointwise action fixes𝔪 ^ n.TauCeti.IsLocalRing.smul_mem_maximalIdeal_pow: the membership form of the same statement.
@[simp]
theorem
TauCeti.IsLocalRing.smul_maximalIdeal_pow
{G : Type u_1}
[Group G]
{S : Type u_2}
[CommRing S]
[IsLocalRing S]
[MulSemiringAction G S]
(σ : G)
(n : ℕ)
:
A group acting by ring automorphisms on a local ring fixes every power of the maximal ideal:
each automorphism is a surjective ring homomorphism, hence maps 𝔪 onto 𝔪.
theorem
TauCeti.IsLocalRing.smul_mem_maximalIdeal_pow
{G : Type u_1}
[Group G]
{S : Type u_2}
[CommRing S]
[IsLocalRing S]
[MulSemiringAction G S]
(σ : G)
{n : ℕ}
{x : S}
(hx : x ∈ IsLocalRing.maximalIdeal S ^ n)
:
A group acting by ring automorphisms on a local ring preserves the powers of the maximal ideal.