Mathlib.Algebra.Group.Action.Defs

Mul.toSMul instance

(α : Type*) [Mul α] : SMul α α

Full source

/-- See also `Monoid.toMulAction` and `MulZeroClass.toSMulWithZero`. -/
@[to_additive "See also `AddMonoid.toAddAction`"]
instance (priority := 910) Mul.toSMul (α : Type*) [Mul α] : SMul α α := ⟨(· * ·)⟩

Multiplication as Scalar Multiplication

Informal description

For any type $\alpha$ with a multiplication operation, there is a canonical scalar multiplication operation on $\alpha$ where the scalar multiplication $a \• b$ is defined to be the product $a * b$.

Mul.toSMulMulOpposite instance

(α : Type*) [Mul α] : SMul αᵐᵒᵖ α

Full source

/-- Like `Mul.toSMul`, but multiplies on the right.

See also `Monoid.toOppositeMulAction` and `MonoidWithZero.toOppositeMulActionWithZero`. -/
@[to_additive "Like `Add.toVAdd`, but adds on the right.

  See also `AddMonoid.toOppositeAddAction`."]
instance (priority := 910) Mul.toSMulMulOpposite (α : Type*) [Mul α] : SMul αᵐᵒᵖ α where
  smul a b := b * a.unop

Right Multiplication as Scalar Multiplication via Opposite

Informal description

For any type $\alpha$ with a multiplication operation, there is a canonical scalar multiplication operation of $\alpha^\text{op}$ on $\alpha$ defined by $a^\text{op} \• b = b * a$, where $a^\text{op}$ denotes the element $a$ in the multiplicative opposite $\alpha^\text{op}$.

smul_eq_mul theorem

{α : Type*} [Mul α] (a b : α) : a • b = a * b

Full source

@[to_additive (attr := simp)]
lemma smul_eq_mul {α : Type*} [Mul α] (a b : α) : a • b = a * b := rfl

Scalar Multiplication Equals Multiplication: $a \• b = a * b$

Informal description

For any type $\alpha$ equipped with a multiplication operation, the scalar multiplication $a \• b$ is equal to the product $a * b$ for all $a, b \in \alpha$.

op_smul_eq_mul theorem

{α : Type*} [Mul α] (a b : α) : MulOpposite.op a • b = b * a

Full source

@[to_additive]
lemma op_smul_eq_mul {α : Type*} [Mul α] (a b : α) : MulOpposite.op a • b = b * a := rfl

Scalar multiplication via opposite equals right multiplication: $\text{op}(a) \• b = b * a$

Informal description

For any type $\alpha$ with a multiplication operation and elements $a, b \in \alpha$, the scalar multiplication of the multiplicative opposite of $a$ on $b$ equals the product $b * a$, i.e., $\text{op}(a) \• b = b * a$.

MulOpposite.smul_eq_mul_unop theorem

[Mul α] (a : αᵐᵒᵖ) (b : α) : a • b = b * a.unop

Full source

@[to_additive (attr := simp)]
lemma MulOpposite.smul_eq_mul_unop [Mul α] (a : αᵐᵒᵖ) (b : α) : a • b = b * a.unop := rfl

Scalar Multiplication via Opposite Equals Right Multiplication: $a \• b = b * \text{unop}(a)$

Informal description

For any type $\alpha$ with a multiplication operation, and for any elements $a$ in the multiplicative opposite $\alpha^\text{op}$ and $b$ in $\alpha$, the scalar multiplication $a \• b$ is equal to the product $b * \text{unop}(a)$, where $\text{unop}$ is the canonical projection from $\alpha^\text{op}$ to $\alpha$.

AddAction structure

(G : Type*) (P : Type*) [AddMonoid G] extends VAdd G P

Full source

/-- Type class for additive monoid actions. -/
class AddAction (G : Type*) (P : Type*) [AddMonoid G] extends VAdd G P where
  /-- Zero is a neutral element for `+ᵥ` -/
  protected zero_vadd : ∀ p : P, (0 : G) +ᵥ p = p
  /-- Associativity of `+` and `+ᵥ` -/
  add_vadd : ∀ (g₁ g₂ : G) (p : P), (g₁ + g₂) +ᵥ p = g₁ +ᵥ g₂ +ᵥ p

Additive Monoid Action

Informal description

The structure representing an additive monoid action, where an additive monoid $ G $ acts on a type $ P $ via an additive operation $ +ᵥ $. This extends the notation class `VAdd` with the additional properties of an additive monoid action.

MulAction structure

(α : Type*) (β : Type*) [Monoid α] extends SMul α β

Full source

/-- Typeclass for multiplicative actions by monoids. This generalizes group actions. -/
@[to_additive (attr := ext)]
class MulAction (α : Type*) (β : Type*) [Monoid α] extends SMul α β where
  /-- One is the neutral element for `•` -/
  protected one_smul : ∀ b : β, (1 : α) • b = b
  /-- Associativity of `•` and `*` -/
  mul_smul : ∀ (x y : α) (b : β), (x * y) • b = x • y • b

Multiplicative Action of a Monoid

Informal description

The structure `MulAction α β` represents a multiplicative action of a monoid `α` on a type `β`, extending the scalar multiplication operation `SMul α β`. This generalizes the notion of group actions to monoids.

VAddCommClass structure

(M N α : Type*) [VAdd M α] [VAdd N α]

Full source

/-- A typeclass mixin saying that two additive actions on the same space commute. -/
class VAddCommClass (M N α : Type*) [VAdd M α] [VAdd N α] : Prop where
  /-- `+ᵥ` is left commutative -/
  vadd_comm : ∀ (m : M) (n : N) (a : α), m +ᵥ (n +ᵥ a) = n +ᵥ (m +ᵥ a)

Commutativity of Additive Actions

Informal description

The structure `VAddCommClass M N α` asserts that two additive actions of `M` and `N` on `α` commute, meaning that for any `m : M`, `n : N`, and `a : α`, the actions satisfy `m +ᵥ (n +ᵥ a) = n +ᵥ (m +ᵥ a)`.

SMulCommClass structure

(M N α : Type*) [SMul M α] [SMul N α]

Full source

/-- A typeclass mixin saying that two multiplicative actions on the same space commute. -/
@[to_additive]
class SMulCommClass (M N α : Type*) [SMul M α] [SMul N α] : Prop where
  /-- `•` is left commutative -/
  smul_comm : ∀ (m : M) (n : N) (a : α), m • n • a = n • m • a

Commutativity of Scalar Multiplications

Informal description

The structure `SMulCommClass M N α` asserts that the scalar multiplications by `M` and `N` on `α` commute with each other, i.e., for any `m : M`, `n : N`, and `a : α`, we have $m \cdot (n \cdot a) = n \cdot (m \cdot a)$.

SMulCommClass.symm theorem

(M N α : Type*) [SMul M α] [SMul N α] [SMulCommClass M N α] : SMulCommClass N M α

Full source

/-- Commutativity of actions is a symmetric relation. This lemma can't be an instance because this
would cause a loop in the instance search graph. -/
@[to_additive]
lemma SMulCommClass.symm (M N α : Type*) [SMul M α] [SMul N α] [SMulCommClass M N α] :
    SMulCommClass N M α where smul_comm a' a b := (smul_comm a a' b).symm

Symmetry of Commuting Scalar Actions

Informal description

For any types $M$, $N$, and $\alpha$ equipped with scalar multiplication operations $M \times \alpha \to \alpha$ and $N \times \alpha \to \alpha$, if the scalar multiplications 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$, $a \in \alpha$), then the scalar multiplications of $N$ and $M$ on $\alpha$ also commute.

Function.Injective.smulCommClass theorem

 [SMul M α] [SMul N α] [SMul M β] [SMul N β] [SMulCommClass M N β] {f : α → β} (hf : Injective f)
  (h₁ : ∀ (c : M) x, f (c • x) = c • f x) (h₂ : ∀ (c : N) x, f (c • x) = c • f x) : SMulCommClass M N α

