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

ink

class MulSemiringAction (M : Type u) (R : Type v) [inst : Monoid M] [inst : Semiring R] extends DistribMulAction : Type (maxuv)

• Multipliying 1 by a scalar gives 1

  smul_one : ∀ (g : M), g • 1 = 1

• Scalara multiplication distributes across multiplication

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

Typeclass for multiplicative actions by monoids on semirings.

This combines DistribMulAction with MulDistribMulAction.

ink

instance MulSemiringAction.toMulDistribMulAction (M : Type u_1) [inst : Monoid M] (R : Type v) [inst : Semiring R] [h : MulSemiringAction M R] : MulDistribMulAction M R

Equations

• MulSemiringAction.toMulDistribMulAction M R = MulDistribMulAction.mk (_ : ∀ (g : M) (x y : R), g • (x * y) = g • x * g • y) (_ : ∀ (g : M), g • 1 = 1)

ink

@[simp]

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

ink

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

Each element of the monoid defines a semiring homomorphism.

Equations

• One or more equations did not get rendered due to their size.

ink

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

ink

@[simp]

theorem MulSemiringAction.toRingEquiv_apply (G : Type u_1) [inst : Group G] (R : Type v) [inst : Semiring R] [inst : MulSemiringAction G R] (x : G) : ∀ (a : R), ↑(MulSemiringAction.toRingEquiv G R x) a = x • a

ink

@[simp]

theorem MulSemiringAction.toRingEquiv_symm_apply (G : Type u_1) [inst : Group G] (R : Type v) [inst : Semiring R] [inst : MulSemiringAction G R] (x : G) : ∀ (a : R), ↑(RingEquiv.symm (MulSemiringAction.toRingEquiv G R x)) a = x⁻¹ • a

ink

def MulSemiringAction.toRingEquiv (G : Type u_1) [inst : Group G] (R : Type v) [inst : Semiring R] [inst : MulSemiringAction G R] (x : G) : R ≃+* R

Each element of the group defines a semiring isomorphism.

Equations

• One or more equations did not get rendered due to their size.

ink

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

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

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

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