# mathlibdocumentation

group_theory.group_action.opposite

# Scalar actions on and by Mᵐᵒᵖ#

This file defines the actions on the opposite type has_scalar R Mᵐᵒᵖ, and actions by the opposite type, has_scalar Rᵐᵒᵖ M.

Note that mul_opposite.has_scalar is provided in an earlier file as it is needed to provide the add_monoid.nsmul and add_comm_group.gsmul fields.

### Actions on the opposite type #

Actions on the opposite type just act on the underlying type.

@[protected, instance]
Equations
@[protected, instance]
def mul_opposite.mul_action (α : Type u_1) (R : Type u_2) [monoid R] [ α] :
Equations
@[protected, instance]
def mul_opposite.distrib_mul_action (α : Type u_1) (R : Type u_2) [monoid R] [add_monoid α] [ α] :
Equations
@[protected, instance]
def mul_opposite.mul_distrib_mul_action (α : Type u_1) (R : Type u_2) [monoid R] [monoid α]  :
Equations
@[protected, instance]
def mul_opposite.is_scalar_tower (α : Type u_1) {M : Type u_2} {N : Type u_3} [ N] [ α] [ α] [ α] :
@[protected, instance]
def mul_opposite.smul_comm_class (α : Type u_1) {M : Type u_2} {N : Type u_3} [ α] [ α] [ α] :
@[protected, instance]
def add_opposite.vadd_comm_class (α : Type u_1) {M : Type u_2} {N : Type u_3} [ α] [ α] [ α] :
@[protected, instance]
def mul_opposite.is_central_scalar (α : Type u_1) (R : Type u_2) [ α] [ α] [ α] :
theorem mul_opposite.op_smul_eq_op_smul_op (α : Type u_1) {R : Type u_2} [ α] [ α] [ α] (r : R) (a : α) :
theorem mul_opposite.unop_smul_eq_unop_smul_unop (α : Type u_1) {R : Type u_2} [ α] [ α] [ α] (r : Rᵐᵒᵖ) (a : αᵐᵒᵖ) :

### Actions by the opposite type (right actions) #

In has_mul.to_has_scalar in another file, we define the left action a₁ • a₂ = a₁ * a₂. For the multiplicative opposite, we define mul_opposite.op a₁ • a₂ = a₂ * a₁, with the multiplication reversed.

@[protected, instance]
def has_mul.to_has_opposite_scalar (α : Type u_1) [has_mul α] :

Like has_mul.to_has_scalar, but multiplies on the right.

See also monoid.to_opposite_mul_action and monoid_with_zero.to_opposite_mul_action_with_zero.

Equations
@[protected, instance]
α
Equations
@[simp]
theorem op_smul_eq_mul (α : Type u_1) [has_mul α] {a a' : α} :
a' = a' * a
@[simp]
= a' + a
@[protected, instance]

The right regular action of a group on itself is transitive.

@[protected, instance]
@[protected, instance]
α
@[protected, instance]
def semigroup.opposite_smul_comm_class (α : Type u_1) [semigroup α] :
α
@[protected, instance]
def semigroup.opposite_smul_comm_class' (α : Type u_1) [semigroup α] :
α
@[protected, instance]
α
@[protected, instance]
def comm_semigroup.is_central_scalar (α : Type u_1)  :
@[protected, instance]
def monoid.to_opposite_mul_action (α : Type u_1) [monoid α] :

Like monoid.to_mul_action, but multiplies on the right.

Equations
@[protected, instance]
Equations
@[protected, instance]
def is_scalar_tower.opposite_mid {M : Type u_1} {N : Type u_2} [monoid N] [ N] [ N] :
N
@[protected, instance]
def smul_comm_class.opposite_mid {M : Type u_1} {N : Type u_2} [monoid N] [ N] [ N] :
N
@[protected, instance]

monoid.to_opposite_mul_action is faithful on cancellative monoids.

@[protected, instance]
@[protected, instance]

monoid.to_opposite_mul_action is faithful on nontrivial cancellative monoids with zero.