mathlib3 documentation

group_theory.group_action.opposite

Scalar actions on and by Mᵐᵒᵖ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Note that mul_opposite.has_smul 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_smul M N] [has_smul M α] [has_smul N α] [is_scalar_tower M N α] :
@[protected, instance]
def add_opposite.vadd_assoc_class (α : Type u_1) {M : Type u_2} {N : Type u_3} [has_vadd M N] [has_vadd M α] [has_vadd N α] [vadd_assoc_class M N α] :
@[protected, instance]
def mul_opposite.smul_comm_class (α : Type u_1) {M : Type u_2} {N : Type u_3} [has_smul M α] [has_smul 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]
@[protected, instance]

Actions by the opposite type (right actions) #

In has_mul.to_has_smul 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]

Like has_mul.to_has_smul, 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]

Like has_add.to_has_vadd, but adds on the right.

See also add_monoid.to_opposite_add_action.

Equations
theorem op_smul_eq_mul (α : Type u_1) [has_mul α] {a a' : α} :
theorem op_vadd_eq_add (α : Type u_1) [has_add α] {a a' : α} :
@[simp]
theorem mul_opposite.smul_eq_mul_unop (α : Type u_1) [has_mul α] {a : αᵐᵒᵖ} {a' : α} :
@[simp]
theorem add_opposite.vadd_eq_add_unop (α : Type u_1) [has_add α] {a : αᵃᵒᵖ} {a' : α} :
@[protected, instance]

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

@[protected, instance]

The right regular action of an additive group on itself is transitive.

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

Like monoid.to_mul_action, but multiplies on the right.

Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[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.