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_10) (P : Type u_11) [VAdd G P] : Prop

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.

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

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.

theorem vadd_left_injective' {M : Type u_1} {α : Type u_6} [VAdd M α] [FaithfulVAdd M α] : Function.Injective fun (x : M) (x_1 : α) => x +ᵥ x_1

theorem smul_left_injective' {M : Type u_1} {α : Type u_6} [SMul M α] [FaithfulSMul M α] : Function.Injective fun (x : M) (x_1 : α) => x • x_1

instance Add.toVAdd (α : Type u_10) [Add α] : VAdd α α

See also AddMonoid.toAddAction

Equations

• Add.toVAdd α = { vadd := fun (x x_1 : α) => x + x_1 }

instance Mul.toSMul (α : Type u_10) [Mul α] : SMul α α

See also Monoid.toMulAction and MulZeroClass.toSMulWithZero.

Equations

• Mul.toSMul α = { smul := fun (x x_1 : α) => x * x_1 }

@[simp]

theorem vadd_eq_add (α : Type u_10) [Add α] {a : α} {a' : α} : a +ᵥ a' = a + a'

@[simp]

theorem smul_eq_mul (α : Type u_10) [Mul α] {a : α} {a' : α} : a • a' = a * a'

class AddAction (G : Type u_10) (P : Type u_11) [AddMonoid G] extends VAdd : Type (max u_10 u_11)

Type class for additive monoid actions.

• vadd : G → P → P
• 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 +ᵥ

theorem AddAction.ext_iff {G : Type u_10} {P : Type u_11} : ∀ {inst : AddMonoid G} (x y : AddAction G P), x = y ↔ VAdd.vadd = VAdd.vadd

theorem MulAction.ext {α : Type u_10} {β : Type u_11} : ∀ {inst : Monoid α} (x y : MulAction α β), SMul.smul = SMul.smul → x = y

theorem AddAction.ext {G : Type u_10} {P : Type u_11} : ∀ {inst : AddMonoid G} (x y : AddAction G P), VAdd.vadd = VAdd.vadd → x = y

theorem MulAction.ext_iff {α : Type u_10} {β : Type u_11} : ∀ {inst : Monoid α} (x y : MulAction α β), x = y ↔ SMul.smul = SMul.smul

class MulAction (α : Type u_10) (β : Type u_11) [Monoid α] extends SMul : Type (max u_10 u_11)

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 *

(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_10) (α : Type u_11) [VAdd M α] : Prop

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.

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

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.

theorem AddAction.exists_vadd_eq (M : Type u_1) {α : Type u_6} [VAdd M α] [AddAction.IsPretransitive M α] (x : α) (y : α) : ∃ (m : M), m +ᵥ x = y

theorem MulAction.exists_smul_eq (M : Type u_1) {α : Type u_6} [SMul M α] [MulAction.IsPretransitive M α] (x : α) (y : α) : ∃ (m : M), m • x = y

theorem AddAction.surjective_vadd (M : Type u_1) {α : Type u_6} [VAdd M α] [AddAction.IsPretransitive M α] (x : α) : Function.Surjective fun (c : M) => c +ᵥ x

theorem MulAction.surjective_smul (M : Type u_1) {α : Type u_6} [SMul M α] [MulAction.IsPretransitive M α] (x : α) : Function.Surjective fun (c : M) => c • x

instance AddAction.Regular.isPretransitive {G : Type u_3} [AddGroup G] : AddAction.IsPretransitive G G

The regular action of a group on itself is transitive.

Equations

• ⋯ = ⋯

instance MulAction.Regular.isPretransitive {G : Type u_3} [Group G] : MulAction.IsPretransitive G G

The regular action of a group on itself is transitive.

Equations

• ⋯ = ⋯

Scalar tower and commuting actions

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

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

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

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

theorem VAddCommClass.symm (M : Type u_10) (N : Type u_11) (α : Type u_12) [VAdd M α] [VAdd N α] [VAddCommClass M N α] : VAddCommClass 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.

theorem SMulCommClass.symm (M : Type u_10) (N : Type u_11) (α : Type u_12) [SMul M α] [SMul N α] [SMulCommClass M N α] : SMulCommClass 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.

theorem Function.Injective.smulCommClass {M : Type u_1} {N : Type u_2} {α : Type u_6} {β : Type u_7} [SMul M α] [SMul N α] [SMul M β] [SMul N β] [SMulCommClass M N β] {f : α → β} (hf : Function.Injective f) (h₁ : ∀ (c : M) (x : α), f (c • x) = c • f x) (h₂ : ∀ (c : N) (x : α), f (c • x) = c • f x) : SMulCommClass M N α

theorem Function.Surjective.smulCommClass {M : Type u_1} {N : Type u_2} {α : Type u_6} {β : Type u_7} [SMul M α] [SMul N α] [SMul M β] [SMul N β] [SMulCommClass M N α] {f : α → β} (hf : Function.Surjective f) (h₁ : ∀ (c : M) (x : α), f (c • x) = c • f x) (h₂ : ∀ (c : N) (x : α), f (c • x) = c • f x) : SMulCommClass M N β

instance vaddCommClass_self (M : Type u_10) (α : Type u_11) [AddCommMonoid M] [AddAction M α] : VAddCommClass M M α

Equations

• ⋯ = ⋯

instance smulCommClass_self (M : Type u_10) (α : Type u_11) [CommMonoid M] [MulAction M α] : SMulCommClass M M α

Equations

• ⋯ = ⋯

class VAddAssocClass (M : Type u_10) (N : Type u_11) (α : Type u_12) [VAdd M N] [VAdd N α] [VAdd M α] : Prop

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

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

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 •

@[simp]

theorem vadd_assoc {α : Type u_6} {M : Type u_10} {N : Type u_11} [VAdd M N] [VAdd N α] [VAdd M α] [VAddAssocClass M N α] (x : M) (y : N) (z : α) : x +ᵥ y +ᵥ z = x +ᵥ (y +ᵥ z)

@[simp]

theorem smul_assoc {α : Type u_6} {M : Type u_10} {N : Type u_11} [SMul M N] [SMul N α] [SMul M α] [IsScalarTower M N α] (x : M) (y : N) (z : α) : (x • y) • z = x • y • z

instance AddSemigroup.isScalarTower {α : Type u_6} [AddSemigroup α] : VAddAssocClass α α α

Equations

• ⋯ = ⋯

instance Semigroup.isScalarTower {α : Type u_6} [Semigroup α] : IsScalarTower α α α

Equations

• ⋯ = ⋯

class IsCentralVAdd (M : Type u_10) (α : Type u_11) [VAdd M α] [VAdd Mᵃᵒᵖ α] : Prop

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 : α), AddOpposite.op m +ᵥ a = m +ᵥ a

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

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

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 : α), MulOpposite.op m • a = m • a

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

theorem IsCentralVAdd.unop_vadd_eq_vadd {M : Type u_10} {α : Type u_11} [VAdd M α] [VAdd Mᵃᵒᵖ α] [IsCentralVAdd M α] (m : Mᵃᵒᵖ) (a : α) : AddOpposite.unop m +ᵥ a = m +ᵥ a

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

instance VAddCommClass.op_left {M : Type u_1} {N : Type u_2} {α : Type u_6} [VAdd M α] [VAdd Mᵃᵒᵖ α] [IsCentralVAdd M α] [VAdd N α] [VAddCommClass M N α] : VAddCommClass Mᵃᵒᵖ N α

Equations

• ⋯ = ⋯

instance SMulCommClass.op_left {M : Type u_1} {N : Type u_2} {α : Type u_6} [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] [SMul N α] [SMulCommClass M N α] : SMulCommClass Mᵐᵒᵖ N α

