mathlib documentation

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]
def add_opposite.add_action (α : Type u_1) (R : Type u_2) [add_monoid R] [add_action R α] :
Equations
@[protected, instance]
def mul_opposite.mul_action (α : Type u_1) (R : Type u_2) [monoid R] [mul_action R α] :
Equations
@[protected, instance]
def mul_opposite.is_scalar_tower (α : Type u_1) {M : Type u_2} {N : Type u_3} [has_scalar M N] [has_scalar M α] [has_scalar N α] [is_scalar_tower M N α] :
@[protected, instance]
def mul_opposite.smul_comm_class (α : Type u_1) {M : Type u_2} {N : Type u_3} [has_scalar M α] [has_scalar N α] [smul_comm_class M N α] :
@[protected, instance]
def add_opposite.vadd_comm_class (α : Type u_1) {M : Type u_2} {N : Type u_3} [has_vadd M α] [has_vadd N α] [vadd_comm_class M N α] :
@[protected, instance]
def mul_opposite.is_central_scalar (α : Type u_1) (R : Type u_2) [has_scalar R α] [has_scalar Rᵐᵒᵖ α] [is_central_scalar R α] :
theorem mul_opposite.op_smul_eq_op_smul_op (α : Type u_1) {R : Type u_2} [has_scalar R α] [has_scalar Rᵐᵒᵖ α] [is_central_scalar R α] (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]
def has_add.to_has_opposite_scalar (α : Type u_1) [has_add α] :
Equations
@[simp]
theorem op_smul_eq_mul (α : Type u_1) [has_mul α] {a a' : α} :
@[simp]
theorem op_vadd_eq_add (α : Type u_1) [has_add α] {a a' : α} :
@[protected, instance]

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

@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[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]
def is_scalar_tower.opposite_mid {M : Type u_1} {N : Type u_2} [monoid N] [has_scalar M N] [smul_comm_class M N N] :
@[protected, instance]
def smul_comm_class.opposite_mid {M : Type u_1} {N : Type u_2} [monoid N] [has_scalar M N] [is_scalar_tower M N N] :
@[protected, instance]

monoid.to_opposite_mul_action is faithful on cancellative monoids.

@[protected, instance]

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