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.

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 α] : AddAction R αᵃᵒᵖ

Equations

• AddOpposite.addAction α R = AddAction.mk ⋯ ⋯

instance MulOpposite.mulAction (α : Type u_1) (R : Type u_2) [Monoid R] [MulAction R α] : MulAction R αᵐᵒᵖ

Equations

• MulOpposite.mulAction α R = MulAction.mk ⋯ ⋯

instance MulOpposite.distribMulAction (α : Type u_1) (R : Type u_2) [Monoid R] [AddMonoid α] [DistribMulAction R α] : DistribMulAction R αᵐᵒᵖ

Equations

• MulOpposite.distribMulAction α R = DistribMulAction.mk ⋯ ⋯

instance MulOpposite.mulDistribMulAction (α : Type u_1) (R : Type u_2) [Monoid R] [Monoid α] [MulDistribMulAction R α] : MulDistribMulAction R αᵐᵒᵖ

Equations

• MulOpposite.mulDistribMulAction α R = MulDistribMulAction.mk ⋯ ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance AddOpposite.isCentralVAdd (α : Type u_1) (R : Type u_2) [VAdd R α] [VAdd Rᵃᵒᵖ α] [IsCentralVAdd R α] : IsCentralVAdd R αᵃᵒᵖ

Equations

• ⋯ = ⋯

instance MulOpposite.isCentralScalar (α : Type u_1) (R : Type u_2) [SMul R α] [SMul Rᵐᵒᵖ α] [IsCentralScalar R α] : IsCentralScalar R αᵐᵒᵖ

Equations

• ⋯ = ⋯

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

theorem MulOpposite.unop_smul_eq_unop_smul_unop (α : Type u_1) {R : Type u_2} [SMul R α] [SMul Rᵐᵒᵖ α] [IsCentralScalar R α] (r : Rᵐᵒᵖ) (a : αᵐᵒᵖ) : MulOpposite.unop (r • a) = MulOpposite.unop r • MulOpposite.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_•>_» : Lean.TrailingParserDescr

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

In lemma names this is still called smul.

Equations

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

def RightActions.«term_•>_».delab : 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_smul.

Equations

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

def RightActions.«term_<•_».delab : 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_+ᵥ>_».delab : 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

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

def RightActions.«term_<+ᵥ_».delab : 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

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

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

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

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

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

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 α] : VAdd αᵃᵒᵖ α

Like Add.toVAdd, but adds on the right.

See also AddMonoid.to_OppositeAddAction.

Equations

• Add.toHasOppositeVAdd α = { vadd := fun (c : αᵃᵒᵖ) (x : α) => x + AddOpposite.unop c }

instance Mul.toHasOppositeSMul (α : Type u_1) [Mul α] : SMul αᵐᵒᵖ α

Like Mul.toSMul, but multiplies on the right.

See also Monoid.toOppositeMulAction and MonoidWithZero.toOppositeMulActionWithZero.

Equations

• Mul.toHasOppositeSMul α = { smul := fun (c : αᵐᵒᵖ) (x : α) => x * MulOpposite.unop c }

theorem op_vadd_eq_add (α : Type u_1) [Add α] {a : α} {a' : α} : AddOpposite.op a +ᵥ a' = 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' : α} : a +ᵥ a' = a' + AddOpposite.unop a

@[simp]

theorem MulOpposite.smul_eq_mul_unop (α : Type u_1) [Mul α] {a : αᵐᵒᵖ} {a' : α} : a • a' = a' * MulOpposite.unop a

instance AddAction.OppositeRegular.isPretransitive {G : Type u_2} [AddGroup G] : AddAction.IsPretransitive Gᵃᵒᵖ G

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

Equations

• ⋯ = ⋯

instance MulAction.OppositeRegular.isPretransitive {G : Type u_2} [Group G] : MulAction.IsPretransitive Gᵐᵒᵖ G

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

Equations

• ⋯ = ⋯

instance AddSemigroup.opposite_vaddCommClass (α : Type u_1) [AddSemigroup α] : VAddCommClass αᵃᵒᵖ α α

Equations

• ⋯ = ⋯

instance Semigroup.opposite_smulCommClass (α : Type u_1) [Semigroup α] : SMulCommClass αᵐᵒᵖ α α

Equations

• ⋯ = ⋯

instance AddSemigroup.opposite_vaddCommClass' (α : Type u_1) [AddSemigroup α] : VAddCommClass α αᵃᵒᵖ α

Equations

• ⋯ = ⋯

instance Semigroup.opposite_smulCommClass' (α : Type u_1) [Semigroup α] : SMulCommClass α αᵐᵒᵖ α

Equations

• ⋯ = ⋯

instance AddCommSemigroup.isCentralVAdd (α : Type u_1) [AddCommSemigroup α] : IsCentralVAdd α α

Equations

• ⋯ = ⋯

instance CommSemigroup.isCentralScalar (α : Type u_1) [CommSemigroup α] : IsCentralScalar α α

Equations

• ⋯ = ⋯

theorem AddMonoid.toOppositeAddAction.proof_2 (α : Type u_1) [AddMonoid α] : ∀ (x x_1 : αᵃᵒᵖ) (x_2 : α), x_2 + (AddOpposite.unop x_1 + AddOpposite.unop x) = x_2 + AddOpposite.unop x_1 + AddOpposite.unop x

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

instance AddMonoid.toOppositeAddAction (α : Type u_1) [AddMonoid α] : AddAction αᵃᵒᵖ α

Like AddMonoid.toAddAction, but adds on the right.

Equations

• AddMonoid.toOppositeAddAction α = AddAction.mk ⋯ ⋯

instance Monoid.toOppositeMulAction (α : Type u_1) [Monoid α] : MulAction αᵐᵒᵖ α

Like Monoid.toMulAction, but multiplies on the right.

Equations

• Monoid.toOppositeMulAction α = MulAction.mk ⋯ ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance AddLeftCancelMonoid.toFaithfulVAdd_opposite (α : Type u_1) [AddLeftCancelMonoid α] : FaithfulVAdd αᵃᵒᵖ α

AddMonoid.toOppositeAddAction is faithful on cancellative monoids.

Equations

• ⋯ = ⋯

instance LeftCancelMonoid.toFaithfulSMul_opposite (α : Type u_1) [LeftCancelMonoid α] : FaithfulSMul αᵐᵒᵖ α

Monoid.toOppositeMulAction is faithful on cancellative monoids.

Equations

• ⋯ = ⋯

instance CancelMonoidWithZero.toFaithfulSMul_opposite (α : Type u_1) [CancelMonoidWithZero α] [Nontrivial α] : FaithfulSMul αᵐᵒᵖ α

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

Equations

• ⋯ = ⋯