Equations

• ⋯ = ⋯

instance VAddCommClass.op_right {M : Type u_1} {N : Type u_2} {α : Type u_6} [VAdd M α] [VAdd N α] [VAdd Nᵃᵒᵖ α] [IsCentralVAdd N α] [VAddCommClass M N α] : VAddCommClass M Nᵃᵒᵖ α

Equations

• ⋯ = ⋯

instance SMulCommClass.op_right {M : Type u_1} {N : Type u_2} {α : Type u_6} [SMul M α] [SMul N α] [SMul Nᵐᵒᵖ α] [IsCentralScalar N α] [SMulCommClass M N α] : SMulCommClass M Nᵐᵒᵖ α

Equations

• ⋯ = ⋯

instance VAddAssocClass.op_left {M : Type u_1} {N : Type u_2} {α : Type u_6} [VAdd M α] [VAdd Mᵃᵒᵖ α] [IsCentralVAdd M α] [VAdd M N] [VAdd Mᵃᵒᵖ N] [IsCentralVAdd M N] [VAdd N α] [VAddAssocClass M N α] : VAddAssocClass Mᵃᵒᵖ N α

Equations

• ⋯ = ⋯

instance IsScalarTower.op_left {M : Type u_1} {N : Type u_2} {α : Type u_6} [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] [SMul M N] [SMul Mᵐᵒᵖ N] [IsCentralScalar M N] [SMul N α] [IsScalarTower M N α] : IsScalarTower Mᵐᵒᵖ N α

Equations

• ⋯ = ⋯

instance VAddAssocClass.op_right {M : Type u_1} {N : Type u_2} {α : Type u_6} [VAdd M α] [VAdd M N] [VAdd N α] [VAdd Nᵃᵒᵖ α] [IsCentralVAdd N α] [VAddAssocClass M N α] : VAddAssocClass M Nᵃᵒᵖ α

Equations

• ⋯ = ⋯

instance IsScalarTower.op_right {M : Type u_1} {N : Type u_2} {α : Type u_6} [SMul M α] [SMul M N] [SMul N α] [SMul Nᵐᵒᵖ α] [IsCentralScalar N α] [IsScalarTower M N α] : IsScalarTower M Nᵐᵒᵖ α

Equations

• ⋯ = ⋯

def VAdd.comp.vadd {M : Type u_1} {N : Type u_2} {α : Type u_6} [VAdd M α] (g : N → M) (n : N) (a : α) : α

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

Equations

• VAdd.comp.vadd g n a = g n +ᵥ a

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

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

Equations

• SMul.comp.smul g n a = g n • a

@[reducible]

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

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

Equations

• VAdd.comp α g = { vadd := VAdd.comp.vadd g }

@[reducible]

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

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

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

Equations

• SMul.comp α g = { smul := SMul.comp.smul g }

theorem VAdd.comp.isScalarTower {M : Type u_1} {N : Type u_2} {α : Type u_6} {β : Type u_7} [VAdd M α] [VAdd M β] [VAdd α β] [VAddAssocClass M α β] (g : N → M) : VAddAssocClass N α β

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_6} {β : Type u_7} [SMul M α] [SMul M β] [SMul α β] [IsScalarTower M α β] (g : N → M) : IsScalarTower N α β

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_6} {β : Type u_7} [VAdd M α] [VAdd β α] [VAddCommClass M β α] (g : N → M) : VAddCommClass N β α

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_6} {β : Type u_7} [SMul M α] [SMul β α] [SMulCommClass M β α] (g : N → M) : SMulCommClass 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_6} {β : Type u_7} [VAdd M α] [VAdd β α] [VAddCommClass β M α] (g : N → M) : VAddCommClass β N α

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_6} {β : Type u_7} [SMul M α] [SMul β α] [SMulCommClass β M α] (g : N → M) : SMulCommClass β N α

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

theorem add_vadd_comm {α : Type u_6} {β : Type u_7} [Add β] [VAdd α β] [VAddCommClass α β β] (s : α) (x : β) (y : β) : x + (s +ᵥ y) = s +ᵥ (x + y)

theorem mul_smul_comm {α : Type u_6} {β : Type u_7} [Mul β] [SMul α β] [SMulCommClass α β β] (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_6} {β : Type u_7} [Add β] [VAdd α β] [VAddAssocClass α β β] (r : α) (x : β) (y : β) : r +ᵥ x + y = r +ᵥ (x + y)

theorem smul_mul_assoc {α : Type u_6} {β : Type u_7} [Mul β] [SMul α β] [IsScalarTower α β β] (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_6} {β : Type u_7} [SubNegMonoid β] [VAdd α β] [VAddAssocClass α β β] (r : α) (x : β) (y : β) : r +ᵥ x - y = r +ᵥ (x - y)

theorem smul_div_assoc {α : Type u_6} {β : Type u_7} [DivInvMonoid β] [SMul α β] [IsScalarTower α β β] (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_6} {β : Type u_7} {γ : Type u_8} {δ : Type u_9} [VAdd α β] [VAdd α γ] [VAdd β δ] [VAdd α δ] [VAdd γ δ] [VAddAssocClass α β δ] [VAddAssocClass α γ δ] [VAddCommClass β γ δ] (a : α) (b : β) (c : γ) (d : δ) : a +ᵥ b +ᵥ (c +ᵥ d) = a +ᵥ c +ᵥ (b +ᵥ d)

theorem smul_smul_smul_comm {α : Type u_6} {β : Type u_7} {γ : Type u_8} {δ : Type u_9} [SMul α β] [SMul α γ] [SMul β δ] [SMul α δ] [SMul γ δ] [IsScalarTower α β δ] [IsScalarTower α γ δ] [SMulCommClass β γ δ] (a : α) (b : β) (c : γ) (d : δ) : (a • b) • c • d = (a • c) • b • d

theorem AddCommute.vadd_right {M : Type u_1} {α : Type u_6} [VAdd M α] [Add α] [VAddCommClass M α α] [VAddAssocClass M α α] {a : α} {b : α} (h : AddCommute a b) (r : M) : AddCommute a (r +ᵥ b)

theorem Commute.smul_right {M : Type u_1} {α : Type u_6} [SMul M α] [Mul α] [SMulCommClass M α α] [IsScalarTower M α α] {a : α} {b : α} (h : Commute a b) (r : M) : Commute a (r • b)

theorem AddCommute.vadd_left {M : Type u_1} {α : Type u_6} [VAdd M α] [Add α] [VAddCommClass M α α] [VAddAssocClass M α α] {a : α} {b : α} (h : AddCommute a b) (r : M) : AddCommute (r +ᵥ a) b

theorem Commute.smul_left {M : Type u_1} {α : Type u_6} [SMul M α] [Mul α] [SMulCommClass M α α] [IsScalarTower M α α] {a : α} {b : α} (h : Commute a b) (r : M) : Commute (r • a) b

theorem vadd_vadd {M : Type u_1} {α : Type u_6} [AddMonoid M] [AddAction M α] (a₁ : M) (a₂ : M) (b : α) : a₁ +ᵥ (a₂ +ᵥ b) = a₁ + a₂ +ᵥ b

theorem smul_smul {M : Type u_1} {α : Type u_6} [Monoid M] [MulAction M α] (a₁ : M) (a₂ : M) (b : α) : a₁ • a₂ • b = (a₁ * a₂) • b

@[simp]

theorem zero_vadd (M : Type u_1) {α : Type u_6} [AddMonoid M] [AddAction M α] (b : α) : 0 +ᵥ b = b

