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 #

source

class FaithfulVAdd (G : Type u_11) (P : Type u_12) [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.

Instances

source

theorem FaithfulVAdd.eq_of_vadd_eq_vadd {G : Type u_11} {P : Type u_12} [VAdd G P] [self : FaithfulVAdd G P] {g₁ : G} {g₂ : G} :

(∀ (p : P), g₁ +ᵥ p = g₂ +ᵥ p) → g₁ = g₂

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

source

class FaithfulSMul (M : Type u_11) (α : Type u_12) [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.

Instances

source

theorem FaithfulSMul.eq_of_smul_eq_smul {M : Type u_11} {α : Type u_12} [SMul M α] [self : FaithfulSMul M α] {m₁ : M} {m₂ : M} :

(∀ (a : α), m₁ • a = m₂ • a) → m₁ = m₂

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

source

theorem vadd_left_injective' {M : Type u_1} {α : Type u_7} [VAdd M α] [FaithfulVAdd M α] :

Function.Injective fun (x : M) (x_1 : α) => x +ᵥ x_1

source

theorem smul_left_injective' {M : Type u_1} {α : Type u_7} [SMul M α] [FaithfulSMul M α] :

Function.Injective fun (x : M) (x_1 : α) => x • x_1

source

@[instance 910]

instance Add.toVAdd (α : Type u_11) [Add α] :

VAdd α α

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

source

class AddAction.IsPretransitive (M : Type u_11) (α : Type u_12) [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.

Instances

source

theorem AddAction.IsPretransitive.exists_vadd_eq {M : Type u_11} {α : Type u_12} [VAdd M α] [self : AddAction.IsPretransitive M α] (x : α) (y : α) :

∃ (g : M), g +ᵥ x = y

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

source

class MulAction.IsPretransitive (M : Type u_11) (α : Type u_12) [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.

Instances

source

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

∃ (g : M), g • x = y

There is g such that g • x = y.

source

theorem AddAction.exists_vadd_eq (M : Type u_1) {α : Type u_7} [VAdd M α] [AddAction.IsPretransitive M α] (x : α) (y : α) :

∃ (m : M), m +ᵥ x = y

source

theorem MulAction.exists_smul_eq (M : Type u_1) {α : Type u_7} [SMul M α] [MulAction.IsPretransitive M α] (x : α) (y : α) :

∃ (m : M), m • x = y

source

theorem AddAction.surjective_vadd (M : Type u_1) {α : Type u_7} [VAdd M α] [AddAction.IsPretransitive M α] (x : α) :

Function.Surjective fun (c : M) => c +ᵥ x

source

theorem MulAction.surjective_smul (M : Type u_1) {α : Type u_7} [SMul M α] [MulAction.IsPretransitive M α] (x : α) :

Function.Surjective fun (c : M) => c • x

source

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

⋯ = ⋯

source

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 #

source

class VAddCommClass (M : Type u_11) (N : Type u_12) (α : Type u_13) [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

Instances

source

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

m +ᵥ (n +ᵥ a) = n +ᵥ (m +ᵥ a)

+ᵥ is left commutative

source

class SMulCommClass (M : Type u_11) (N : Type u_12) (α : Type u_13) [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

Instances

source

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

m • n • a = n • m • a

• is left commutative

source

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

source

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

source

theorem Function.Injective.vaddCommClass {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [VAdd M α] [VAdd N α] [VAdd M β] [VAdd N β] [VAddCommClass 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) :

VAddCommClass M N α

source

theorem Function.Injective.smulCommClass {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [SMul M α] [SMul N α] [SMul M β] [SMul N β] [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 α

source

theorem Function.Surjective.vaddCommClass {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [VAdd M α] [VAdd N α] [VAdd M β] [VAdd N β] [VAddCommClass 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) :

VAddCommClass M N β

source

theorem Function.Surjective.smulCommClass {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [SMul M α] [SMul N α] [SMul M β] [SMul N β] [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 β

source

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

VAddCommClass M M α

Equations

⋯ = ⋯

source

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

SMulCommClass M M α

Equations

⋯ = ⋯

source

class VAddAssocClass (M : Type u_11) (N : Type u_12) (α : Type u_13) [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 +ᵥ

Instances

source

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

x +ᵥ y +ᵥ z = x +ᵥ (y +ᵥ z)

Associativity of +ᵥ

source

class IsScalarTower (M : Type u_11) (N : Type u_12) (α : Type u_13) [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 •

Instances

source

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

(x • y) • z = x • y • z

Associativity of •

source

@[simp]

theorem vadd_assoc {α : Type u_7} {M : Type u_11} {N : Type u_12} [VAdd M N] [VAdd N α] [VAdd M α] [VAddAssocClass M N α] (x : M) (y : N) (z : α) :

x +ᵥ y +ᵥ z = x +ᵥ (y +ᵥ z)

source

@[simp]

theorem smul_assoc {α : Type u_7} {M : Type u_11} {N : Type u_12} [SMul M N] [SMul N α] [SMul M α] [IsScalarTower M N α] (x : M) (y : N) (z : α) :

(x • y) • z = x • y • z

source

instance AddSemigroup.isScalarTower {α : Type u_7} [AddSemigroup α] :

VAddAssocClass α α α

Equations

⋯ = ⋯

source

instance Semigroup.isScalarTower {α : Type u_7} [Semigroup α] :

IsScalarTower α α α

Equations

⋯ = ⋯

source

class IsCentralVAdd (M : Type u_11) (α : Type u_12) [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.

Instances

source

theorem IsCentralVAdd.op_vadd_eq_vadd {M : Type u_11} {α : Type u_12} [VAdd M α] [VAdd Mᵃᵒᵖ α] [self : IsCentralVAdd M α] (m : M) (a : α) :

AddOpposite.op m +ᵥ a = m +ᵥ a

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

source

class IsCentralScalar (M : Type u_11) (α : Type u_12) [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.

Instances

source

@[simp]

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

MulOpposite.op m • a = m • a

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

source

theorem IsCentralVAdd.unop_vadd_eq_vadd {M : Type u_11} {α : Type u_12} [VAdd M α] [VAdd Mᵃᵒᵖ α] [IsCentralVAdd M α] (m : Mᵃᵒᵖ) (a : α) :

AddOpposite.unop m +ᵥ a = m +ᵥ a

source

theorem IsCentralScalar.unop_smul_eq_smul {M : Type u_11} {α : Type u_12} [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] (m : Mᵐᵒᵖ) (a : α) :

MulOpposite.unop m • a = m • a

source

@[instance 50]

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

VAddCommClass Mᵃᵒᵖ N α

Equations

⋯ = ⋯

source

@[instance 50]

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

SMulCommClass Mᵐᵒᵖ N α

Equations

⋯ = ⋯

source

@[instance 50]

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

VAddCommClass M Nᵃᵒᵖ α

Equations

⋯ = ⋯

source

@[instance 50]

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

SMulCommClass M Nᵐᵒᵖ α

Equations

⋯ = ⋯

source

@[instance 50]

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

VAddAssocClass Mᵃᵒᵖ N α

Equations

⋯ = ⋯

source

@[instance 50]

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

IsScalarTower Mᵐᵒᵖ N α

Equations

⋯ = ⋯

source

@[instance 50]

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

VAddAssocClass M Nᵃᵒᵖ α

Equations

⋯ = ⋯

source

@[instance 50]

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

IsScalarTower M Nᵐᵒᵖ α

Equations

⋯ = ⋯

source

def VAdd.comp.vadd {M : Type u_1} {N : Type u_2} {α : Type u_7} [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

source

def SMul.comp.smul {M : Type u_1} {N : Type u_2} {α : Type u_7} [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

source

@[reducible]

def VAdd.comp {M : Type u_1} {N : Type u_2} (α : Type u_7) [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 }

source

@[reducible]

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

SMul N α

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

Equations

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

source

theorem VAdd.comp.isScalarTower {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [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.

source

theorem SMul.comp.isScalarTower {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [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.

source

theorem VAdd.comp.vaddCommClass {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [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.

source

theorem SMul.comp.smulCommClass {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [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.

source

theorem VAdd.comp.vaddCommClass' {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [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.

source

theorem SMul.comp.smulCommClass' {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [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.

source

theorem add_vadd_comm {α : Type u_7} {β : Type u_8} [Add β] [VAdd α β] [VAddCommClass α β β] (s : α) (x : β) (y : β) :

x + (s +ᵥ y) = s +ᵥ (x + y)

source

theorem mul_smul_comm {α : Type u_7} {β : Type u_8} [Mul β] [SMul α β] [SMulCommClass α β β] (s : α) (x : β) (y : β) :

x * s • y = s • (x * y)

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

source

theorem vadd_add_assoc {α : Type u_7} {β : Type u_8} [Add β] [VAdd α β] [VAddAssocClass α β β] (r : α) (x : β) (y : β) :

r +ᵥ x + y = r +ᵥ (x + y)

source

theorem smul_mul_assoc {α : Type u_7} {β : Type u_8} [Mul β] [SMul α β] [IsScalarTower α β β] (r : α) (x : β) (y : β) :

r • x * y = r • (x * y)

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

source

theorem vadd_sub_assoc {α : Type u_7} {β : Type u_8} [SubNegMonoid β] [VAdd α β] [VAddAssocClass α β β] (r : α) (x : β) (y : β) :

r +ᵥ x - y = r +ᵥ (x - y)

source

theorem smul_div_assoc {α : Type u_7} {β : Type u_8} [DivInvMonoid β] [SMul α β] [IsScalarTower α β β] (r : α) (x : β) (y : β) :

r • x / y = r • (x / y)

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

source

theorem vadd_vadd_vadd_comm {α : Type u_7} {β : Type u_8} {γ : Type u_9} {δ : Type u_10} [VAdd α β] [VAdd α γ] [VAdd β δ] [VAdd α δ] [VAdd γ δ] [VAddAssocClass α β δ] [VAddAssocClass α γ δ] [VAddCommClass β γ δ] (a : α) (b : β) (c : γ) (d : δ) :

a +ᵥ b +ᵥ (c +ᵥ d) = a +ᵥ c +ᵥ (b +ᵥ d)

source

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

(a • b) • c • d = (a • c) • b • d

source

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

AddCommute a (r +ᵥ b)

source

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

Commute a (r • b)

source

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

AddCommute (r +ᵥ a) b

source

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

Commute (r • a) b

source

theorem vadd_vadd {M : Type u_1} {α : Type u_7} [AddMonoid M] [AddAction M α] (a₁ : M) (a₂ : M) (b : α) :

a₁ +ᵥ (a₂ +ᵥ b) = a₁ + a₂ +ᵥ b

source

theorem smul_smul {M : Type u_1} {α : Type u_7} [Monoid M] [MulAction M α] (a₁ : M) (a₂ : M) (b : α) :

a₁ • a₂ • b = (a₁ * a₂) • b

source

@[simp]

theorem zero_vadd (M : Type u_1) {α : Type u_7} [AddMonoid M] [AddAction M α] (b : α) :

0 +ᵥ b = b

source

@[simp]

theorem one_smul (M : Type u_1) {α : Type u_7} [Monoid M] [MulAction M α] (b : α) :

1 • b = b

source

theorem zero_vadd_eq_id (M : Type u_1) {α : Type u_7} [AddMonoid M] [AddAction M α] :

(fun (x : α) => 0 +ᵥ x) = id

VAdd version of zero_add_eq_id

source

theorem one_smul_eq_id (M : Type u_1) {α : Type u_7} [Monoid M] [MulAction M α] :

(fun (x : α) => 1 • x) = id

SMul version of one_mul_eq_id

source

theorem comp_vadd_left (M : Type u_1) {α : Type u_7} [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

source

theorem comp_smul_left (M : Type u_1) {α : Type u_7} [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

source

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

source

@[reducible]

def Function.Injective.addAction {M : Type u_1} {α : Type u_7} {β : Type u_8} [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 ⋯ ⋯

source

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)

source

@[reducible]

def Function.Injective.mulAction {M : Type u_1} {α : Type u_7} {β : Type u_8} [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 ⋯ ⋯

source

@[reducible]

def Function.Surjective.addAction {M : Type u_1} {α : Type u_7} {β : Type u_8} [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 ⋯ ⋯

source

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

source

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) (a : M) (a : M) (y : β) :

a✝ + a +ᵥ y = a✝ +ᵥ (a +ᵥ y)

source

@[reducible]

def Function.Surjective.mulAction {M : Type u_1} {α : Type u_7} {β : Type u_8} [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 ⋯ ⋯

source

@[reducible]

def Function.Surjective.addActionLeft {R : Type u_11} {S : Type u_12} {M : Type u_13} [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 ⋯ ⋯

source

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

source

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)

source

@[reducible]

def Function.Surjective.mulActionLeft {R : Type u_11} {S : Type u_12} {M : Type u_13} [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 ⋯ ⋯

source

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

a + b + c = a + (b + c)

source

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

0 + a = a

source

@[instance 910]

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 ⋯ ⋯

source

@[instance 910]

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 ⋯ ⋯

source

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

VAddAssocClass M M α

Equations

⋯ = ⋯

source

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

IsScalarTower M M α

Equations

⋯ = ⋯

source

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

r +ᵥ x + (s +ᵥ y) = r + s +ᵥ (x + y)

source

theorem smul_mul_smul {M : Type u_1} {α : Type u_7} [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 α.

source

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

source

@[simp]

theorem neg_vadd_vadd {G : Type u_3} {α : Type u_7} [AddGroup G] [AddAction G α] (g : G) (a : α) :

-g +ᵥ (g +ᵥ a) = a

source

@[simp]

theorem inv_smul_smul {G : Type u_3} {α : Type u_7} [Group G] [MulAction G α] (g : G) (a : α) :

g⁻¹ • g • a = a

source

@[simp]

theorem vadd_neg_vadd {G : Type u_3} {α : Type u_7} [AddGroup G] [AddAction G α] (g : G) (a : α) :

g +ᵥ (-g +ᵥ a) = a

source

@[simp]

theorem smul_inv_smul {G : Type u_3} {α : Type u_7} [Group G] [MulAction G α] (g : G) (a : α) :

g • g⁻¹ • a = a

source

theorem neg_vadd_eq_iff {G : Type u_3} {α : Type u_7} [AddGroup G] [AddAction G α] {g : G} {a : α} {b : α} :

-g +ᵥ a = b ↔ a = g +ᵥ b

source

theorem inv_smul_eq_iff {G : Type u_3} {α : Type u_7} [Group G] [MulAction G α] {g : G} {a : α} {b : α} :

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

source

theorem eq_neg_vadd_iff {G : Type u_3} {α : Type u_7} [AddGroup G] [AddAction G α] {g : G} {a : α} {b : α} :

a = -g +ᵥ b ↔ g +ᵥ a = b

source

theorem eq_inv_smul_iff {G : Type u_3} {α : Type u_7} [Group G] [MulAction G α] {g : G} {a : α} {b : α} :

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

source

@[simp]

theorem Commute.smul_right_iff {G : Type u_3} {H : Type u_4} [Group G] [Mul H] [MulAction G H] [SMulCommClass G H H] [IsScalarTower G H H] {g : G} {a : H} {b : H} :

Commute a (g • b) ↔ Commute a b

source

@[simp]

theorem Commute.smul_left_iff {G : Type u_3} {H : Type u_4} [Group G] [Mul H] [MulAction G H] [SMulCommClass G H H] [IsScalarTower G H H] {g : G} {a : H} {b : H} :

Commute (g • a) b ↔ Commute a b

source

theorem smul_inv {G : Type u_3} {H : Type u_4} [Group G] [Group H] [MulAction G H] [SMulCommClass G H H] [IsScalarTower G H H] (g : G) (a : H) :

(g • a)⁻¹ = g⁻¹ • a⁻¹

source

theorem smul_zpow {G : Type u_3} {H : Type u_4} [Group G] [Group H] [MulAction G H] [SMulCommClass G H H] [IsScalarTower G H H] (g : G) (a : H) (n : ℤ) :

(g • a) ^ n = g ^ n • a ^ n

source

theorem SMulCommClass.of_commMonoid (A : Type u_11) (B : Type u_12) (G : Type u_13) [CommMonoid G] [SMul A G] [SMul B G] [IsScalarTower A G G] [IsScalarTower B G G] :

SMulCommClass A B G

source

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₂

source

def AddAction.toFun (M : Type u_1) (α : Type u_7) [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' := ⋯ }

source

def MulAction.toFun (M : Type u_1) (α : Type u_7) [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' := ⋯ }

source

@[simp]

theorem AddAction.toFun_apply {M : Type u_1} {α : Type u_7} [AddMonoid M] [AddAction M α] (x : M) (y : α) :

(AddAction.toFun M α) y x = x +ᵥ y

source

@[simp]

theorem MulAction.toFun_apply {M : Type u_1} {α : Type u_7} [Monoid M] [MulAction M α] (x : M) (y : α) :

(MulAction.toFun M α) y x = x • y

source

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

source

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)

source

@[reducible]

def AddAction.compHom {M : Type u_1} {N : Type u_2} (α : Type u_7) [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 ⋯ ⋯

source

@[reducible]

def MulAction.compHom {M : Type u_1} {N : Type u_2} (α : Type u_7) [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 ⋯ ⋯

source

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

a +ᵥ x = f a +ᵥ x

source

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

a • x = f a • x

source

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

AddAction.IsPretransitive E G

source

theorem MulAction.isPretransitive_compHom {E : Type u_11} {F : Type u_12} {G : Type u_13} [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.

source

theorem AddAction.IsPretransitive.of_vadd_eq {M : Type u_11} {N : Type u_12} {α : Type u_13} [VAdd M α] [VAdd N α] [AddAction.IsPretransitive M α] (f : M → N) (hf : ∀ {c : M} {x : α}, f c +ᵥ x = c +ᵥ x) :

AddAction.IsPretransitive N α

source

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

MulAction.IsPretransitive N α

source

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

AddAction.IsPretransitive N α

source

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

MulAction.IsPretransitive N α

source

theorem vadd_zero_vadd {α : Type u_7} {M : Type u_11} (N : Type u_12) [AddMonoid N] [VAdd M N] [AddAction N α] [VAdd M α] [VAddAssocClass M N α] (x : M) (y : α) :

x +ᵥ 0 +ᵥ y = x +ᵥ y

source

theorem smul_one_smul {α : Type u_7} {M : Type u_11} (N : Type u_12) [Monoid N] [SMul M N] [MulAction N α] [SMul M α] [IsScalarTower M N α] (x : M) (y : α) :

(x • 1) • y = x • y

source

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

AddAction.IsPretransitive N α

source

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

MulAction.IsPretransitive N α

source

@[simp]

theorem vadd_zero_add {M : Type u_11} {N : Type u_12} [AddZeroClass N] [VAdd M N] [VAddAssocClass M N N] (x : M) (y : N) :

x +ᵥ 0 + y = x +ᵥ y

source

@[simp]

theorem smul_one_mul {M : Type u_11} {N : Type u_12} [MulOneClass N] [SMul M N] [IsScalarTower M N N] (x : M) (y : N) :

x • 1 * y = x • y

source

@[simp]

theorem add_vadd_zero {M : Type u_11} {N : Type u_12} [AddZeroClass N] [VAdd M N] [VAddCommClass M N N] (x : M) (y : N) :

y + (x +ᵥ 0) = x +ᵥ y

source

@[simp]

theorem mul_smul_one {M : Type u_11} {N : Type u_12} [MulOneClass N] [SMul M N] [SMulCommClass M N N] (x : M) (y : N) :

y * x • 1 = x • y

source

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

VAddAssocClass M N N

source

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

IsScalarTower M N N

source

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

VAddCommClass M N N

source

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

SMulCommClass M N N

source

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

source

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

0 +ᵥ 0 = 0

source

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

source

@[simp]

theorem AddMonoidHom.vaddZeroHom_apply {M : Type u_11} {N : Type u_12} [AddMonoid M] [AddZeroClass N] [AddAction M N] [VAddAssocClass M N N] (x : M) :

AddMonoidHom.vaddZeroHom x = x +ᵥ 0

source

@[simp]

theorem MonoidHom.smulOneHom_apply {M : Type u_11} {N : Type u_12} [Monoid M] [MulOneClass N] [MulAction M N] [IsScalarTower M N N] (x : M) :

MonoidHom.smulOneHom x = x • 1

source

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

source

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) => ⟨AddAction.compHom N f, ⋯⟩) ((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

source

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, property⟩) → motive x

Equations

⋯ = ⋯

source

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, 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

source

def addMonoidHomEquivAddActionIsScalarTower (M : Type u_11) (N : Type u_12) [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.

source

theorem addMonoidHomEquivAddActionIsScalarTower.proof_2 (M : Type u_1) (N : Type u_2) [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) => ⟨AddAction.compHom N f, ⋯⟩) f) = f

source

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

VAddAssocClass M N N

source

def monoidHomEquivMulActionIsScalarTower (M : Type u_11) (N : Type u_12) [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