mathlib documentation

group_theory.group_action.defs

Definitions of group actions #

This file defines a hierarchy of group action type-classes:

The hierarchy is extended further by module, defined elsewhere.

Also provided are type-classes regarding the interaction of different group actions,

Notation #

Implementation details #

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

Tags #

group action

source
@[class]
structure has_vadd (G : Type u_9) (P : Type u_10) :
Type (max u_10 u_9)
  • vadd : G → P → P

Type class for the +ᵥ notation.

Instances
source
@[class]
structure has_scalar (M : Type u_9) (α : Type u_10) :
Type (max u_10 u_9)
  • smul : M → α → α

Typeclass for types with a scalar multiplication operation, denoted • (\bu)

Instances
source
@[class]
structure has_faithful_vadd (G : Type u_9) (P : Type u_10) [has_vadd G P] :
Prop
  • eq_of_vadd_eq_vadd : ∀ {g₁ g₂ : G}, (∀ (p : P), g₁ +ᵥ p = g₂ +ᵥ p) → g₁ = g₂

Typeclass for faithful actions.

Instances
source
@[class]
structure has_faithful_scalar (M : Type u_9) (α : Type u_10) [has_scalar M α] :
Prop
  • eq_of_smul_eq_smul : ∀ {m₁ m₂ : M}, (∀ (a : α), m₁ • a = m₂ • a) → m₁ = m₂

Typeclass for faithful actions.

Instances
source
theorem vadd_left_injective' {M : Type u_1} {α : Type u_6} [has_vadd M α] [has_faithful_vadd M α] :
function.injective has_vadd.vadd
source
theorem smul_left_injective' {M : Type u_1} {α : Type u_6} [has_scalar M α] [has_faithful_scalar M α] :
function.injective has_scalar.smul
source
@[instance]
def has_mul.to_has_scalar (α : Type u_1) [has_mul α] :
has_scalar α α

See also monoid.to_mul_action and mul_zero_class.to_smul_with_zero.