@[simp]

theorem one_smul (M : Type u_1) {α : Type u_6} [Monoid M] [MulAction M α] (b : α) : 1 • b = b

theorem zero_vadd_eq_id (M : Type u_1) {α : Type u_6} [AddMonoid M] [AddAction M α] : (fun (x : α) => 0 +ᵥ x) = id

VAdd version of zero_add_eq_id

theorem one_smul_eq_id (M : Type u_1) {α : Type u_6} [Monoid M] [MulAction M α] : (fun (x : α) => 1 • x) = id

SMul version of one_mul_eq_id

theorem comp_vadd_left (M : Type u_1) {α : Type u_6} [AddMonoid M] [AddAction M α] (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_6} [Monoid M] [MulAction M α] (a₁ : M) (a₂ : M) : ((fun (x : α) => a₁ • x) ∘ fun (x : α) => a₂ • x) = fun (x : α) => (a₁ * a₂) • x

SMul version of comp_mul_left

@[reducible]

def Function.Injective.addAction {M : Type u_1} {α : Type u_6} {β : Type u_7} [AddMonoid M] [AddAction M α] [VAdd M β] (f : β → α) (hf : Function.Injective f) (smul : ∀ (c : M) (x : β), f (c +ᵥ x) = c +ᵥ f x) : AddAction M β

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

Equations

• Function.Injective.addAction f hf smul = AddAction.mk ⋯ ⋯

theorem Function.Injective.addAction.proof_1 {M : Type u_2} {α : Type u_3} {β : Type u_1} [AddMonoid M] [AddAction M α] [VAdd M β] (f : β → α) (hf : Function.Injective f) (smul : ∀ (c : M) (x : β), f (c +ᵥ x) = c +ᵥ f x) (x : β) : 0 +ᵥ x = x

theorem Function.Injective.addAction.proof_2 {M : Type u_2} {α : Type u_3} {β : Type u_1} [AddMonoid M] [AddAction M α] [VAdd M β] (f : β → α) (hf : Function.Injective f) (smul : ∀ (c : M) (x : β), f (c +ᵥ x) = c +ᵥ f x) (c₁ : M) (c₂ : M) (x : β) : c₁ + c₂ +ᵥ x = c₁ +ᵥ (c₂ +ᵥ x)

@[reducible]

def Function.Injective.mulAction {M : Type u_1} {α : Type u_6} {β : Type u_7} [Monoid M] [MulAction M α] [SMul M β] (f : β → α) (hf : Function.Injective f) (smul : ∀ (c : M) (x : β), f (c • x) = c • f x) : MulAction M β

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

Equations

• Function.Injective.mulAction f hf smul = MulAction.mk ⋯ ⋯

theorem Function.Surjective.addAction.proof_1 {M : Type u_2} {α : Type u_3} {β : Type u_1} [AddMonoid M] [AddAction M α] [VAdd M β] (f : α → β) (hf : Function.Surjective f) (smul : ∀ (c : M) (x : α), f (c +ᵥ x) = c +ᵥ f x) (y : β) : 0 +ᵥ y = y

@[reducible]

def Function.Surjective.addAction {M : Type u_1} {α : Type u_6} {β : Type u_7} [AddMonoid M] [AddAction M α] [VAdd M β] (f : α → β) (hf : Function.Surjective f) (smul : ∀ (c : M) (x : α), f (c +ᵥ x) = c +ᵥ f x) : AddAction M β

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

Equations

• Function.Surjective.addAction f hf smul = AddAction.mk ⋯ ⋯

theorem Function.Surjective.addAction.proof_2 {M : Type u_2} {α : Type u_3} {β : Type u_1} [AddMonoid M] [AddAction M α] [VAdd M β] (f : α → β) (hf : Function.Surjective f) (smul : ∀ (c : M) (x : α), f (c +ᵥ x) = c +ᵥ f x) (c₁ : M) (c₂ : M) (y : β) : c₁ + c₂ +ᵥ y = c₁ +ᵥ (c₂ +ᵥ y)

@[reducible]

def Function.Surjective.mulAction {M : Type u_1} {α : Type u_6} {β : Type u_7} [Monoid M] [MulAction M α] [SMul M β] (f : α → β) (hf : Function.Surjective f) (smul : ∀ (c : M) (x : α), f (c • x) = c • f x) : MulAction M β

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

Equations

• Function.Surjective.mulAction f hf smul = MulAction.mk ⋯ ⋯

theorem Function.Surjective.addActionLeft.proof_2 {R : Type u_3} {S : Type u_2} {M : Type u_1} [AddMonoid R] [AddAction R M] [AddMonoid S] [VAdd S M] (f : R →+ S) (hf : Function.Surjective ⇑f) (hsmul : ∀ (c : R) (x : M), f c +ᵥ x = c +ᵥ x) (y₁ : S) (y₂ : S) (b : M) : y₁ + y₂ +ᵥ b = y₁ +ᵥ (y₂ +ᵥ b)

@[reducible]

def Function.Surjective.addActionLeft {R : Type u_10} {S : Type u_11} {M : Type u_12} [AddMonoid R] [AddAction R M] [AddMonoid S] [VAdd S M] (f : R →+ S) (hf : Function.Surjective ⇑f) (hsmul : ∀ (c : R) (x : M), f c +ᵥ x = c +ᵥ x) : AddAction S M

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

Equations

• Function.Surjective.addActionLeft f hf hsmul = AddAction.mk ⋯ ⋯

theorem Function.Surjective.addActionLeft.proof_1 {R : Type u_3} {S : Type u_2} {M : Type u_1} [AddMonoid R] [AddAction R M] [AddMonoid S] [VAdd S M] (f : R →+ S) (hsmul : ∀ (c : R) (x : M), f c +ᵥ x = c +ᵥ x) (b : M) : 0 +ᵥ b = b

@[reducible]

def Function.Surjective.mulActionLeft {R : Type u_10} {S : Type u_11} {M : Type u_12} [Monoid R] [MulAction R M] [Monoid S] [SMul S M] (f : R →* S) (hf : Function.Surjective ⇑f) (hsmul : ∀ (c : R) (x : M), f c • x = c • x) : MulAction S M

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

• Function.Surjective.mulActionLeft f hf hsmul = MulAction.mk ⋯ ⋯

instance AddMonoid.toAddAction (M : Type u_1) [AddMonoid M] : AddAction M M

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

This is promoted to an AddTorsor by addGroup_is_addTorsor.

Equations

• AddMonoid.toAddAction M = AddAction.mk ⋯ ⋯

theorem AddMonoid.toAddAction.proof_1 (M : Type u_1) [AddMonoid M] (a : M) : 0 + a = a

theorem AddMonoid.toAddAction.proof_2 (M : Type u_1) [AddMonoid M] (a : M) (b : M) (c : M) : a + b + c = a + (b + c)

instance Monoid.toMulAction (M : Type u_1) [Monoid M] : MulAction M M

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

This is promoted to a module by Semiring.toModule.

Equations

• Monoid.toMulAction M = MulAction.mk ⋯ ⋯

instance VAddAssocClass.left (M : Type u_1) {α : Type u_6} [AddMonoid M] [AddAction M α] : VAddAssocClass M M α

Equations

• ⋯ = ⋯

instance IsScalarTower.left (M : Type u_1) {α : Type u_6} [Monoid M] [MulAction M α] : IsScalarTower M M α

Equations

• ⋯ = ⋯

theorem vadd_add_vadd {M : Type u_1} {α : Type u_6} [AddMonoid M] [AddAction M α] [Add α] (r : M) (s : M) (x : α) (y : α) [VAddAssocClass M α α] [VAddCommClass M α α] : r +ᵥ x + (s +ᵥ y) = r + s +ᵥ (x + y)

