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
- to_distrib_mul_action : distrib_mul_action M R
- 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
- ring_aut.apply_mul_semiring_action
- punit.mul_semiring_action
- submonoid.mul_semiring_action
- subgroup.mul_semiring_action
- subsemiring.mul_semiring_action
- subring.mul_semiring_action
- alg_equiv.apply_mul_semiring_action
- conj_act.units_mul_semiring_action
- ring_con.quotient.mul_semiring_action
- localization.mul_semiring_action
Instances of other typeclasses for mul_semiring_action
- mul_semiring_action.has_sizeof_inst
Each element of the monoid defines a semiring homomorphism.
Equations
- mul_semiring_action.to_ring_hom M R x = {to_fun := (mul_distrib_mul_action.to_monoid_hom R x).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
Each element of the group defines a semiring isomorphism.
Equations
- mul_semiring_action.to_ring_equiv G R x = {to_fun := (distrib_mul_action.to_add_equiv R x).to_fun, inv_fun := (distrib_mul_action.to_add_equiv R x).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}
Compose a mul_semiring_action
with a monoid_hom
, with action f r' • m
.
See note [reducible non-instances].
Equations
- mul_semiring_action.comp_hom R f = {to_distrib_mul_action := {to_mul_action := {to_has_smul := {smul := has_smul.comp.smul ⇑f}, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}, smul_one := _, smul_mul := _}
Note that smul_inv'
refers to the group case, and smul_inv
has an additional inverse
on x
.