# Definitions of group actions #

This file defines a hierarchy of group action type-classes on top of the previously defined notation classes SMul and its additive version VAdd:

• MulAction M α and its additive version AddAction G P are typeclasses used for actions of multiplicative and additive monoids and groups; they extend notation classes SMul and VAdd that are defined in Algebra.Group.Defs;
• DistribMulAction M A is a typeclass for an action of a multiplicative monoid on an additive monoid such that a • (b + c) = a • b + a • c and a • 0 = 0.

The hierarchy is extended further by Module, defined elsewhere.

Also provided are typeclasses for faithful and transitive actions, and typeclasses regarding the interaction of different group actions,

• SMulCommClass M N α and its additive version VAddCommClass M N α;
• IsScalarTower M N α and its additive version VAddAssocClass M N α;
• IsCentralScalar M α and its additive version IsCentralVAdd M N α.

## Notation #

• a • b is used as notation for SMul.smul a b.
• a +ᵥ b is used as notation for VAdd.vadd a b.

## Implementation details #

This file should avoid depending on other parts of GroupTheory, to avoid import cycles. More sophisticated lemmas belong in GroupTheory.GroupAction.

## Tags #

group action

### Faithful actions #

class FaithfulVAdd (G : Type u_11) (P : Type u_12) [VAdd G P] :

Typeclass for faithful actions.

• eq_of_vadd_eq_vadd : ∀ {g₁ g₂ : G}, (∀ (p : P), g₁ +ᵥ p = g₂ +ᵥ p)g₁ = g₂

Two elements g₁ and g₂ are equal whenever they act in the same way on all points.

Instances
theorem FaithfulVAdd.eq_of_vadd_eq_vadd {G : Type u_11} {P : Type u_12} [VAdd G P] [self : ] {g₁ : G} {g₂ : G} :
(∀ (p : P), g₁ +ᵥ p = g₂ +ᵥ p)g₁ = g₂

Two elements g₁ and g₂ are equal whenever they act in the same way on all points.

class FaithfulSMul (M : Type u_11) (α : Type u_12) [SMul M α] :

Typeclass for faithful actions.

• eq_of_smul_eq_smul : ∀ {m₁ m₂ : M}, (∀ (a : α), m₁ a = m₂ a)m₁ = m₂

Two elements m₁ and m₂ are equal whenever they act in the same way on all points.

Instances
theorem FaithfulSMul.eq_of_smul_eq_smul {M : Type u_11} {α : Type u_12} [SMul M α] [self : ] {m₁ : M} {m₂ : M} :
(∀ (a : α), m₁ a = m₂ a)m₁ = m₂

Two elements m₁ and m₂ are equal whenever they act in the same way on all points.

theorem vadd_left_injective' {M : Type u_1} {α : Type u_7} [VAdd M α] [] :
Function.Injective fun (x1 : M) (x2 : α) => x1 +ᵥ x2
theorem smul_left_injective' {M : Type u_1} {α : Type u_7} [SMul M α] [] :
Function.Injective fun (x1 : M) (x2 : α) => x1 x2
@[instance 910]

See also AddMonoid.toAddAction

Equations
• = { vadd := fun (x1 x2 : α) => x1 + x2 }
@[instance 910]
instance Mul.toSMul (α : Type u_11) [Mul α] :
SMul α α

See also Monoid.toMulAction and MulZeroClass.toSMulWithZero.

Equations
• = { smul := fun (x1 x2 : α) => x1 * x2 }
@[simp]
a +ᵥ a' = a + a'
@[simp]
theorem smul_eq_mul (α : Type u_11) [Mul α] {a : α} {a' : α} :
a a' = a * a'

AddMonoid.toAddAction is faithful on additive cancellative monoids.

Equations
• =
instance RightCancelMonoid.faithfulSMul {α : Type u_7} :

Monoid.toMulAction is faithful on cancellative monoids.

Equations
• =
class AddAction (G : Type u_11) (P : Type u_12) [] extends :
Type (max u_11 u_12)

Type class for additive monoid actions.

• zero_vadd : ∀ (p : P), 0 +ᵥ p = p

Zero is a neutral element for +ᵥ

• add_vadd : ∀ (g₁ g₂ : G) (p : P), g₁ + g₂ +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p)

Associativity of + and +ᵥ

Instances
theorem AddAction.zero_vadd {G : Type u_11} {P : Type u_12} [] [self : ] (p : P) :
0 +ᵥ p = p

Zero is a neutral element for +ᵥ

theorem AddAction.add_vadd {G : Type u_11} {P : Type u_12} [] [self : ] (g₁ : G) (g₂ : G) (p : P) :
g₁ + g₂ +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p)

Associativity of + and +ᵥ

theorem AddAction.ext_iff {G : Type u_11} {P : Type u_12} :
theorem MulAction.ext_iff {α : Type u_11} {β : Type u_12} :
∀ {inst : } {x y : }, x = y SMul.smul = SMul.smul
theorem AddAction.ext {G : Type u_11} {P : Type u_12} :
theorem MulAction.ext {α : Type u_11} {β : Type u_12} :
∀ {inst : } {x y : }, SMul.smul = SMul.smulx = y
class MulAction (α : Type u_11) (β : Type u_12) [] extends :
Type (max u_11 u_12)

Typeclass for multiplicative actions by monoids. This generalizes group actions.

• smul : αββ
• one_smul : ∀ (b : β), 1 b = b

One is the neutral element for •

• mul_smul : ∀ (x y : α) (b : β), (x * y) b = x y b

Associativity of • and *

Instances
theorem MulAction.one_smul {α : Type u_11} {β : Type u_12} [] [self : ] (b : β) :
1 b = b

One is the neutral element for •

theorem MulAction.mul_smul {α : Type u_11} {β : Type u_12} [] [self : ] (x : α) (y : α) (b : β) :
(x * y) b = x y b