theorem smul_mul_smul {M : Type u_1} {α : Type u_6} [Monoid M] [MulAction M α] [Mul α] (r : M) (s : M) (x : α) (y : α) [IsScalarTower M α α] [SMulCommClass M α α] : r • x * s • y = (r * s) • (x * y)

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

theorem smul_pow {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] [MulAction M N] [IsScalarTower M N N] [SMulCommClass M N N] (r : M) (x : N) (n : ℕ) : (r • x) ^ n = r ^ n • x ^ n

theorem AddAction.toFun.proof_1 (M : Type u_1) (α : Type u_2) [AddMonoid M] [AddAction M α] (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_6) [AddMonoid M] [AddAction M α] : α ↪ M → α

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

Equations

• AddAction.toFun M α = { toFun := fun (y : α) (x : M) => x +ᵥ y, inj' := ⋯ }

def MulAction.toFun (M : Type u_1) (α : Type u_6) [Monoid M] [MulAction M α] : α ↪ M → α

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

Equations

• MulAction.toFun M α = { toFun := fun (y : α) (x : M) => x • y, inj' := ⋯ }

@[simp]

theorem AddAction.toFun_apply {M : Type u_1} {α : Type u_6} [AddMonoid M] [AddAction M α] (x : M) (y : α) : (AddAction.toFun M α) y x = x +ᵥ y

@[simp]

theorem MulAction.toFun_apply {M : Type u_1} {α : Type u_6} [Monoid M] [MulAction M α] (x : M) (y : α) : (MulAction.toFun M α) y x = x • y

@[reducible]

def AddAction.compHom {M : Type u_1} {N : Type u_2} (α : Type u_6) [AddMonoid M] [AddAction M α] [AddMonoid N] (g : N →+ M) : AddAction 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].

Equations

• AddAction.compHom α g = AddAction.mk ⋯ ⋯

theorem AddAction.compHom.proof_1 {M : Type u_3} {N : Type u_2} (α : Type u_1) [AddMonoid M] [AddAction M α] [AddMonoid N] (g : N →+ M) : ∀ (x : α), 0 +ᵥ x = x

theorem AddAction.compHom.proof_2 {M : Type u_3} {N : Type u_2} (α : Type u_1) [AddMonoid M] [AddAction M α] [AddMonoid N] (g : N →+ M) : ∀ (x x_1 : N) (x_2 : α), x + x_1 +ᵥ x_2 = x +ᵥ (x_1 +ᵥ x_2)

@[reducible]

def MulAction.compHom {M : Type u_1} {N : Type u_2} (α : Type u_6) [Monoid M] [MulAction M α] [Monoid N] (g : N →* M) : MulAction 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

• MulAction.compHom α g = MulAction.mk ⋯ ⋯

theorem AddAction.compHom_vadd_def {E : Type u_10} {F : Type u_11} {G : Type u_12} [AddMonoid E] [AddMonoid F] [AddAction F G] (f : E →+ F) (a : E) (x : G) : a +ᵥ x = f a +ᵥ x

theorem MulAction.compHom_smul_def {E : Type u_10} {F : Type u_11} {G : Type u_12} [Monoid E] [Monoid F] [MulAction F G] (f : E →* F) (a : E) (x : G) : a • x = f a • x

theorem AddAction.isPretransitive_compHom {E : Type u_10} {F : Type u_11} {G : Type u_12} [AddMonoid E] [AddMonoid F] [AddAction F G] [AddAction.IsPretransitive F G] {f : E →+ F} (hf : Function.Surjective ⇑f) : AddAction.IsPretransitive E G

theorem MulAction.isPretransitive_compHom {E : Type u_10} {F : Type u_11} {G : Type u_12} [Monoid E] [Monoid F] [MulAction F G] [MulAction.IsPretransitive F G] {f : E →* F} (hf : Function.Surjective ⇑f) : MulAction.IsPretransitive E G

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_10} {N : Type u_11} {α : Type u_12} [VAdd M α] [VAdd N α] [AddAction.IsPretransitive M α] (f : M → N) (hf : ∀ {c : M} {x : α}, f c +ᵥ x = c +ᵥ x) : AddAction.IsPretransitive N α

theorem MulAction.IsPretransitive.of_smul_eq {M : Type u_10} {N : Type u_11} {α : Type u_12} [SMul M α] [SMul N α] [MulAction.IsPretransitive M α] (f : M → N) (hf : ∀ {c : M} {x : α}, f c • x = c • x) : MulAction.IsPretransitive N α

theorem AddAction.IsPretransitive.of_compHom {M : Type u_10} {N : Type u_11} {α : Type u_12} [AddMonoid M] [AddMonoid N] [AddAction N α] (f : M →+ N) [h : AddAction.IsPretransitive M α] : AddAction.IsPretransitive N α

theorem MulAction.IsPretransitive.of_compHom {M : Type u_10} {N : Type u_11} {α : Type u_12} [Monoid M] [Monoid N] [MulAction N α] (f : M →* N) [h : MulAction.IsPretransitive M α] : MulAction.IsPretransitive N α

theorem vadd_zero_vadd {α : Type u_6} {M : Type u_10} (N : Type u_11) [AddMonoid N] [VAdd M N] [AddAction N α] [VAdd M α] [VAddAssocClass M N α] (x : M) (y : α) : x +ᵥ 0 +ᵥ y = x +ᵥ y

theorem smul_one_smul {α : Type u_6} {M : Type u_10} (N : Type u_11) [Monoid N] [SMul M N] [MulAction N α] [SMul M α] [IsScalarTower M N α] (x : M) (y : α) : (x • 1) • y = x • y

theorem AddAction.IsPretransitive.of_isScalarTower (M : Type u_10) {N : Type u_11} {α : Type u_12} [AddMonoid N] [VAdd M N] [AddAction N α] [VAdd M α] [VAddAssocClass M N α] [AddAction.IsPretransitive M α] : AddAction.IsPretransitive N α

theorem MulAction.IsPretransitive.of_isScalarTower (M : Type u_10) {N : Type u_11} {α : Type u_12} [Monoid N] [SMul M N] [MulAction N α] [SMul M α] [IsScalarTower M N α] [MulAction.IsPretransitive M α] : MulAction.IsPretransitive N α

@[simp]

theorem vadd_zero_add {M : Type u_10} {N : Type u_11} [AddZeroClass N] [VAdd M N] [VAddAssocClass M N N] (x : M) (y : N) : x +ᵥ 0 + y = x +ᵥ y

@[simp]

theorem smul_one_mul {M : Type u_10} {N : Type u_11} [MulOneClass N] [SMul M N] [IsScalarTower M N N] (x : M) (y : N) : x • 1 * y = x • y

@[simp]

theorem add_vadd_zero {M : Type u_10} {N : Type u_11} [AddZeroClass N] [VAdd M N] [VAddCommClass M N N] (x : M) (y : N) : y + (x +ᵥ 0) = x +ᵥ y

@[simp]

theorem mul_smul_one {M : Type u_10} {N : Type u_11} [MulOneClass N] [SMul M N] [SMulCommClass M N N] (x : M) (y : N) : y * x • 1 = x • y

theorem VAddAssocClass.of_vadd_zero_add {M : Type u_10} {N : Type u_11} [AddMonoid N] [VAdd M N] (h : ∀ (x : M) (y : N), x +ᵥ 0 + y = x +ᵥ y) : VAddAssocClass M N N