Full source

@[to_additive]
lemma Function.Injective.smulCommClass [SMul M α] [SMul N α] [SMul M β] [SMul N β]
    [SMulCommClass M N β] {f : α → β} (hf : Injective f) (h₁ : ∀ (c : M) x, f (c • x) = c • f x)
    (h₂ : ∀ (c : N) x, f (c • x) = c • f x) : SMulCommClass M N α where
  smul_comm c₁ c₂ x := hf <| by simp only [h₁, h₂, smul_comm c₁ c₂ (f x)]

Inheritance of Commuting Scalar Actions via Injective Map

Informal description

Let $M$ and $N$ be types with scalar multiplication actions on types $\alpha$ and $\beta$. Suppose $f : \alpha \to \beta$ is an injective function such that for all $c \in M$ and $x \in \alpha$, $f(c \cdot x) = c \cdot f(x)$, and similarly for $N$. If the scalar multiplications of $M$ and $N$ commute on $\beta$ (i.e., $m \cdot (n \cdot y) = n \cdot (m \cdot y)$ for all $m \in M$, $n \in N$, $y \in \beta$), then the scalar multiplications of $M$ and $N$ also commute on $\alpha$.

Function.Surjective.smulCommClass theorem

 [SMul M α] [SMul N α] [SMul M β] [SMul N β] [SMulCommClass M N α] {f : α → β} (hf : Surjective f)
  (h₁ : ∀ (c : M) x, f (c • x) = c • f x) (h₂ : ∀ (c : N) x, f (c • x) = c • f x) : SMulCommClass M N β

Full source

@[to_additive]
lemma Function.Surjective.smulCommClass [SMul M α] [SMul N α] [SMul M β] [SMul N β]
    [SMulCommClass M N α] {f : α → β} (hf : Surjective f) (h₁ : ∀ (c : M) x, f (c • x) = c • f x)
    (h₂ : ∀ (c : N) x, f (c • x) = c • f x) : SMulCommClass M N β where
  smul_comm c₁ c₂ := hf.forall.2 fun x ↦ by simp only [← h₁, ← h₂, smul_comm c₁ c₂ x]

Commutation of Scalar Actions via Surjective Map

Informal description

Let $M$ and $N$ be types with scalar multiplication actions on types $\alpha$ and $\beta$, and let $f : \alpha \to \beta$ be a surjective function. Suppose that for all $c \in M$ and $x \in \alpha$, $f(c \cdot x) = c \cdot f(x)$, and similarly for $N$. If the scalar multiplications of $M$ and $N$ commute on $\alpha$ (i.e., $m \cdot (n \cdot x) = n \cdot (m \cdot x)$ for all $m \in M$, $n \in N$, $x \in \alpha$), then the scalar multiplications of $M$ and $N$ also commute on $\beta$.

smulCommClass_self instance

(M α : Type*) [CommMonoid M] [MulAction M α] : SMulCommClass M M α

Full source

@[to_additive]
instance smulCommClass_self (M α : Type*) [CommMonoid M] [MulAction M α] : SMulCommClass M M α where
  smul_comm a a' b := by rw [← mul_smul, mul_comm, mul_smul]

Commutativity of Scalar Multiplication in Commutative Monoid Actions

Informal description

For any commutative monoid $M$ acting multiplicatively on a type $\alpha$, the scalar multiplication operations of $M$ on $\alpha$ commute with each other. That is, for all $m_1, m_2 \in M$ and $a \in \alpha$, we have $m_1 \cdot (m_2 \cdot a) = m_2 \cdot (m_1 \cdot a)$.

VAddAssocClass structure

(M N α : Type*) [VAdd M N] [VAdd N α] [VAdd M α]

Full source

/-- An instance of `VAddAssocClass M N α` states that the additive action of `M` on `α` is
determined by the additive actions of `M` on `N` and `N` on `α`. -/
class VAddAssocClass (M N α : Type*) [VAdd M N] [VAdd N α] [VAdd M α] : Prop where
  /-- Associativity of `+ᵥ` -/
  vadd_assoc : ∀ (x : M) (y : N) (z : α), (x +ᵥ y) +ᵥ z = x +ᵥ y +ᵥ z

Associative Additive Action Class

Informal description

The structure `VAddAssocClass M N α` asserts that the additive action of `M` on `α` is determined by the additive actions of `M` on `N` and `N` on `α`. In other words, for any `m : M`, `n : N`, and `a : α`, the action satisfies the associativity property `m +ᵥ (n +ᵥ a) = (m +ᵥ n) +ᵥ a`.

IsScalarTower structure

(M N α : Type*) [SMul M N] [SMul N α] [SMul M α]

Full source

/-- An instance of `IsScalarTower M N α` states that the multiplicative
action of `M` on `α` is determined by the multiplicative actions of `M` on `N`
and `N` on `α`. -/
@[to_additive]
class IsScalarTower (M N α : Type*) [SMul M N] [SMul N α] [SMul M α] : Prop where
  /-- Associativity of `•` -/
  smul_assoc : ∀ (x : M) (y : N) (z : α), (x • y) • z = x • y • z

Scalar Multiplication Tower Property

Informal description

The structure `IsScalarTower M N α` asserts that the scalar multiplication of `M` on `α` is determined by the scalar multiplication of `M` on `N` and `N` on `α`. In other words, for any $x \in M$, $y \in N$, and $z \in \alpha$, the equality $(x \cdot y) \cdot z = x \cdot (y \cdot z)$ holds, where $\cdot$ denotes the respective scalar multiplication operations.

smul_assoc theorem

 {M N} [SMul M N] [SMul N α] [SMul M α] [IsScalarTower M N α] (x : M) (y : N) (z : α) : (x • y) • z = x • y • z

Full source

@[to_additive (attr := simp)]
lemma smul_assoc {M N} [SMul M N] [SMul N α] [SMul M α] [IsScalarTower M N α] (x : M) (y : N)
    (z : α) : (x • y) • z = x • y • z := IsScalarTower.smul_assoc x y z

Associativity of Scalar Multiplication in a Scalar Tower

Informal description

For any elements $x \in M$, $y \in N$, and $z \in \alpha$ in a scalar tower structure where $M$ acts on $N$ and $N$ acts on $\alpha$, the scalar multiplications satisfy the associativity property $(x \cdot y) \cdot z = x \cdot (y \cdot z)$.

Semigroup.isScalarTower instance

[Semigroup α] : IsScalarTower α α α

Full source

@[to_additive]
instance Semigroup.isScalarTower [Semigroup α] : IsScalarTower α α α := ⟨mul_assoc⟩

Scalar Tower Property in Semigroups

Informal description

For any semigroup $\alpha$, the scalar multiplication operation on $\alpha$ forms a scalar tower. That is, for any elements $x, y, z \in \alpha$, the scalar multiplications satisfy the associativity property $(x \cdot y) \cdot z = x \cdot (y \cdot z)$.

IsCentralVAdd structure

(M α : Type*) [VAdd M α] [VAdd Mᵃᵒᵖ α]

Full source

/-- A typeclass indicating that the right (aka `AddOpposite`) and left actions by `M` on `α` are
equal, that is that `M` acts centrally on `α`. This can be thought of as a version of commutativity
for `+ᵥ`. -/
class IsCentralVAdd (M α : Type*) [VAdd M α] [VAdd Mᵃᵒᵖ α] : Prop where
  /-- The right and left actions of `M` on `α` are equal. -/
  op_vadd_eq_vadd : ∀ (m : M) (a : α), AddOpposite.opAddOpposite.op m +ᵥ a = m +ᵥ a

Central Additive Action

Informal description

