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) [Monoid M] [Semiring R] extends DistribMulAction : Type (max u v)

Typeclass for multiplicative actions by monoids on semirings.

This combines DistribMulAction with MulDistribMulAction.

• smul : M → R → R
• 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

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

Multipliying 1 by a scalar gives 1

theorem MulSemiringAction.smul_mul {M : Type u} {R : Type v} [Monoid M] [Semiring R] [self : MulSemiringAction M R] (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) [Monoid M] (R : Type v) [Semiring R] [h : MulSemiringAction M R] : MulDistribMulAction M R

Equations

• MulSemiringAction.toMulDistribMulAction M R = MulDistribMulAction.mk ⋯ ⋯

@[simp]

theorem MulSemiringAction.toRingHom_apply (M : Type u_1) [Monoid M] (R : Type v) [Semiring R] [MulSemiringAction M R] (x : M) : ∀ (x_1 : R), (MulSemiringAction.toRingHom M R x) x_1 = x • x_1

def MulSemiringAction.toRingHom (M : Type u_1) [Monoid M] (R : Type v) [Semiring R] [MulSemiringAction M R] (x : M) : R →+* R

Each element of the monoid defines a semiring homomorphism.

Equations

• MulSemiringAction.toRingHom M R x = let __src := MulDistribMulAction.toMonoidHom R x; let __src_1 := DistribMulAction.toAddMonoidHom R x; { toMonoidHom := __src, map_zero' := ⋯, map_add' := ⋯ }

theorem toRingHom_injective (M : Type u_1) [Monoid M] (R : Type v) [Semiring R] [MulSemiringAction M R] [FaithfulSMul M R] : Function.Injective (MulSemiringAction.toRingHom M R)

instance RingHom.applyMulSemiringAction (R : Type v) [Semiring R] : MulSemiringAction (R →+* R) R

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

This generalizes Function.End.applyMulAction.

Equations

• RingHom.applyMulSemiringAction R = MulSemiringAction.mk ⋯ ⋯

@[simp]

theorem RingHom.smul_def (R : Type v) [Semiring R] (f : R →+* R) (a : R) : f • a = f a

instance RingHom.applyFaithfulSMul (R : Type v) [Semiring R] : FaithfulSMul (R →+* R) R

RingHom.applyMulSemiringAction is faithful.

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev MulSemiringAction.compHom {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] (R : Type v) [Semiring R] (f : N →* M) [MulSemiringAction M R] : MulSemiringAction N R

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

Equations

• MulSemiringAction.compHom R f = let __src := DistribMulAction.compHom R f; let __src_1 := MulDistribMulAction.compHom R f; MulSemiringAction.mk ⋯ ⋯

@[simp]

theorem smul_inv'' {M : Type u_1} [Monoid M] {F : Type v} [DivisionRing F] [MulSemiringAction M 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.