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.

ink

def AddOpposite.addAction.proof_1 (α : Type u_1) (R : Type u_2) [inst : AddMonoid R] [inst : AddAction R α] (x : αᵃᵒᵖ) : 0 +ᵥ x = x

Equations

• (_ : 0 +ᵥ x = x) = (_ : 0 +ᵥ x = x)

ink

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

• (_ : r₁ + r₂ +ᵥ x = r₁ +ᵥ (r₂ +ᵥ x)) = (_ : r₁ + r₂ +ᵥ x = r₁ +ᵥ (r₂ +ᵥ x))

ink

instance AddOpposite.addAction (α : Type u_1) (R : Type u_2) [inst : AddMonoid R] [inst : AddAction R α] : AddAction R αᵃᵒᵖ

Equations

• AddOpposite.addAction α R = AddAction.mk (_ : ∀ (x : αᵃᵒᵖ), 0 +ᵥ x = x) (_ : ∀ (r₁ r₂ : R) (x : αᵃᵒᵖ), r₁ + r₂ +ᵥ x = r₁ +ᵥ (r₂ +ᵥ x))

ink

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

Equations

• MulOpposite.mulAction α R = MulAction.mk (_ : ∀ (x : αᵐᵒᵖ), 1 • x = x) (_ : ∀ (r₁ r₂ : R) (x : αᵐᵒᵖ), (r₁ * r₂) • x = r₁ • r₂ • x)

ink

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

Equations

• MulOpposite.distribMulAction α R = DistribMulAction.mk (_ : ∀ (r : R), r • 0 = 0) (_ : ∀ (r : R) (x₁ x₂ : αᵐᵒᵖ), r • (x₁ + x₂) = r • x₁ + r • x₂)

ink

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

Equations

• MulOpposite.mulDistribMulAction α R = MulDistribMulAction.mk (_ : ∀ (r : R) (x₁ x₂ : αᵐᵒᵖ), r • (x₁ * x₂) = r • x₁ * r • x₂) (_ : ∀ (r : R), r • 1 = 1)

ink

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 α] : VAddAssocClass M N αᵃᵒᵖ

Equations

• (_ : VAddAssocClass M N αᵃᵒᵖ) = (_ : VAddAssocClass M N αᵃᵒᵖ)

ink

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 α] : VAddAssocClass M N αᵃᵒᵖ

Equations

• AddOpposite.isScalarTower = AddOpposite.isScalarTower.proof_1

ink

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 α] : IsScalarTower M N αᵐᵒᵖ

Equations

• MulOpposite.isScalarTower = MulOpposite.isScalarTower.proof_1

ink

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

Equations

• AddOpposite.vaddCommClass = AddOpposite.vaddCommClass.proof_1

ink

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 α] : VAddCommClass M N αᵃᵒᵖ

Equations

• (_ : VAddCommClass M N αᵃᵒᵖ) = (_ : VAddCommClass M N αᵃᵒᵖ)

ink

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

Equations

• MulOpposite.smulCommClass = MulOpposite.smulCommClass.proof_1

ink

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

Equations

• AddOpposite.isCentralVAdd = AddOpposite.isCentralVAdd.proof_1

ink

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

Equations

• (_ : IsCentralVAdd R αᵃᵒᵖ) = (_ : IsCentralVAdd R αᵃᵒᵖ)

ink

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

Equations

• MulOpposite.isCentralScalar = MulOpposite.isCentralScalar.proof_1

ink

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 }

ink

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.

ink

instance Add.toHasOppositeVAdd (α : Type u_1) [inst : Add α] : VAdd αᵃᵒᵖ α

Like Add.toVAdd, but adds on the right.

See also AddMonoid.to_OppositeAddAction.

Equations

• Add.toHasOppositeVAdd α = { vadd := fun c x => x + c.unop }

ink

instance Mul.toHasOppositeSMul (α : Type u_1) [inst : 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 * c.unop }

ink

