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.

Notation

With open scoped RightActions, this provides:

• r •> m as an alias for r • m
• m <• r as an alias for MulOpposite.op r • m
• v +ᵥ> p as an alias for v +ᵥ p
• p <+ᵥ v as an alias for AddOpposite.op v +ᵥ p

Actions on the opposite type

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

instance MulOpposite.instMulAction {M : Type u_1} {α : Type u_3} [Monoid M] [MulAction M α] : MulAction M αᵐᵒᵖ

Equations

• MulOpposite.instMulAction = { toSMul := MulOpposite.instSMul, one_smul := ⋯, mul_smul := ⋯ }

instance AddOpposite.instAddAction {M : Type u_1} {α : Type u_3} [AddMonoid M] [AddAction M α] : AddAction M αᵃᵒᵖ

Equations

• AddOpposite.instAddAction = { toVAdd := AddOpposite.instVAdd, zero_vadd := ⋯, add_vadd := ⋯ }

instance MulOpposite.instIsScalarTower {M : Type u_1} {N : Type u_2} {α : Type u_3} [SMul M N] [SMul M α] [SMul N α] [IsScalarTower M N α] : IsScalarTower M N αᵐᵒᵖ

instance AddOpposite.instVAddAssocClass {M : Type u_1} {N : Type u_2} {α : Type u_3} [VAdd M N] [VAdd M α] [VAdd N α] [VAddAssocClass M N α] : VAddAssocClass M N αᵃᵒᵖ

instance MulOpposite.instSMulCommClass {M : Type u_1} {N : Type u_2} {α : Type u_3} [SMul M α] [SMul N α] [SMulCommClass M N α] : SMulCommClass M N αᵐᵒᵖ

instance AddOpposite.instVAddCommClass {M : Type u_1} {N : Type u_2} {α : Type u_3} [VAdd M α] [VAdd N α] [VAddCommClass M N α] : VAddCommClass M N αᵃᵒᵖ

instance MulOpposite.instIsCentralScalar {M : Type u_1} {α : Type u_3} [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] : IsCentralScalar M αᵐᵒᵖ

instance AddOpposite.instIsCentralVAdd {M : Type u_1} {α : Type u_3} [VAdd M α] [VAdd Mᵃᵒᵖ α] [IsCentralVAdd M α] : IsCentralVAdd M αᵃᵒᵖ

theorem MulOpposite.op_smul_eq_op_smul_op {M : Type u_1} {α : Type u_3} [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] (r : M) (a : α) : op (r • a) = op r • op a

theorem AddOpposite.op_vadd_eq_op_vadd_op {M : Type u_1} {α : Type u_3} [VAdd M α] [VAdd Mᵃᵒᵖ α] [IsCentralVAdd M α] (r : M) (a : α) : op (r +ᵥ a) = op r +ᵥ op a

theorem MulOpposite.unop_smul_eq_unop_smul_unop {M : Type u_1} {α : Type u_3} [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] (r : Mᵐᵒᵖ) (a : αᵐᵒᵖ) : unop (r • a) = unop r • unop a

theorem AddOpposite.unop_vadd_eq_unop_vadd_unop {M : Type u_1} {α : Type u_3} [VAdd M α] [VAdd Mᵃᵒᵖ α] [IsCentralVAdd M α] (r : Mᵃᵒᵖ) (a : αᵃᵒᵖ) : unop (r +ᵥ a) = unop r +ᵥ unop a

Right actions

In this section we establish SMul αᵐᵒᵖ β as the canonical spelling of right scalar multiplication of β by α, and provide convenient notations.

def RightActions.«term_•>_».«delab_app.HSMul.hSMul» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def RightActions.«term_•>_» : Lean.TrailingParserDescr

With open scoped RightActions, an alternative symbol for left actions, r • m.

In lemma names this is still called smul.

Equations

• RightActions.«term_•>_» = Lean.ParserDescr.trailingNode `RightActions.«term_•>_» 74 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " •> ") (Lean.ParserDescr.cat `term 74))

def RightActions.«term_<•_» : Lean.TrailingParserDescr

With open scoped RightActions, a shorthand for right actions, op r • m.

In lemma names this is still called op_smul.

Equations

• RightActions.«term_<•_» = Lean.ParserDescr.trailingNode `RightActions.«term_<•_» 73 73 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <• ") (Lean.ParserDescr.cat `term 74))

def RightActions.«term_<•_».«delab_app.HSMul.hSMul» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def RightActions.«term_+ᵥ>_» : Lean.TrailingParserDescr

With open scoped RightActions, an alternative symbol for left actions, r • m.

In lemma names this is still called vadd.

Equations

