doc-next-gen

Mathlib.Algebra.Group.Action.Opposite

Module docstring

{"# 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. ","### Right actions

In this section we establish SMul αᵐᵒᵖ β as the canonical spelling of right scalar multiplication of β by α, and provide convenient notations. ","### Actions by the opposite type (right actions) "}

MulOpposite.instMulAction instance
[Monoid M] [MulAction M α] : MulAction M αᵐᵒᵖ
Full source 
@[to_additive]
instance instMulAction [Monoid M] [MulAction M α] : MulAction M αᵐᵒᵖ where
  one_smul _ := unop_injective <| one_smul _ _
  mul_smul _ _ _ := unop_injective <| mul_smul _ _ _
Multiplicative Action on the Multiplicative Opposite
Informal description
For any monoid $M$ acting on a type $\alpha$, the multiplicative opposite $\alpha^\text{op}$ inherits a multiplicative action from $M$. This action is defined by $m \cdot \text{op}(a) = \text{op}(m \cdot a)$ for any $m \in M$ and $a \in \alpha$.
MulOpposite.instIsScalarTower instance
[SMul M N] [SMul M α] [SMul N α] [IsScalarTower M N α] : IsScalarTower M N αᵐᵒᵖ
Full source 
@[to_additive]
instance instIsScalarTower [SMul M N] [SMul M α] [SMul N α] [IsScalarTower M N α] :
    IsScalarTower M N αᵐᵒᵖ where
  smul_assoc _ _ _ := unop_injective <| smul_assoc _ _ _
Scalar Tower Structure on the Multiplicative Opposite
Informal description
For any types $M$, $N$, and $\alpha$ with scalar multiplication operations $[SMul M N]$, $[SMul M \alpha]$, and $[SMul N \alpha]$, if the scalar multiplications form a tower structure on $\alpha$ (i.e., $(m \cdot n) \cdot a = m \cdot (n \cdot a)$ for all $m \in M$, $n \in N$, and $a \in \alpha$), then the same tower structure holds for the multiplicative opposite $\alpha^\text{op}$. Specifically, the scalar multiplication on $\alpha^\text{op}$ satisfies $(m \cdot n) \cdot \text{op}(a) = m \cdot (n \cdot \text{op}(a))$ for all $m \in M$, $n \in N$, and $a \in \alpha$.
MulOpposite.instSMulCommClass instance
[SMul M α] [SMul N α] [SMulCommClass M N α] : SMulCommClass M N αᵐᵒᵖ
Full source 
@[to_additive]
instance instSMulCommClass [SMul M α] [SMul N α] [SMulCommClass M N α] :
    SMulCommClass M N αᵐᵒᵖ where
  smul_comm _ _ _ := unop_injective <| smul_comm _ _ _
Commutativity of Scalar Actions on the Multiplicative Opposite
Informal description
For any types $M$ and $N$ with scalar multiplication actions on a type $\alpha$, if the actions of $M$ and $N$ on $\alpha$ commute (i.e., $m \cdot (n \cdot a) = n \cdot (m \cdot a)$ for all $m \in M$, $n \in N$, and $a \in \alpha$), then the actions of $M$ and $N$ on the multiplicative opposite $\alpha^\text{op}$ also commute.
MulOpposite.instIsCentralScalar instance
[SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] : IsCentralScalar M αᵐᵒᵖ
Full source 
@[to_additive]
instance instIsCentralScalar [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] :
    IsCentralScalar M αᵐᵒᵖ where
  op_smul_eq_smul _ _ := unop_injective <| op_smul_eq_smul _ _
Central Scalar Action on Multiplicative Opposite
Informal description
For any type $M$ with a scalar multiplication operation on a type $\alpha$, if $M$ acts centrally on $\alpha$ (meaning the left and right scalar multiplications coincide), then $M$ also acts centrally on the multiplicative opposite $\alpha^\text{op}$.
MulOpposite.op_smul_eq_op_smul_op theorem
[SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] (r : M) (a : α) : op (r • a) = op r • op a
Full source 
@[to_additive]
lemma op_smul_eq_op_smul_op [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] (r : M) (a : α) :
    op (r • a) = op r • op a := (op_smul_eq_smul r (op a)).symm
Compatibility of canonical embedding with scalar multiplication in multiplicative opposites
Informal description
Let $M$ and $\alpha$ be types equipped with scalar multiplication operations, and suppose $M$ acts centrally on $\alpha$. For any element $r \in M$ and $a \in \alpha$, the canonical embedding into the multiplicative opposite satisfies $\text{op}(r \cdot a) = \text{op}(r) \cdot \text{op}(a)$.
MulOpposite.unop_smul_eq_unop_smul_unop theorem
[SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] (r : Mᵐᵒᵖ) (a : αᵐᵒᵖ) : unop (r • a) = unop r • unop a
Full source 
@[to_additive]
lemma unop_smul_eq_unop_smul_unop [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] (r : Mᵐᵒᵖ)
    (a : αᵐᵒᵖ) : unop (r • a) = unop r • unop a := (unop_smul_eq_smul r (unop a)).symm
Compatibility of unary operation with scalar multiplication in multiplicative opposites
Informal description
Let $M$ and $\alpha$ be types equipped with scalar multiplication operations, and suppose $M$ acts centrally on $\alpha$. For any element $r$ in the multiplicative opposite $M^\text{op}$ and any element $a$ in the multiplicative opposite $\alpha^\text{op}$, the unary operation of scalar multiplication satisfies $\text{unop}(r \cdot a) = \text{unop}(r) \cdot \text{unop}(a)$.
RightActions.term_•>_ definition
: Lean.TrailingParserDescr✝
Full source 
/-- With `open scoped RightActions`, an alternative symbol for left actions, `r • m`.

In lemma names this is still called `smul`. -/
scoped notation3:74 r:75 " •> " m:74 => r • m
Left scalar multiplication notation for right actions
Informal description
The notation `r •> m` is an alternative notation for the left scalar multiplication `r • m`, where `r` is a scalar and `m` is an element of the module being acted upon. This notation is used when working with right actions and is enabled by `open scoped RightActions`.
RightActions.term_•>_.delab_app.HSMul.hSMul definition
: Delab✝
Full source 
/-- With `open scoped RightActions`, an alternative symbol for left actions, `r • m`.

In lemma names this is still called `smul`. -/
scoped notation3:74 r:75 " •> " m:74 => r • m
Alternative notation for left scalar multiplication
Informal description
The notation `r •> m` is defined as an alternative representation for the left scalar multiplication `r • m`, where `r` is a scalar and `m` is an element being acted upon.
RightActions.term_<•_ definition
: Lean.TrailingParserDescr✝
Full source 
/-- With `open scoped RightActions`, a shorthand for right actions, `op r • m`.

In lemma names this is still called `op_smul`. -/
scoped notation3:73 m:73 " <• " r:74 => MulOpposite.op r • m
Right scalar multiplication notation
Informal description
The notation `m <• r` represents the right scalar multiplication of `m` by `r`, defined as `MulOpposite.op r • m`. This is used as a shorthand for right actions when the `RightActions` scope is open.
RightActions.term_<•_.delab_app.HSMul.hSMul definition
: Delab✝
Full source 
/-- With `open scoped RightActions`, a shorthand for right actions, `op r • m`.

In lemma names this is still called `op_smul`. -/
scoped notation3:73 m:73 " <• " r:74 => MulOpposite.op r • m
Right scalar multiplication notation
Informal description
The notation `m <• r` represents the right scalar multiplication of `m` by `r`, defined as `MulOpposite.op r • m`. This is used as a shorthand for right actions when working with opposite types.
RightActions.term_+ᵥ>_ definition
: Lean.TrailingParserDescr✝
Full source 
/-- With `open scoped RightActions`, an alternative symbol for left actions, `r • m`.

In lemma names this is still called `vadd`. -/
scoped notation3:74 r:75 " +ᵥ> " m:74 => r +ᵥ m
Alternative notation for left additive action
Informal description
The notation `r +ᵥ> m` is an alternative symbol for the left action `r +ᵥ m`, where `r` is a scalar and `m` is an element of the acted-upon type. This notation is used when `RightActions` is opened in scope.
RightActions.term_+ᵥ>_.delab_app.HVAdd.hVAdd definition
: Delab✝
Full source 
/-- With `open scoped RightActions`, an alternative symbol for left actions, `r • m`.

In lemma names this is still called `vadd`. -/
scoped notation3:74 r:75 " +ᵥ> " m:74 => r +ᵥ m
Alternative notation for left vector action
Informal description
The notation `r +ᵥ> m` is defined as an alternative syntax for the left action `r +ᵥ m`, where `+ᵥ` represents the vector addition action. This notation is available when working within the `RightActions` scope.
RightActions.term_<+ᵥ_ definition
: Lean.TrailingParserDescr✝
Full source 
/-- With `open scoped RightActions`, a shorthand for right actions, `op r +ᵥ m`.

In lemma names this is still called `op_vadd`. -/
scoped notation3:73 m:73 " <+ᵥ " r:74 => AddOpposite.op r +ᵥ m
Right action notation for additive operations
Informal description
The notation `m <+ᵥ r` is defined as shorthand for the right action of `r` on `m`, which is equivalent to `AddOpposite.op r +ᵥ m`. This notation is used when working with right actions in the context of `AddOpposite`.
RightActions.term_<+ᵥ_.delab_app.HVAdd.hVAdd definition
: Delab✝
Full source 
/-- With `open scoped RightActions`, a shorthand for right actions, `op r +ᵥ m`.

In lemma names this is still called `op_vadd`. -/
scoped notation3:73 m:73 " <+ᵥ " r:74 => AddOpposite.op r +ᵥ m
Right action notation for additive opposite
Informal description
The notation `m <+ᵥ r` is defined as shorthand for the right action `AddOpposite.op r +ᵥ m`, where `r` is an element of the additive opposite type acting on `m`. This notation is used when working with right actions in the context of `AddOpposite`.
op_smul_op_smul theorem
(b : β) (a₁ a₂ : α) : b <• a₁ <• a₂ = b <• (a₁ * a₂)
Full source 
@[to_additive]
lemma op_smul_op_smul (b : β) (a₁ a₂ : α) : b <• a₁b <• a₁ <• a₂ = b <• (a₁ * a₂) := smul_smul _ _ _
Compatibility of Right Actions with Multiplication in Opposite Monoid
Informal description
For any elements $b \in \beta$ and $a_1, a_2 \in \alpha$, the right action of $a_1$ followed by the right action of $a_2$ on $b$ is equal to the right action of the product $a_1 * a_2$ on $b$. In symbols: $$(b <\bullet a_1) <\bullet a_2 = b <\bullet (a_1 * a_2)$$
op_smul_mul theorem
(b : β) (a₁ a₂ : α) : b <• (a₁ * a₂) = b <• a₁ <• a₂
Full source 
@[to_additive]
lemma op_smul_mul (b : β) (a₁ a₂ : α) : b <• (a₁ * a₂) = b <• a₁b <• a₁ <• a₂ := mul_smul _ _ _
Right Scalar Multiplication Distributes Over Monoid Multiplication
Informal description
For any element $b$ in a type $\beta$ and any elements $a_1, a_2$ in a monoid $\alpha$, the right scalar multiplication of $b$ by the product $a_1 * a_2$ equals the successive right scalar multiplications of $b$ by $a_1$ and then by $a_2$. In other words, $b <\bullet (a_1 * a_2) = (b <\bullet a_1) <\bullet a_2$.
Semigroup.opposite_smulCommClass instance
[Semigroup α] : SMulCommClass αᵐᵒᵖ α α
Full source 
@[to_additive]
instance Semigroup.opposite_smulCommClass [Semigroup α] : SMulCommClass αᵐᵒᵖ α α where
  smul_comm _ _ _ := mul_assoc _ _ _
Scalar Commutativity for Opposite Semigroup Actions
Informal description
For any semigroup $\alpha$, the multiplicative opposite $\alpha^\text{op}$ and $\alpha$ form a scalar commuting class acting on $\alpha$. This means that for any $a \in \alpha^\text{op}$, $b \in \alpha$, and $c \in \alpha$, the operations satisfy $(a \cdot b) \cdot c = (b \cdot a) \cdot c$.
Semigroup.opposite_smulCommClass' instance
[Semigroup α] : SMulCommClass α αᵐᵒᵖ α
Full source 
@[to_additive]
instance Semigroup.opposite_smulCommClass' [Semigroup α] : SMulCommClass α αᵐᵒᵖ α :=
  SMulCommClass.symm _ _ _
Scalar Commutativity for Semigroup Actions with Opposite Elements
Informal description
For any semigroup $\alpha$, the multiplicative opposite $\alpha^\text{op}$ and $\alpha$ form a scalar commuting class acting on $\alpha$. This means that for any $a \in \alpha$, $b \in \alpha^\text{op}$, and $c \in \alpha$, the operations satisfy $(a \cdot b) \cdot c = (b \cdot a) \cdot c$.
CommSemigroup.isCentralScalar instance
[CommSemigroup α] : IsCentralScalar α α
Full source 
@[to_additive]
instance CommSemigroup.isCentralScalar [CommSemigroup α] : IsCentralScalar α α where
  op_smul_eq_smul _ _ := mul_comm _ _
Central Scalar Multiplication in Commutative Semigroups
Informal description
For any commutative semigroup $\alpha$, the scalar multiplication action of $\alpha$ on itself is central, meaning that left and right scalar multiplications coincide.
Monoid.toOppositeMulAction instance
[Monoid α] : MulAction αᵐᵒᵖ α
Full source 
/-- Like `Monoid.toMulAction`, but multiplies on the right. -/
@[to_additive "Like `AddMonoid.toAddAction`, but adds on the right."]
instance Monoid.toOppositeMulAction [Monoid α] : MulAction αᵐᵒᵖ α where
  smul := (· • ·)
  one_smul := mul_one
  mul_smul _ _ _ := (mul_assoc _ _ _).symm
Right Multiplication Action by the Multiplicative Opposite
Informal description
For any monoid $\alpha$, the multiplicative opposite $\alpha^\text{op}$ acts on $\alpha$ by right multiplication. Specifically, for $a \in \alpha^\text{op}$ and $b \in \alpha$, the action is defined as $a \cdot b = b \cdot \text{op}^{-1}(a)$, where $\text{op}^{-1}$ is the inverse of the canonical embedding $\text{op} : \alpha \to \alpha^\text{op}$.
IsScalarTower.opposite_mid instance
{M N} [Mul N] [SMul M N] [SMulCommClass M N N] : IsScalarTower M Nᵐᵒᵖ N
Full source 
@[to_additive]
instance IsScalarTower.opposite_mid {M N} [Mul N] [SMul M N] [SMulCommClass M N N] :
    IsScalarTower M Nᵐᵒᵖ N where
  smul_assoc _ _ _ := mul_smul_comm _ _ _
Scalar Tower Property for Scalar Multiplication on the Multiplicative Opposite
Informal description
For any types $M$ and $N$ with a multiplication operation on $N$ and a scalar multiplication action of $M$ on $N$, if the scalar multiplication action commutes with the multiplication in $N$ (i.e., $[SMulCommClass M N N]$), then the scalar multiplication action of $M$ on the multiplicative opposite $N^\text{op}$ forms a scalar tower with the multiplication in $N$.
SMulCommClass.opposite_mid instance
{M N} [Mul N] [SMul M N] [IsScalarTower M N N] : SMulCommClass M Nᵐᵒᵖ N
Full source 
@[to_additive]
instance SMulCommClass.opposite_mid {M N} [Mul N] [SMul M N] [IsScalarTower M N N] :
    SMulCommClass M Nᵐᵒᵖ N where
  smul_comm x y z := by
    induction y using MulOpposite.rec'
    simp only [smul_mul_assoc, MulOpposite.smul_eq_mul_unop]
Commutativity of Scalar Multiplication with Opposite Multiplication in Scalar Tower Context
Informal description
For any types $M$ and $N$ with a multiplication operation on $N$ and a scalar multiplication action of $M$ on $N$, if the scalar multiplication action forms a scalar tower with the multiplication in $N$ (i.e., $[IsScalarTower M N N]$), then the scalar multiplication action of $M$ on $N$ commutes with the multiplication in the multiplicative opposite $N^\text{op}$.