Associativity of • and *

### (Pre)transitive action #

M acts pretransitively on α if for any x y there is g such that g • x = y (or g +ᵥ x = y for an additive action). A transitive action should furthermore have α nonempty.

In this section we define typeclasses MulAction.IsPretransitive and AddAction.IsPretransitive and provide MulAction.exists_smul_eq/AddAction.exists_vadd_eq, MulAction.surjective_smul/AddAction.surjective_vadd as public interface to access this property. We do not provide typeclasses *Action.IsTransitive; users should assume [MulAction.IsPretransitive M α] [Nonempty α] instead.

class AddAction.IsPretransitive (M : Type u_11) (α : Type u_12) [VAdd M α] :

M acts pretransitively on α if for any x y there is g such that g +ᵥ x = y. A transitive action should furthermore have α nonempty.

• exists_vadd_eq : ∀ (x y : α), ∃ (g : M), g +ᵥ x = y

There is g such that g +ᵥ x = y.

Instances
theorem AddAction.IsPretransitive.exists_vadd_eq {M : Type u_11} {α : Type u_12} [VAdd M α] [self : ] (x : α) (y : α) :
∃ (g : M), g +ᵥ x = y

There is g such that g +ᵥ x = y.

class MulAction.IsPretransitive (M : Type u_11) (α : Type u_12) [SMul M α] :

M acts pretransitively on α if for any x y there is g such that g • x = y. A transitive action should furthermore have α nonempty.

• exists_smul_eq : ∀ (x y : α), ∃ (g : M), g x = y

There is g such that g • x = y.

Instances
theorem MulAction.IsPretransitive.exists_smul_eq {M : Type u_11} {α : Type u_12} [SMul M α] [self : ] (x : α) (y : α) :
∃ (g : M), g x = y

There is g such that g • x = y.

theorem AddAction.exists_vadd_eq (M : Type u_1) {α : Type u_7} [VAdd M α] (x : α) (y : α) :
∃ (m : M), m +ᵥ x = y
theorem MulAction.exists_smul_eq (M : Type u_1) {α : Type u_7} [SMul M α] (x : α) (y : α) :
∃ (m : M), m x = y
theorem AddAction.surjective_vadd (M : Type u_1) {α : Type u_7} [VAdd M α] (x : α) :
Function.Surjective fun (c : M) => c +ᵥ x
theorem MulAction.surjective_smul (M : Type u_1) {α : Type u_7} [SMul M α] (x : α) :
Function.Surjective fun (c : M) => c x
instance AddAction.Regular.isPretransitive {G : Type u_3} [] :

The regular action of a group on itself is transitive.

Equations
• =
instance MulAction.Regular.isPretransitive {G : Type u_3} [] :

The regular action of a group on itself is transitive.

Equations
• =

### Scalar tower and commuting actions #

class VAddCommClass (M : Type u_11) (N : Type u_12) (α : Type u_13) [VAdd M α] [VAdd N α] :

A typeclass mixin saying that two additive actions on the same space commute.

• vadd_comm : ∀ (m : M) (n : N) (a : α), m +ᵥ (n +ᵥ a) = n +ᵥ (m +ᵥ a)

+ᵥ is left commutative

Instances
theorem VAddCommClass.vadd_comm {M : Type u_11} {N : Type u_12} {α : Type u_13} [VAdd M α] [VAdd N α] [self : ] (m : M) (n : N) (a : α) :
m +ᵥ (n +ᵥ a) = n +ᵥ (m +ᵥ a)

+ᵥ is left commutative

class SMulCommClass (M : Type u_11) (N : Type u_12) (α : Type u_13) [SMul M α] [SMul N α] :

A typeclass mixin saying that two multiplicative actions on the same space commute.

• smul_comm : ∀ (m : M) (n : N) (a : α), m n a = n m a

• is left commutative

Instances
theorem SMulCommClass.smul_comm {M : Type u_11} {N : Type u_12} {α : Type u_13} [SMul M α] [SMul N α] [self : ] (m : M) (n : N) (a : α) :
m n a = n m a

• is left commutative

theorem VAddCommClass.symm (M : Type u_11) (N : Type u_12) (α : Type u_13) [VAdd M α] [VAdd N α] [] :

Commutativity of additive actions is a symmetric relation. This lemma can't be an instance because this would cause a loop in the instance search graph.

theorem SMulCommClass.symm (M : Type u_11) (N : Type u_12) (α : Type u_13) [SMul M α] [SMul N α] [] :

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.

