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.

source
@[protected, instance]
def add_opposite.add_action (α : Type u_1) (R : Type u_2) [add_monoid R] [add_action R α] :
add_action R αᵃᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.mul_action (α : Type u_1) (R : Type u_2) [monoid R] [mul_action R α] :
mul_action R αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.distrib_mul_action (α : Type u_1) (R : Type u_2) [monoid R] [add_monoid α] [distrib_mul_action R α] :
distrib_mul_action R αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.mul_distrib_mul_action (α : Type u_1) (R : Type u_2) [monoid R] [monoid α] [mul_distrib_mul_action R α] :
mul_distrib_mul_action R αᵐᵒᵖ
Equations
source
@[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 α] :
is_scalar_tower M N αᵐᵒᵖ
source
@[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 α] :
smul_comm_class M N αᵐᵒᵖ
source
@[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 α] :
vadd_comm_class M N αᵃᵒᵖ
source
@[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 α] :
is_central_scalar R αᵐᵒᵖ
source
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 : α) :
mul_opposite.op (r • a) = mul_opposite.op r • mul_opposite.op a
source
theorem mul_opposite.unop_smul_eq_unop_smul_unop (α : Type u_1) {R : Type u_2} [has_scalar R α] [has_scalar Rᵐᵒᵖ α] [is_central_scalar R α] (r : Rᵐᵒᵖ) (a : αᵐᵒᵖ) :
mul_opposite.unop (r • a) = mul_opposite.unop r • mul_opposite.unop 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.

source
@[protected, instance]
def has_mul.to_has_opposite_scalar (α : Type u_1) [has_mul α] :
has_scalar αᵐᵒᵖ α

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
source
@[protected, instance]
def has_add.to_has_opposite_scalar (α : Type u_1) [has_add α] :
has_vadd αᵃᵒᵖ α
Equations
source
theorem op_smul_eq_mul (α : Type u_1) [has_mul α] {a a' : α} :
mul_opposite.op a • a' = a' * a
source
theorem op_vadd_eq_add (α : Type u_1) [has_add α] {a a' : α} :
add_opposite.op a +ᵥ a' = a' + a
source
@[simp]
theorem mul_opposite.smul_eq_mul_unop (α : Type u_1) [has_mul α] {a : αᵐᵒᵖ} {a' : α} :
a • a' = a' * mul_opposite.unop a
source
@[simp]
theorem add_opposite.vadd_eq_add_unop (α : Type u_1) [has_add α] {a : αᵃᵒᵖ} {a' : α} :
a +ᵥ a' = a' + add_opposite.unop a
source
@[protected, instance]
def mul_action.opposite_regular.is_pretransitive {G : Type u_1} [group G] :
mul_action.is_pretransitive Gᵐᵒᵖ G

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

source
@[protected, instance]
def add_action.opposite_regular.is_pretransitive {G : Type u_1} [add_group G] :
add_action.is_pretransitive Gᵃᵒᵖ G

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

source
@[protected, instance]
def add_semigroup.opposite_vadd_comm_class (α : Type u_1) [add_semigroup α] :
vadd_comm_class αᵃᵒᵖ α α
source
@[protected, instance]
def semigroup.opposite_smul_comm_class (α : Type u_1) [semigroup α] :
smul_comm_class αᵐᵒᵖ α α
source
@[protected, instance]
def semigroup.opposite_smul_comm_class' (α : Type u_1) [semigroup α] :
smul_comm_class α αᵐᵒᵖ α
source
@[protected, instance]
def add_semigroup.opposite_vadd_comm_class' (α : Type u_1) [add_semigroup α] :
vadd_comm_class α αᵃᵒᵖ α
source
@[protected, instance]
def comm_semigroup.is_central_scalar (α : Type u_1) [comm_semigroup α] :
is_central_scalar α α
source
@[protected, instance]
def monoid.to_opposite_mul_action (α : Type u_1) [monoid α] :
mul_action αᵐᵒᵖ α

Like monoid.to_mul_action, but multiplies on the right.

Equations
source
@[protected, instance]
def add_monoid.to_opposite_add_action (α : Type u_1) [add_monoid α] :
add_action αᵃᵒᵖ α
Equations
source
@[protected, instance]
def is_scalar_tower.opposite_mid {M : Type u_1} {N : Type u_2} [has_mul N] [has_scalar M N] [smul_comm_class M N N] :
is_scalar_tower M Nᵐᵒᵖ N
source
@[protected, instance]
def smul_comm_class.opposite_mid {M : Type u_1} {N : Type u_2} [has_mul N] [has_scalar M N] [is_scalar_tower M N N] :
smul_comm_class M Nᵐᵒᵖ N
source
@[protected, instance]
def left_cancel_monoid.to_has_faithful_opposite_scalar (α : Type u_1) [left_cancel_monoid α] :
has_faithful_scalar αᵐᵒᵖ α

monoid.to_opposite_mul_action is faithful on cancellative monoids.

source
@[protected, instance]
def add_left_cancel_monoid.to_has_faithful_opposite_scalar (α : Type u_1) [add_left_cancel_monoid α] :
has_faithful_vadd αᵃᵒᵖ α
source
@[protected, instance]
def cancel_monoid_with_zero.to_has_faithful_opposite_scalar (α : Type u_1) [cancel_monoid_with_zero α] [nontrivial α] :
has_faithful_scalar αᵐᵒᵖ α

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