# mathlib3documentation

algebra.group_ring_action.basic

# Group action on rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the typeclass of monoid acting on semirings mul_semiring_action M R, and the corresponding typeclass of invariant subrings.

Note that algebra does not satisfy the axioms of mul_semiring_action.

## Implementation notes #

There is no separate typeclass for group acting on rings, group acting on fields, etc. They are all grouped under mul_semiring_action.

## Tags #

group action, invariant subring

@[class]
structure mul_semiring_action (M : Type u) (R : Type v) [monoid M] [semiring R] :
Type (max u v)
• to_distrib_mul_action :
• smul_one : (g : M), g 1 = 1
• smul_mul : (g : M) (x y : R), g (x * y) = g x * g y

Typeclass for multiplicative actions by monoids on semirings.

This combines distrib_mul_action with mul_distrib_mul_action.

Instances of this typeclass
Instances of other typeclasses for mul_semiring_action
• mul_semiring_action.has_sizeof_inst
@[protected, instance]
def mul_semiring_action.to_mul_distrib_mul_action (M : Type u_1) [monoid M] (R : Type v) [semiring R] [h : R] :
Equations
@[simp]
theorem mul_semiring_action.to_ring_hom_apply (M : Type u_1) [monoid M] (R : Type v) [semiring R] [ R] (x : M) (ᾰ : R) :
=
def mul_semiring_action.to_ring_hom (M : Type u_1) [monoid M] (R : Type v) [semiring R] [ R] (x : M) :
R →+* R

Each element of the monoid defines a semiring homomorphism.

Equations
theorem to_ring_hom_injective (M : Type u_1) [monoid M] (R : Type v) [semiring R] [ R] [ R] :
@[simp]
theorem mul_semiring_action.to_ring_equiv_apply (G : Type u_3) [group G] (R : Type v) [semiring R] [ R] (x : G) (ᾰ : R) :
=
def mul_semiring_action.to_ring_equiv (G : Type u_3) [group G] (R : Type v) [semiring R] [ R] (x : G) :
R ≃+* R

Each element of the group defines a semiring isomorphism.

Equations
@[simp]
theorem mul_semiring_action.to_ring_equiv_symm_apply (G : Type u_3) [group G] (R : Type v) [semiring R] [ R] (x : G) (ᾰ : R) :
.symm) =
@[reducible]
def mul_semiring_action.comp_hom {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (R : Type v) [semiring R] (f : N →* M) [ R] :

Compose a mul_semiring_action with a monoid_hom, with action f r' • m. See note [reducible non-instances].

Equations
@[simp]
theorem smul_inv'' {M : Type u_1} [monoid M] {F : Type v} [ F] (x : M) (m : F) :
x m⁻¹ = (x m)⁻¹

Note that smul_inv' refers to the group case, and smul_inv has an additional inverse on x.