mathlib documentation

algebra.group_ring_action

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

@[class]
structure mul_semiring_action (M : Type u) (R : Type v) [monoid M] [semiring R] :
Type (max u v)

Typeclass for multiplicative actions by monoids on semirings.

This combines distrib_mul_action with mul_distrib_mul_action.

Instances
@[simp]
theorem mul_semiring_action.to_ring_hom_apply (M : Type u) [monoid M] (R : Type v) [semiring R] [mul_semiring_action M R] (x : M) (ᾰ : R) :
def mul_semiring_action.to_ring_hom (M : Type u) [monoid M] (R : Type v) [semiring R] [mul_semiring_action M R] (x : M) :
R →+* R

Each element of the monoid defines a semiring homomorphism.

Equations
@[simp]
theorem mul_semiring_action.to_ring_equiv_apply (G : Type u) [group G] (R : Type v) [semiring R] [mul_semiring_action G R] (x : G) (ᾰ : R) :
def mul_semiring_action.to_ring_equiv (G : Type u) [group G] (R : Type v) [semiring R] [mul_semiring_action G R] (x : G) :
R ≃+* R

Each element of the group defines a semiring isomorphism.

Equations
@[simp]
@[instance]
def subgroup.mul_semiring_action {G : Type u} [group G] {R : Type v} [semiring R] [mul_semiring_action G R] (H : subgroup G) :

A stronger version of subgroup.distrib_mul_action.

Equations
@[instance]
def subsemiring.mul_semiring_action {R : Type v} [semiring R] {R' : Type u_1} [semiring R'] [mul_semiring_action R' R] (H : subsemiring R') :

A stronger version of subsemiring.distrib_mul_action.

Equations
@[instance]
def subring.mul_semiring_action {R : Type v} [semiring R] {R' : Type u_1} [ring R'] [mul_semiring_action R' R] (H : subring R') :

A stronger version of subring.distrib_mul_action.

Equations
@[instance]
def subsemiring.pointwise_mul_action (M : Type u) [monoid M] (R : Type v) [semiring R] [mul_semiring_action M R] :

The action on a subsemiring corresponding to applying the action to every element.

This is available as an instance in the pointwise locale.

Equations
@[simp]
theorem subsemiring.coe_pointwise_smul (M : Type u) [monoid M] (R : Type v) [semiring R] [mul_semiring_action M R] (m : M) (S : subsemiring R) :
(m S) = m S
@[simp]
theorem subsemiring.pointwise_smul_to_add_submonoid (M : Type u) [monoid M] (R : Type v) [semiring R] [mul_semiring_action M R] (m : M) (S : subsemiring R) :
theorem subsemiring.smul_mem_pointwise_smul (M : Type u) [monoid M] (R : Type v) [semiring R] [mul_semiring_action M R] (m : M) (r : R) (S : subsemiring R) :
r Sm r m S
@[instance]
def subring.pointwise_mul_action (M : Type u) [monoid M] {R' : Type u_1} [ring R'] [mul_semiring_action M R'] :

The action on a subring corresponding to applying the action to every element.

This is available as an instance in the pointwise locale.

Equations
@[simp]
theorem subring.coe_pointwise_smul (M : Type u) [monoid M] {R' : Type u_1} [ring R'] [mul_semiring_action M R'] (m : M) (S : subring R') :
(m S) = m S
@[simp]
theorem subring.pointwise_smul_to_add_subgroup (M : Type u) [monoid M] {R' : Type u_1} [ring R'] [mul_semiring_action M R'] (m : M) (S : subring R') :
@[simp]
theorem subring.pointwise_smul_to_subsemiring (M : Type u) [monoid M] {R' : Type u_1} [ring R'] [mul_semiring_action M R'] (m : M) (S : subring R') :
theorem subring.smul_mem_pointwise_smul (M : Type u) [monoid M] {R' : Type u_1} [ring R'] [mul_semiring_action M R'] (m : M) (r : R') (S : subring R') :
r Sm r m S
@[simp]
theorem smul_inv'' {M : Type u} [monoid M] {F : Type v} [division_ring F] [mul_semiring_action 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.

@[class]
structure is_invariant_subring (M : Type u) [monoid M] {R : Type v} [ring R] [mul_semiring_action M R] (S : subring R) :
Prop
  • smul_mem : ∀ (m : M) {x : R}, x Sm x S

A typeclass for subrings invariant under a mul_semiring_action.

Instances
@[instance]
Equations