• RightActions.«term_+ᵥ>_» = Lean.ParserDescr.trailingNode `RightActions.«term_+ᵥ>_» 74 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " +ᵥ> ") (Lean.ParserDescr.cat `term 74))

def RightActions.«term_+ᵥ>_».«delab_app.HVAdd.hVAdd» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def RightActions.«term_<+ᵥ_» : Lean.TrailingParserDescr

With open scoped RightActions, a shorthand for right actions, op r +ᵥ m.

In lemma names this is still called op_vadd.

Equations

• RightActions.«term_<+ᵥ_» = Lean.ParserDescr.trailingNode `RightActions.«term_<+ᵥ_» 73 73 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <+ᵥ ") (Lean.ParserDescr.cat `term 74))

def RightActions.«term_<+ᵥ_».«delab_app.HVAdd.hVAdd» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

theorem op_smul_op_smul {α : Type u_3} {β : Type u_4} [Monoid α] [MulAction αᵐᵒᵖ β] (b : β) (a₁ a₂ : α) : MulOpposite.op a₂ • MulOpposite.op a₁ • b = MulOpposite.op (a₁ * a₂) • b

theorem op_vadd_op_vadd {α : Type u_3} {β : Type u_4} [AddMonoid α] [AddAction αᵃᵒᵖ β] (b : β) (a₁ a₂ : α) : AddOpposite.op a₂ +ᵥ AddOpposite.op a₁ +ᵥ b = AddOpposite.op (a₁ + a₂) +ᵥ b

theorem op_smul_mul {α : Type u_3} {β : Type u_4} [Monoid α] [MulAction αᵐᵒᵖ β] (b : β) (a₁ a₂ : α) : MulOpposite.op (a₁ * a₂) • b = MulOpposite.op a₂ • MulOpposite.op a₁ • b

theorem op_vadd_add {α : Type u_3} {β : Type u_4} [AddMonoid α] [AddAction αᵃᵒᵖ β] (b : β) (a₁ a₂ : α) : AddOpposite.op (a₁ + a₂) +ᵥ b = AddOpposite.op a₂ +ᵥ AddOpposite.op a₁ +ᵥ b

Actions by the opposite type (right actions)

instance Semigroup.opposite_smulCommClass {α : Type u_3} [Semigroup α] : SMulCommClass αᵐᵒᵖ α α

instance AddSemigroup.opposite_vaddCommClass {α : Type u_3} [AddSemigroup α] : VAddCommClass αᵃᵒᵖ α α

instance Semigroup.opposite_smulCommClass' {α : Type u_3} [Semigroup α] : SMulCommClass α αᵐᵒᵖ α

instance AddSemigroup.opposite_vaddCommClass' {α : Type u_3} [AddSemigroup α] : VAddCommClass α αᵃᵒᵖ α

instance CommSemigroup.isCentralScalar {α : Type u_3} [CommSemigroup α] : IsCentralScalar α α

instance AddCommSemigroup.isCentralVAdd {α : Type u_3} [AddCommSemigroup α] : IsCentralVAdd α α

instance Monoid.toOppositeMulAction {α : Type u_3} [Monoid α] : MulAction αᵐᵒᵖ α

Like Monoid.toMulAction, but multiplies on the right.

Equations

• Monoid.toOppositeMulAction = { smul := fun (x1 : αᵐᵒᵖ) (x2 : α) => x1 • x2, one_smul := ⋯, mul_smul := ⋯ }

instance AddMonoid.toOppositeAddAction {α : Type u_3} [AddMonoid α] : AddAction αᵃᵒᵖ α

Like AddMonoid.toAddAction, but adds on the right.

Equations

• AddMonoid.toOppositeAddAction = { vadd := fun (x1 : αᵃᵒᵖ) (x2 : α) => x1 +ᵥ x2, zero_vadd := ⋯, add_vadd := ⋯ }

instance IsScalarTower.opposite_mid {M : Type u_5} {N : Type u_6} [Mul N] [SMul M N] [SMulCommClass M N N] : IsScalarTower M Nᵐᵒᵖ N

instance VAddAssocClass.opposite_mid {M : Type u_5} {N : Type u_6} [Add N] [VAdd M N] [VAddCommClass M N N] : VAddAssocClass M Nᵃᵒᵖ N

instance SMulCommClass.opposite_mid {M : Type u_5} {N : Type u_6} [Mul N] [SMul M N] [IsScalarTower M N N] : SMulCommClass M Nᵐᵒᵖ N

instance VAddCommClass.opposite_mid {M : Type u_5} {N : Type u_6} [Add N] [VAdd M N] [VAddAssocClass M N N] : VAddCommClass M Nᵃᵒᵖ N