Documentation

Mathlib.GroupTheory.GroupAction.Opposite

Scalar actions on and by Mᵐᵒᵖ #

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

Note that MulOpposite.smul is provided in an earlier file as it is needed to provide the AddMonoid.nsmul and AddCommGroup.zsmul fields.

Actions on the opposite type #

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

theorem AddOpposite.addAction.proof_1 (α : Type u_1) (R : Type u_2) [AddMonoid R] [AddAction R α] (x : αᵃᵒᵖ) :
0 +ᵥ x = x
theorem AddOpposite.addAction.proof_2 (α : Type u_1) (R : Type u_2) [AddMonoid R] [AddAction R α] (r₁ : R) (r₂ : R) (x : αᵃᵒᵖ) :
r₁ + r₂ +ᵥ x = r₁ +ᵥ (r₂ +ᵥ x)
instance AddOpposite.addAction (α : Type u_1) (R : Type u_2) [AddMonoid R] [AddAction R α] :
instance MulOpposite.mulAction (α : Type u_1) (R : Type u_2) [Monoid R] [MulAction R α] :
theorem AddOpposite.isScalarTower.proof_1 (α : Type u_1) {M : Type u_2} {N : Type u_3} [VAdd M N] [VAdd M α] [VAdd N α] [VAddAssocClass M N α] :
instance AddOpposite.isScalarTower (α : Type u_1) {M : Type u_2} {N : Type u_3} [VAdd M N] [VAdd M α] [VAdd N α] [VAddAssocClass M N α] :
instance MulOpposite.isScalarTower (α : Type u_1) {M : Type u_2} {N : Type u_3} [SMul M N] [SMul M α] [SMul N α] [IsScalarTower M N α] :
instance AddOpposite.vaddCommClass (α : Type u_1) {M : Type u_2} {N : Type u_3} [VAdd M α] [VAdd N α] [VAddCommClass M N α] :
theorem AddOpposite.vaddCommClass.proof_1 (α : Type u_1) {M : Type u_2} {N : Type u_3} [VAdd M α] [VAdd N α] [VAddCommClass M N α] :
instance MulOpposite.smulCommClass (α : Type u_1) {M : Type u_2} {N : Type u_3} [SMul M α] [SMul N α] [SMulCommClass M N α] :
instance AddOpposite.isCentralVAdd (α : Type u_1) (R : Type u_2) [VAdd R α] [VAdd Rᵃᵒᵖ α] [IsCentralVAdd R α] :
theorem MulOpposite.op_smul_eq_op_smul_op (α : Type u_1) {R : Type u_2} [SMul R α] [SMul Rᵐᵒᵖ α] [IsCentralScalar R α] (r : R) (a : α) :

Actions by the opposite type (right actions) #

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

instance Add.toHasOppositeVAdd (α : Type u_1) [Add α] :

Like Add.toVAdd, but adds on the right.

See also AddMonoid.to_OppositeAddAction.

instance Mul.toHasOppositeSMul (α : Type u_1) [Mul α] :

Like Mul.toSMul, but multiplies on the right.

See also Monoid.toOppositeMulAction and MonoidWithZero.toOppositeMulActionWithZero.

theorem op_vadd_eq_add (α : Type u_1) [Add α] {a : α} {a' : α} :
theorem op_smul_eq_mul (α : Type u_1) [Mul α] {a : α} {a' : α} :
MulOpposite.op a a' = a' * a
@[simp]
theorem AddOpposite.vadd_eq_add_unop (α : Type u_1) [Add α] {a : αᵃᵒᵖ} {a' : α} :
@[simp]
theorem MulOpposite.smul_eq_mul_unop (α : Type u_1) [Mul α] {a : αᵐᵒᵖ} {a' : α} :

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

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

Like AddMonoid.toAddAction, but adds on the right.

theorem AddMonoid.toOppositeAddAction.proof_1 (α : Type u_1) [AddMonoid α] (a : α) :
a + 0 = a

Like Monoid.toMulAction, but multiplies on the right.

instance VAddAssocClass.opposite_mid {M : Type u_2} {N : Type u_3} [Add N] [VAdd M N] [VAddCommClass M N N] :
instance IsScalarTower.opposite_mid {M : Type u_2} {N : Type u_3} [Mul N] [SMul M N] [SMulCommClass M N N] :
instance VAddCommClass.opposite_mid {M : Type u_2} {N : Type u_3} [Add N] [VAdd M N] [VAddAssocClass M N N] :
instance SMulCommClass.opposite_mid {M : Type u_2} {N : Type u_3} [Mul N] [SMul M N] [IsScalarTower M N N] :

Monoid.toOppositeMulAction is faithful on nontrivial cancellative monoids with zero.