theorem op_vadd_eq_add (α : Type u_1) [inst : Add α] {a : α} {a' : α} : { unop := a } +ᵥ a' = a' + a

ink

theorem op_smul_eq_mul (α : Type u_1) [inst : Mul α] {a : α} {a' : α} : { unop := a } • a' = a' * a

ink

@[simp]

theorem AddOpposite.vadd_eq_add_unop (α : Type u_1) [inst : Add α] {a : αᵃᵒᵖ} {a' : α} : a +ᵥ a' = a' + a.unop

ink

@[simp]

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

ink

def AddAction.OppositeRegular.isPretransitive.proof_1 {G : Type u_1} [inst : AddGroup G] : AddAction.IsPretransitive Gᵃᵒᵖ G

Equations

• (_ : AddAction.IsPretransitive Gᵃᵒᵖ G) = (_ : AddAction.IsPretransitive Gᵃᵒᵖ G)

ink

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

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

Equations

• @AddAction.OppositeRegular.isPretransitive = @AddAction.OppositeRegular.isPretransitive.proof_1

ink

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

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

Equations

• @MulAction.OppositeRegular.isPretransitive = @MulAction.OppositeRegular.isPretransitive.proof_1

ink

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

Equations

• AddSemigroup.opposite_vaddCommClass = AddSemigroup.opposite_vaddCommClass.proof_1

ink

def AddSemigroup.opposite_vaddCommClass.proof_1 (α : Type u_1) [inst : AddSemigroup α] : VAddCommClass αᵃᵒᵖ α α

Equations

• (_ : VAddCommClass αᵃᵒᵖ α α) = (_ : VAddCommClass αᵃᵒᵖ α α)

ink

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

Equations

• Semigroup.opposite_smulCommClass = Semigroup.opposite_smulCommClass.proof_1

ink

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

Equations

• AddSemigroup.opposite_vaddCommClass' = AddSemigroup.opposite_vaddCommClass'.proof_1

ink

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

Equations

• (_ : VAddCommClass α αᵃᵒᵖ α) = (_ : VAddCommClass α αᵃᵒᵖ α)

ink

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

Equations

• Semigroup.opposite_smulCommClass' = Semigroup.opposite_smulCommClass'.proof_1

ink

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

Equations

• AddCommSemigroup.isCentralVAdd = AddCommSemigroup.isCentralVAdd.proof_1

ink

def AddCommSemigroup.isCentralVAdd.proof_1 (α : Type u_1) [inst : AddCommSemigroup α] : IsCentralVAdd α α

Equations

• (_ : IsCentralVAdd α α) = (_ : IsCentralVAdd α α)

ink

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

Equations

• CommSemigroup.isCentralScalar = CommSemigroup.isCentralScalar.proof_1

ink

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)

ink

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

Like AddMonoid.toAddAction, but adds on the right.

Equations

• AddMonoid.toOppositeAddAction α = AddAction.mk (_ : ∀ (a : α), a + 0 = a) (_ : ∀ (x x_1 : αᵃᵒᵖ) (x_2 : α), x_2 + (x_1.unop + x.unop) = x_2 + x_1.unop + x.unop)

ink

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

Like Monoid.toMulAction, but multiplies on the right.

Equations

• Monoid.toOppositeMulAction α = MulAction.mk (_ : ∀ (a : α), a * 1 = a) (_ : ∀ (x x_1 : αᵐᵒᵖ) (x_2 : α), x_2 * (x_1.unop * x.unop) = x_2 * x_1.unop * x.unop)

ink

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

Equations

• @VAddAssocClass.opposite_mid = @VAddAssocClass.opposite_mid.proof_1

ink

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] : VAddAssocClass M Nᵃᵒᵖ N

Equations

• (_ : VAddAssocClass M Nᵃᵒᵖ N) = (_ : VAddAssocClass M Nᵃᵒᵖ N)

ink

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

Equations

• @IsScalarTower.opposite_mid = @IsScalarTower.opposite_mid.proof_1

ink

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] : VAddCommClass M Nᵃᵒᵖ N

Equations

• (_ : VAddCommClass M Nᵃᵒᵖ N) = (_ : VAddCommClass M Nᵃᵒᵖ N)

ink

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

Equations

• @VAddCommClass.opposite_mid = @VAddCommClass.opposite_mid.proof_1

ink

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

Equations

• @SMulCommClass.opposite_mid = @SMulCommClass.opposite_mid.proof_1

ink

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

AddMonoid.toOppositeAddAction is faithful on cancellative monoids.

Equations

• AddLeftCancelMonoid.toFaithfulVAdd_opposite = AddLeftCancelMonoid.toFaithfulVAdd_opposite.proof_1

ink

def AddLeftCancelMonoid.toFaithfulVAdd_opposite.proof_1 (α : Type u_1) [inst : AddLeftCancelMonoid α] : FaithfulVAdd αᵃᵒᵖ α

Equations

• (_ : FaithfulVAdd αᵃᵒᵖ α) = (_ : FaithfulVAdd αᵃᵒᵖ α)

ink

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

Monoid.toOppositeMulAction is faithful on cancellative monoids.

Equations

• LeftCancelMonoid.toFaithfulSMul_opposite = LeftCancelMonoid.toFaithfulSMul_opposite.proof_1

ink

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

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

Equations

• CancelMonoidWithZero.toFaithfulSMul_opposite = CancelMonoidWithZero.toFaithfulSMul_opposite.proof_1