mathlib3 documentation

group_theory.group_action.defs

Definitions of group actions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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,

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

Faithful actions #

@[protected, instance]
def has_mul.to_has_smul (α : Type u_1) [has_mul α] :
has_smul α α

See also monoid.to_mul_action and mul_zero_class.to_smul_with_zero.

Equations
@[protected, instance]
def has_add.to_has_vadd (α : Type u_1) [has_add α] :
has_vadd α α

See also add_monoid.to_add_action

Equations
@[simp]
theorem vadd_eq_add (α : Type u_1) [has_add α] {a a' : α} :
a +ᵥ a' = a + a'
@[simp]
theorem smul_eq_mul (α : Type u_1) [has_mul α] {a a' : α} :
a a' = a * a'
theorem add_action.ext {G : Type u_10} {P : Type u_11} {_inst_1 : add_monoid G} (x y : add_action G P) (h : add_action.to_has_vadd = add_action.to_has_vadd) :
x = y
theorem add_action.ext_iff {G : Type u_10} {P : Type u_11} {_inst_1 : add_monoid G} (x y : add_action G P) :
theorem mul_action.ext {α : Type u_10} {β : Type u_11} {_inst_1 : monoid α} (x y : mul_action α β) (h : mul_action.to_has_smul = mul_action.to_has_smul) :
x = y
@[ext, class]
structure mul_action (α : Type u_10) (β : Type u_11) [monoid α] :
Type (max u_10 u_11)

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

Instances of this typeclass
Instances of other typeclasses for mul_action
  • mul_action.has_sizeof_inst
theorem mul_action.ext_iff {α : Type u_10} {β : Type u_11} {_inst_1 : monoid α} (x y : mul_action α β) :

(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 mul_action.is_pretransitive and add_action.is_pretransitive and provide mul_action.exists_smul_eq/add_action.exists_vadd_eq, mul_action.surjective_smul/add_action.surjective_vadd as public interface to access this property. We do not provide typeclasses *_action.is_transitive; users should assume [mul_action.is_pretransitive M α] [nonempty α] instead.

@[class]
structure add_action.is_pretransitive (M : Type u_10) (α : Type u_11) [has_vadd M α] :
Prop
  • exists_vadd_eq : (x y : α), (g : M), g +ᵥ x = y

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

Instances of this typeclass
@[class]
structure mul_action.is_pretransitive (M : Type u_10) (α : Type u_11) [has_smul M α] :
Prop
  • exists_smul_eq : (x y : α), (g : M), g x = y

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

Instances of this typeclass
theorem add_action.exists_vadd_eq (M : Type u_1) {α : Type u_6} [has_vadd M α] [add_action.is_pretransitive M α] (x y : α) :
(m : M), m +ᵥ x = y
theorem mul_action.exists_smul_eq (M : Type u_1) {α : Type u_6} [has_smul M α] [mul_action.is_pretransitive M α] (x y : α) :
(m : M), m x = y
theorem mul_action.surjective_smul (M : Type u_1) {α : Type u_6} [has_smul M α] [mul_action.is_pretransitive M α] (x : α) :
function.surjective (λ (c : M), c x)
theorem add_action.surjective_vadd (M : Type u_1) {α : Type u_6} [has_vadd M α] [add_action.is_pretransitive M α] (x : α) :
function.surjective (λ (c : M), c +ᵥ x)
@[protected, instance]

The regular action of a group on itself is transitive.

@[protected, instance]

The regular action of a group on itself is transitive.

Scalar tower and commuting actions #

@[class]
structure smul_comm_class (M : Type u_10) (N : Type u_11) (α : Type u_12) [has_smul M α] [has_smul N α] :
Prop

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

Instances of this typeclass

Frequently, we find ourselves wanting to express a bilinear map M →ₗ[R] N →ₗ[R] P or an equivalence between maps (M →ₗ[R] N) ≃ₗ[R] (M' →ₗ[R] N') where the maps have an associated ring R. Unfortunately, using definitions like these requires that R satisfy comm_semiring R, and not just semiring R. Using M →ₗ[R] N →+ P and (M →ₗ[R] N) ≃+ (M' →ₗ[R] N') avoids this problem, but throws away structure that is useful for when we do have a commutative (semi)ring.

To avoid making this compromise, we instead state these definitions as M →ₗ[R] N →ₗ[S] P or (M →ₗ[R] N) ≃ₗ[S] (M' →ₗ[R] N') and require smul_comm_class S R on the appropriate modules. When the caller has comm_semiring R, they can set S = R and smul_comm_class_self will populate the instance. If the caller only has semiring R they can still set either R = ℕ or S = ℕ, and add_comm_monoid.nat_smul_comm_class or add_comm_monoid.nat_smul_comm_class' will populate the typeclass, which is still sufficient to recover a ≃+ or →+ structure.

An example of where this is used is linear_map.prod_equiv.

theorem smul_comm_class.symm (M : Type u_1) (N : Type u_2) (α : Type u_3) [has_smul M α] [has_smul N α] [smul_comm_class M 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 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 α] :

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.

@[protected, instance]
def vadd_comm_class_self (M : Type u_1) (α : Type u_2) [add_comm_monoid M] [add_action M α] :
@[protected, instance]
def smul_comm_class_self (M : Type u_1) (α : Type u_2) [comm_monoid M] [mul_action M α] :
@[class]
structure is_scalar_tower (M : Type u_10) (N : Type u_11) (α : Type u_12) [has_smul M N] [has_smul N α] [has_smul M α] :
Prop

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 of this typeclass
@[simp]
theorem vadd_assoc {α : Type u_6} {M : Type u_1} {N : Type u_2} [has_vadd M N] [has_vadd N α] [has_vadd M α] [vadd_assoc_class M N α] (x : M) (y : N) (z : α) :
x +ᵥ y +ᵥ z = x +ᵥ (y +ᵥ z)
@[simp]
theorem smul_assoc {α : Type u_6} {M : Type u_1} {N : Type u_2} [has_smul M N] [has_smul N α] [has_smul M α] [is_scalar_tower M N α] (x : M) (y : N) (z : α) :
(x y) z = x y z
@[protected, instance]
def semigroup.is_scalar_tower {α : Type u_6} [semigroup α] :
@[protected, instance]
@[class]
structure is_central_vadd (M : Type u_10) (α : Type u_11) [has_vadd M α] [has_vadd Mᵃᵒᵖ α] :
Prop

A typeclass indicating that the right (aka add_opposite) 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 +ᵥ.

Instances of this typeclass
@[class]
structure is_central_scalar (M : Type u_10) (α : Type u_11) [has_smul M α] [has_smul Mᵐᵒᵖ α] :
Prop

A typeclass indicating that the right (aka mul_opposite) 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 .

Instances of this typeclass
theorem is_central_scalar.unop_smul_eq_smul {M : Type u_1} {α : Type u_2} [has_smul M α] [has_smul Mᵐᵒᵖ α] [is_central_scalar M α] (m : Mᵐᵒᵖ) (a : α) :
theorem is_central_vadd.unop_vadd_eq_vadd {M : Type u_1} {α : Type u_2} [has_vadd M α] [has_vadd Mᵃᵒᵖ α] [is_central_vadd M α] (m : Mᵃᵒᵖ) (a : α) :
@[protected, instance]
def smul_comm_class.op_left {M : Type u_1} {N : Type u_2} {α : Type u_6} [has_smul M α] [has_smul Mᵐᵒᵖ α] [is_central_scalar M α] [has_smul N α] [smul_comm_class M N α] :
@[protected, instance]
def vadd_comm_class.op_left {M : Type u_1} {N : Type u_2} {α : Type u_6} [has_vadd M α] [has_vadd Mᵃᵒᵖ α] [is_central_vadd M α] [has_vadd N α] [vadd_comm_class M N α] :
@[protected, instance]
def smul_comm_class.op_right {M : Type u_1} {N : Type u_2} {α : Type u_6} [has_smul M α] [has_smul N α] [has_smul Nᵐᵒᵖ α] [is_central_scalar N α] [smul_comm_class M N α] :
@[protected, instance]
def vadd_comm_class.op_right {M : Type u_1} {N : Type u_2} {α : Type u_6} [has_vadd M α] [has_vadd N α] [has_vadd Nᵃᵒᵖ α] [is_central_vadd N α] [vadd_comm_class M N α] :
@[protected, instance]
def is_scalar_tower.op_left {M : Type u_1} {N : Type u_2} {α : Type u_6} [has_smul M α] [has_smul Mᵐᵒᵖ α] [is_central_scalar M α] [has_smul M N] [has_smul Mᵐᵒᵖ N] [is_central_scalar M N] [has_smul N α] [is_scalar_tower M N α] :
@[protected, instance]
def vadd_assoc_class.op_left {M : Type u_1} {N : Type u_2} {α : Type u_6} [has_vadd M α] [has_vadd Mᵃᵒᵖ α] [is_central_vadd M α] [has_vadd M N] [has_vadd Mᵃᵒᵖ N] [is_central_vadd M N] [has_vadd N α] [vadd_assoc_class M N α] :
@[protected, instance]
def is_scalar_tower.op_right {M : Type u_1} {N : Type u_2} {α : Type u_6} [has_smul M α] [has_smul M N] [has_smul N α] [has_smul Nᵐᵒᵖ α] [is_central_scalar N α] [is_scalar_tower M N α] :
@[protected, instance]
def vadd_assoc_class.op_right {M : Type u_1} {N : Type u_2} {α : Type u_6} [has_vadd M α] [has_vadd M N] [has_vadd N α] [has_vadd Nᵃᵒᵖ α] [is_central_vadd N α] [vadd_assoc_class M N α] :
@[simp]
def has_smul.comp.smul {M : Type u_1} {N : Type u_2} {α : Type u_6} [has_smul M α] (g : N M) (n : N) (a : α) :
α

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

Equations
@[simp]
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.

Equations
@[reducible]
def has_smul.comp {M : Type u_1} {N : Type u_2} (α : Type u_6) [has_smul M α] (g : N M) :

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 has_smul.comp.smul to prevent typeclass inference unfolding too far.

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

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

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

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

theorem has_vadd.comp.vadd_assoc_class {M : Type u_1} {N : Type u_2} {α : Type u_6} {β : Type u_7} [has_vadd M α] [has_vadd M β] [has_vadd α β] [vadd_assoc_class M α β] (g : N M) :

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

theorem has_smul.comp.smul_comm_class {M : Type u_1} {N : Type u_2} {α : Type u_6} {β : Type u_7} [has_smul M α] [has_smul β α] [smul_comm_class M β α] (g : N M) :

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

theorem has_vadd.comp.vadd_comm_class {M : Type u_1} {N : Type u_2} {α : Type u_6} {β : Type u_7} [has_vadd M α] [has_vadd β α] [vadd_comm_class M β α] (g : N M) :

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

theorem has_vadd.comp.vadd_comm_class' {M : Type u_1} {N : Type u_2} {α : Type u_6} {β : Type u_7} [has_vadd M α] [has_vadd β α] [vadd_comm_class β M α] (g : N M) :

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

theorem has_smul.comp.smul_comm_class' {M : Type u_1} {N : Type u_2} {α : Type u_6} {β : Type u_7} [has_smul M α] [has_smul β α] [smul_comm_class β M α] (g : N M) :

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

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)
@[nolint]
theorem mul_smul_comm {α : Type u_6} {β : Type u_7} [has_mul β] [has_smul α β] [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 α β.

@[nolint]
theorem smul_mul_assoc {α : Type u_6} {β : Type u_7} [has_mul β] [has_smul α β] [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 α β.

theorem vadd_add_assoc {α : Type u_6} {β : Type u_7} [has_add β] [has_vadd α β] [vadd_assoc_class α β β] (r : α) (x y : β) :
r +ᵥ x + y = r +ᵥ (x + y)
theorem smul_smul_smul_comm {α : Type u_6} {β : Type u_7} {γ : Type u_8} {δ : Type u_9} [has_smul α β] [has_smul α γ] [has_smul β δ] [has_smul α δ] [has_smul γ δ] [is_scalar_tower α β δ] [is_scalar_tower α γ δ] [smul_comm_class β γ δ] (a : α) (b : β) (c : γ) (d : δ) :
(a b) c d = (a c) b d
theorem vadd_vadd_vadd_comm {α : Type u_6} {β : Type u_7} {γ : Type u_8} {δ : Type u_9} [has_vadd α β] [has_vadd α γ] [has_vadd β δ] [has_vadd α δ] [has_vadd γ δ] [vadd_assoc_class α β δ] [vadd_assoc_class α γ δ] [vadd_comm_class β γ δ] (a : α) (b : β) (c : γ) (d : δ) :
a +ᵥ b +ᵥ (c +ᵥ d) = a +ᵥ c +ᵥ (b +ᵥ d)
theorem add_commute.vadd_right {M : Type u_1} {α : Type u_6} [has_vadd M α] [has_add α] [vadd_comm_class M α α] [vadd_assoc_class M α α] {a b : α} (h : add_commute a b) (r : M) :
theorem commute.smul_right {M : Type u_1} {α : Type u_6} [has_smul M α] [has_mul α] [smul_comm_class M α α] [is_scalar_tower M α α] {a b : α} (h : commute a b) (r : M) :
commute a (r b)
theorem commute.smul_left {M : Type u_1} {α : Type u_6} [has_smul M α] [has_mul α] [smul_comm_class M α α] [is_scalar_tower M α α] {a b : α} (h : commute a b) (r : M) :
commute (r a) b
theorem add_commute.vadd_left {M : Type u_1} {α : Type u_6} [has_vadd M α] [has_add α] [vadd_comm_class M α α] [vadd_assoc_class M α α] {a b : α} (h : add_commute a b) (r : M) :
theorem ite_smul {M : Type u_1} {α : Type u_6} [has_smul M α] (p : Prop) [decidable p] (a₁ a₂ : M) (b : α) :
ite p a₁ a₂ b = ite p (a₁ b) (a₂ b)
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)
theorem smul_ite {M : Type u_1} {α : Type u_6} [has_smul M α] (p : Prop) [decidable p] (a : M) (b₁ b₂ : α) :
a ite p b₁ b₂ = ite p (a b₁) (a b₂)
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₂)
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
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
@[simp]
theorem one_smul (M : Type u_1) {α : Type u_6} [monoid M] [mul_action M α] (b : α) :
1 b = b
@[simp]
theorem zero_vadd (M : Type u_1) {α : Type u_6} [add_monoid M] [add_action M α] (b : α) :
0 +ᵥ b = b
theorem one_smul_eq_id (M : Type u_1) {α : Type u_6} [monoid M] [mul_action M α] :

has_smul version of one_mul_eq_id

theorem zero_vadd_eq_id (M : Type u_1) {α : Type u_6} [add_monoid M] [add_action M α] :

has_vadd version of zero_add_eq_id

theorem comp_smul_left (M : Type u_1) {α : Type u_6} [monoid M] [mul_action M α] (a₁ a₂ : M) :

has_smul version of comp_mul_left

theorem comp_vadd_left (M : Type u_1) {α : Type u_6} [add_monoid M] [add_action M α] (a₁ a₂ : M) :

has_vadd version of comp_add_left

@[protected, reducible]
def function.injective.mul_action {M : Type u_1} {α : Type u_6} {β : Type u_7} [monoid M] [mul_action M α] [has_smul M β] (f : β α) (hf : function.injective f) (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
@[protected, reducible]
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) :

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

Equations
@[protected, reducible]
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) :

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

Equations
@[protected, reducible]
def function.surjective.mul_action {M : Type u_1} {α : Type u_6} {β : Type u_7} [monoid M] [mul_action M α] [has_smul M β] (f : α β) (hf : function.surjective f) (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
@[reducible]
def function.surjective.mul_action_left {R : Type u_1} {S : Type u_2} {M : Type u_3} [monoid R] [mul_action R M] [monoid S] [has_smul S M] (f : R →* S) (hf : function.surjective f) (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.distrib_mul_action_left and function.surjective.module_left.

Equations
@[reducible]
def function.surjective.add_action_left {R : Type u_1} {S : Type u_2} {M : Type u_3} [add_monoid R] [add_action R M] [add_monoid S] [has_vadd S M] (f : R →+ S) (hf : function.surjective f) (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
@[protected, instance]
def monoid.to_mul_action (M : Type u_1) [monoid M] :

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

This is promoted to a module by semiring.to_module.

Equations
@[protected, instance]

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

This is promoted to an add_torsor by add_group_is_add_torsor.

Equations
@[protected, instance]
def is_scalar_tower.left (M : Type u_1) {α : Type u_6} [monoid M] [mul_action M α] :
@[protected, instance]
def vadd_assoc_class.left (M : Type u_1) {α : Type u_6} [add_monoid M] [add_action M α] :
theorem vadd_add_vadd {M : Type u_1} {α : Type u_6} [add_monoid M] [add_action M α] [has_add α] (r s : M) (x y : α) [vadd_assoc_class M α α] [vadd_comm_class M α α] :
r +ᵥ x + (s +ᵥ y) = r + s +ᵥ (x + y)
@[nolint]
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 α.

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

Equations
@[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
@[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
@[reducible]
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) :

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
@[reducible]
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) :

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
@[simp]
theorem vadd_zero_vadd {α : Type u_6} {M : Type u_1} (N : Type u_2) [add_monoid N] [has_vadd M N] [add_action N α] [has_vadd M α] [vadd_assoc_class M N α] (x : M) (y : α) :
x +ᵥ 0 +ᵥ y = x +ᵥ y
@[simp]
theorem smul_one_smul {α : Type u_6} {M : Type u_1} (N : Type u_2) [monoid N] [has_smul M N] [mul_action N α] [has_smul M α] [is_scalar_tower M N α] (x : M) (y : α) :
(x 1) y = x y
@[simp]
theorem vadd_zero_add {M : Type u_1} {N : Type u_2} [add_zero_class N] [has_vadd M N] [vadd_assoc_class M N N] (x : M) (y : N) :
x +ᵥ 0 + y = x +ᵥ y
@[simp]
theorem smul_one_mul {M : Type u_1} {N : Type u_2} [mul_one_class N] [has_smul M N] [is_scalar_tower M N N] (x : M) (y : N) :
x 1 * y = x y
@[simp]
theorem add_vadd_zero {M : Type u_1} {N : Type u_2} [add_zero_class N] [has_vadd M N] [vadd_comm_class M N N] (x : M) (y : N) :
y + (x +ᵥ 0) = x +ᵥ y
@[simp]
theorem mul_smul_one {M : Type u_1} {N : Type u_2} [mul_one_class N] [has_smul M N] [smul_comm_class M N N] (x : M) (y : N) :
y * x 1 = x y
theorem vadd_assoc_class.of_vadd_zero_add {M : Type u_1} {N : Type u_2} [add_monoid N] [has_vadd M N] (h : (x : M) (y : N), x +ᵥ 0 + y = x +ᵥ y) :
theorem is_scalar_tower.of_smul_one_mul {M : Type u_1} {N : Type u_2} [monoid N] [has_smul M N] (h : (x : M) (y : N), x 1 * y = x y) :
theorem smul_comm_class.of_mul_smul_one {M : Type u_1} {N : Type u_2} [monoid N] [has_smul M N] (H : (x : M) (y : N), y * x 1 = x y) :
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) :
@[simp]
theorem smul_one_hom_apply {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] [mul_action M N] [is_scalar_tower M N N] (x : M) :
@[simp]
theorem vadd_zero_hom_apply {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] [add_action M N] [vadd_assoc_class M N N] (x : M) :
def vadd_zero_hom {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] [add_action M N] [vadd_assoc_class M N N] :
M →+ N

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

Equations
def smul_one_hom {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] [mul_action M N] [is_scalar_tower M N N] :
M →* N

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

Equations
@[class]
structure smul_zero_class (M : Type u_10) (A : Type u_11) [has_zero A] :
Type (max u_10 u_11)

Typeclass for scalar multiplication that preserves 0 on the right.

Instances of this typeclass
Instances of other typeclasses for smul_zero_class
  • smul_zero_class.has_sizeof_inst
@[simp]
theorem smul_zero {M : Type u_1} {A : Type u_4} [has_zero A] [smul_zero_class M A] (a : M) :
a 0 = 0
@[protected, reducible]
def function.injective.smul_zero_class {M : Type u_1} {A : Type u_4} {B : Type u_5} [has_zero A] [smul_zero_class M A] [has_zero B] [has_smul M B] (f : zero_hom B A) (hf : function.injective f) (smul : (c : M) (x : B), f (c x) = c f x) :

Pullback a zero-preserving scalar multiplication along an injective zero-preserving map. See note [reducible non-instances].

Equations
@[protected, reducible]
def zero_hom.smul_zero_class {M : Type u_1} {A : Type u_4} {B : Type u_5} [has_zero A] [smul_zero_class M A] [has_zero B] [has_smul M B] (f : zero_hom A B) (smul : (c : M) (x : A), f (c x) = c f x) :

Pushforward a zero-preserving scalar multiplication along a zero-preserving map. See note [reducible non-instances].

Equations
@[reducible]
def function.surjective.smul_zero_class_left {R : Type u_1} {S : Type u_2} {M : Type u_3} [has_zero M] [smul_zero_class R M] [has_smul S M] (f : R S) (hf : function.surjective f) (hsmul : (c : R) (x : M), f c x = c x) :

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

See also function.surjective.distrib_mul_action_left.

Equations
@[reducible]
def smul_zero_class.comp_fun {M : Type u_1} {N : Type u_2} (A : Type u_4) [has_zero A] [smul_zero_class M A] (f : N M) :

Compose a smul_zero_class with a function, with scalar multiplication f r' • m. See note [reducible non-instances].

Equations
def smul_zero_class.to_zero_hom {M : Type u_1} (A : Type u_4) [has_zero A] [smul_zero_class M A] (x : M) :

Each element of the scalars defines a zero-preserving map.

Equations
@[simp]
theorem smul_zero_class.to_zero_hom_apply {M : Type u_1} (A : Type u_4) [has_zero A] [smul_zero_class M A] (x : M) (ᾰ : A) :
theorem distrib_smul.ext {M : Type u_10} {A : Type u_11} {_inst_1 : add_zero_class A} (x y : distrib_smul M A) (h : distrib_smul.to_smul_zero_class = distrib_smul.to_smul_zero_class) :
x = y
@[ext, class]
structure distrib_smul (M : Type u_10) (A : Type u_11) [add_zero_class A] :
Type (max u_10 u_11)

Typeclass for scalar multiplication that preserves 0 and + on the right.

This is exactly distrib_mul_action without the mul_action part.

Instances of this typeclass
Instances of other typeclasses for distrib_smul
  • distrib_smul.has_sizeof_inst
@[simp]
theorem smul_add {M : Type u_1} {A : Type u_4} [add_zero_class A] [distrib_smul M A] (a : M) (b₁ b₂ : A) :
a (b₁ + b₂) = a b₁ + a b₂
@[protected, reducible]
def function.injective.distrib_smul {M : Type u_1} {A : Type u_4} {B : Type u_5} [add_zero_class A] [distrib_smul M A] [add_zero_class B] [has_smul M B] (f : B →+ A) (hf : function.injective f) (smul : (c : M) (x : B), f (c x) = c f x) :

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

Equations
@[protected, reducible]
def function.surjective.distrib_smul {M : Type u_1} {A : Type u_4} {B : Type u_5} [add_zero_class A] [distrib_smul M A] [add_zero_class B] [has_smul M B] (f : A →+ B) (hf : function.surjective f) (smul : (c : M) (x : A), f (c x) = c f x) :

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

Equations
@[reducible]
def function.surjective.distrib_smul_left {R : Type u_1} {S : Type u_2} {M : Type u_3} [add_zero_class M] [distrib_smul R M] [has_smul S M] (f : R S) (hf : function.surjective f) (hsmul : (c : R) (x : M), f c x = c x) :

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

See also function.surjective.distrib_mul_action_left.

Equations
@[reducible]
def distrib_smul.comp_fun {M : Type u_1} {N : Type u_2} (A : Type u_4) [add_zero_class A] [distrib_smul M A] (f : N M) :

Compose a distrib_smul with a function, with scalar multiplication f r' • m. See note [reducible non-instances].

Equations
@[simp]
theorem distrib_smul.to_add_monoid_hom_apply {M : Type u_1} (A : Type u_4) [add_zero_class A] [distrib_smul M A] (x : M) (ᾰ : A) :
def distrib_smul.to_add_monoid_hom {M : Type u_1} (A : Type u_4) [add_zero_class A] [distrib_smul M A] (x : M) :
A →+ A

Each element of the scalars defines a additive monoid homomorphism.

Equations
theorem distrib_mul_action.ext {M : Type u_10} {A : Type u_11} {_inst_1 : monoid M} {_inst_2 : add_monoid A} (x y : distrib_mul_action M A) (h : distrib_mul_action.to_mul_action = distrib_mul_action.to_mul_action) :
x = y
@[ext, class]
structure distrib_mul_action (M : Type u_10) (A : Type u_11) [monoid M] [add_monoid A] :
Type (max u_10 u_11)

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

Instances of this typeclass
Instances of other typeclasses for distrib_mul_action
  • distrib_mul_action.has_sizeof_inst

Since Lean 3 does not have definitional eta for structures, we have to make sure that the definition of distrib_mul_action.to_distrib_smul was done correctly, and the two paths from distrib_mul_action to has_smul are indeed definitionally equal.

@[protected, reducible]
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_smul M B] (f : B →+ A) (hf : function.injective f) (smul : (c : M) (x : B), f (c x) = c f x) :

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

Equations
@[protected, reducible]
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_smul M B] (f : A →+ B) (hf : function.surjective f) (smul : (c : M) (x : A), f (c x) = c f x) :

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

Equations
@[reducible]
def function.surjective.distrib_mul_action_left {R : Type u_1} {S : Type u_2} {M : Type u_3} [monoid R] [add_monoid M] [distrib_mul_action R M] [monoid S] [has_smul S M] (f : R →* S) (hf : function.surjective f) (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.mul_action_left and function.surjective.module_left.

Equations
@[reducible]
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) :

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

Equations
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
@[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) :

Each element of the monoid defines an additive monoid homomorphism.

Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[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)
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
@[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₂
@[protected, reducible]
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_smul M B] (f : B →* A) (hf : function.injective f) (smul : (c : M) (x : B), f (c x) = c f x) :

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

Equations
@[protected, reducible]
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_smul M B] (f : A →* B) (hf : function.surjective f) (smul : (c : M) (x : A), f (c x) = c f x) :

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

