Documentation

Mathlib.Algebra.Group.Action.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.

Notation #

With open scoped RightActions, this provides:

Actions on the opposite type #

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

theorem AddOpposite.instAddAction.proof_2 {M : Type u_2} {α : Type u_1} [AddMonoid M] [AddAction M α] :
∀ (x x_1 : M) (x_2 : αᵃᵒᵖ), x + x_1 +ᵥ x_2 = x +ᵥ (x_1 +ᵥ x_2)
instance AddOpposite.instAddAction {M : Type u_2} {α : Type u_4} [AddMonoid M] [AddAction M α] :
Equations
theorem AddOpposite.instAddAction.proof_1 {M : Type u_2} {α : Type u_1} [AddMonoid M] [AddAction M α] :
∀ (x : αᵃᵒᵖ), 0 +ᵥ x = x
instance MulOpposite.instMulAction {M : Type u_2} {α : Type u_4} [Monoid M] [MulAction M α] :
Equations
instance AddOpposite.instIsScalarTower {M : Type u_2} {N : Type u_3} {α : Type u_4} [VAdd M N] [VAdd M α] [VAdd N α] [VAddAssocClass M N α] :
Equations
  • =
instance MulOpposite.instIsScalarTower {M : Type u_2} {N : Type u_3} {α : Type u_4} [SMul M N] [SMul M α] [SMul N α] [IsScalarTower M N α] :
Equations
  • =
instance AddOpposite.instVAddCommClass {M : Type u_2} {N : Type u_3} {α : Type u_4} [VAdd M α] [VAdd N α] [VAddCommClass M N α] :
Equations
  • =
instance MulOpposite.instSMulCommClass {M : Type u_2} {N : Type u_3} {α : Type u_4} [SMul M α] [SMul N α] [SMulCommClass M N α] :
Equations
  • =
instance AddOpposite.instIsCentralVAdd {M : Type u_2} {α : Type u_4} [VAdd M α] [VAdd Mᵃᵒᵖ α] [IsCentralVAdd M α] :
Equations
  • =
Equations
  • =
theorem AddOpposite.op_vadd_eq_op_vadd_op {M : Type u_2} {α : Type u_4} [VAdd M α] [VAdd Mᵃᵒᵖ α] [IsCentralVAdd M α] (r : M) (a : α) :
theorem MulOpposite.op_smul_eq_op_smul_op {M : Type u_2} {α : Type u_4} [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] (r : M) (a : α) :

Right actions #

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

Pretty printer defined by notation3 command.

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

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

    In lemma names this is still called smul.

    Equations
    Instances For

      Pretty printer defined by notation3 command.

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

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

        In lemma names this is still called op_smul.

        Equations
        Instances For

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

          In lemma names this is still called vadd.

          Equations
          Instances For

            Pretty printer defined by notation3 command.

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

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

              In lemma names this is still called op_vadd.

              Equations
              Instances For

                Pretty printer defined by notation3 command.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem op_vadd_op_vadd {α : Type u_5} {β : Type u_6} [AddMonoid α] [AddAction αᵃᵒᵖ β] (b : β) (a₁ : α) (a₂ : α) :
                  theorem op_smul_op_smul {α : Type u_5} {β : Type u_6} [Monoid α] [MulAction αᵐᵒᵖ β] (b : β) (a₁ : α) (a₂ : α) :
                  theorem op_vadd_add {α : Type u_5} {β : Type u_6} [AddMonoid α] [AddAction αᵃᵒᵖ β] (b : β) (a₁ : α) (a₂ : α) :
                  theorem op_smul_mul {α : Type u_5} {β : Type u_6} [Monoid α] [MulAction αᵐᵒᵖ β] (b : β) (a₁ : α) (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.

                  instance Add.toHasOppositeVAdd {α : Type u_4} [Add α] :

                  Like Add.toVAdd, but adds on the right.

                  See also AddMonoid.toOppositeAddAction.

                  Equations
                  instance Mul.toHasOppositeSMul {α : Type u_4} [Mul α] :

                  Like Mul.toSMul, but multiplies on the right.

                  See also Monoid.toOppositeMulAction and MonoidWithZero.toOppositeMulActionWithZero.

                  Equations
                  theorem op_vadd_eq_add {α : Type u_4} [Add α] {a : α} {a' : α} :
                  theorem op_smul_eq_mul {α : Type u_4} [Mul α] {a : α} {a' : α} :
                  MulOpposite.op a a' = a' * a
                  @[simp]
                  theorem AddOpposite.vadd_eq_add_unop {α : Type u_4} [Add α] {a : αᵃᵒᵖ} {a' : α} :
                  @[simp]
                  theorem MulOpposite.smul_eq_mul_unop {α : Type u_4} [Mul α] {a : αᵐᵒᵖ} {a' : α} :

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

                  Equations
                  • =

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

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

                  Like AddMonoid.toAddAction, but adds on the right.

                  Equations

                  Like Monoid.toMulAction, but multiplies on the right.

                  Equations
                  instance VAddAssocClass.opposite_mid {M : Type u_5} {N : Type u_6} [Add N] [VAdd M N] [VAddCommClass M N N] :
                  Equations
                  • =
                  instance IsScalarTower.opposite_mid {M : Type u_5} {N : Type u_6} [Mul N] [SMul M N] [SMulCommClass M N N] :
                  Equations
                  • =
                  instance VAddCommClass.opposite_mid {M : Type u_5} {N : Type u_6} [Add N] [VAdd M N] [VAddAssocClass M N N] :
                  Equations
                  • =
                  instance SMulCommClass.opposite_mid {M : Type u_5} {N : Type u_6} [Mul N] [SMul M N] [IsScalarTower M N N] :
                  Equations
                  • =

                  AddMonoid.toOppositeAddAction is faithful on cancellative monoids.

                  Equations
                  • =

                  Monoid.toOppositeMulAction is faithful on cancellative monoids.

                  Equations
                  • =