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.instSMulMulOpposite 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.

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

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) [inst : Add α] :

Like Add.toVAdd, but adds on the right.

See also AddMonoid.to_OppositeAddAction.

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

Like Mul.toSMul, but multiplies on the right.

See also Monoid.toOppositeMulAction and MonoidWithZero.toOppositeMulActionWithZero.

Equations
theorem op_vadd_eq_add (α : Type u_1) [inst : Add α] {a : α} {a' : α} :
{ unop := a } +ᵥ a' = a' + a
theorem op_smul_eq_mul (α : Type u_1) [inst : Mul α] {a : α} {a' : α} :
{ unop := a } a' = a' * a
@[simp]
theorem AddOpposite.vadd_eq_add_unop (α : Type u_1) [inst : Add α] {a : αᵃᵒᵖ} {a' : α} :
a +ᵥ a' = a' + a.unop
@[simp]
theorem MulOpposite.smul_eq_mul_unop (α : Type u_1) [inst : Mul α] {a : αᵐᵒᵖ} {a' : α} :
a a' = a' * a.unop
Equations
def AddMonoid.toOppositeAddAction.proof_1 (α : Type u_1) [inst : AddMonoid α] :
∀ (x x_1 : αᵃᵒᵖ) (x_2 : α), x_2 + (x_1.unop + x.unop) = x_2 + x_1.unop + x.unop
Equations
  • (_ : x + (x.unop + x.unop) = x + x.unop + x.unop) = (_ : x + (x.unop + x.unop) = x + x.unop + x.unop)
instance AddMonoid.toOppositeAddAction (α : Type u_1) [inst : AddMonoid α] :

Like AddMonoid.toAddAction, but adds on the right.

Equations
instance Monoid.toOppositeMulAction (α : Type u_1) [inst : Monoid α] :

Like Monoid.toMulAction, but multiplies on the right.

Equations
def VAddAssocClass.opposite_mid.proof_1 {M : Type u_1} {N : Type u_2} [inst : Add N] [inst : VAdd M N] [inst : VAddCommClass M N N] :
Equations
def VAddCommClass.opposite_mid.proof_1 {M : Type u_1} {N : Type u_2} [inst : Add N] [inst : VAdd M N] [inst : VAddAssocClass M N N] :
Equations