theorem Function.Injective.vaddCommClass {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [VAdd M α] [VAdd N α] [VAdd M β] [VAdd N β] [] {f : αβ} (hf : ) (h₁ : ∀ (c : M) (x : α), f (c +ᵥ x) = c +ᵥ f x) (h₂ : ∀ (c : N) (x : α), f (c +ᵥ x) = c +ᵥ f x) :
theorem Function.Injective.smulCommClass {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [SMul M α] [SMul N α] [SMul M β] [SMul N β] [] {f : αβ} (hf : ) (h₁ : ∀ (c : M) (x : α), f (c x) = c f x) (h₂ : ∀ (c : N) (x : α), f (c x) = c f x) :
theorem Function.Surjective.vaddCommClass {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [VAdd M α] [VAdd N α] [VAdd M β] [VAdd N β] [] {f : αβ} (hf : ) (h₁ : ∀ (c : M) (x : α), f (c +ᵥ x) = c +ᵥ f x) (h₂ : ∀ (c : N) (x : α), f (c +ᵥ x) = c +ᵥ f x) :
theorem Function.Surjective.smulCommClass {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [SMul M α] [SMul N α] [SMul M β] [SMul N β] [] {f : αβ} (hf : ) (h₁ : ∀ (c : M) (x : α), f (c x) = c f x) (h₂ : ∀ (c : N) (x : α), f (c x) = c f x) :
instance vaddCommClass_self (M : Type u_11) (α : Type u_12) [] [] :
Equations
• =
instance smulCommClass_self (M : Type u_11) (α : Type u_12) [] [] :
Equations
• =
class VAddAssocClass (M : Type u_11) (N : Type u_12) (α : Type u_13) [VAdd M N] [VAdd N α] [VAdd M α] :

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

• vadd_assoc : ∀ (x : M) (y : N) (z : α), x +ᵥ y +ᵥ z = x +ᵥ (y +ᵥ z)

Associativity of +ᵥ

Instances
theorem VAddAssocClass.vadd_assoc {M : Type u_11} {N : Type u_12} {α : Type u_13} [VAdd M N] [VAdd N α] [VAdd M α] [self : ] (x : M) (y : N) (z : α) :
x +ᵥ y +ᵥ z = x +ᵥ (y +ᵥ z)

Associativity of +ᵥ

class IsScalarTower (M : Type u_11) (N : Type u_12) (α : Type u_13) [SMul M N] [SMul N α] [SMul M α] :

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

• smul_assoc : ∀ (x : M) (y : N) (z : α), (x y) z = x y z

Associativity of •

Instances
theorem IsScalarTower.smul_assoc {M : Type u_11} {N : Type u_12} {α : Type u_13} [SMul M N] [SMul N α] [SMul M α] [self : ] (x : M) (y : N) (z : α) :
(x y) z = x y z

Associativity of •

@[simp]
theorem vadd_assoc {α : Type u_7} {M : Type u_11} {N : Type u_12} [VAdd M N] [VAdd N α] [VAdd M α] [] (x : M) (y : N) (z : α) :
x +ᵥ y +ᵥ z = x +ᵥ (y +ᵥ z)
@[simp]
theorem smul_assoc {α : Type u_7} {M : Type u_11} {N : Type u_12} [SMul M N] [SMul N α] [SMul M α] [] (x : M) (y : N) (z : α) :
(x y) z = x y z
instance AddSemigroup.isScalarTower {α : Type u_7} [] :
Equations
• =
instance Semigroup.isScalarTower {α : Type u_7} [] :
Equations
• =
class IsCentralVAdd (M : Type u_11) (α : Type u_12) [VAdd M α] [VAdd Mᵃᵒᵖ α] :

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 +ᵥ.

• op_vadd_eq_vadd : ∀ (m : M) (a : α), = m +ᵥ a

The right and left actions of M on α are equal.

Instances
= m +ᵥ a

The right and left actions of M on α are equal.

class IsCentralScalar (M : Type u_11) (α : Type u_12) [SMul M α] [SMul Mᵐᵒᵖ α] :

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

• op_smul_eq_smul : ∀ (m : M) (a : α), = m a

The right and left actions of M on α are equal.

Instances
@[simp]
theorem IsCentralScalar.op_smul_eq_smul {M : Type u_11} {α : Type u_12} [SMul M α] [SMul Mᵐᵒᵖ α] [self : ] (m : M) (a : α) :
= m a

The right and left actions of M on α are equal.

= m +ᵥ a
theorem IsCentralScalar.unop_smul_eq_smul {M : Type u_11} {α : Type u_12} [SMul M α] [SMul Mᵐᵒᵖ α] [] (m : Mᵐᵒᵖ) (a : α) :
= m a
@[instance 50]
instance VAddCommClass.op_left {M : Type u_1} {N : Type u_2} {α : Type u_7} [VAdd M α] [VAdd Mᵃᵒᵖ α] [] [VAdd N α] [] :
Equations
• =
@[instance 50]
instance SMulCommClass.op_left {M : Type u_1} {N : Type u_2} {α : Type u_7} [SMul M α] [SMul Mᵐᵒᵖ α] [] [SMul N α] [] :
Equations
• =
@[instance 50]
instance VAddCommClass.op_right {M : Type u_1} {N : Type u_2} {α : Type u_7} [VAdd M α] [VAdd N α] [VAdd Nᵃᵒᵖ α] [] [] :
Equations
• =
@[instance 50]
instance SMulCommClass.op_right {M : Type u_1} {N : Type u_2} {α : Type u_7} [SMul M α] [SMul N α] [SMul Nᵐᵒᵖ α] [] [] :
Equations
• =
@[instance 50]
Equations
• =
@[instance 50]
instance IsScalarTower.op_left {M : Type u_1} {N : Type u_2} {α : Type u_7} [SMul M α] [SMul Mᵐᵒᵖ α] [] [SMul M N] [SMul Mᵐᵒᵖ N] [] [SMul N α] [] :
Equations
• =
@[instance 50]
instance VAddAssocClass.op_right {M : Type u_1} {N : Type u_2} {α : Type u_7} [VAdd M α] [VAdd M N] [VAdd N α] [VAdd Nᵃᵒᵖ α] [] [] :
Equations
• =
@[instance 50]
instance IsScalarTower.op_right {M : Type u_1} {N : Type u_2} {α : Type u_7} [SMul M α] [SMul M N] [SMul N α] [SMul Nᵐᵒᵖ α] [] [] :
Equations
• =
def VAdd.comp.vadd {M : Type u_1} {N : Type u_2} {α : Type u_7} [VAdd M α] (g : NM) (n : N) (a : α) :
α

Auxiliary definition for VAdd.comp, AddAction.compHom, etc.

Equations
Instances For
def SMul.comp.smul {M : Type u_1} {N : Type u_2} {α : Type u_7} [SMul M α] (g : NM) (n : N) (a : α) :
α

Auxiliary definition for SMul.comp, MulAction.compHom, DistribMulAction.compHom, Module.compHom, etc.

Equations
Instances For
@[reducible, inline]
abbrev VAdd.comp {M : Type u_1} {N : Type u_2} (α : Type u_7) [VAdd M α] (g : NM) :

An additive action of M on α and a function N → M induces an additive action of N on α.

Equations
• = { vadd := }
Instances For
@[reducible, inline]
abbrev SMul.comp {M : Type u_1} {N : Type u_2} (α : Type u_7) [SMul M α] (g : NM) :
SMul N α

An action of M on α and a function N → M induces an action of N on α.

Equations
• = { smul := }
Instances For
theorem VAdd.comp.isScalarTower {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [VAdd M α] [VAdd M β] [VAdd α β] [] (g : NM) :

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.

theorem SMul.comp.isScalarTower {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [SMul M α] [SMul M β] [SMul α β] [] (g : NM) :

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.

theorem VAdd.comp.vaddCommClass {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [VAdd M α] [VAdd β α] [] (g : NM) :

This cannot be an instance because it can cause infinite loops whenever the VAdd arguments are still metavariables.

theorem SMul.comp.smulCommClass {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [SMul M α] [SMul β α] [] (g : NM) :

This cannot be an instance because it can cause infinite loops whenever the SMul arguments are still metavariables.

theorem VAdd.comp.vaddCommClass' {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [VAdd M α] [VAdd β α] [] (g : NM) :

This cannot be an instance because it can cause infinite loops whenever the VAdd arguments are still metavariables.

theorem SMul.comp.smulCommClass' {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [SMul M α] [SMul β α] [] (g : NM) :

This cannot be an instance because it can cause infinite loops whenever the SMul arguments are still metavariables.

theorem add_vadd_comm {α : Type u_7} {β : Type u_8} [Add β] [VAdd α β] [] (s : α) (x : β) (y : β) :
x + (s +ᵥ y) = s +ᵥ (x + y)
theorem mul_smul_comm {α : Type u_7} {β : Type u_8} [Mul β] [SMul α β] [] (s : α) (x : β) (y : β) :
x * s y = s (x * y)

Note that the SMulCommClass α β β typeclass argument is usually satisfied by Algebra α β.

theorem vadd_add_assoc {α : Type u_7} {β : Type u_8} [Add β] [VAdd α β] [] (r : α) (x : β) (y : β) :
r +ᵥ x + y = r +ᵥ (x + y)
theorem smul_mul_assoc {α : Type u_7} {β : Type u_8} [Mul β] [SMul α β] [] (r : α) (x : β) (y : β) :
r x * y = r (x * y)

Note that the IsScalarTower α β β typeclass argument is usually satisfied by Algebra α β.

theorem vadd_sub_assoc {α : Type u_7} {β : Type u_8} [] [VAdd α β] [] (r : α) (x : β) (y : β) :
r +ᵥ x - y = r +ᵥ (x - y)
theorem smul_div_assoc {α : Type u_7} {β : Type u_8} [] [SMul α β] [] (r : α) (x : β) (y : β) :
r x / y = r (x / y)

Note that the IsScalarTower α β β typeclass argument is usually satisfied by Algebra α β.

theorem vadd_vadd_vadd_comm {α : Type u_7} {β : Type u_8} {γ : Type u_9} {δ : Type u_10} [VAdd α β] [VAdd α γ] [VAdd β δ] [VAdd α δ] [VAdd γ δ] [] [] [] (a : α) (b : β) (c : γ) (d : δ) :
a +ᵥ b +ᵥ (c +ᵥ d) = a +ᵥ c +ᵥ (b +ᵥ d)
theorem smul_smul_smul_comm {α : Type u_7} {β : Type u_8} {γ : Type u_9} {δ : Type u_10} [SMul α β] [SMul α γ] [SMul β δ] [SMul α δ] [SMul γ δ] [] [] [] (a : α) (b : β) (c : γ) (d : δ) :
(a b) c d = (a c) b d
a +ᵥ b + (c +ᵥ d) = a + c +ᵥ (b + d)
theorem smul_mul_smul_comm {α : Type u_7} {β : Type u_8} [Mul α] [Mul β] [SMul α β] [] [] [] (a : α) (b : β) (c : α) (d : β) :
a b * c d = (a * c) (b * d)

Note that the IsScalarTower α β β and SMulCommClass α β β typeclass arguments are usually satisfied by Algebra α β.

@[deprecated]
theorem smul_mul_smul {α : Type u_7} {β : Type u_8} [Mul α] [Mul β] [SMul α β] [] [] [] (a : α) (b : β) (c : α) (d : β) :
a b * c d = (a * c) (b * d)

Alias of smul_mul_smul_comm.

Note that the IsScalarTower α β β and SMulCommClass α β β typeclass arguments are usually satisfied by Algebra α β.

@[deprecated]
a +ᵥ b + (c +ᵥ d) = a + c +ᵥ (b + d)
a + b +ᵥ (c + d) = a +ᵥ c + (b +ᵥ d)
theorem mul_smul_mul_comm {α : Type u_7} {β : Type u_8} [Mul α] [Mul β] [SMul α β] [] [] [] (a : α) (b : α) (c : β) (d : β) :
(a * b) (c * d) = a c * b d

Note that the IsScalarTower α β β and SMulCommClass α β β typeclass arguments are usually satisfied by Algebra α β.

theorem AddCommute.vadd_right {M : Type u_1} {α : Type u_7} [VAdd M α] [Add α] [] [] {a : α} {b : α} (h : ) (r : M) :
theorem Commute.smul_right {M : Type u_1} {α : Type u_7} [SMul M α] [Mul α] [] [] {a : α} {b : α} (h : Commute a b) (r : M) :
Commute a (r b)
theorem AddCommute.vadd_left {M : Type u_1} {α : Type u_7} [VAdd M α] [Add α] [] [] {a : α} {b : α} (h : ) (r : M) :
theorem Commute.smul_left {M : Type u_1} {α : Type u_7} [SMul M α] [Mul α] [] [] {a : α} {b : α} (h : Commute a b) (r : M) :
Commute (r a) b
theorem vadd_vadd {M : Type u_1} {α : Type u_7} [] [] (a₁ : M) (a₂ : M) (b : α) :
a₁ +ᵥ (a₂ +ᵥ b) = a₁ + a₂ +ᵥ b
theorem smul_smul {M : Type u_1} {α : Type u_7} [] [] (a₁ : M) (a₂ : M) (b : α) :
a₁ a₂ b = (a₁ * a₂) b
@[simp]
theorem zero_vadd (M : Type u_1) {α : Type u_7} [] [] (b : α) :
0 +ᵥ b = b
@[simp]
theorem one_smul (M : Type u_1) {α : Type u_7} [] [] (b : α) :
1 b = b
theorem zero_vadd_eq_id (M : Type u_1) {α : Type u_7} [] [] :
(fun (x : α) => 0 +ᵥ x) = id

VAdd version of zero_add_eq_id

theorem one_smul_eq_id (M : Type u_1) {α : Type u_7} [] [] :
(fun (x : α) => 1 x) = id

SMul version of one_mul_eq_id

theorem comp_vadd_left (M : Type u_1) {α : Type u_7} [] [] (a₁ : M) (a₂ : M) :
((fun (x : α) => a₁ +ᵥ x) fun (x : α) => a₂ +ᵥ x) = fun (x : α) => a₁ + a₂ +ᵥ x

VAdd version of comp_add_left

theorem comp_smul_left (M : Type u_1) {α : Type u_7} [] [] (a₁ : M) (a₂ : M) :
((fun (x : α) => a₁ x) fun (x : α) => a₂ x) = fun (x : α) => (a₁ * a₂) x

SMul version of comp_mul_left

theorem Function.Injective.addAction.proof_2 {M : Type u_2} {α : Type u_3} {β : Type u_1} [] [] [VAdd M β] (f : βα) (hf : ) (smul : ∀ (c : M) (x : β), f (c +ᵥ x) = c +ᵥ f x) (c₁ : M) (c₂ : M) (x : β) :
c₁ + c₂ +ᵥ x = c₁ +ᵥ (c₂ +ᵥ x)
theorem Function.Injective.addAction.proof_1 {M : Type u_2} {α : Type u_3} {β : Type u_1} [] [] [VAdd M β] (f : βα) (hf : ) (smul : ∀ (c : M) (x : β), f (c +ᵥ x) = c +ᵥ f x) (x : β) :
0 +ᵥ x = x
@[reducible, inline]
abbrev Function.Injective.addAction {M : Type u_1} {α : Type u_7} {β : Type u_8} [] [] [VAdd M β] (f : βα) (hf : ) (smul : ∀ (c : M) (x : β), f (c +ᵥ x) = c +ᵥ f x) :

Pullback an additive action along an injective map respecting +ᵥ.

Equations
Instances For
@[reducible, inline]
abbrev Function.Injective.mulAction {M : Type u_1} {α : Type u_7} {β : Type u_8} [] [] [SMul M β] (f : βα) (hf : ) (smul : ∀ (c : M) (x : β), f (c x) = c f x) :

Pullback a multiplicative action along an injective map respecting •. See note [reducible non-instances].

Equations
Instances For
theorem Function.Surjective.addAction.proof_2 {M : Type u_2} {α : Type u_3} {β : Type u_1} [] [] [VAdd M β] (f : αβ) (hf : ) (smul : ∀ (c : M) (x : α), f (c +ᵥ x) = c +ᵥ f x) (a : M) (a : M) (y : β) :
a✝ + a +ᵥ y = a✝ +ᵥ (a +ᵥ y)
@[reducible, inline]
abbrev Function.Surjective.addAction {M : Type u_1} {α : Type u_7} {β : Type u_8} [] [] [VAdd M β] (f : αβ) (hf : ) (smul : ∀ (c : M) (x : α), f (c +ᵥ x) = c +ᵥ f x) :

Pushforward an additive action along a surjective map respecting +ᵥ.

Equations
Instances For
theorem Function.Surjective.addAction.proof_1 {M : Type u_2} {α : Type u_3} {β : Type u_1} [] [] [VAdd M β] (f : αβ) (hf : ) (smul : ∀ (c : M) (x : α), f (c +ᵥ x) = c +ᵥ f x) (y : β) :
0 +ᵥ y = y
@[reducible, inline]
abbrev Function.Surjective.mulAction {M : Type u_1} {α : Type u_7} {β : Type u_8} [] [] [SMul M β] (f : αβ) (hf : ) (smul : ∀ (c : M) (x : α), f (c x) = c f x) :

Pushforward a multiplicative action along a surjective map respecting •. See note [reducible non-instances].

Equations
Instances For
@[reducible, inline]
abbrev Function.Surjective.addActionLeft {R : Type u_11} {S : Type u_12} {M : Type u_13} [] [] [] [VAdd S M] (f : R →+ S) (hf : ) (hsmul : ∀ (c : R) (x : M), f c +ᵥ x = c +ᵥ x) :

Push forward the action of R on M along a compatible surjective map f : R →+ S.

Equations
Instances For
theorem Function.Surjective.addActionLeft.proof_2 {R : Type u_3} {S : Type u_2} {M : Type u_1} [] [] [] [VAdd S M] (f : R →+ S) (hf : ) (hsmul : ∀ (c : R) (x : M), f c +ᵥ x = c +ᵥ x) (y₁ : S) (y₂ : S) (b : M) :
y₁ + y₂ +ᵥ b = y₁ +ᵥ (y₂ +ᵥ b)
theorem Function.Surjective.addActionLeft.proof_1 {R : Type u_3} {S : Type u_2} {M : Type u_1} [] [] [] [VAdd S M] (f : R →+ S) (hsmul : ∀ (c : R) (x : M), f c +ᵥ x = c +ᵥ x) (b : M) :
0 +ᵥ b = b
@[reducible, inline]
abbrev Function.Surjective.mulActionLeft {R : Type u_11} {S : Type u_12} {M : Type u_13} [] [] [] [SMul S M] (f : R →* S) (hf : ) (hsmul : ∀ (c : R) (x : M), f c x = c x) :

Push forward the action of R on M along a compatible surjective map f : R →* S.

See also Function.Surjective.distribMulActionLeft and Function.Surjective.moduleLeft.

Equations
Instances For
theorem AddMonoid.toAddAction.proof_2 (M : Type u_1) [] (a : M) (b : M) (c : M) :
a + b + c = a + (b + c)
@[instance 910]

The regular action of a monoid on itself by left addition.

This is promoted to an AddTorsor by addGroup_is_addTorsor.

Equations
0 + a = a
@[instance 910]
instance Monoid.toMulAction (M : Type u_1) [] :

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

This is promoted to a module by Semiring.toModule.

Equations
instance VAddAssocClass.left (M : Type u_1) {α : Type u_7} [] [] :
Equations
• =
instance IsScalarTower.left (M : Type u_1) {α : Type u_7} [] [] :
Equations
• =
theorem smul_pow {M : Type u_1} {N : Type u_2} [] [] [] [] [] (r : M) (x : N) (n : ) :
(r x) ^ n = r ^ n x ^ n
@[simp]
theorem neg_vadd_vadd {G : Type u_3} {α : Type u_7} [] [] (g : G) (a : α) :
-g +ᵥ (g +ᵥ a) = a
@[simp]
theorem inv_smul_smul {G : Type u_3} {α : Type u_7} [] [] (g : G) (a : α) :
g⁻¹ g a = a
@[simp]
theorem vadd_neg_vadd {G : Type u_3} {α : Type u_7} [] [] (g : G) (a : α) :
g +ᵥ (-g +ᵥ a) = a
@[simp]
theorem smul_inv_smul {G : Type u_3} {α : Type u_7} [] [] (g : G) (a : α) :
g g⁻¹ a = a
theorem neg_vadd_eq_iff {G : Type u_3} {α : Type u_7} [] [] {g : G} {a : α} {b : α} :
-g +ᵥ a = b a = g +ᵥ b
theorem inv_smul_eq_iff {G : Type u_3} {α : Type u_7} [] [] {g : G} {a : α} {b : α} :
g⁻¹ a = b a = g b
theorem eq_neg_vadd_iff {G : Type u_3} {α : Type u_7} [] [] {g : G} {a : α} {b : α} :
a = -g +ᵥ b g +ᵥ a = b
theorem eq_inv_smul_iff {G : Type u_3} {α : Type u_7} [] [] {g : G} {a : α} {b : α} :
a = g⁻¹ b g a = b
@[simp]
theorem Commute.smul_right_iff {G : Type u_3} {H : Type u_4} [] [Mul H] [] [] [] {g : G} {a : H} {b : H} :
Commute a (g b) Commute a b
@[simp]
theorem Commute.smul_left_iff {G : Type u_3} {H : Type u_4} [] [Mul H] [] [] [] {g : G} {a : H} {b : H} :
Commute (g a) b Commute a b
theorem smul_inv {G : Type u_3} {H : Type u_4} [] [] [] [] [] (g : G) (a : H) :
theorem smul_zpow {G : Type u_3} {H : Type u_4} [] [] [] [] [] (g : G) (a : H) (n : ) :
(g a) ^ n = g ^ n a ^ n
theorem SMulCommClass.of_commMonoid (A : Type u_11) (B : Type u_12) (G : Type u_13) [] [SMul A G] [SMul B G] [] [] :
theorem AddAction.toFun.proof_1 (M : Type u_1) (α : Type u_2) [] [] (y₁ : α) (y₂ : α) (H : (fun (y : α) (x : M) => x +ᵥ y) y₁ = (fun (y : α) (x : M) => x +ᵥ y) y₂) :
y₁ = y₂
def AddAction.toFun (M : Type u_1) (α : Type u_7) [] [] :
α Mα

Embedding of α into functions M → α induced by an additive action of M on α.

Equations
• = { toFun := fun (y : α) (x : M) => x +ᵥ y, inj' := }
Instances For
def MulAction.toFun (M : Type u_1) (α : Type u_7) [] [] :
α Mα

Embedding of α into functions M → α induced by a multiplicative action of M on α.

Equations
• = { toFun := fun (y : α) (x : M) => x y, inj' := }
Instances For
@[simp]
theorem AddAction.toFun_apply {M : Type u_1} {α : Type u_7} [] [] (x : M) (y : α) :
(AddAction.toFun M α) y x = x +ᵥ y
@[simp]
theorem MulAction.toFun_apply {M : Type u_1} {α : Type u_7} [] [] (x : M) (y : α) :
(MulAction.toFun M α) y x = x y
@[reducible, inline]
abbrev AddAction.compHom {M : Type u_1} {N : Type u_2} (α : Type u_7) [] [] [] (g : N →+ M) :

An additive action of M on α and an additive monoid homomorphism N → M induce an additive action of N on α.

See note [reducible non-instances].

Equations
Instances For
theorem AddAction.compHom.proof_2 {M : Type u_3} {N : Type u_2} (α : Type u_1) [] [] [] (g : N →+ M) :
∀ (x x_1 : N) (x_2 : α), x + x_1 +ᵥ x_2 = x +ᵥ (x_1 +ᵥ x_2)
theorem AddAction.compHom.proof_1 {M : Type u_3} {N : Type u_2} (α : Type u_1) [] [] [] (g : N →+ M) :
∀ (x : α), 0 +ᵥ x = x
@[reducible, inline]
abbrev MulAction.compHom {M : Type u_1} {N : Type u_2} (α : Type u_7) [] [] [] (g : N →* M) :

A multiplicative action of M on α and a monoid homomorphism N → M induce a multiplicative action of N on α.

See note [reducible non-instances].

Equations
Instances For
theorem AddAction.compHom_vadd_def {E : Type u_11} {F : Type u_12} {G : Type u_13} [] [] [] (f : E →+ F) (a : E) (x : G) :
a +ᵥ x = f a +ᵥ x
theorem MulAction.compHom_smul_def {E : Type u_11} {F : Type u_12} {G : Type u_13} [] [] [] (f : E →* F) (a : E) (x : G) :
a x = f a x
theorem AddAction.isPretransitive_compHom {E : Type u_11} {F : Type u_12} {G : Type u_13} [] [] [] {f : E →+ F} (hf : ) :
theorem MulAction.isPretransitive_compHom {E : Type u_11} {F : Type u_12} {G : Type u_13} [] [] [] {f : E →* F} (hf : ) :

If an action is transitive, then composing this action with a surjective homomorphism gives again a transitive action.

theorem AddAction.IsPretransitive.of_vadd_eq {M : Type u_11} {N : Type u_12} {α : Type u_13} [VAdd M α] [VAdd N α] (f : MN) (hf : ∀ {c : M} {x : α}, f c +ᵥ x = c +ᵥ x) :
theorem MulAction.IsPretransitive.of_smul_eq {M : Type u_11} {N : Type u_12} {α : Type u_13} [SMul M α] [SMul N α] (f : MN) (hf : ∀ {c : M} {x : α}, f c x = c x) :
theorem AddAction.IsPretransitive.of_compHom {M : Type u_11} {N : Type u_12} {α : Type u_13} [] [] [] (f : M →+ N) [h : ] :
theorem MulAction.IsPretransitive.of_compHom {M : Type u_11} {N : Type u_12} {α : Type u_13} [] [] [] (f : M →* N) [h : ] :
theorem vadd_zero_vadd {α : Type u_7} {M : Type u_11} (N : Type u_12) [] [VAdd M N] [] [VAdd M α] [] (x : M) (y : α) :
x +ᵥ 0 +ᵥ y = x +ᵥ y
theorem smul_one_smul {α : Type u_7} {M : Type u_11} (N : Type u_12) [] [SMul M N] [] [SMul M α] [] (x : M) (y : α) :
(x 1) y = x y
theorem AddAction.IsPretransitive.of_isScalarTower (M : Type u_11) {N : Type u_12} {α : Type u_13} [] [VAdd M N] [] [VAdd M α] [] :
theorem MulAction.IsPretransitive.of_isScalarTower (M : Type u_11) {N : Type u_12} {α : Type u_13} [] [SMul M N] [] [SMul M α] [] :
@[simp]
theorem vadd_zero_add {M : Type u_11} {N : Type u_12} [] [VAdd M N] [] (x : M) (y : N) :
x +ᵥ 0 + y = x +ᵥ y
@[simp]
theorem smul_one_mul {M : Type u_11} {N : Type u_12} [] [SMul M N] [] (x : M) (y : N) :
x 1 * y = x y
@[simp]
theorem add_vadd_zero {M : Type u_11} {N : Type u_12} [] [VAdd M N] [] (x : M) (y : N) :
y + (x +ᵥ 0) = x +ᵥ y
@[simp]
theorem mul_smul_one {M : Type u_11} {N : Type u_12} [] [SMul M N] [] (x : M) (y : N) :
y * x 1 = x y
theorem VAddAssocClass.of_vadd_zero_add {M : Type u_11} {N : Type u_12} [] [VAdd M N] (h : ∀ (x : M) (y : N), x +ᵥ 0 + y = x +ᵥ y) :
theorem IsScalarTower.of_smul_one_mul {M : Type u_11} {N : Type u_12} [] [SMul M N] (h : ∀ (x : M) (y : N), x 1 * y = x y) :
theorem VAddCommClass.of_add_vadd_zero {M : Type u_11} {N : Type u_12} [] [VAdd M N] (H : ∀ (x : M) (y : N), y + (x +ᵥ 0) = x +ᵥ y) :
theorem SMulCommClass.of_mul_smul_one {M : Type u_11} {N : Type u_12} [] [SMul M N] (H : ∀ (x : M) (y : N), y * x 1 = x y) :
theorem AddMonoidHom.vaddZeroHom.proof_1 {M : Type u_2} {N : Type u_1} [] [] [] :
0 +ᵥ 0 = 0
theorem AddMonoidHom.vaddZeroHom.proof_2 {M : Type u_2} {N : Type u_1} [] [] [] [] (x : M) (y : M) :
{ toFun := fun (x : M) => x +ᵥ 0, map_zero' := }.toFun (x + y) = { toFun := fun (x : M) => x +ᵥ 0, map_zero' := }.toFun x + { toFun := fun (x : M) => x +ᵥ 0, map_zero' := }.toFun y
def AddMonoidHom.vaddZeroHom {M : Type u_11} {N : Type u_12} [] [] [] [] :
M →+ N

If the additive action of M on N is compatible with addition on N, then fun x ↦ x +ᵥ 0 is an additive monoid homomorphism from M to N.

Equations
• AddMonoidHom.vaddZeroHom = { toFun := fun (x : M) => x +ᵥ 0, map_zero' := , map_add' := }
Instances For
@[simp]
theorem MonoidHom.smulOneHom_apply {M : Type u_11} {N : Type u_12} [] [] [] [] (x : M) :
MonoidHom.smulOneHom x = x 1
@[simp]
theorem AddMonoidHom.vaddZeroHom_apply {M : Type u_11} {N : Type u_12} [] [] [] [] (x : M) :
def MonoidHom.smulOneHom {M : Type u_11} {N : Type u_12} [] [] [] [] :
M →* N

If the multiplicative action of M on N is compatible with multiplication on N, then fun x ↦ x • 1 is a monoid homomorphism from M to N.

Equations
• MonoidHom.smulOneHom = { toFun := fun (x : M) => x 1, map_one' := , map_mul' := }
Instances For
def addMonoidHomEquivAddActionIsScalarTower (M : Type u_11) (N : Type u_12) [] [] :
(M →+ N) { _inst : // }

A monoid homomorphism between two additive monoids M and N can be equivalently specified by an additive action of M on N that is compatible with the addition on N.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem addMonoidHomEquivAddActionIsScalarTower.proof_1 (M : Type u_1) (N : Type u_2) [] [] (f : M →+ N) :
theorem addMonoidHomEquivAddActionIsScalarTower.proof_2 (M : Type u_1) (N : Type u_2) [] [] (f : M →+ N) :
(fun (x : { _inst : // }) => match x with | val, property => AddMonoidHom.vaddZeroHom) ((fun (f : M →+ N) => , ) f) = f
theorem addMonoidHomEquivAddActionIsScalarTower.proof_3 (M : Type u_1) (N : Type u_2) [] [] :
∀ (x : { _inst : // }), (fun (f : M →+ N) => , ) ((fun (x : { _inst : // }) => match x with | val, property => AddMonoidHom.vaddZeroHom) x) = x
def monoidHomEquivMulActionIsScalarTower (M : Type u_11) (N : Type u_12) [] [] :
(M →* N) { _inst : // }

A monoid homomorphism between two monoids M and N can be equivalently specified by a multiplicative action of M on N that is compatible with the multiplication on N.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Function.End (α : Type u_7) :
Type u_7

The monoid of endomorphisms.

Note that this is generalized by CategoryTheory.End to categories other than Type u.

Equations
• = (αα)
Instances For
instance instMonoidEnd (α : Type u_7) :
Equations
instance instInhabitedEnd (α : Type u_7) :
Equations
• = { default := 1 }
instance Function.End.applyMulAction {α : Type u_7} :

The tautological action by Function.End α on α.

This is generalized to bundled endomorphisms by:

• Equiv.Perm.applyMulAction
• AddMonoid.End.applyDistribMulAction
• AddMonoid.End.applyModule
• AddAut.applyDistribMulAction
• MulAut.applyMulDistribMulAction
• LinearEquiv.applyDistribMulAction
• LinearMap.applyModule
• RingHom.applyMulSemiringAction
• RingAut.applyMulSemiringAction
• AlgEquiv.applyMulSemiringAction
Equations
• Function.End.applyMulAction =
@[simp]
theorem Function.End.smul_def {α : Type u_7} (f : ) (a : α) :
f a = f a
theorem Function.End.mul_def {α : Type u_7} (f : ) (g : ) :
f * g = f g
theorem Function.End.one_def {α : Type u_7} :
1 = id

Function.End.applyMulAction is faithful.

Equations
• =
def MulAction.toEndHom {M : Type u_1} {α : Type u_7} [] [] :

The monoid hom representing a monoid action.

When M is a group, see MulAction.toPermHom.

Equations
• MulAction.toEndHom = { toFun := fun (x1 : M) (x2 : α) => x1 x2, map_one' := , map_mul' := }
Instances For
@[reducible, inline]
abbrev MulAction.ofEndHom {M : Type u_1} {α : Type u_7} [] (f : ) :

The monoid action induced by a monoid hom to Function.End α

See note [reducible non-instances].

Equations
Instances For

### Additive, Multiplicative#

instance Additive.vadd {α : Type u_7} {β : Type u_8} [SMul α β] :
Equations
instance Multiplicative.smul {α : Type u_7} {β : Type u_8} [VAdd α β] :
SMul β
Equations
• Multiplicative.smul = { smul := fun (a : ) (x : β) => Multiplicative.toAdd a +ᵥ x }
@[simp]
theorem toMul_smul {α : Type u_7} {β : Type u_8} [SMul α β] (a : ) (b : β) :
Additive.toMul a b = a +ᵥ b
@[simp]
theorem ofMul_vadd {α : Type u_7} {β : Type u_8} [SMul α β] (a : α) (b : β) :
Additive.ofMul a +ᵥ b = a b
@[simp]
theorem toAdd_vadd {α : Type u_7} {β : Type u_8} [VAdd α β] (a : ) (b : β) :
Multiplicative.toAdd a +ᵥ b = a b
@[simp]
theorem ofAdd_smul {α : Type u_7} {β : Type u_8} [VAdd α β] (a : α) (b : β) :
Multiplicative.ofAdd a b = a +ᵥ b
instance Additive.addAction {α : Type u_7} {β : Type u_8} [] [] :
Equations
instance Multiplicative.mulAction {α : Type u_7} {β : Type u_8} [] [] :
Equations
• Multiplicative.mulAction =
instance Additive.addAction_isPretransitive {α : Type u_7} {β : Type u_8} [] [] :
Equations
• =
instance Multiplicative.mulAction_isPretransitive {α : Type u_7} {β : Type u_8} [] [] :
Equations
• =
instance Additive.vaddCommClass {α : Type u_7} {β : Type u_8} {γ : Type u_9} [SMul α γ] [SMul β γ] [] :
Equations
• =
instance Multiplicative.smulCommClass {α : Type u_7} {β : Type u_8} {γ : Type u_9} [VAdd α γ] [VAdd β γ] [] :
Equations
• =

The tautological additive action by Additive (Function.End α) on α.

Equations
def AddAction.toEndHom {M : Type u_1} {α : Type u_7} [] [] :
M →+

When M is a group, see AddAction.toPermHom.

Equations
Instances For
@[reducible, inline]
abbrev AddAction.ofEndHom {M : Type u_1} {α : Type u_7} [] (f : M →+ ) :

The additive action induced by a hom to Additive (Function.End α)

See note [reducible non-instances].

Equations
Instances For