Group action on rings #
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
- submonoid.mul_semiring_action
- subgroup.mul_semiring_action
- subsemiring.mul_semiring_action
- subring.mul_semiring_action
- is_invariant_subring.to_mul_semiring_action
- punit.mul_semiring_action
- alg_equiv.apply_mul_semiring_action
- localization.mul_semiring_action
- conj_act.units_mul_semiring_action
- polynomial.mul_semiring_action
- is_invariant_subfield.to_mul_semiring_action
- polynomial.gal.apply_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' := _}
A stronger version of submonoid.distrib_mul_action
.
Equations
- H.mul_semiring_action = {to_distrib_mul_action := {to_mul_action := {to_has_smul := {smul := has_smul.smul H.has_smul}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, smul_one := _, smul_mul := _}
A stronger version of subgroup.distrib_mul_action
.
Equations
A stronger version of subsemiring.distrib_mul_action
.
Equations
A stronger version of subring.distrib_mul_action
.
Equations
Note that smul_inv'
refers to the group case, and smul_inv
has an additional inverse
on x
.
A typeclass for subrings invariant under a mul_semiring_action
.
Instances of this typeclass
Equations
- is_invariant_subring.to_mul_semiring_action M S = {to_distrib_mul_action := {to_mul_action := {to_has_smul := {smul := λ (m : M) (x : ↥S), ⟨m • ↑x, _⟩}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, smul_one := _, smul_mul := _}