Equations
@[reducible]
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) :

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

Equations
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
@[simp]

Each element of the monoid defines a monoid homomorphism.

Equations
@[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)⁻¹
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
@[protected]
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
Instances for function.End
@[protected, instance]
def function.End.monoid (α : Type u_6) :
Equations
@[protected, instance]
Equations
@[simp]
theorem function.End.smul_def {α : Type u_6} (f : function.End α) (a : α) :
f a = f a
@[protected, instance]

The tautological action by add_monoid.End α on α.

This generalizes function.End.apply_mul_action.

Equations
@[simp]
theorem add_monoid.End.smul_def {α : Type u_6} [add_monoid α] (f : add_monoid.End α) (a : α) :
f a = f a
def mul_action.to_End_hom {M : Type u_1} {α : Type u_6} [monoid M] [mul_action M α] :

The monoid hom representing a monoid action.

When M is a group, see mul_action.to_perm_hom.

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

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

See note [reducible non-instances].

Equations
@[protected, instance]

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

Equations
def add_action.to_End_hom {M : Type u_1} {α : Type u_6} [add_monoid M] [add_action M α] :

The additive monoid hom representing an additive monoid action.

When M is a group, see add_action.to_perm_hom.

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

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

See note [reducible non-instances].

Equations

additive, multiplicative #