theorem IsScalarTower.of_smul_one_mul {M : Type u_10} {N : Type u_11} [Monoid N] [SMul M N] (h : ∀ (x : M) (y : N), x • 1 * y = x • y) : IsScalarTower M N N

theorem VAddCommClass.of_add_vadd_zero {M : Type u_10} {N : Type u_11} [AddMonoid N] [VAdd M N] (H : ∀ (x : M) (y : N), y + (x +ᵥ 0) = x +ᵥ y) : VAddCommClass M N N

theorem SMulCommClass.of_mul_smul_one {M : Type u_10} {N : Type u_11} [Monoid N] [SMul M N] (H : ∀ (x : M) (y : N), y * x • 1 = x • y) : SMulCommClass M N N

def AddMonoidHom.vaddZeroHom {M : Type u_10} {N : Type u_11} [AddMonoid M] [AddZeroClass N] [AddAction M N] [VAddAssocClass M N N] : 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 = { toZeroHom := { toFun := fun (x : M) => x +ᵥ 0, map_zero' := ⋯ }, map_add' := ⋯ }

theorem AddMonoidHom.vaddZeroHom.proof_1 {M : Type u_2} {N : Type u_1} [AddMonoid M] [AddZeroClass N] [AddAction M N] : 0 +ᵥ 0 = 0

theorem AddMonoidHom.vaddZeroHom.proof_2 {M : Type u_2} {N : Type u_1} [AddMonoid M] [AddZeroClass N] [AddAction M N] [VAddAssocClass M N N] (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

@[simp]

theorem MonoidHom.smulOneHom_apply {M : Type u_10} {N : Type u_11} [Monoid M] [MulOneClass N] [MulAction M N] [IsScalarTower M N N] (x : M) : MonoidHom.smulOneHom x = x • 1

@[simp]

theorem AddMonoidHom.vaddZeroHom_apply {M : Type u_10} {N : Type u_11} [AddMonoid M] [AddZeroClass N] [AddAction M N] [VAddAssocClass M N N] (x : M) : AddMonoidHom.vaddZeroHom x = x +ᵥ 0

def MonoidHom.smulOneHom {M : Type u_10} {N : Type u_11} [Monoid M] [MulOneClass N] [MulAction M N] [IsScalarTower M N N] : 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 = { toOneHom := { toFun := fun (x : M) => x • 1, map_one' := ⋯ }, map_mul' := ⋯ }

abbrev addMonoidHomEquivAddActionIsScalarTower.match_1 (M : Type u_1) (N : Type u_2) [AddMonoid M] [AddMonoid N] (motive : { _inst : AddAction M N // VAddAssocClass M N N } → Sort u_3) : (x : { _inst : AddAction M N // VAddAssocClass M N N }) → ((val : AddAction M N) → (property : VAddAssocClass M N N) → motive { val := val, property := property }) → motive x

Equations

• addMonoidHomEquivAddActionIsScalarTower.match_1 M N motive x h_1 = Subtype.casesOn x fun (val : AddAction M N) (property : VAddAssocClass M N N) => h_1 val property

theorem addMonoidHomEquivAddActionIsScalarTower.proof_3 (M : Type u_1) (N : Type u_2) [AddMonoid M] [AddMonoid N] : ∀ (x : { _inst : AddAction M N // VAddAssocClass M N N }), (fun (f : M →+ N) => { val := AddAction.compHom N f, property := ⋯ }) ((fun (x : { _inst : AddAction M N // VAddAssocClass M N N }) => addMonoidHomEquivAddActionIsScalarTower.match_1 M N (fun (x : { _inst : AddAction M N // VAddAssocClass M N N }) => M →+ N) x fun (val : AddAction M N) (property : VAddAssocClass M N N) => AddMonoidHom.vaddZeroHom) x) = x

def addMonoidHomEquivAddActionIsScalarTower (M : Type u_10) (N : Type u_11) [AddMonoid M] [AddMonoid N] : (M →+ N) ≃ { _inst : AddAction M N // VAddAssocClass M N N }

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.

theorem addMonoidHomEquivAddActionIsScalarTower.proof_1 (M : Type u_2) (N : Type u_1) [AddMonoid M] [AddMonoid N] (f : M →+ N) : VAddAssocClass M N N

theorem addMonoidHomEquivAddActionIsScalarTower.proof_2 (M : Type u_2) (N : Type u_1) [AddMonoid M] [AddMonoid N] (f : M →+ N) : (fun (x : { _inst : AddAction M N // VAddAssocClass M N N }) => addMonoidHomEquivAddActionIsScalarTower.match_1 M N (fun (x : { _inst : AddAction M N // VAddAssocClass M N N }) => M →+ N) x fun (val : AddAction M N) (property : VAddAssocClass M N N) => AddMonoidHom.vaddZeroHom) ((fun (f : M →+ N) => { val := AddAction.compHom N f, property := ⋯ }) f) = f

abbrev addMonoidHomEquivAddActionIsScalarTower.match_2 (M : Type u_1) (N : Type u_2) [AddMonoid M] [AddMonoid N] (motive : { _inst : AddAction M N // VAddAssocClass M N N } → Prop) : ∀ (x : { _inst : AddAction M N // VAddAssocClass M N N }), (∀ (val : AddAction M N) (property : VAddAssocClass M N N), motive { val := val, property := property }) → motive x

Equations

• ⋯ = ⋯

def monoidHomEquivMulActionIsScalarTower (M : Type u_10) (N : Type u_11) [Monoid M] [Monoid N] : (M →* N) ≃ { _inst : MulAction M N // IsScalarTower M N N }

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.

class SMulZeroClass (M : Type u_10) (A : Type u_11) [Zero A] extends SMul : Type (max u_10 u_11)

Typeclass for scalar multiplication that preserves 0 on the right.

• smul : M → A → A
• smul_zero : ∀ (a : M), a • 0 = 0

  Multiplying 0 by a scalar gives 0

@[simp]

theorem smul_zero {M : Type u_1} {A : Type u_4} [Zero A] [SMulZeroClass M A] (a : M) : a • 0 = 0

theorem smul_ite_zero {M : Type u_1} {A : Type u_4} [Zero A] [SMulZeroClass M A] (p : Prop) [Decidable p] (a : M) (b : A) : (a • if p then b else 0) = if p then a • b else 0

theorem smul_eq_zero_of_right {M : Type u_1} {A : Type u_4} [Zero A] [SMulZeroClass M A] (a : M) {b : A} (h : b = 0) : a • b = 0

theorem right_ne_zero_of_smul {M : Type u_1} {A : Type u_4} [Zero A] [SMulZeroClass M A] {a : M} {b : A} : a • b ≠ 0 → b ≠ 0

@[reducible]

def Function.Injective.smulZeroClass {M : Type u_1} {A : Type u_4} {B : Type u_5} [Zero A] [SMulZeroClass M A] [Zero B] [SMul M B] (f : ZeroHom B A) (hf : Function.Injective ⇑f) (smul : ∀ (c : M) (x : B), f (c • x) = c • f x) : SMulZeroClass M B

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

Equations

• Function.Injective.smulZeroClass f hf smul = SMulZeroClass.mk ⋯

@[reducible]

def ZeroHom.smulZeroClass {M : Type u_1} {A : Type u_4} {B : Type u_5} [Zero A] [SMulZeroClass M A] [Zero B] [SMul M B] (f : ZeroHom A B) (smul : ∀ (c : M) (x : A), f (c • x) = c • f x) : SMulZeroClass M B

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

Equations

• ZeroHom.smulZeroClass f smul = SMulZeroClass.mk ⋯

@[reducible]

def Function.Surjective.smulZeroClassLeft {R : Type u_10} {S : Type u_11} {M : Type u_12} [Zero M] [SMulZeroClass R M] [SMul S M] (f : R → S) (hf : Function.Surjective f) (hsmul : ∀ (c : R) (x : M), f c • x = c • x) : SMulZeroClass S M

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

See also Function.Surjective.distribMulActionLeft.

Equations

• Function.Surjective.smulZeroClassLeft f hf hsmul = SMulZeroClass.mk ⋯

@[reducible]

def SMulZeroClass.compFun {M : Type u_1} {N : Type u_2} (A : Type u_4) [Zero A] [SMulZeroClass M A] (f : N → M) : SMulZeroClass N A

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

Equations

• SMulZeroClass.compFun A f = SMulZeroClass.mk ⋯

@[simp]

theorem SMulZeroClass.toZeroHom_apply {M : Type u_1} (A : Type u_4) [Zero A] [SMulZeroClass M A] (x : M) : ∀ (x_1 : A), (SMulZeroClass.toZeroHom A x) x_1 = x • x_1

def SMulZeroClass.toZeroHom {M : Type u_1} (A : Type u_4) [Zero A] [SMulZeroClass M A] (x : M) : ZeroHom A A

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

Equations

• SMulZeroClass.toZeroHom A x = { toFun := fun (x_1 : A) => x • x_1, map_zero' := ⋯ }

theorem DistribSMul.ext_iff {M : Type u_10} {A : Type u_11} : ∀ {inst : AddZeroClass A} (x y : DistribSMul M A), x = y ↔ SMul.smul = SMul.smul

theorem DistribSMul.ext {M : Type u_10} {A : Type u_11} : ∀ {inst : AddZeroClass A} (x y : DistribSMul M A), SMul.smul = SMul.smul → x = y

class DistribSMul (M : Type u_10) (A : Type u_11) [AddZeroClass A] extends SMulZeroClass : Type (max u_10 u_11)

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

This is exactly DistribMulAction without the MulAction part.

• smul : M → A → A
• smul_zero : ∀ (a : M), a • 0 = 0
• smul_add : ∀ (a : M) (x y : A), a • (x + y) = a • x + a • y

  Scalar multiplication distributes across addition

theorem smul_add {M : Type u_1} {A : Type u_4} [AddZeroClass A] [DistribSMul M A] (a : M) (b₁ : A) (b₂ : A) : a • (b₁ + b₂) = a • b₁ + a • b₂

instance AddMonoidHom.smulZeroClass {M : Type u_1} {A : Type u_4} {B : Type u_5} [AddZeroClass A] [DistribSMul M A] [AddZeroClass B] : SMulZeroClass M (B →+ A)

Equations

• AddMonoidHom.smulZeroClass = SMulZeroClass.mk ⋯

@[reducible]

def Function.Injective.distribSMul {M : Type u_1} {A : Type u_4} {B : Type u_5} [AddZeroClass A] [DistribSMul M A] [AddZeroClass B] [SMul M B] (f : B →+ A) (hf : Function.Injective ⇑f) (smul : ∀ (c : M) (x : B), f (c • x) = c • f x) : DistribSMul M B

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

Equations

• Function.Injective.distribSMul f hf smul = let __src := Function.Injective.smulZeroClass (↑f) hf smul; DistribSMul.mk ⋯

@[reducible]

def Function.Surjective.distribSMul {M : Type u_1} {A : Type u_4} {B : Type u_5} [AddZeroClass A] [DistribSMul M A] [AddZeroClass B] [SMul M B] (f : A →+ B) (hf : Function.Surjective ⇑f) (smul : ∀ (c : M) (x : A), f (c • x) = c • f x) : DistribSMul M B

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

Equations

• Function.Surjective.distribSMul f hf smul = let __src := ZeroHom.smulZeroClass (↑f) smul; DistribSMul.mk ⋯

@[reducible]

def Function.Surjective.distribSMulLeft {R : Type u_10} {S : Type u_11} {M : Type u_12} [AddZeroClass M] [DistribSMul R M] [SMul S M] (f : R → S) (hf : Function.Surjective f) (hsmul : ∀ (c : R) (x : M), f c • x = c • x) : DistribSMul S M

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

See also Function.Surjective.distribMulActionLeft.

Equations

• Function.Surjective.distribSMulLeft f hf hsmul = let __src := Function.Surjective.smulZeroClassLeft f hf hsmul; DistribSMul.mk ⋯

@[reducible]

def DistribSMul.compFun {M : Type u_1} {N : Type u_2} (A : Type u_4) [AddZeroClass A] [DistribSMul M A] (f : N → M) : DistribSMul N A

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

Equations

• DistribSMul.compFun A f = let __src := SMulZeroClass.compFun A f; DistribSMul.mk ⋯

@[simp]

theorem DistribSMul.toAddMonoidHom_apply {M : Type u_1} (A : Type u_4) [AddZeroClass A] [DistribSMul M A] (x : M) : ∀ (x_1 : A), (DistribSMul.toAddMonoidHom A x) x_1 = (fun (x : M) (x_2 : A) => x • x_2) x x_1

def DistribSMul.toAddMonoidHom {M : Type u_1} (A : Type u_4) [AddZeroClass A] [DistribSMul M A] (x : M) : A →+ A

Each element of the scalars defines an additive monoid homomorphism.

Equations

• DistribSMul.toAddMonoidHom A x = let __src := SMulZeroClass.toZeroHom A x; { toZeroHom := { toFun := (fun (x : M) (x_1 : A) => x • x_1) x, map_zero' := ⋯ }, map_add' := ⋯ }

theorem DistribMulAction.ext {M : Type u_10} {A : Type u_11} : ∀ {inst : Monoid M} {inst_1 : AddMonoid A} (x y : DistribMulAction M A), SMul.smul = SMul.smul → x = y

theorem DistribMulAction.ext_iff {M : Type u_10} {A : Type u_11} : ∀ {inst : Monoid M} {inst_1 : AddMonoid A} (x y : DistribMulAction M A), x = y ↔ SMul.smul = SMul.smul

class DistribMulAction (M : Type u_10) (A : Type u_11) [Monoid M] [AddMonoid A] extends MulAction : Type (max u_10 u_11)

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

• smul : M → A → A
• one_smul : ∀ (b : A), 1 • b = b
• mul_smul : ∀ (x y : M) (b : A), (x * y) • b = x • y • b
• smul_zero : ∀ (a : M), a • 0 = 0

  Multiplying 0 by a scalar gives 0

• smul_add : ∀ (a : M) (x y : A), a • (x + y) = a • x + a • y

  Scalar multiplication distributes across addition

instance DistribMulAction.toDistribSMul {M : Type u_1} {A : Type u_4} [Monoid M] [AddMonoid A] [DistribMulAction M A] : DistribSMul M A

Equations

• DistribMulAction.toDistribSMul = let __src := inst; DistribSMul.mk ⋯

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

@[reducible]

def Function.Injective.distribMulAction {M : Type u_1} {A : Type u_4} {B : Type u_5} [Monoid M] [AddMonoid A] [DistribMulAction M A] [AddMonoid B] [SMul M B] (f : B →+ A) (hf : Function.Injective ⇑f) (smul : ∀ (c : M) (x : B), f (c • x) = c • f x) : DistribMulAction M B

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

Equations

• Function.Injective.distribMulAction f hf smul = let __src := Function.Injective.distribSMul f hf smul; let __src_1 := Function.Injective.mulAction (⇑f) hf smul; DistribMulAction.mk ⋯ ⋯

@[reducible]

def Function.Surjective.distribMulAction {M : Type u_1} {A : Type u_4} {B : Type u_5} [Monoid M] [AddMonoid A] [DistribMulAction M A] [AddMonoid B] [SMul M B] (f : A →+ B) (hf : Function.Surjective ⇑f) (smul : ∀ (c : M) (x : A), f (c • x) = c • f x) : DistribMulAction M B

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

Equations

• Function.Surjective.distribMulAction f hf smul = let __src := Function.Surjective.distribSMul f hf smul; let __src_1 := Function.Surjective.mulAction (⇑f) hf smul; DistribMulAction.mk ⋯ ⋯

@[reducible]

def Function.Surjective.distribMulActionLeft {R : Type u_10} {S : Type u_11} {M : Type u_12} [Monoid R] [AddMonoid M] [DistribMulAction R M] [Monoid S] [SMul S M] (f : R →* S) (hf : Function.Surjective ⇑f) (hsmul : ∀ (c : R) (x : M), f c • x = c • x) : DistribMulAction S M

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

See also Function.Surjective.mulActionLeft and Function.Surjective.moduleLeft.

Equations

• One or more equations did not get rendered due to their size.

@[reducible]

def DistribMulAction.compHom {M : Type u_1} {N : Type u_2} (A : Type u_4) [Monoid M] [AddMonoid A] [DistribMulAction M A] [Monoid N] (f : N →* M) : DistribMulAction N A

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

Equations

• DistribMulAction.compHom A f = let __src := DistribSMul.compFun A ⇑f; let __src_1 := MulAction.compHom A f; DistribMulAction.mk ⋯ ⋯

@[simp]

theorem DistribMulAction.toAddMonoidHom_apply {M : Type u_1} (A : Type u_4) [Monoid M] [AddMonoid A] [DistribMulAction M A] (x : M) : ∀ (x_1 : A), (DistribMulAction.toAddMonoidHom A x) x_1 = x • x_1

def DistribMulAction.toAddMonoidHom {M : Type u_1} (A : Type u_4) [Monoid M] [AddMonoid A] [DistribMulAction M A] (x : M) : A →+ A

Each element of the monoid defines an additive monoid homomorphism.

Equations

• DistribMulAction.toAddMonoidHom A x = DistribSMul.toAddMonoidHom A x

@[simp]

theorem DistribMulAction.toAddMonoidEnd_apply (M : Type u_1) (A : Type u_4) [Monoid M] [AddMonoid A] [DistribMulAction M A] (x : M) : (DistribMulAction.toAddMonoidEnd M A) x = DistribMulAction.toAddMonoidHom A x

def DistribMulAction.toAddMonoidEnd (M : Type u_1) (A : Type u_4) [Monoid M] [AddMonoid A] [DistribMulAction M A] : M →* AddMonoid.End A

Each element of the monoid defines an additive monoid homomorphism.

Equations

• DistribMulAction.toAddMonoidEnd M A = { toOneHom := { toFun := DistribMulAction.toAddMonoidHom A, map_one' := ⋯ }, map_mul' := ⋯ }

instance AddMonoid.nat_smulCommClass (M : Type u_1) (A : Type u_4) [Monoid M] [AddMonoid A] [DistribMulAction M A] : SMulCommClass ℕ M A

Equations

• ⋯ = ⋯

instance AddMonoid.nat_smulCommClass' (M : Type u_1) (A : Type u_4) [Monoid M] [AddMonoid A] [DistribMulAction M A] : SMulCommClass M ℕ A

Equations

• ⋯ = ⋯

instance AddGroup.int_smulCommClass {M : Type u_1} {A : Type u_4} [Monoid M] [AddGroup A] [DistribMulAction M A] : SMulCommClass ℤ M A

Equations

• ⋯ = ⋯

instance AddGroup.int_smulCommClass' {M : Type u_1} {A : Type u_4} [Monoid M] [AddGroup A] [DistribMulAction M A] : SMulCommClass M ℤ A

Equations

• ⋯ = ⋯

@[simp]

theorem smul_neg {M : Type u_1} {A : Type u_4} [Monoid M] [AddGroup A] [DistribMulAction M A] (r : M) (x : A) : r • -x = -(r • x)

theorem smul_sub {M : Type u_1} {A : Type u_4} [Monoid M] [AddGroup A] [DistribMulAction M A] (r : M) (x : A) (y : A) : r • (x - y) = r • x - r • y

theorem MulDistribMulAction.ext {M : Type u_10} {A : Type u_11} : ∀ {inst : Monoid M} {inst_1 : Monoid A} (x y : MulDistribMulAction M A), SMul.smul = SMul.smul → x = y

theorem MulDistribMulAction.ext_iff {M : Type u_10} {A : Type u_11} : ∀ {inst : Monoid M} {inst_1 : Monoid A} (x y : MulDistribMulAction M A), x = y ↔ SMul.smul = SMul.smul

class MulDistribMulAction (M : Type u_10) (A : Type u_11) [Monoid M] [Monoid A] extends MulAction : Type (max u_10 u_11)

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

• smul : M → A → A
• one_smul : ∀ (b : A), 1 • b = b
• mul_smul : ∀ (x y : M) (b : A), (x * y) • b = x • y • b
• smul_mul : ∀ (r : M) (x y : A), r • (x * y) = r • x * r • y

  Distributivity of • across *

• smul_one : ∀ (r : M), r • 1 = 1

  Multiplying 1 by a scalar gives 1

theorem smul_mul' {M : Type u_1} {A : Type u_4} [Monoid M] [Monoid A] [MulDistribMulAction M A] (a : M) (b₁ : A) (b₂ : A) : a • (b₁ * b₂) = a • b₁ * a • b₂

@[reducible]

def Function.Injective.mulDistribMulAction {M : Type u_1} {A : Type u_4} {B : Type u_5} [Monoid M] [Monoid A] [MulDistribMulAction M A] [Monoid B] [SMul M B] (f : B →* A) (hf : Function.Injective ⇑f) (smul : ∀ (c : M) (x : B), f (c • x) = c • f x) : MulDistribMulAction M B

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

Equations

• Function.Injective.mulDistribMulAction f hf smul = let __src := Function.Injective.mulAction (⇑f) hf smul; MulDistribMulAction.mk ⋯ ⋯

@[reducible]

def Function.Surjective.mulDistribMulAction {M : Type u_1} {A : Type u_4} {B : Type u_5} [Monoid M] [Monoid A] [MulDistribMulAction M A] [Monoid B] [SMul M B] (f : A →* B) (hf : Function.Surjective ⇑f) (smul : ∀ (c : M) (x : A), f (c • x) = c • f x) : MulDistribMulAction M B

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

Equations

• Function.Surjective.mulDistribMulAction f hf smul = let __src := Function.Surjective.mulAction (⇑f) hf smul; MulDistribMulAction.mk ⋯ ⋯

@[reducible]

def MulDistribMulAction.compHom {M : Type u_1} {N : Type u_2} (A : Type u_4) [Monoid M] [Monoid A] [MulDistribMulAction M A] [Monoid N] (f : N →* M) : MulDistribMulAction N A

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

Equations

• MulDistribMulAction.compHom A f = let __src := MulAction.compHom A f; MulDistribMulAction.mk ⋯ ⋯

def MulDistribMulAction.toMonoidHom {M : Type u_1} (A : Type u_4) [Monoid M] [Monoid A] [MulDistribMulAction M A] (r : M) : A →* A

Scalar multiplication by r as a MonoidHom.

Equations

• MulDistribMulAction.toMonoidHom A r = { toOneHom := { toFun := fun (x : A) => r • x, map_one' := ⋯ }, map_mul' := ⋯ }

@[simp]

theorem MulDistribMulAction.toMonoidHom_apply {M : Type u_1} {A : Type u_4} [Monoid M] [Monoid A] [MulDistribMulAction M A] (r : M) (x : A) : (MulDistribMulAction.toMonoidHom A r) x = r • x

@[simp]

theorem smul_pow' {M : Type u_1} {A : Type u_4} [Monoid M] [Monoid A] [MulDistribMulAction M A] (r : M) (x : A) (n : ℕ) : r • x ^ n = (r • x) ^ n

@[simp]

theorem MulDistribMulAction.toMonoidEnd_apply (M : Type u_1) (A : Type u_4) [Monoid M] [Monoid A] [MulDistribMulAction M A] (r : M) : (MulDistribMulAction.toMonoidEnd M A) r = MulDistribMulAction.toMonoidHom A r

def MulDistribMulAction.toMonoidEnd (M : Type u_1) (A : Type u_4) [Monoid M] [Monoid A] [MulDistribMulAction M A] : M →* Monoid.End A

Each element of the monoid defines a monoid homomorphism.

Equations

• MulDistribMulAction.toMonoidEnd M A = { toOneHom := { toFun := MulDistribMulAction.toMonoidHom A, map_one' := ⋯ }, map_mul' := ⋯ }

@[simp]

theorem smul_inv' {M : Type u_1} {A : Type u_4} [Monoid M] [Group A] [MulDistribMulAction 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] [MulDistribMulAction M A] (r : M) (x : A) (y : A) : r • (x / y) = r • x / r • y

def Function.End (α : Type u_6) : Type u_6

The monoid of endomorphisms.

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

Equations

• Function.End α = (α → α)

instance instMonoidEnd (α : Type u_6) : Monoid (Function.End α)

Equations

• instMonoidEnd α = Monoid.mk ⋯ ⋯ npowRec ⋯ ⋯

instance instInhabitedEnd (α : Type u_6) : Inhabited (Function.End α)

Equations

• instInhabitedEnd α = { default := 1 }

instance Function.End.applyMulAction {α : Type u_6} : MulAction (Function.End α) α

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 = MulAction.mk ⋯ ⋯

@[simp]

theorem Function.End.smul_def {α : Type u_6} (f : Function.End α) (a : α) : f • a = f a

theorem Function.End.mul_def {α : Type u_6} (f : Function.End α) (g : Function.End α) : f * g = f ∘ g

theorem Function.End.one_def {α : Type u_6} : 1 = id

instance Function.End.apply_FaithfulSMul {α : Type u_6} : FaithfulSMul (Function.End α) α

Function.End.applyMulAction is faithful.

Equations

• ⋯ = ⋯

instance AddMonoid.End.applyDistribMulAction {α : Type u_6} [AddMonoid α] : DistribMulAction (AddMonoid.End α) α

The tautological action by AddMonoid.End α on α.

This generalizes Function.End.applyMulAction.

Equations

• AddMonoid.End.applyDistribMulAction = DistribMulAction.mk ⋯ ⋯

@[simp]

theorem AddMonoid.End.smul_def {α : Type u_6} [AddMonoid α] (f : AddMonoid.End α) (a : α) : f • a = f a

instance AddMonoid.End.applyFaithfulSMul {α : Type u_6} [AddMonoid α] : FaithfulSMul (AddMonoid.End α) α

AddMonoid.End.applyDistribMulAction is faithful.

Equations

• ⋯ = ⋯

def MulAction.toEndHom {M : Type u_1} {α : Type u_6} [Monoid M] [MulAction M α] : M →* Function.End α

The monoid hom representing a monoid action.

When M is a group, see MulAction.toPermHom.

Equations

• MulAction.toEndHom = { toOneHom := { toFun := fun (x : M) (x_1 : α) => x • x_1, map_one' := ⋯ }, map_mul' := ⋯ }

@[reducible]

def MulAction.ofEndHom {M : Type u_1} {α : Type u_6} [Monoid M] (f : M →* Function.End α) : MulAction M α

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

See note [reducible non-instances].

Equations

• MulAction.ofEndHom f = MulAction.compHom α f

Additive, Multiplicative

instance Additive.vadd {α : Type u_6} {β : Type u_7} [SMul α β] : VAdd (Additive α) β

Equations

• Additive.vadd = { vadd := fun (a : Additive α) (x : β) => Additive.toMul a • x }

instance Multiplicative.smul {α : Type u_6} {β : Type u_7} [VAdd α β] : SMul (Multiplicative α) β

Equations

• Multiplicative.smul = { smul := fun (a : Multiplicative α) (x : β) => Multiplicative.toAdd a +ᵥ x }

@[simp]

theorem toMul_smul {α : Type u_6} {β : Type u_7} [SMul α β] (a : Additive α) (b : β) : Additive.toMul a • b = a +ᵥ b

@[simp]

theorem ofMul_vadd {α : Type u_6} {β : Type u_7} [SMul α β] (a : α) (b : β) : Additive.ofMul a +ᵥ b = a • b

@[simp]

theorem toAdd_vadd {α : Type u_6} {β : Type u_7} [VAdd α β] (a : Multiplicative α) (b : β) : Multiplicative.toAdd a +ᵥ b = a • b

@[simp]

theorem ofAdd_smul {α : Type u_6} {β : Type u_7} [VAdd α β] (a : α) (b : β) : Multiplicative.ofAdd a • b = a +ᵥ b

instance Additive.addAction {α : Type u_6} {β : Type u_7} [Monoid α] [MulAction α β] : AddAction (Additive α) β

Equations

• Additive.addAction = AddAction.mk ⋯ ⋯

instance Multiplicative.mulAction {α : Type u_6} {β : Type u_7} [AddMonoid α] [AddAction α β] : MulAction (Multiplicative α) β

Equations

• Multiplicative.mulAction = MulAction.mk ⋯ ⋯

instance Additive.addAction_isPretransitive {α : Type u_6} {β : Type u_7} [Monoid α] [MulAction α β] [MulAction.IsPretransitive α β] : AddAction.IsPretransitive (Additive α) β

Equations

• ⋯ = ⋯

instance Multiplicative.mulAction_isPretransitive {α : Type u_6} {β : Type u_7} [AddMonoid α] [AddAction α β] [AddAction.IsPretransitive α β] : MulAction.IsPretransitive (Multiplicative α) β

Equations

• ⋯ = ⋯

instance Additive.vaddCommClass {α : Type u_6} {β : Type u_7} {γ : Type u_8} [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : VAddCommClass (Additive α) (Additive β) γ

Equations

• ⋯ = ⋯

instance Multiplicative.smulCommClass {α : Type u_6} {β : Type u_7} {γ : Type u_8} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : SMulCommClass (Multiplicative α) (Multiplicative β) γ

Equations

• ⋯ = ⋯

instance AddAction.functionEnd {α : Type u_6} : AddAction (Additive (Function.End α)) α

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

Equations

• AddAction.functionEnd = inferInstance

def AddAction.toEndHom {M : Type u_1} {α : Type u_6} [AddMonoid M] [AddAction M α] : M →+ Additive (Function.End α)

The additive monoid hom representing an additive monoid action.

When M is a group, see AddAction.toPermHom.

Equations

• AddAction.toEndHom = MonoidHom.toAdditive'' MulAction.toEndHom

@[reducible]

def AddAction.ofEndHom {M : Type u_1} {α : Type u_6} [AddMonoid M] (f : M →+ Additive (Function.End α)) : AddAction M α

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

See note [reducible non-instances].

Equations

• AddAction.ofEndHom f = AddAction.compHom α f