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.

source
theorem AddOpposite.addAction.proof_1 (α : Type u_1) (R : Type u_2) [AddMonoid R] [AddAction R α] (x : αᵃᵒᵖ) :
0 +ᵥ x = x
source
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)
source
instance AddOpposite.addAction (α : Type u_1) (R : Type u_2) [AddMonoid R] [AddAction R α] :
AddAction R αᵃᵒᵖ
source
instance MulOpposite.mulAction (α : Type u_1) (R : Type u_2) [Monoid R] [MulAction R α] :
MulAction R αᵐᵒᵖ
source
instance MulOpposite.distribMulAction (α : Type u_1) (R : Type u_2) [Monoid R] [AddMonoid α] [DistribMulAction R α] :
DistribMulAction R αᵐᵒᵖ
source
instance MulOpposite.mulDistribMulAction (α : Type u_1) (R : Type u_2) [Monoid R] [Monoid α] [MulDistribMulAction R α] :
MulDistribMulAction R αᵐᵒᵖ
source
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 α] :
VAddAssocClass M N αᵃᵒᵖ
source
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 αᵃᵒᵖ
source
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 αᵐᵒᵖ
source
instance AddOpposite.vaddCommClass (α : Type u_1) {M : Type u_2} {N : Type u_3} [VAdd M α] [VAdd N α] [VAddCommClass M N α] :
VAddCommClass M N αᵃᵒᵖ
source
theorem AddOpposite.vaddCommClass.proof_1 (α : Type u_1) {M : Type u_2} {N : Type u_3} [VAdd M α] [VAdd N α] [VAddCommClass M N α] :
VAddCommClass M N αᵃᵒᵖ
source
instance MulOpposite.smulCommClass (α : Type u_1) {M : Type u_2} {N : Type u_3} [SMul M α] [SMul N α] [SMulCommClass M N α] :
SMulCommClass M N αᵐᵒᵖ
source
instance AddOpposite.isCentralVAdd (α : Type u_1) (R : Type u_2) [VAdd R α] [VAdd Rᵃᵒᵖ α] [IsCentralVAdd R α] :
IsCentralVAdd R αᵃᵒᵖ
source
theorem AddOpposite.isCentralVAdd.proof_1 (α : Type u_1) (R : Type u_2) [VAdd R α] [VAdd Rᵃᵒᵖ α] [IsCentralVAdd R α] :
IsCentralVAdd R αᵃᵒᵖ
source
instance MulOpposite.isCentralScalar (α : Type u_1) (R : Type u_2) [SMul R α] [SMul Rᵐᵒᵖ α] [IsCentralScalar R α] :
IsCentralScalar R αᵐᵒᵖ
source
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
source
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

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.

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

Like Add.toVAdd, but adds on the right.

See also AddMonoid.to_OppositeAddAction.

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

Like Mul.toSMul, but multiplies on the right.

See also Monoid.toOppositeMulAction and MonoidWithZero.toOppositeMulActionWithZero.

source
theorem op_vadd_eq_add (α : Type u_1) [Add α] {a : α} {a' : α} :
AddOpposite.op a +ᵥ a' = a' + a
source
theorem op_smul_eq_mul (α : Type u_1) [Mul α] {a : α} {a' : α} :
MulOpposite.op a • a' = a' * a
source
@[simp]
theorem AddOpposite.vadd_eq_add_unop (α : Type u_1) [Add α] {a : αᵃᵒᵖ} {a' : α} :
a +ᵥ a' = a' + AddOpposite.unop a
source
@[simp]
theorem MulOpposite.smul_eq_mul_unop (α : Type u_1) [Mul α] {a : αᵐᵒᵖ} {a' : α} :
a • a' = a' * MulOpposite.unop a
source
theorem AddAction.OppositeRegular.isPretransitive.proof_1 {G : Type u_1} [AddGroup G] :
AddAction.IsPretransitive Gᵃᵒᵖ G
source
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.

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

source
instance AddSemigroup.opposite_vaddCommClass (α : Type u_1) [AddSemigroup α] :
VAddCommClass αᵃᵒᵖ α α
source
theorem AddSemigroup.opposite_vaddCommClass.proof_1 (α : Type u_1) [AddSemigroup α] :
VAddCommClass αᵃᵒᵖ α α
source
instance Semigroup.opposite_smulCommClass (α : Type u_1) [Semigroup α] :
SMulCommClass αᵐᵒᵖ α α
source
instance AddSemigroup.opposite_vaddCommClass' (α : Type u_1) [AddSemigroup α] :
VAddCommClass α αᵃᵒᵖ α
source
theorem AddSemigroup.opposite_vaddCommClass'.proof_1 (α : Type u_1) [AddSemigroup α] :
VAddCommClass α αᵃᵒᵖ α
source
instance Semigroup.opposite_smulCommClass' (α : Type u_1) [Semigroup α] :
SMulCommClass α αᵐᵒᵖ α
source
instance AddCommSemigroup.isCentralVAdd (α : Type u_1) [AddCommSemigroup α] :
IsCentralVAdd α α
source
theorem AddCommSemigroup.isCentralVAdd.proof_1 (α : Type u_1) [AddCommSemigroup α] :
IsCentralVAdd α α
source
instance CommSemigroup.isCentralScalar (α : Type u_1) [CommSemigroup α] :
IsCentralScalar α α
source
instance AddMonoid.toOppositeAddAction (α : Type u_1) [AddMonoid α] :
AddAction αᵃᵒᵖ α

Like AddMonoid.toAddAction, but adds on the right.

source
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
source
theorem AddMonoid.toOppositeAddAction.proof_1 (α : Type u_1) [AddMonoid α] (a : α) :
a + 0 = a
source
instance Monoid.toOppositeMulAction (α : Type u_1) [Monoid α] :
MulAction αᵐᵒᵖ α

Like Monoid.toMulAction, but multiplies on the right.

source
theorem VAddAssocClass.opposite_mid.proof_1 {M : Type u_1} {N : Type u_2} [Add N] [VAdd M N] [VAddCommClass M N N] :
VAddAssocClass M Nᵃᵒᵖ N
source
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
source
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
source
theorem VAddCommClass.opposite_mid.proof_1 {M : Type u_1} {N : Type u_2} [Add N] [VAdd M N] [VAddAssocClass M N N] :
VAddCommClass M Nᵃᵒᵖ N
source
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
source
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
source
instance AddLeftCancelMonoid.toFaithfulVAdd_opposite (α : Type u_1) [AddLeftCancelMonoid α] :
FaithfulVAdd αᵃᵒᵖ α

AddMonoid.toOppositeAddAction is faithful on cancellative monoids.

source
theorem AddLeftCancelMonoid.toFaithfulVAdd_opposite.proof_1 (α : Type u_1) [AddLeftCancelMonoid α] :
FaithfulVAdd αᵃᵒᵖ α
source
instance LeftCancelMonoid.toFaithfulSMul_opposite (α : Type u_1) [LeftCancelMonoid α] :
FaithfulSMul αᵐᵒᵖ α

Monoid.toOppositeMulAction is faithful on cancellative monoids.

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

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