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.

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.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 α] :
Equations
instance MulOpposite.mulAction (α : Type u_1) (R : Type u_2) [Monoid R] [MulAction R α] :
Equations
instance AddOpposite.isScalarTower (α : Type u_1) {M : Type u_2} {N : Type u_3} [VAdd M N] [VAdd M α] [VAdd 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 α] :
Equations
  • =
instance AddOpposite.vaddCommClass (α : Type u_1) {M : Type u_2} {N : Type u_3} [VAdd M α] [VAdd 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 α] :
Equations
  • =
instance AddOpposite.isCentralVAdd (α : Type u_1) (R : Type u_2) [VAdd R α] [VAdd Rᵃᵒᵖ α] [IsCentralVAdd R α] :
Equations
  • =
instance MulOpposite.isCentralScalar (α : Type u_1) (R : Type u_2) [SMul R α] [SMul 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 : α) :

Right actions #

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

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.
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
      • One or more equations did not get rendered due to their size.
      Instances For

        Pretty printer defined by notation3 command.

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

                  Like Add.toVAdd, but adds on the right.

                  See also AddMonoid.to_OppositeAddAction.

                  Equations
                  instance Mul.toHasOppositeSMul (α : Type u_1) [Mul α] :

                  Like Mul.toSMul, but multiplies on the right.

                  See also Monoid.toOppositeMulAction and MonoidWithZero.toOppositeMulActionWithZero.

                  Equations
                  theorem op_vadd_eq_add (α : Type u_1) [Add α] {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' : α} :
                  @[simp]
                  theorem MulOpposite.smul_eq_mul_unop (α : Type u_1) [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_2} {N : Type u_3} [Add N] [VAdd M N] [VAddCommClass 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] :
                  Equations
                  • =
                  instance VAddCommClass.opposite_mid {M : Type u_2} {N : Type u_3} [Add N] [VAdd M N] [VAddAssocClass 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] :
                  Equations
                  • =

                  AddMonoid.toOppositeAddAction is faithful on cancellative monoids.

                  Equations
                  • =

                  Monoid.toOppositeMulAction is faithful on cancellative monoids.

                  Equations
                  • =

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

                  Equations
                  • =