@[protected, instance]
def additive.has_vadd {α : Type u_6} {β : Type u_7} [has_smul α β] :
Equations
@[protected, instance]
def multiplicative.has_smul {α : Type u_6} {β : Type u_7} [has_vadd α β] :
Equations
@[simp]
theorem to_mul_smul {α : Type u_6} {β : Type u_7} [has_smul α β] (a : additive α) (b : β) :
@[simp]
theorem of_mul_vadd {α : Type u_6} {β : Type u_7} [has_smul α β] (a : α) (b : β) :
@[simp]
theorem to_add_vadd {α : Type u_6} {β : Type u_7} [has_vadd α β] (a : multiplicative α) (b : β) :
@[simp]
theorem of_add_smul {α : Type u_6} {β : Type u_7} [has_vadd α β] (a : α) (b : β) :
@[protected, instance]
def additive.add_action {α : Type u_6} {β : Type u_7} [monoid α] [mul_action α β] :
Equations
@[protected, instance]
@[protected, instance]
def additive.vadd_comm_class {α : Type u_6} {β : Type u_7} {γ : Type u_8} [has_smul α γ] [has_smul β γ] [smul_comm_class α β γ] :
@[protected, instance]
def multiplicative.smul_comm_class {α : Type u_6} {β : Type u_7} {γ : Type u_8} [has_vadd α γ] [has_vadd β γ] [vadd_comm_class α β γ] :