The structure `IsCentralVAdd M α` indicates that the right (via the additive opposite `Mᵃᵒᵖ`) and left actions of `M` on `α` are equal. This can be viewed as a form of commutativity for the additive action `+ᵥ`.

IsCentralScalar structure

(M α : Type*) [SMul M α] [SMul Mᵐᵒᵖ α]

Full source

/-- A typeclass indicating that the right (aka `MulOpposite`) and left actions by `M` on `α` are
equal, that is that `M` acts centrally on `α`. This can be thought of as a version of commutativity
for `•`. -/
@[to_additive]
class IsCentralScalar (M α : Type*) [SMul M α] [SMul Mᵐᵒᵖ α] : Prop where
  /-- The right and left actions of `M` on `α` are equal. -/
  op_smul_eq_smul : ∀ (m : M) (a : α), MulOpposite.op m • a = m • a

Central scalar action

Informal description

The structure `IsCentralScalar M α` indicates that the right (via the multiplicative opposite `Mᵐᵒᵖ`) and left actions of `M` on `α` are equal. This can be viewed as a form of commutativity for the scalar multiplication `•`.

IsCentralScalar.unop_smul_eq_smul theorem

 {M α : Type*} [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] (m : Mᵐᵒᵖ) (a : α) : MulOpposite.unop m • a = m • a

Full source

@[to_additive]
lemma IsCentralScalar.unop_smul_eq_smul {M α : Type*} [SMul M α] [SMul Mᵐᵒᵖ α]
    [IsCentralScalar M α] (m : Mᵐᵒᵖ) (a : α) : MulOpposite.unop m • a = m • a := by
  induction m; exact (IsCentralScalar.op_smul_eq_smul _ a).symm

Equality of Opposite and Original Scalar Multiplication in Central Scalar Action

Informal description

For a type $M$ with a scalar multiplication action on a type $\alpha$, and with an instance of `IsCentralScalar M α`, the scalar multiplication by an element $m$ in the multiplicative opposite $M^\text{op}$ is equal to the scalar multiplication by the original element $\text{unop}(m) \in M$. That is, for any $m \in M^\text{op}$ and $a \in \alpha$, we have $\text{unop}(m) \cdot a = m \cdot a$.

SMulCommClass.op_left instance

 [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] [SMul N α] [SMulCommClass M N α] : SMulCommClass Mᵐᵒᵖ N α

Full source

@[to_additive]
instance (priority := 50) SMulCommClass.op_left [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α]
    [SMul N α] [SMulCommClass M N α] : SMulCommClass Mᵐᵒᵖ N α :=
  ⟨fun m n a ↦ by rw [← unop_smul_eq_smul m (n • a), ← unop_smul_eq_smul m a, smul_comm]⟩

Commutativity of Scalar Actions with Multiplicative Opposite

Informal description

For a type $M$ with a scalar multiplication action on a type $\alpha$, where the actions of $M$ and its multiplicative opposite $M^\text{op}$ on $\alpha$ coincide (i.e., $M$ has a central scalar action on $\alpha$), and for another type $N$ with a scalar multiplication action on $\alpha$ such that the actions of $M$ and $N$ on $\alpha$ commute, the actions of $M^\text{op}$ and $N$ on $\alpha$ also commute.

SMulCommClass.op_right instance

 [SMul M α] [SMul N α] [SMul Nᵐᵒᵖ α] [IsCentralScalar N α] [SMulCommClass M N α] : SMulCommClass M Nᵐᵒᵖ α

Full source

@[to_additive]
instance (priority := 50) SMulCommClass.op_right [SMul M α] [SMul N α] [SMul Nᵐᵒᵖ α]
    [IsCentralScalar N α] [SMulCommClass M N α] : SMulCommClass M Nᵐᵒᵖ α :=
  ⟨fun m n a ↦ by rw [← unop_smul_eq_smul n (m • a), ← unop_smul_eq_smul n a, smul_comm]⟩

Commutation of Scalar Multiplication with Multiplicative Opposite Action

Informal description

For types $M$, $N$, and $\alpha$ with scalar multiplication actions, if the scalar multiplications by $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$, $a \in \alpha$), and if the scalar multiplication by $N$ on $\alpha$ is central (i.e., the right and left actions of $N$ on $\alpha$ coincide), then the scalar multiplications by $M$ and the multiplicative opposite $N^\text{op}$ on $\alpha$ also commute.

IsScalarTower.op_left instance

 [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] [SMul M N] [SMul Mᵐᵒᵖ N] [IsCentralScalar M N] [SMul N α]
  [IsScalarTower M N α] : IsScalarTower Mᵐᵒᵖ N α

Full source

@[to_additive]
instance (priority := 50) IsScalarTower.op_left [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α]
    [SMul M N] [SMul Mᵐᵒᵖ N] [IsCentralScalar M N] [SMul N α] [IsScalarTower M N α] :
    IsScalarTower Mᵐᵒᵖ N α where
  smul_assoc m n a := by rw [← unop_smul_eq_smul m (n • a), ← unop_smul_eq_smul m n, smul_assoc]

Scalar Tower Property for Multiplicative Opposite Action

Informal description

For types $M$, $N$, and $\alpha$ with scalar multiplication actions, if $M$ acts centrally on both $N$ and $\alpha$, and there is a scalar tower property for $M$, $N$, and $\alpha$, then the multiplicative opposite $M^\text{op}$ also forms a scalar tower with $N$ and $\alpha$. Specifically, for any $m \in M^\text{op}$, $n \in N$, and $a \in \alpha$, the equality $(m \cdot n) \cdot a = m \cdot (n \cdot a)$ holds, where $\cdot$ denotes the respective scalar multiplication operations.

IsScalarTower.op_right instance

 [SMul M α] [SMul M N] [SMul N α] [SMul Nᵐᵒᵖ α] [IsCentralScalar N α] [IsScalarTower M N α] : IsScalarTower M Nᵐᵒᵖ α

Full source

@[to_additive]
instance (priority := 50) IsScalarTower.op_right [SMul M α] [SMul M N] [SMul N α]
    [SMul Nᵐᵒᵖ α] [IsCentralScalar N α] [IsScalarTower M N α] : IsScalarTower M Nᵐᵒᵖ α where
  smul_assoc m n a := by
    rw [← unop_smul_eq_smul n a, ← unop_smul_eq_smul (m • n) a, MulOpposite.unop_smul, smul_assoc]

Scalar Tower Property with Multiplicative Opposite

Informal description

For types $M$, $N$, and $\alpha$ with scalar multiplication operations $M$ on $N$, $N$ on $\alpha$, and $M$ on $\alpha$, if $N$ has a central scalar action on $\alpha$ and the scalar multiplications satisfy the tower property $(x \cdot y) \cdot z = x \cdot (y \cdot z)$ for all $x \in M$, $y \in N$, $z \in \alpha$, then the scalar multiplications also satisfy the tower property when $N$ is replaced by its multiplicative opposite $N^\text{op}$.

SMul.comp.smul definition

(g : N → M) (n : N) (a : α) : α

Full source

/-- Auxiliary definition for `SMul.comp`, `MulAction.compHom`,
`DistribMulAction.compHom`, `Module.compHom`, etc. -/
@[to_additive (attr := simp) " Auxiliary definition for `VAdd.comp`, `AddAction.compHom`, etc. "]
def comp.smul (g : N → M) (n : N) (a : α) : α := g n • a

Composition of scalar multiplication via a function

Informal description

Given a function $ g : N \to M $, an element $ n \in N $, and an element $ a \in \alpha $, the scalar multiplication $ n \bullet a $ is defined as $ g(n) \bullet a $, where the scalar multiplication on the right is the existing scalar multiplication of $ M $ on $ \alpha $.

SMul.comp abbrev

(g : N → M) : SMul N α

Full source

