# Group action on rings #

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

Note that Algebra does not satisfy the axioms of MulSemiringAction.

## Implementation notes #

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

## Tags #

group action, invariant subring

class MulSemiringAction (M : Type u) (R : Type v) [] [] extends :
Type (max u v)

Typeclass for multiplicative actions by monoids on semirings.

This combines DistribMulAction with MulDistribMulAction.

• smul : MRR
• one_smul : ∀ (b : R), 1 b = b
• mul_smul : ∀ (x y : M) (b : R), (x * y) b = x y b
• smul_zero : ∀ (a : M), a 0 = 0
• smul_add : ∀ (a : M) (x y : R), a (x + y) = a x + a y
• smul_one : ∀ (g : M), g 1 = 1

Multipliying 1 by a scalar gives 1

• smul_mul : ∀ (g : M) (x y : R), g (x * y) = g x * g y

Scalar multiplication distributes across multiplication

Instances
theorem MulSemiringAction.smul_one {M : Type u} {R : Type v} [] [] [self : ] (g : M) :
g 1 = 1

Multipliying 1 by a scalar gives 1

theorem MulSemiringAction.smul_mul {M : Type u} {R : Type v} [] [] [self : ] (g : M) (x : R) (y : R) :
g (x * y) = g x * g y

Scalar multiplication distributes across multiplication

@[instance 100]
instance MulSemiringAction.toMulDistribMulAction (M : Type u_1) [] (R : Type v) [] [h : ] :
Equations
@[simp]
theorem MulSemiringAction.toRingHom_apply (M : Type u_1) [] (R : Type v) [] [] (x : M) :
∀ (x_1 : R), () x_1 = x x_1
def MulSemiringAction.toRingHom (M : Type u_1) [] (R : Type v) [] [] (x : M) :
R →+* R

Each element of the monoid defines a semiring homomorphism.

Equations
• = let __src := ; let __src_1 := ; { toMonoidHom := __src, map_zero' := , map_add' := }
Instances For
theorem toRingHom_injective (M : Type u_1) [] (R : Type v) [] [] [] :

The tautological action by R →+* R on R.

This generalizes Function.End.applyMulAction.

Equations
@[simp]
theorem RingHom.smul_def (R : Type v) [] (f : R →+* R) (a : R) :
f a = f a
instance RingHom.applyFaithfulSMul (R : Type v) [] :

RingHom.applyMulSemiringAction is faithful.

Equations
• =
@[reducible, inline]
abbrev MulSemiringAction.compHom {M : Type u_1} {N : Type u_2} [] [] (R : Type v) [] (f : N →* M) [] :

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

Equations
• = let __src := ; let __src_1 := ;
Instances For