Equations
source
@[instance]
def has_add.to_has_scalar (α : Type u_1) [has_add α] :
has_vadd α α
source
@[simp]
theorem vadd_eq_add (α : Type u_1) [has_add α] {a a' : α} :
a +ᵥ a' = a + a'
source
@[simp]
theorem smul_eq_mul (α : Type u_1) [has_mul α] {a a' : α} :
a • a' = a * a'
source
@[class]
structure add_action (G : Type u_9) (P : Type u_10) [add_monoid G] :
Type (max u_10 u_9)
  • to_has_vadd : has_vadd G P
  • zero_vadd : ∀ (p : P), 0 +ᵥ p = p
  • add_vadd : ∀ (g₁ g₂ : G) (p : P), g₁ + g₂ +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p)

Type class for additive monoid actions.

Instances
source
@[class]
structure mul_action (α : Type u_9) (β : Type u_10) [monoid α] :
Type (max u_10 u_9)
  • to_has_scalar : has_scalar α β
  • one_smul : ∀ (b : β), 1 • b = b
  • mul_smul : ∀ (x y : α) (b : β), (x * y) • b = x • y • b

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

Instances
source
@[class]
structure vadd_comm_class (M : Type u_9) (N : Type u_10) (α : Type u_11) [has_vadd M α] [has_vadd N α] :
Prop

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

Instances
source
@[class]
structure smul_comm_class (M : Type u_9) (N : Type u_10) (α : Type u_11) [has_scalar M α] [has_scalar N α] :
Prop
  • smul_comm : ∀ (m : M) (n : N) (a : α), m • n • a = n • m • a

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

Instances
source
theorem smul_comm_class.symm (M : Type u_1) (N : Type u_2) (α : Type u_3) [has_scalar M α] [has_scalar N α] [smul_comm_class M N α] :
smul_comm_class N M α

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.

source
theorem vadd_comm_class.symm (M : Type u_1) (N : Type u_2) (α : Type u_3) [has_vadd M α] [has_vadd N α] [vadd_comm_class M N α] :
vadd_comm_class N M α

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.

source
@[instance]
def vadd_comm_class_self (M : Type u_1) (α : Type u_2) [add_comm_monoid M] [add_action M α] :
vadd_comm_class M M α
source
@[instance]
def smul_comm_class_self (M : Type u_1) (α : Type u_2) [comm_monoid M] [mul_action M α] :
smul_comm_class M M α
source
@[class]
structure is_scalar_tower (M : Type u_9) (N : Type u_10) (α : Type u_11) [has_scalar M N] [has_scalar N α] [has_scalar M α] :
Prop
  • smul_assoc : ∀ (x : M) (y : N) (z : α), (x • y) • z = x • y • z

An instance of is_scalar_tower M N α states that the multiplicative action of M on α is determined by the multiplicative actions of M on N and N on α.

Instances
source
@[simp]
theorem smul_assoc {α : Type u_6} {M : Type u_1} {N : Type u_2} [has_scalar M N] [has_scalar N α] [has_scalar M α] [is_scalar_tower M N α] (x : M) (y : N) (z : α) :
(x • y) • z = x • y • z
source
@[instance]
def semigroup.is_scalar_tower {α : Type u_6} [semigroup α] :
is_scalar_tower α α α
source
def has_vadd.comp.vadd {M : Type u_1} {N : Type u_2} {α : Type u_6} [has_vadd M α] (g : N → M) (n : N) (a : α) :
α

Auxiliary definition for has_vadd.comp, add_action.comp_hom, etc.

source
@[simp]
def has_scalar.comp.smul {M : Type u_1} {N : Type u_2} {α : Type u_6} [has_scalar M α] (g : N → M) (n : N) (a : α) :
α

Auxiliary definition for has_scalar.comp, mul_action.comp_hom, distrib_mul_action.comp_hom, module.comp_hom, etc.

Equations
source
def has_vadd.comp {M : Type u_1} {N : Type u_2} (α : Type u_6) [has_vadd M α] (g : N → M) :
has_vadd N α

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

source
def has_scalar.comp {M : Type u_1} {N : Type u_2} (α : Type u_6) [has_scalar M α] (g : N → M) :
has_scalar N α

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

See note [reducible non-instances]. Since this is reducible, we make sure to go via has_scalar.comp.smul to prevent typeclass inference unfolding too far.

Equations
source
theorem has_scalar.comp.is_scalar_tower {M : Type u_1} {N : Type u_2} {α : Type u_6} {β : Type u_7} [has_scalar M α] [has_scalar M β] [has_scalar α β] [is_scalar_tower M α β] (g : N → M) :
is_scalar_tower N α β

Given a tower of scalar actions M → α → β, if we use has_scalar.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 has_scalar arguments are still metavariables.

source
@[instance]
def has_scalar.comp.smul_comm_class {M : Type u_1} {N : Type u_2} {α : Type u_6} {β : Type u_7} [has_scalar M α] [has_scalar β α] [smul_comm_class M β α] (g : N → M) :
smul_comm_class N β α
source
@[instance]
def has_scalar.comp.smul_comm_class' {M : Type u_1} {N : Type u_2} {α : Type u_6} {β : Type u_7} [has_scalar M α] [has_scalar β α] [smul_comm_class β M α] (g : N → M) :
smul_comm_class β N α
source
theorem ite_smul {M : Type u_1} {α : Type u_6} [has_scalar M α] (p : Prop) [decidable p] (a₁ a₂ : M) (b : α) :
ite p a₁ a₂ • b = ite p (a₁ • b) (a₂ • b)
source
theorem ite_vadd {M : Type u_1} {α : Type u_6} [has_vadd M α] (p : Prop) [decidable p] (a₁ a₂ : M) (b : α) :
ite p a₁ a₂ +ᵥ b = ite p (a₁ +ᵥ b) (a₂ +ᵥ b)
source
theorem smul_ite {M : Type u_1} {α : Type u_6} [has_scalar M α] (p : Prop) [decidable p] (a : M) (b₁ b₂ : α) :
a • ite p b₁ b₂ = ite p (a • b₁) (a • b₂)
source
theorem vadd_ite {M : Type u_1} {α : Type u_6} [has_vadd M α] (p : Prop) [decidable p] (a : M) (b₁ b₂ : α) :
a +ᵥ ite p b₁ b₂ = ite p (a +ᵥ b₁) (a +ᵥ b₂)
source
theorem smul_smul {M : Type u_1} {α : Type u_6} [monoid M] [mul_action M α] (a₁ a₂ : M) (b : α) :
a₁ • a₂ • b = (a₁ * a₂) • b
source
theorem vadd_vadd {M : Type u_1} {α : Type u_6} [add_monoid M] [add_action M α] (a₁ a₂ : M) (b : α) :
a₁ +ᵥ (a₂ +ᵥ b) = a₁ + a₂ +ᵥ b
source
@[simp]
theorem one_smul (M : Type u_1) {α : Type u_6} [monoid M] [mul_action M α] (b : α) :
1 • b = b
source
@[simp]
theorem zero_vadd (M : Type u_1) {α : Type u_6} [add_monoid M] [add_action M α] (b : α) :
0 +ᵥ b = b
source
def function.injective.mul_action {M : Type u_1} {α : Type u_6} {β : Type u_7} [monoid M] [mul_action M α] [has_scalar M β] (f : β → α) (hf : function.injective f) (smul : ∀ (c : M) (x : β), f (c • x) = c • f x) :
mul_action M β

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

Equations
source
def function.injective.add_action {M : Type u_1} {α : Type u_6} {β : Type u_7} [add_monoid M] [add_action M α] [has_vadd M β] (f : β → α) (hf : function.injective f) (smul : ∀ (c : M) (x : β), f (c +ᵥ x) = c +ᵥ f x) :
add_action M β

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

source
def function.surjective.add_action {M : Type u_1} {α : Type u_6} {β : Type u_7} [add_monoid M] [add_action M α] [has_vadd M β] (f : α → β) (hf : function.surjective f) (smul : ∀ (c : M) (x : α), f (c +ᵥ x) = c +ᵥ f x) :
add_action M β

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

source
def function.surjective.mul_action {M : Type u_1} {α : Type u_6} {β : Type u_7} [monoid M] [mul_action M α] [has_scalar M β] (f : α → β) (hf : function.surjective f) (smul : ∀ (c : M) (x : α), f (c • x) = c • f x) :
mul_action M β

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

Equations
source
@[instance]
def monoid.to_mul_action (M : Type u_1) [monoid M] :
mul_action M M

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

This is promoted to a module by semiring.to_module.

Equations
source
@[instance]
def add_monoid.to_add_action (M : Type u_1) [add_monoid M] :
add_action M M

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

This is promoted to an add_torsor by add_group_is_add_torsor.

source
@[instance]
def is_scalar_tower.left (M : Type u_1) {α : Type u_6} [monoid M] [mul_action M α] :
is_scalar_tower M M α
source
theorem add_vadd_comm {α : Type u_6} {β : Type u_7} [has_add β] [has_vadd α β] [vadd_comm_class α β β] (s : α) (x y : β) :
x + (s +ᵥ y) = s +ᵥ (x + y)
source
theorem mul_smul_comm {α : Type u_6} {β : Type u_7} [has_mul β] [has_scalar α β] [smul_comm_class α β β] (s : α) (x y : β) :
x * s • y = s • x * y

Note that the smul_comm_class α β β typeclass argument is usually satisfied by algebra α β.

source
theorem smul_mul_assoc {α : Type u_6} {β : Type u_7} [has_mul β] [has_scalar α β] [is_scalar_tower α β β] (r : α) (x y : β) :
(r • x) * y = r • x * y

Note that the is_scalar_tower α β β typeclass argument is usually satisfied by algebra α β.

source
theorem smul_mul_smul {M : Type u_1} {α : Type u_6} [monoid M] [mul_action M α] [has_mul α] (r s : M) (x y : α) [is_scalar_tower M α α] [smul_comm_class M α α] :
(r • x) * s • y = (r * s) • x * y

Note that the is_scalar_tower M α α and smul_comm_class M α α typeclass arguments are usually satisfied by algebra M α.

source
def mul_action.to_fun (M : Type u_1) (α : Type u_6) [monoid M] [mul_action M α] :
α ↪ M → α

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

Equations
source
def add_action.to_fun (M : Type u_1) (α : Type u_6) [add_monoid M] [add_action M α] :
α ↪ M → α

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

source
@[simp]
theorem mul_action.to_fun_apply {M : Type u_1} {α : Type u_6} [monoid M] [mul_action M α] (x : M) (y : α) :
⇑(mul_action.to_fun M α) y x = x • y
source
@[simp]
theorem add_action.to_fun_apply {M : Type u_1} {α : Type u_6} [add_monoid M] [add_action M α] (x : M) (y : α) :
⇑(add_action.to_fun M α) y x = x +ᵥ y
source
def mul_action.comp_hom {M : Type u_1} {N : Type u_2} (α : Type u_6) [monoid M] [mul_action M α] [monoid N] (g : N →* M) :
mul_action N α

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
source
def add_action.comp_hom {M : Type u_1} {N : Type u_2} (α : Type u_6) [add_monoid M] [add_action M α] [add_monoid N] (g : N →+ M) :
add_action N α

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

source
@[simp]
theorem smul_one_smul {α : Type u_6} {M : Type u_1} (N : Type u_2) [monoid N] [has_scalar M N] [mul_action N α] [has_scalar M α] [is_scalar_tower M N α] (x : M) (y : α) :
(x • 1) • y = x • y
source
@[simp]
theorem smul_one_mul {M : Type u_1} {N : Type u_2} [monoid N] [has_scalar M N] [is_scalar_tower M N N] (x : M) (y : N) :
(x • 1) * y = x • y
source
@[simp]
theorem add_vadd_zero {M : Type u_1} {N : Type u_2} [add_monoid N] [has_vadd M N] [vadd_comm_class M N N] (x : M) (y : N) :
y + (x +ᵥ 0) = x +ᵥ y
source
@[simp]
theorem mul_smul_one {M : Type u_1} {N : Type u_2} [monoid N] [has_scalar M N] [smul_comm_class M N N] (x : M) (y : N) :
y * x • 1 = x • y
source
theorem is_scalar_tower.of_smul_one_mul {M : Type u_1} {N : Type u_2} [monoid N] [has_scalar M N] (h : ∀ (x : M) (y : N), (x • 1) * y = x • y) :
is_scalar_tower M N N
source
theorem smul_comm_class.of_mul_smul_one {M : Type u_1} {N : Type u_2} [monoid N] [has_scalar M N] (H : ∀ (x : M) (y : N), y * x • 1 = x • y) :
smul_comm_class M N N
source
theorem vadd_comm_class.of_add_vadd_zero {M : Type u_1} {N : Type u_2} [add_monoid N] [has_vadd M N] (H : ∀ (x : M) (y : N), y + (x +ᵥ 0) = x +ᵥ y) :
vadd_comm_class M N N
source
@[class]
structure distrib_mul_action (M : Type u_9) (A : Type u_10) [monoid M] [add_monoid A] :
Type (max u_10 u_9)
  • to_mul_action : mul_action M A
  • smul_add : ∀ (r : M) (x y : A), r • (x + y) = r • x + r • y
  • smul_zero : ∀ (r : M), r • 0 = 0

Typeclass for multiplicative actions on additive structures. This generalizes group modules.

Instances
source
@[simp]
theorem smul_add {M : Type u_1} {A : Type u_4} [monoid M] [add_monoid A] [distrib_mul_action M A] (a : M) (b₁ b₂ : A) :
a • (b₁ + b₂) = a • b₁ + a • b₂
source
@[simp]
theorem smul_zero {M : Type u_1} {A : Type u_4} [monoid M] [add_monoid A] [distrib_mul_action M A] (a : M) :
a • 0 = 0
source
def function.injective.distrib_mul_action {M : Type u_1} {A : Type u_4} {B : Type u_5} [monoid M] [add_monoid A] [distrib_mul_action M A] [add_monoid B] [has_scalar M B] (f : B →+ A) (hf : function.injective ⇑f) (smul : ∀ (c : M) (x : B), ⇑f (c • x) = c • ⇑f x) :
distrib_mul_action M B

Pullback a distributive multiplicative action along an injective additive monoid homomorphism. See note [reducible non-instances].

Equations
source
def function.surjective.distrib_mul_action {M : Type u_1} {A : Type u_4} {B : Type u_5} [monoid M] [add_monoid A] [distrib_mul_action M A] [add_monoid B] [has_scalar M B] (f : A →+ B) (hf : function.surjective ⇑f) (smul : ∀ (c : M) (x : A), ⇑f (c • x) = c • ⇑f x) :
distrib_mul_action M B

Pushforward a distributive multiplicative action along a surjective additive monoid homomorphism. See note [reducible non-instances].

Equations
source
def distrib_mul_action.comp_hom {M : Type u_1} {N : Type u_2} (A : Type u_4) [monoid M] [add_monoid A] [distrib_mul_action M A] [monoid N] (f : N →* M) :
distrib_mul_action N A

Compose a distrib_mul_action with a monoid_hom, with action f r' • m. See note [reducible non-instances].

Equations
source
def distrib_mul_action.to_add_monoid_hom {M : Type u_1} (A : Type u_4) [monoid M] [add_monoid A] [distrib_mul_action M A] (x : M) :
A →+ A

Each element of the monoid defines a additive monoid homomorphism.

Equations
source
@[simp]
theorem distrib_mul_action.to_add_monoid_hom_apply {M : Type u_1} (A : Type u_4) [monoid M] [add_monoid A] [distrib_mul_action M A] (x : M) (ᾰ : A) :
⇑(distrib_mul_action.to_add_monoid_hom A x) ᾰ = x • ᾰ
source
@[simp]
theorem distrib_mul_action.to_add_monoid_End_apply (M : Type u_1) (A : Type u_4) [monoid M] [add_monoid A] [distrib_mul_action M A] (x : M) :
⇑(distrib_mul_action.to_add_monoid_End M A) x = distrib_mul_action.to_add_monoid_hom A x
source
def distrib_mul_action.to_add_monoid_End (M : Type u_1) (A : Type u_4) [monoid M] [add_monoid A] [distrib_mul_action M A] :
M →* add_monoid.End A

Each element of the monoid defines an additive monoid homomorphism.

Equations
source
@[simp]
theorem smul_neg {M : Type u_1} {A : Type u_4} [monoid M] [add_group A] [distrib_mul_action M A] (r : M) (x : A) :
r • -x = -(r • x)
source
theorem smul_sub {M : Type u_1} {A : Type u_4} [monoid M] [add_group A] [distrib_mul_action M A] (r : M) (x y : A) :
r • (x - y) = r • x - r • y
source
@[class]
structure mul_distrib_mul_action (M : Type u_9) (A : Type u_10) [monoid M] [monoid A] :
Type (max u_10 u_9)
  • to_mul_action : mul_action M A
  • smul_mul : ∀ (r : M) (x y : A), r • x * y = (r • x) * r • y
  • smul_one : ∀ (r : M), r • 1 = 1

Typeclass for multiplicative actions on multiplicative structures. This generalizes conjugation actions.

Instances
source
@[simp]
theorem smul_mul' {M : Type u_1} {A : Type u_4} [monoid M] [monoid A] [mul_distrib_mul_action M A] (a : M) (b₁ b₂ : A) :
a • b₁ * b₂ = (a • b₁) * a • b₂
source
def function.injective.mul_distrib_mul_action {M : Type u_1} {A : Type u_4} {B : Type u_5} [monoid M] [monoid A] [mul_distrib_mul_action M A] [monoid B] [has_scalar M B] (f : B →* A) (hf : function.injective ⇑f) (smul : ∀ (c : M) (x : B), ⇑f (c • x) = c • ⇑f x) :
mul_distrib_mul_action M B

Pullback a multiplicative distributive multiplicative action along an injective monoid homomorphism. See note [reducible non-instances].

Equations
source
def function.surjective.mul_distrib_mul_action {M : Type u_1} {A : Type u_4} {B : Type u_5} [monoid M] [monoid A] [mul_distrib_mul_action M A] [monoid B] [has_scalar M B] (f : A →* B) (hf : function.surjective ⇑f) (smul : ∀ (c : M) (x : A), ⇑f (c • x) = c • ⇑f x) :
mul_distrib_mul_action M B

Pushforward a multiplicative distributive multiplicative action along a surjective monoid homomorphism. See note [reducible non-instances].

Equations
source
def mul_distrib_mul_action.comp_hom {M : Type u_1} {N : Type u_2} (A : Type u_4) [monoid M] [monoid A] [mul_distrib_mul_action M A] [monoid N] (f : N →* M) :
mul_distrib_mul_action N A

Compose a mul_distrib_mul_action with a monoid_hom, with action f r' • m. See note [reducible non-instances].

Equations
source
def mul_distrib_mul_action.to_monoid_hom {M : Type u_1} (A : Type u_4) [monoid M] [monoid A] [mul_distrib_mul_action M A] (r : M) :
A →* A

Scalar multiplication by r as a monoid_hom.

Equations
source
@[simp]
theorem mul_distrib_mul_action.to_monoid_hom_apply {M : Type u_1} {A : Type u_4} [monoid M] [monoid A] [mul_distrib_mul_action M A] (r : M) (x : A) :
⇑(mul_distrib_mul_action.to_monoid_hom A r) x = r • x
source
@[simp]
theorem mul_distrib_mul_action.to_monoid_End_apply (M : Type u_1) (A : Type u_4) [monoid M] [monoid A] [mul_distrib_mul_action M A] (r : M) :
⇑(mul_distrib_mul_action.to_monoid_End M A) r = mul_distrib_mul_action.to_monoid_hom A r
source
def mul_distrib_mul_action.to_monoid_End (M : Type u_1) (A : Type u_4) [monoid M] [monoid A] [mul_distrib_mul_action M A] :
M →* monoid.End A

Each element of the monoid defines a monoid homomorphism.

Equations
source
@[simp]
theorem smul_inv' {M : Type u_1} {A : Type u_4} [monoid M] [group A] [mul_distrib_mul_action M A] (r : M) (x : A) :
r • x⁻¹ = (r • x)⁻¹
source
theorem smul_div' {M : Type u_1} {A : Type u_4} [monoid M] [group A] [mul_distrib_mul_action M A] (r : M) (x y : A) :
r • (x / y) = r • x / r • y
source
def function.End (α : Type u_6) :
Type u_6

The monoid of endomorphisms.

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

Equations
source
@[instance]
def function.End.monoid (α : Type u_6) :
monoid (function.End α)
Equations
source
@[instance]
def function.End.inhabited (α : Type u_6) :
inhabited (function.End α)
Equations
source
@[instance]
def function.End.apply_mul_action {α : Type u_6} :
mul_action (function.End α) α

The tautological action by function.End α on α.

This is generalized to bundled endomorphisms by:

Equations
source
@[simp]
theorem function.End.smul_def {α : Type u_6} (f : function.End α) (a : α) :
f • a = f a
source
@[instance]
def function.End.apply_has_faithful_scalar {α : Type u_6} :
has_faithful_scalar (function.End α) α

function.End.apply_mul_action is faithful.

source
@[instance]
def add_monoid.End.apply_distrib_mul_action {α : Type u_6} [add_monoid α] :
distrib_mul_action (add_monoid.End α) α

The tautological action by add_monoid.End α on α.

This generalizes function.End.apply_mul_action.

Equations
source
@[simp]
theorem add_monoid.End.smul_def {α : Type u_6} [add_monoid α] (f : add_monoid.End α) (a : α) :
f • a = ⇑f a
source
@[instance]
def add_monoid.End.apply_has_faithful_scalar {α : Type u_6} [add_monoid α] :
has_faithful_scalar (add_monoid.End α) α

add_monoid.End.apply_distrib_mul_action is faithful.

source
def mul_action.to_End_hom {M : Type u_1} {α : Type u_6} [monoid M] [mul_action M α] :
M →* function.End α

The monoid hom representing a monoid action.

When M is a group, see mul_action.to_perm_hom.

Equations
source
def mul_action.of_End_hom {M : Type u_1} {α : Type u_6} [monoid M] (f : M →* function.End α) :
mul_action M α

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

See note [reducible non-instances].

Equations
source
@[instance]
def add_action.function_End {α : Type u_6} :
add_action (additive (function.End α)) α

The tautological additive action by additive (function.End α) on α.

Equations
source
def add_action.to_End_hom {M : Type u_1} {α : Type u_6} [add_monoid M] [add_action M α] :
M →+ additive (function.End α)

The additive monoid hom representing an additive monoid action.

When M is a group, see add_action.to_perm_hom.

Equations
source
def add_action.of_End_hom {M : Type u_1} {α : Type u_6} [add_monoid M] (f : M →+ additive (function.End α)) :
add_action M α

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

See note [reducible non-instances].

Equations