Group action on rings #
This file defines the typeclass of monoid acting on semirings MulSemiringAction M R
.
An example of a MulSemiringAction
is the action of the Galois group Gal(L/K)
on
the big field L
. Note that Algebra
does not in general 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
.
Note #
The corresponding typeclass of subrings invariant under such an action, IsInvariantSubring
, is
defined in Mathlib/Algebra/Ring/Action/Invariant.lean
.
Tags #
group action
Typeclass for multiplicative actions by monoids on semirings.
This combines DistribMulAction
with MulDistribMulAction
.
- smul : M → R → R
Multipliying
1
by a scalar gives1
Scalar multiplication distributes across multiplication
Instances
Equations
Each element of the monoid defines a semiring homomorphism.
Equations
- MulSemiringAction.toRingHom M R x = { toMonoidHom := MulDistribMulAction.toMonoidHom R x, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The tautological action by R →+* R
on R
.
This generalizes Function.End.applyMulAction
.
Equations
RingHom.applyMulSemiringAction
is faithful.
Compose a MulSemiringAction
with a MonoidHom
, with action f r' • m
.
See note [reducible non-instances].