The kernel of the automorphism representation of a group acting on a ring

A group G acting on a semiring S by ring automorphisms is represented by MulSemiringAction.toRingAut G S. This file reads off the kernel of that representation: an element lies in it exactly when it fixes every element of S, so the kernel is trivial precisely because the action is faithful. When S is moreover generated over a base ring R by a single element ξ and the action is by R-algebra maps, faithfulness can be tested at ξ alone.

Main results

• TauCeti.MulSemiringAction.mem_ker_toRingAut_iff: membership in the kernel is acting trivially on every element.
• TauCeti.MulSemiringAction.ker_toRingAut_eq_bot: a faithful action is a faithful representation.
• TauCeti.eq_one_of_smul_eq_of_adjoin_singleton_eq_top: for a faithful action by R-algebra maps, only the identity fixes a single generator of S over R.
• TauCeti.smul_left_injective_of_adjoin_singleton_eq_top: under the same hypotheses, distinct group elements move the generator to distinct elements.

theorem TauCeti.MulSemiringAction.mem_ker_toRingAut_iff {G : Type u_1} [Group G] {S : Type u_2} [Semiring S] [MulSemiringAction G S] {σ : G} : σ ∈ (MulSemiringAction.toRingAut G S).ker ↔ ∀ (x : S), σ • x = x

Membership in the kernel of the automorphism representation means acting trivially on every element.

theorem TauCeti.MulSemiringAction.ker_toRingAut_eq_bot {G : Type u_1} [Group G] {S : Type u_2} [Semiring S] [MulSemiringAction G S] [FaithfulSMul G S] : (MulSemiringAction.toRingAut G S).ker = ⊥

A faithful action by ring automorphisms has trivial kernel.

theorem TauCeti.eq_one_of_smul_eq_of_adjoin_singleton_eq_top {G : Type u_1} [Monoid G] {S : Type u_2} [Semiring S] [MulSemiringAction G S] {R : Type u_3} [CommSemiring R] [Algebra R S] [SMulCommClass G R S] [FaithfulSMul G S] {ξ : S} (hξ : R[ξ] = ⊤) {σ : G} (h : σ • ξ = ξ) : σ = 1

For a faithful action by R-algebra maps on S = R[ξ], an element fixing the generator ξ is the identity.

theorem TauCeti.smul_left_injective_of_adjoin_singleton_eq_top {G : Type u_1} [Group G] {S : Type u_2} [Semiring S] [MulSemiringAction G S] {R : Type u_3} [CommSemiring R] [Algebra R S] [SMulCommClass G R S] [FaithfulSMul G S] {ξ : S} (hξ : R[ξ] = ⊤) : Function.Injective fun (σ : G) => σ • ξ

For a faithful action by R-algebra maps on S = R[ξ], the orbit map at ξ is injective.