/-- An action of `M` on `α` and a function `N → M` induces an action of `N` on `α`. -/
-- See note [reducible non-instances]
-- Since this is reducible, we make sure to go via
-- `SMul.comp.smul` to prevent typeclass inference unfolding too far
@[to_additive
"An additive action of `M` on `α` and a function `N → M` induces an additive action of `N` on `α`."]
abbrev comp (g : N → M) : SMul N α where smul := SMul.comp.smul g

Induced Scalar Action via Function Composition

Informal description

Given a function $g : N \to M$, the composition of scalar multiplication defines a scalar multiplication action of $N$ on $\alpha$ via $n \bullet a = g(n) \bullet a$ for all $n \in N$ and $a \in \alpha$, where the right-hand side uses the existing scalar multiplication of $M$ on $\alpha$.

SMul.comp.isScalarTower theorem

 [SMul M β] [SMul α β] [IsScalarTower M α β] (g : N → M) : by haveI := comp α g; haveI := comp β g;
  exact IsScalarTower N α β

Full source

/-- Given a tower of scalar actions `M → α → β`, if we use `SMul.comp`
to pull back both of `M`'s actions by a map `g : N → M`, then we obtain a new
tower of scalar actions `N → α → β`.

This cannot be an instance because it can cause infinite loops whenever the `SMul` arguments
are still metavariables. -/
@[to_additive
"Given a tower of additive actions `M → α → β`, if we use `SMul.comp` to pull back both of
`M`'s actions by a map `g : N → M`, then we obtain a new tower of scalar actions `N → α → β`.

This cannot be an instance because it can cause infinite loops whenever the `SMul` arguments
are still metavariables."]
lemma comp.isScalarTower [SMul M β] [SMul α β] [IsScalarTower M α β] (g : N → M) : by
    haveI := comp α g; haveI := comp β g; exact IsScalarTower N α β where
  __ := comp α g
  __ := comp β g
  smul_assoc n := smul_assoc (g n)

Induced Scalar Tower Property via Function Composition

Informal description

Given types $M$, $N$, $\alpha$, and $\beta$ with scalar multiplication actions: - $M$ acts on $\beta$ - $\alpha$ acts on $\beta$ - The actions form a scalar tower $M \to \alpha \to \beta$ (i.e., $(m \cdot a) \cdot b = m \cdot (a \cdot b)$ for all $m \in M$, $a \in \alpha$, $b \in \beta$) For any function $g : N \to M$, the induced scalar actions of $N$ on $\alpha$ and $\beta$ via $g$ (defined by $n \cdot a := g(n) \cdot a$ and $n \cdot b := g(n) \cdot b$) form a scalar tower $N \to \alpha \to \beta$.

SMul.comp.smulCommClass theorem

 [SMul β α] [SMulCommClass M β α] (g : N → M) :
  haveI := comp α g
  SMulCommClass N β α

Full source

/-- This cannot be an instance because it can cause infinite loops whenever the `SMul` arguments
are still metavariables. -/
@[to_additive
"This cannot be an instance because it can cause infinite loops whenever the `VAdd` arguments
are still metavariables."]
lemma comp.smulCommClass [SMul β α] [SMulCommClass M β α] (g : N → M) :
    haveI := comp α g
    SMulCommClass N β α where
  __ := comp α g
  smul_comm n := smul_comm (g n)

Induced Commuting Scalar Actions via Function Composition

Informal description

Let $\alpha$ and $\beta$ be types equipped with scalar multiplication actions by $M$ and $\beta$ respectively, such that the actions of $M$ and $\beta$ on $\alpha$ commute (i.e., $m \cdot (b \cdot a) = b \cdot (m \cdot a)$ for all $m \in M$, $b \in \beta$, $a \in \alpha$). Given a function $g : N \to M$, the induced scalar multiplication of $N$ on $\alpha$ via $g$ makes the actions of $N$ and $\beta$ on $\alpha$ commute as well. That is, for all $n \in N$, $b \in \beta$, and $a \in \alpha$, we have $n \cdot (b \cdot a) = b \cdot (n \cdot a)$, where $n \cdot a := g(n) \cdot a$.

SMul.comp.smulCommClass' theorem

 [SMul β α] [SMulCommClass β M α] (g : N → M) :
  haveI := comp α g
  SMulCommClass β N α

Full source

/-- This cannot be an instance because it can cause infinite loops whenever the `SMul` arguments
are still metavariables. -/
@[to_additive
"This cannot be an instance because it can cause infinite loops whenever the `VAdd` arguments
are still metavariables."]
lemma comp.smulCommClass' [SMul β α] [SMulCommClass β M α] (g : N → M) :
    haveI := comp α g
    SMulCommClass β N α where
  __ := comp α g
  smul_comm _ n := smul_comm _ (g n)

Commutativity of Induced Scalar Actions: $\beta$ and $N$ Commute on $\alpha$ via $g$

Informal description

Let $\alpha$ and $\beta$ be types equipped with scalar multiplication actions by $\beta$ and $M$ respectively, such that the actions of $\beta$ and $M$ on $\alpha$ commute (i.e., $b \cdot (m \cdot a) = m \cdot (b \cdot a)$ for all $b \in \beta$, $m \in M$, $a \in \alpha$). Given a function $g : N \to M$, the induced scalar multiplication of $N$ on $\alpha$ via $g$ makes the actions of $\beta$ and $N$ on $\alpha$ commute as well. That is, for all $b \in \beta$, $n \in N$, and $a \in \alpha$, we have $b \cdot (n \cdot a) = n \cdot (b \cdot a)$, where $n \cdot a := g(n) \cdot a$.

mul_smul_comm theorem

[Mul β] [SMul α β] [SMulCommClass α β β] (s : α) (x y : β) : x * s • y = s • (x * y)

Full source

/-- Note that the `SMulCommClass α β β` typeclass argument is usually satisfied by `Algebra α β`. -/
@[to_additive]
lemma mul_smul_comm [Mul β] [SMul α β] [SMulCommClass α β β] (s : α) (x y : β) :
    x * s • y = s • (x * y) := (smul_comm s x y).symm

Commutativity of Multiplication and Scalar Multiplication: $x \cdot (s \cdot y) = s \cdot (x \cdot y)$

Informal description

Let $\beta$ be a type with a multiplication operation and $\alpha$ a type with a scalar multiplication action on $\beta$. If the scalar multiplications by $\alpha$ and $\beta$ on $\beta$ commute (i.e., $a \cdot (b \cdot c) = b \cdot (a \cdot c)$ for all $a \in \alpha$, $b, c \in \beta$), then for any $s \in \alpha$ and $x, y \in \beta$, we have the identity: $$ x \cdot (s \cdot y) = s \cdot (x \cdot y). $$

smul_mul_assoc theorem

[Mul β] [SMul α β] [IsScalarTower α β β] (r : α) (x y : β) : r • x * y = r • (x * y)

Full source

/-- Note that the `IsScalarTower α β β` typeclass argument is usually satisfied by `Algebra α β`. -/
@[to_additive]
lemma smul_mul_assoc [Mul β] [SMul α β] [IsScalarTower α β β] (r : α) (x y : β) :
    r • x * y = r • (x * y) := smul_assoc r x y

Associativity of Scalar Multiplication and Multiplication: $r \cdot (x * y) = (r \cdot x) * y$

Informal description

Let $\beta$ be a type with a multiplication operation and $\alpha$ a type with a scalar multiplication action on $\beta$. If the scalar multiplication satisfies the tower property `IsScalarTower α β β`, then for any $r \in \alpha$ and $x, y \in \beta$, we have: $$ r \cdot (x * y) = (r \cdot x) * y. $$

smul_div_assoc theorem

[DivInvMonoid β] [SMul α β] [IsScalarTower α β β] (r : α) (x y : β) : r • x / y = r • (x / y)

Full source

/-- Note that the `IsScalarTower α β β` typeclass argument is usually satisfied by `Algebra α β`. -/
@[to_additive]
lemma smul_div_assoc [DivInvMonoid β] [SMul α β] [IsScalarTower α β β] (r : α) (x y : β) :
    r • x / y = r • (x / y) := by simp [div_eq_mul_inv, smul_mul_assoc]

Scalar Multiplication Distributes Over Division: $r \cdot (x / y) = (r \cdot x) / y$

Informal description

Let $\beta$ be a division-inversion monoid with a scalar multiplication action by $\alpha$ satisfying the scalar tower property `IsScalarTower α β β`. Then for any $r \in \alpha$ and $x, y \in \beta$, we have: $$ r \cdot (x / y) = (r \cdot x) / y. $$

smul_smul_smul_comm theorem

 [SMul α β] [SMul α γ] [SMul β δ] [SMul α δ] [SMul γ δ] [IsScalarTower α β δ] [IsScalarTower α γ δ]
  [SMulCommClass β γ δ] (a : α) (b : β) (c : γ) (d : δ) : (a • b) • c • d = (a • c) • b • d

Full source

@[to_additive]
lemma smul_smul_smul_comm [SMul α β] [SMul α γ] [SMul β δ] [SMul α δ] [SMul γ δ]
    [IsScalarTower α β δ] [IsScalarTower α γ δ] [SMulCommClass β γ δ] (a : α) (b : β) (c : γ)
    (d : δ) : (a • b) • c • d = (a • c) • b • d := by rw [smul_assoc, smul_assoc, smul_comm b]

Commutativity of Iterated Scalar Multiplications in a Scalar Tower

Informal description

Let $\alpha$, $\beta$, $\gamma$, and $\delta$ be types equipped with scalar multiplication operations such that: - $\alpha$ acts on $\beta$, $\gamma$, and $\delta$, - $\beta$ and $\gamma$ act on $\delta$, - The scalar multiplications satisfy the tower properties `IsScalarTower α β δ` and `IsScalarTower α γ δ`, - The scalar multiplications of $\beta$ and $\gamma$ on $\delta$ commute (`SMulCommClass β γ δ`). Then for any elements $a \in \alpha$, $b \in \beta$, $c \in \gamma$, and $d \in \delta$, the following equality holds: $$(a \cdot b) \cdot (c \cdot d) = (a \cdot c) \cdot (b \cdot d).$$

smul_mul_smul_comm theorem

 [Mul α] [Mul β] [SMul α β] [IsScalarTower α β β] [IsScalarTower α α β] [SMulCommClass α β β] (a : α) (b : β) (c : α)
  (d : β) : (a • b) * (c • d) = (a * c) • (b * d)

Full source

/-- Note that the `IsScalarTower α β β` and `SMulCommClass α β β` typeclass arguments are usually
satisfied by `Algebra α β`. -/
@[to_additive]
lemma smul_mul_smul_comm [Mul α] [Mul β] [SMul α β] [IsScalarTower α β β]
    [IsScalarTower α α β] [SMulCommClass α β β] (a : α) (b : β) (c : α) (d : β) :
    (a • b) * (c • d) = (a * c) • (b * d) := by
  have : SMulCommClass β α β := .symm ..; exact smul_smul_smul_comm a b c d

Commutativity of Mixed Scalar and Multiplicative Operations: $(a \cdot b) * (c \cdot d) = (a * c) \cdot (b * d)$

Informal description

Let $\alpha$ and $\beta$ be types equipped with multiplication operations and a scalar multiplication of $\alpha$ on $\beta$. Assume that: 1. The scalar multiplication satisfies the tower properties `IsScalarTower α β β` and `IsScalarTower α α β`, 2. The scalar multiplication of $\alpha$ on $\beta$ commutes with itself (`SMulCommClass α β β`). Then for any elements $a, c \in \alpha$ and $b, d \in \beta$, the following equality holds: $$(a \cdot b) * (c \cdot d) = (a * c) \cdot (b * d),$$ where $*$ denotes multiplication in $\alpha$ and $\beta$, and $\cdot$ denotes scalar multiplication of $\alpha$ on $\beta$.

mul_smul_mul_comm theorem

 [Mul α] [Mul β] [SMul α β] [IsScalarTower α β β] [IsScalarTower α α β] [SMulCommClass α β β] (a b : α) (c d : β) :
  (a * b) • (c * d) = (a • c) * (b • d)

Full source

/-- Note that the `IsScalarTower α β β` and `SMulCommClass α β β` typeclass arguments are usually
satisfied by `Algebra α β`. -/
@[to_additive]
lemma mul_smul_mul_comm [Mul α] [Mul β] [SMul α β] [IsScalarTower α β β]
    [IsScalarTower α α β] [SMulCommClass α β β] (a b : α) (c d : β) :
    (a * b) • (c * d) = (a • c) * (b • d) := smul_smul_smul_comm a b c d

Commutativity of Mixed Multiplication and Scalar Multiplication: $(a * b) \cdot (c * d) = (a \cdot c) * (b \cdot d)$

Informal description

Let $\alpha$ and $\beta$ be types equipped with multiplication operations and a scalar multiplication of $\alpha$ on $\beta$. Assume that: 1. The scalar multiplication satisfies the tower properties `IsScalarTower α β β` and `IsScalarTower α α β`, 2. The scalar multiplication of $\alpha$ on $\beta$ commutes with itself (`SMulCommClass α β β`). Then for any elements $a, b \in \alpha$ and $c, d \in \beta$, the following equality holds: $$(a * b) \cdot (c * d) = (a \cdot c) * (b \cdot d),$$ where $*$ denotes multiplication in $\alpha$ and $\beta$, and $\cdot$ denotes scalar multiplication of $\alpha$ on $\beta$.

Commute.smul_right theorem

[Mul α] [SMulCommClass M α α] [IsScalarTower M α α] {a b : α} (h : Commute a b) (r : M) : Commute a (r • b)

Full source

@[to_additive]
lemma Commute.smul_right [Mul α] [SMulCommClass M α α] [IsScalarTower M α α] {a b : α}
    (h : Commute a b) (r : M) : Commute a (r • b) :=
  (mul_smul_comm _ _ _).trans ((congr_arg _ h).trans <| (smul_mul_assoc _ _ _).symm)

Scalar Multiplication Preserves Commutativity on the Right: $a * (r \cdot b) = (r \cdot b) * a$

Informal description

Let $\alpha$ be a type with a multiplication operation and $M$ a type with a scalar multiplication action on $\alpha$. Assume that: 1. The scalar multiplications by $M$ and $\alpha$ on $\alpha$ commute (`SMulCommClass M \alpha \alpha`), 2. The scalar multiplication satisfies the tower property `IsScalarTower M \alpha \alpha`. If two elements $a, b \in \alpha$ commute (i.e., $a * b = b * a$), then for any scalar $r \in M$, the elements $a$ and $r \cdot b$ also commute, i.e., $a * (r \cdot b) = (r \cdot b) * a$.

Commute.smul_left theorem

[Mul α] [SMulCommClass M α α] [IsScalarTower M α α] {a b : α} (h : Commute a b) (r : M) : Commute (r • a) b

Full source

@[to_additive]
lemma Commute.smul_left [Mul α] [SMulCommClass M α α] [IsScalarTower M α α] {a b : α}
    (h : Commute a b) (r : M) : Commute (r • a) b := (h.symm.smul_right r).symm

Scalar Multiplication Preserves Commutativity on the Left: $(r \cdot a) * b = b * (r \cdot a)$

Informal description

Let $\alpha$ be a type with a multiplication operation and $M$ a type with a scalar multiplication action on $\alpha$. Assume that: 1. The scalar multiplications by $M$ and $\alpha$ on $\alpha$ commute (`SMulCommClass M \alpha \alpha`), 2. The scalar multiplication satisfies the tower property `IsScalarTower M \alpha \alpha`. If two elements $a, b \in \alpha$ commute (i.e., $a * b = b * a$), then for any scalar $r \in M$, the elements $r \cdot a$ and $b$ also commute, i.e., $(r \cdot a) * b = b * (r \cdot a)$.

smul_smul theorem

(a₁ a₂ : M) (b : α) : a₁ • a₂ • b = (a₁ * a₂) • b

Full source

@[to_additive]
lemma smul_smul (a₁ a₂ : M) (b : α) : a₁ • a₂ • b = (a₁ * a₂) • b := (mul_smul _ _ _).symm

Associativity of Scalar Multiplication: $(a_1 \cdot a_2) \cdot b = a_1 \cdot (a_2 \cdot b)$

Informal description

For any elements $a_1, a_2$ of a monoid $M$ and any element $b$ of a type $\alpha$ with a multiplicative action of $M$, the scalar multiplication satisfies the associativity property $(a_1 \cdot a_2) \cdot b = a_1 \cdot (a_2 \cdot b)$, where $\cdot$ denotes both the monoid multiplication in $M$ and the scalar multiplication action on $\alpha$.

one_smul theorem

(b : α) : (1 : M) • b = b

Full source

@[to_additive (attr := simp)]
lemma one_smul (b : α) : (1 : M) • b = b := MulAction.one_smul _

Identity Action Property: $1 \cdot b = b$

Informal description

For any element $b$ in a type $\alpha$ with a multiplicative action by a monoid $M$, the action of the multiplicative identity $1 \in M$ on $b$ is equal to $b$, i.e., $1 \cdot b = b$.

one_smul_eq_id theorem

: (((1 : M) • ·) : α → α) = id

Full source

/-- `SMul` version of `one_mul_eq_id` -/
@[to_additive "`VAdd` version of `zero_add_eq_id`"]
lemma one_smul_eq_id : (((1 : M) • ·) : α → α) = id := funext <| one_smul _

Identity Scalar Multiplication Equals Identity Function

Informal description

The scalar multiplication by the multiplicative identity $1 \in M$ is equal to the identity function on $\alpha$, i.e., $(1 \cdot \cdot) = \text{id}$.

comp_smul_left theorem

(a₁ a₂ : M) : (a₁ • ·) ∘ (a₂ • ·) = (((a₁ * a₂) • ·) : α → α)

Full source

/-- `SMul` version of `comp_mul_left` -/
@[to_additive "`VAdd` version of `comp_add_left`"]
lemma comp_smul_left (a₁ a₂ : M) : (a₁ • ·) ∘ (a₂ • ·) = (((a₁ * a₂) • ·) : α → α) :=
  funext fun _ ↦ (mul_smul _ _ _).symm

Composition of Scalar Multiplications Equals Product Scalar Multiplication

Informal description

For any elements $a_1, a_2$ in a monoid $M$ acting on a type $\alpha$, the composition of the scalar multiplication functions $(a_1 \cdot \cdot) \circ (a_2 \cdot \cdot)$ is equal to the scalar multiplication function by the product $a_1 a_2$, i.e., $(a_1 a_2 \cdot \cdot)$.

smul_iterate theorem

(a : M) : ∀ n : ℕ, (a • · : α → α)^[n] = (a ^ n • ·)

Full source

@[to_additive (attr := simp)]
theorem smul_iterate (a : M) : ∀ n : ℕ, (a • · : α → α)^[n] = (a ^ n • ·)
  | 0 => by simp [funext_iff]
  | n + 1 => by ext; simp [smul_iterate, pow_succ, smul_smul]

Iterated Scalar Multiplication Equals Power Scalar Multiplication: $(a \cdot \cdot)^n = (a^n \cdot \cdot)$

Informal description

For any element $a$ in a monoid $M$ acting on a type $\alpha$, the $n$-th iterate of the scalar multiplication function $(a \cdot \cdot) : \alpha \to \alpha$ is equal to the scalar multiplication function by $a^n$ for all natural numbers $n$, i.e., $(a \cdot \cdot)^n = (a^n \cdot \cdot)$.

smul_iterate_apply theorem

(a : M) (n : ℕ) (x : α) : (a • ·)^[n] x = a ^ n • x

Full source

@[to_additive]
lemma smul_iterate_apply (a : M) (n : ℕ) (x : α) : (a • ·)^[n] x = a ^ n • x := by
  rw [smul_iterate]

Iterated Scalar Multiplication Formula: $(a \cdot \cdot)^n(x) = a^n \cdot x$

Informal description

For any element $a$ in a monoid $M$ acting on a type $\alpha$, any natural number $n$, and any element $x \in \alpha$, the $n$-th iterate of the scalar multiplication function $(a \cdot \cdot)$ applied to $x$ equals the scalar multiplication of $a^n$ with $x$, i.e., $(a \cdot \cdot)^n(x) = a^n \cdot x$.

Function.Injective.mulAction abbrev

[SMul M β] (f : β → α) (hf : Injective f) (smul : ∀ (c : M) (x), f (c • x) = c • f x) : MulAction M β

Full source

/-- Pullback a multiplicative action along an injective map respecting `•`.
See note [reducible non-instances]. -/
@[to_additive
    "Pullback an additive action along an injective map respecting `+ᵥ`."]
protected abbrev Function.Injective.mulAction [SMul M β] (f : β → α) (hf : Injective f)
    (smul : ∀ (c : M) (x), f (c • x) = c • f x) : MulAction M β where
  smul := (· • ·)
  one_smul x := hf <| (smul _ _).trans <| one_smul _ (f x)
  mul_smul c₁ c₂ x := hf <| by simp only [smul, mul_smul]

Injective Pullback of Multiplicative Action

Informal description

Given a monoid $M$ acting on a type $\alpha$ via scalar multiplication, and an injective function $f : \beta \to \alpha$ that preserves the scalar multiplication (i.e., $f(c \cdot x) = c \cdot f(x)$ for all $c \in M$ and $x \in \beta$), then $\beta$ inherits a multiplicative action of $M$ via $f$.

Function.Surjective.mulAction abbrev

[SMul M β] (f : α → β) (hf : Surjective f) (smul : ∀ (c : M) (x), f (c • x) = c • f x) : MulAction M β

Full source

/-- Pushforward a multiplicative action along a surjective map respecting `•`.
See note [reducible non-instances]. -/
@[to_additive
    "Pushforward an additive action along a surjective map respecting `+ᵥ`."]
protected abbrev Function.Surjective.mulAction [SMul M β] (f : α → β) (hf : Surjective f)
    (smul : ∀ (c : M) (x), f (c • x) = c • f x) : MulAction M β where
  smul := (· • ·)
  one_smul := by simp [hf.forall, ← smul]
  mul_smul := by simp [hf.forall, ← smul, mul_smul]

Pushforward of Multiplicative Action Along a Surjective Map

Informal description

Given a monoid $M$ acting on a type $\alpha$ via scalar multiplication $\cdot$, and a surjective function $f \colon \alpha \to \beta$ such that $f(c \cdot x) = c \cdot f(x)$ for all $c \in M$ and $x \in \alpha$, then $\beta$ inherits a multiplicative action of $M$ defined by $c \cdot b := f(c \cdot a)$ where $a$ is any element of $\alpha$ such that $f(a) = b$.

Monoid.toMulAction instance

: MulAction M M

Full source

/-- The regular action of a monoid on itself by left multiplication.

This is promoted to a module by `Semiring.toModule`. -/
-- see Note [lower instance priority]
@[to_additive
"The regular action of a monoid on itself by left addition.

This is promoted to an `AddTorsor` by `addGroup_is_addTorsor`."]
instance (priority := 910) Monoid.toMulAction : MulAction M M where
  smul := (· * ·)
  one_smul := one_mul
  mul_smul := mul_assoc

Left Multiplication Action of a Monoid on Itself

Informal description

Every monoid $M$ acts on itself by left multiplication, where the action is defined by $a \cdot b = a * b$ for $a, b \in M$.

IsScalarTower.left instance

: IsScalarTower M M α

Full source

@[to_additive]
instance IsScalarTower.left : IsScalarTower M M α where
  smul_assoc x y z := mul_smul x y z

Scalar Multiplication Tower Property for a Monoid Acting on Itself

Informal description

For any monoid $M$ acting on a type $\alpha$, the scalar multiplication of $M$ on $\alpha$ satisfies the tower property with respect to itself. That is, for any $x, y \in M$ and $z \in \alpha$, we have $(x \cdot y) \cdot z = x \cdot (y \cdot z)$.

smul_pow theorem

(r : M) (x : N) : ∀ n, (r • x) ^ n = r ^ n • x ^ n

Full source

lemma smul_pow (r : M) (x : N) : ∀ n, (r • x) ^ n = r ^ n • x ^ n
  | 0 => by simp
  | n + 1 => by rw [pow_succ', smul_pow _ _ n, smul_mul_smul_comm, ← pow_succ', ← pow_succ']

Power of Scalar Multiple: $(r \cdot x)^n = r^n \cdot x^n$

Informal description

Let $M$ be a monoid acting on a type $N$ via scalar multiplication, and let $N$ be equipped with a multiplication operation. For any $r \in M$, $x \in N$, and any natural number $n$, the $n$-th power of the scalar multiple $r \cdot x$ is equal to the scalar multiple of the $n$-th powers of $r$ and $x$, i.e., $(r \cdot x)^n = r^n \cdot x^n$.

inv_smul_smul theorem

(g : G) (a : α) : g⁻¹ • g • a = a

Full source

@[to_additive (attr := simp)]
lemma inv_smul_smul (g : G) (a : α) : g⁻¹ • g • a = a := by rw [smul_smul, inv_mul_cancel, one_smul]

Inverse Action Cancellation: $g^{-1} \cdot (g \cdot a) = a$

Informal description

For any element $g$ in a group $G$ acting on a type $\alpha$, and any element $a \in \alpha$, the action of the inverse $g^{-1}$ followed by the action of $g$ on $a$ returns $a$, i.e., $g^{-1} \cdot (g \cdot a) = a$.

smul_inv_smul theorem

(g : G) (a : α) : g • g⁻¹ • a = a

Full source

@[to_additive (attr := simp)]
lemma smul_inv_smul (g : G) (a : α) : g • g⁻¹ • a = a := by rw [smul_smul, mul_inv_cancel, one_smul]

Inverse Action Cancellation: $g \cdot (g^{-1} \cdot a) = a$

Informal description

For any element $g$ in a group $G$ acting on a type $\alpha$, and any element $a \in \alpha$, the action of $g$ followed by the action of its inverse $g^{-1}$ on $a$ returns $a$, i.e., $g \cdot (g^{-1} \cdot a) = a$.

inv_smul_eq_iff theorem

: g⁻¹ • a = b ↔ a = g • b

Full source

@[to_additive] lemma inv_smul_eq_iff : g⁻¹g⁻¹ • a = b ↔ a = g • b :=
  ⟨fun h ↦ by rw [← h, smul_inv_smul], fun h ↦ by rw [h, inv_smul_smul]⟩

Inverse Action Equivalence: $g^{-1} \cdot a = b \leftrightarrow a = g \cdot b$

Informal description

For any element $g$ in a group $G$ acting on a type $\alpha$, and any elements $a, b \in \alpha$, the action of the inverse $g^{-1}$ on $a$ equals $b$ if and only if $a$ equals the action of $g$ on $b$, i.e., $g^{-1} \cdot a = b \leftrightarrow a = g \cdot b$.

Commute.smul_right_iff theorem

: Commute a (g • b) ↔ Commute a b

Full source

@[simp] lemma Commute.smul_right_iff : CommuteCommute a (g • b) ↔ Commute a b :=
  ⟨fun h ↦ inv_smul_smul g b ▸ h.smul_right g⁻¹, fun h ↦ h.smul_right g⟩

Scalar Multiplication Preserves Commutativity: $a \cdot (g \cdot b) = (g \cdot b) \cdot a \leftrightarrow a \cdot b = b \cdot a$

Informal description

For elements $a, b$ in a multiplicative structure $\alpha$ and a scalar $g$ from a group $G$ acting on $\alpha$, the elements $a$ and $g \cdot b$ commute if and only if $a$ and $b$ commute, i.e., $a * (g \cdot b) = (g \cdot b) * a \leftrightarrow a * b = b * a$.

Commute.smul_left_iff theorem

: Commute (g • a) b ↔ Commute a b

Full source

@[simp] lemma Commute.smul_left_iff : CommuteCommute (g • a) b ↔ Commute a b := by
  rw [Commute.symm_iff, Commute.smul_right_iff, Commute.symm_iff]

Scalar Multiplication Preserves Commutativity: $(g \cdot a) \cdot b = b \cdot (g \cdot a) \leftrightarrow a \cdot b = b \cdot a$

Informal description

For elements $a, b$ in a multiplicative structure $\alpha$ and a scalar $g$ from a group $G$ acting on $\alpha$, the elements $g \cdot a$ and $b$ commute if and only if $a$ and $b$ commute, i.e., $(g \cdot a) * b = b * (g \cdot a) \leftrightarrow a * b = b * a$.

smul_inv theorem

(g : G) (a : H) : (g • a)⁻¹ = g⁻¹ • a⁻¹

Full source

lemma smul_inv (g : G) (a : H) : (g • a)⁻¹ = g⁻¹ • a⁻¹ :=
  inv_eq_of_mul_eq_one_right <| by rw [smul_mul_smul_comm, mul_inv_cancel, mul_inv_cancel, one_smul]

Inverse of Scalar Multiplication: $(g \cdot a)^{-1} = g^{-1} \cdot a^{-1}$

Informal description

Let $G$ be a group acting on another group $H$ via scalar multiplication. For any elements $g \in G$ and $a \in H$, the inverse of the scalar multiplication $g \cdot a$ is equal to the scalar multiplication of the inverse of $g$ with the inverse of $a$, i.e., $(g \cdot a)^{-1} = g^{-1} \cdot a^{-1}$.

smul_zpow theorem

(g : G) (a : H) (n : ℤ) : (g • a) ^ n = g ^ n • a ^ n

Full source

lemma smul_zpow (g : G) (a : H) (n : ℤ) : (g • a) ^ n = g ^ n • a ^ n := by
  cases n <;> simp [smul_pow, smul_inv]

Integer Power of Scalar Multiplication: $(g \cdot a)^n = g^n \cdot a^n$

Informal description

Let $G$ be a group acting on another group $H$ via scalar multiplication. For any elements $g \in G$, $a \in H$, and any integer $n \in \mathbb{Z}$, the $n$-th integer power of the scalar multiplication $g \cdot a$ is equal to the scalar multiplication of the $n$-th power of $g$ with the $n$-th power of $a$, i.e., $(g \cdot a)^n = g^n \cdot a^n$.

SMulCommClass.of_commMonoid theorem

(A B G : Type*) [CommMonoid G] [SMul A G] [SMul B G] [IsScalarTower A G G] [IsScalarTower B G G] : SMulCommClass A B G

Full source

lemma SMulCommClass.of_commMonoid
    (A B G : Type*) [CommMonoid G] [SMul A G] [SMul B G]
    [IsScalarTower A G G] [IsScalarTower B G G] :
    SMulCommClass A B G where
  smul_comm r s x := by
    rw [← one_smul G (s • x), ← smul_assoc, ← one_smul G x, ← smul_assoc s 1 x,
      smul_comm, smul_assoc, one_smul, smul_assoc, one_smul]

Commutativity of Scalar Actions in a Commutative Monoid under Scalar Tower Conditions

Informal description

Let $A$, $B$, and $G$ be types, where $G$ is a commutative monoid. Suppose there are scalar multiplication actions of $A$ on $G$ and $B$ on $G$, and that both actions satisfy the scalar tower property with respect to $G$ (i.e., $[IsScalarTower\, A\, G\, G]$ and $[IsScalarTower\, B\, G\, G]$). Then the scalar multiplications of $A$ and $B$ on $G$ commute, i.e., for all $a \in A$, $b \in B$, and $g \in G$, we have: $$ a \cdot (b \cdot g) = b \cdot (a \cdot g). $$

smul_one_smul theorem

 {M} (N) [Monoid N] [SMul M N] [MulAction N α] [SMul M α] [IsScalarTower M N α] (x : M) (y : α) :
  (x • (1 : N)) • y = x • y

Full source

@[to_additive]
lemma smul_one_smul {M} (N) [Monoid N] [SMul M N] [MulAction N α] [SMul M α]
    [IsScalarTower M N α] (x : M) (y : α) : (x • (1 : N)) • y = x • y := by
  rw [smul_assoc, one_smul]

Scalar multiplication identity action: $(x \cdot 1_N) \cdot y = x \cdot y$ under scalar tower condition

Informal description

Let $M$ and $N$ be monoids with a scalar multiplication action of $M$ on $N$, and let $\alpha$ be a type with a multiplicative action of $N$. Suppose there is a scalar tower structure `IsScalarTower M N α`. Then for any $x \in M$ and $y \in \alpha$, the following equality holds: $$(x \cdot 1_N) \cdot y = x \cdot y$$ where $1_N$ is the multiplicative identity in $N$ and $\cdot$ denotes the respective scalar multiplication operations.

smul_one_mul theorem

{M N} [MulOneClass N] [SMul M N] [IsScalarTower M N N] (x : M) (y : N) : x • (1 : N) * y = x • y

Full source

@[to_additive (attr := simp)]
lemma smul_one_mul {M N} [MulOneClass N] [SMul M N] [IsScalarTower M N N] (x : M) (y : N) :
    x • (1 : N) * y = x • y := by rw [smul_mul_assoc, one_mul]

Scalar multiplication identity: $x \cdot 1 * y = x \cdot y$ under scalar tower condition

Informal description

Let $M$ and $N$ be types where $N$ has a multiplicative structure with identity (`MulOneClass`), and suppose there is a scalar multiplication action of $M$ on $N$ that satisfies the scalar tower property (`IsScalarTower M N N`). Then for any $x \in M$ and $y \in N$, we have: $$ x \cdot (1_N) * y = x \cdot y $$ where $1_N$ denotes the multiplicative identity in $N$ and $\cdot$ denotes the scalar multiplication.

mul_smul_one theorem

{M N} [MulOneClass N] [SMul M N] [SMulCommClass M N N] (x : M) (y : N) : y * x • (1 : N) = x • y

Full source

@[to_additive (attr := simp)]
lemma mul_smul_one {M N} [MulOneClass N] [SMul M N] [SMulCommClass M N N] (x : M) (y : N) :
    y * x • (1 : N) = x • y := by rw [← smul_eq_mul, ← smul_comm, smul_eq_mul, mul_one]

Commutativity of scalar multiplication with identity: $y \cdot (x \cdot 1) = x \cdot y$

Informal description

Let $M$ and $N$ be types where $N$ has a multiplicative structure with identity (`MulOneClass`), and suppose the scalar multiplications by $M$ and $N$ on $N$ commute (`SMulCommClass M N N`). Then for any $x \in M$ and $y \in N$, we have: $$ y \cdot (x \cdot 1_N) = x \cdot y $$ where $1_N$ denotes the multiplicative identity in $N$ and $\cdot$ denotes scalar multiplication.

IsScalarTower.of_smul_one_mul theorem

{M N} [Monoid N] [SMul M N] (h : ∀ (x : M) (y : N), x • (1 : N) * y = x • y) : IsScalarTower M N N

Full source

@[to_additive]
lemma IsScalarTower.of_smul_one_mul {M N} [Monoid N] [SMul M N]
    (h : ∀ (x : M) (y : N), x • (1 : N) * y = x • y) : IsScalarTower M N N :=
  ⟨fun x y z ↦ by rw [← h, smul_eq_mul, mul_assoc, h, smul_eq_mul]⟩

Scalar Tower Condition from Identity Multiplication Property

Informal description

Let $M$ and $N$ be types where $N$ is a monoid, and suppose there is a scalar multiplication action of $M$ on $N$. If for all $x \in M$ and $y \in N$ the equality $x \cdot (1_N) * y = x \cdot y$ holds (where $1_N$ is the multiplicative identity in $N$ and $\cdot$ denotes scalar multiplication), then the scalar multiplication forms a scalar tower, i.e., $M$ acts on $N$ in a way compatible with $N$'s multiplication.

SMulCommClass.of_mul_smul_one theorem

{M N} [Monoid N] [SMul M N] (H : ∀ (x : M) (y : N), y * x • (1 : N) = x • y) : SMulCommClass M N N

Full source

@[to_additive]
lemma SMulCommClass.of_mul_smul_one {M N} [Monoid N] [SMul M N]
    (H : ∀ (x : M) (y : N), y * x • (1 : N) = x • y) : SMulCommClass M N N :=
  ⟨fun x y z ↦ by rw [← H x z, smul_eq_mul, ← H, smul_eq_mul, mul_assoc]⟩

Commutativity of scalar multiplications via identity condition: $y \cdot (x \cdot 1) = x \cdot y$ implies `SMulCommClass M N N`

Informal description

Let $M$ and $N$ be monoids with $M$ acting on $N$ via scalar multiplication. If for all $x \in M$ and $y \in N$ the equality $y \cdot (x \cdot 1_N) = x \cdot y$ holds (where $1_N$ is the identity of $N$ and $\cdot$ denotes scalar multiplication), then the scalar multiplications by $M$ and $N$ on $N$ commute, i.e., $M$ and $N$ form a `SMulCommClass` on $N$.

MulDistribMulAction structure

(M N : Type*) [Monoid M] [Monoid N] extends MulAction M N

Full source

/-- Typeclass for multiplicative actions on multiplicative structures. This generalizes
conjugation actions. -/
@[ext]
class MulDistribMulAction (M N : Type*) [Monoid M] [Monoid N] extends MulAction M N where
  /-- Distributivity of `•` across `*` -/
  smul_mul : ∀ (r : M) (x y : N), r • (x * y) = r • x * r • y
  /-- Multiplying `1` by a scalar gives `1` -/
  smul_one : ∀ r : M, r • (1 : N) = 1

Multiplicative Distributive Action

Informal description

The structure `MulDistribMulAction` represents a multiplicative action of a monoid `M` on another monoid `N` that distributes over multiplication, meaning that for any `a ∈ M` and `b₁, b₂ ∈ N`, the action satisfies $a \cdot (b₁ * b₂) = (a \cdot b₁) * (a \cdot b₂)$. This extends the notion of a multiplicative action (`MulAction`) by adding the distributivity condition.

smul_mul' theorem

(a : M) (b₁ b₂ : N) : a • (b₁ * b₂) = a • b₁ * a • b₂

Full source

lemma smul_mul' (a : M) (b₁ b₂ : N) : a • (b₁ * b₂) = a • b₁ * a • b₂ :=
  MulDistribMulAction.smul_mul ..

Distributivity of scalar multiplication over monoid multiplication

Informal description

Let $M$ and $N$ be monoids, with $M$ acting on $N$ via a multiplicative distributive action. For any $a \in M$ and $b_1, b_2 \in N$, the action satisfies $a \cdot (b_1 * b_2) = (a \cdot b_1) * (a \cdot b_2)$.

Mathlib.Algebra.Group.Action.Defs

Notation

Implementation details

Tags