group_theory.group_action.defs

source

@[class]

structure has_faithful_vadd (G : Type u_10) (P : Type u_11) [has_vadd G P] :

Prop

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

Typeclass for faithful actions.

Instances of this typeclass

source

@[class]

structure has_faithful_smul (M : Type u_10) (α : Type u_11) [has_scalar M α] :

Prop

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

Typeclass for faithful actions.

Instances of this typeclass

source

theorem vadd_left_injective' {M : Type u_1} {α : Type u_6} [has_vadd M α] [has_faithful_vadd M α] :

function.injective has_vadd.vadd

source

theorem smul_left_injective' {M : Type u_1} {α : Type u_6} [has_scalar M α] [has_faithful_smul M α] :

function.injective has_scalar.smul

source

@[protected, instance]

def has_mul.to_has_scalar (α : Type u_1) [has_mul α] :

has_scalar α α

Equations

has_mul.to_has_scalar α = {smul := has_mul.mul _inst_1}

source

@[protected, instance]

def has_add.to_has_scalar (α : Type u_1) [has_add α] :

has_vadd α α

Equations

has_add.to_has_scalar α = {vadd := has_add.add _inst_1}

source

@[simp]

theorem vadd_eq_add (α : Type u_1) [has_add α] {a a' : α} :

a +ᵥ a' = a + a'

source

@[simp]

theorem smul_eq_mul (α : Type u_1) [has_mul α] {a a' : α} :

a • a' = a * a'

source

theorem add_action.ext {G : Type u_10} {P : Type u_11} {_inst_1 : add_monoid G} (x y : add_action G P) (h : add_action.to_has_vadd = add_action.to_has_vadd) :

x = y

source

@[ext, class]

structure add_action (G : Type u_10) (P : Type u_11) [add_monoid G] :

Type (max u_10 u_11)

to_has_vadd : has_vadd G P
zero_vadd : ∀ (p : P), 0 +ᵥ p = p
add_vadd : ∀ (g₁ g₂ : G) (p : P), g₁ + g₂ +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p)

Type class for additive monoid actions.

Instances of this typeclass

Instances of other typeclasses for add_action

add_action.has_sizeof_inst

source

theorem add_action.ext_iff {G : Type u_10} {P : Type u_11} {_inst_1 : add_monoid G} (x y : add_action G P) :

x = y ↔ add_action.to_has_vadd = add_action.to_has_vadd

source

theorem mul_action.ext {α : Type u_10} {β : Type u_11} {_inst_1 : monoid α} (x y : mul_action α β) (h : mul_action.to_has_scalar = mul_action.to_has_scalar) :

x = y

source

@[ext, class]

structure mul_action (α : Type u_10) (β : Type u_11) [monoid α] :

Type (max u_10 u_11)

to_has_scalar : has_scalar α β
one_smul : ∀ (b : β), 1 • b = b
mul_smul : ∀ (x y : α) (b : β), (x * y) • b = x • y • b

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

Instances of this typeclass

Instances of other typeclasses for mul_action

mul_action.has_sizeof_inst

source

theorem mul_action.ext_iff {α : Type u_10} {β : Type u_11} {_inst_1 : monoid α} (x y : mul_action α β) :

x = y ↔ mul_action.to_has_scalar = mul_action.to_has_scalar

source

@[protected, instance]

def additive.add_action {α : Type u_6} {β : Type u_7} [monoid α] [mul_action α β] :

add_action (additive α) β

Equations

additive.add_action = {to_has_vadd := {vadd := has_scalar.smul ∘ ⇑additive.to_mul}, zero_vadd := _, add_vadd := _}

source

@[simp]

theorem additive.of_mul_vadd {α : Type u_6} {β : Type u_7} [monoid α] [mul_action α β] (a : α) (b : β) :

⇑additive.of_mul a +ᵥ b = a • b

source

@[protected, instance]

def multiplicative.mul_action {α : Type u_6} {β : Type u_7} [add_monoid α] [add_action α β] :

mul_action (multiplicative α) β

Equations

multiplicative.mul_action = {to_has_scalar := {smul := has_vadd.vadd ∘ ⇑multiplicative.to_add}, one_smul := _, mul_smul := _}

source

@[simp]

theorem multiplicative.of_add_smul {α : Type u_6} {β : Type u_7} [add_monoid α] [add_action α β] (a : α) (b : β) :

⇑multiplicative.of_add a • b = a +ᵥ b

source

@[class]

structure add_action.is_pretransitive (M : Type u_10) (α : Type u_11) [has_vadd M α] :

Prop

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

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

Instances of this typeclass

source

@[class]

structure mul_action.is_pretransitive (M : Type u_10) (α : Type u_11) [has_scalar M α] :

Prop

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

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

Instances of this typeclass

source

theorem add_action.exists_vadd_eq (M : Type u_1) {α : Type u_6} [has_vadd M α] [add_action.is_pretransitive M α] (x y : α) :

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

source

theorem mul_action.exists_smul_eq (M : Type u_1) {α : Type u_6} [has_scalar M α] [mul_action.is_pretransitive M α] (x y : α) :

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

source

theorem mul_action.surjective_smul (M : Type u_1) {α : Type u_6} [has_scalar M α] [mul_action.is_pretransitive M α] (x : α) :

function.surjective (λ (c : M), c • x)

source

theorem add_action.surjective_vadd (M : Type u_1) {α : Type u_6} [has_vadd M α] [add_action.is_pretransitive M α] (x : α) :

function.surjective (λ (c : M), c +ᵥ x)

source

@[protected, instance]

def add_action.regular.is_pretransitive {G : Type u_3} [add_group G] :

add_action.is_pretransitive G G

source

@[protected, instance]

def mul_action.regular.is_pretransitive {G : Type u_3} [group G] :

mul_action.is_pretransitive G G

The regular action of a group on itself is transitive.

source

@[class]

structure vadd_comm_class (M : Type u_10) (N : Type u_11) (α : Type u_12) [has_vadd M α] [has_vadd N α] :

Prop

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

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

Instances of this typeclass

source

@[class]

structure smul_comm_class (M : Type u_10) (N : Type u_11) (α : Type u_12) [has_scalar M α] [has_scalar N α] :

Prop

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

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

Instances of this typeclass

source

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

smul_comm_class N M α

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

source

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

vadd_comm_class N M α

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

source

@[protected, instance]

def vadd_comm_class_self (M : Type u_1) (α : Type u_2) [add_comm_monoid M] [add_action M α] :

vadd_comm_class M M α

source

@[protected, instance]

def smul_comm_class_self (M : Type u_1) (α : Type u_2) [comm_monoid M] [mul_action M α] :

smul_comm_class M M α

source

@[class]

structure is_scalar_tower (M : Type u_10) (N : Type u_11) (α : Type u_12) [has_scalar M N] [has_scalar N α] [has_scalar M α] :

Prop

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

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

Instances of this typeclass

source

@[simp]

theorem smul_assoc {α : Type u_6} {M : Type u_1} {N : Type u_2} [has_scalar M N] [has_scalar N α] [has_scalar M α] [is_scalar_tower M N α] (x : M) (y : N) (z : α) :

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

source

@[protected, instance]

def semigroup.is_scalar_tower {α : Type u_6} [semigroup α] :

is_scalar_tower α α α

source

@[class]

structure is_central_scalar (M : Type u_10) (α : Type u_11) [has_scalar M α] [has_scalar Mᵐᵒᵖ α] :

Prop

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

A typeclass indicating that the right (aka mul_opposite) and left actions by M on α are equal, that is that M acts centrally on α. This can be thought of as a version of commutativity for •.

Instances of this typeclass

source

theorem is_central_scalar.unop_smul_eq_smul {M : Type u_1} {α : Type u_2} [has_scalar M α] [has_scalar Mᵐᵒᵖ α] [is_central_scalar M α] (m : Mᵐᵒᵖ) (a : α) :

mul_opposite.unop m • a = m • a

source

@[protected, instance]

def smul_comm_class.op_left {M : Type u_1} {N : Type u_2} {α : Type u_6} [has_scalar M α] [has_scalar Mᵐᵒᵖ α] [is_central_scalar M α] [has_scalar N α] [smul_comm_class M N α] :

smul_comm_class Mᵐᵒᵖ N α

source

@[protected, instance]

def smul_comm_class.op_right {M : Type u_1} {N : Type u_2} {α : Type u_6} [has_scalar M α] [has_scalar N α] [has_scalar Nᵐᵒᵖ α] [is_central_scalar N α] [smul_comm_class M N α] :

smul_comm_class M Nᵐᵒᵖ α

source

@[protected, instance]

def is_scalar_tower.op_left {M : Type u_1} {N : Type u_2} {α : Type u_6} [has_scalar M α] [has_scalar Mᵐᵒᵖ α] [is_central_scalar M α] [has_scalar M N] [has_scalar Mᵐᵒᵖ N] [is_central_scalar M N] [has_scalar N α] [is_scalar_tower M N α] :

is_scalar_tower Mᵐᵒᵖ N α

source

@[protected, instance]

def is_scalar_tower.op_right {M : Type u_1} {N : Type u_2} {α : Type u_6} [has_scalar M α] [has_scalar M N] [has_scalar N α] [has_scalar Nᵐᵒᵖ α] [is_central_scalar N α] [is_scalar_tower M N α] :

is_scalar_tower M Nᵐᵒᵖ α

source

@[simp]

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

α

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

Equations

has_vadd.comp.vadd g n a = g n +ᵥ a

source

@[simp]

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

α

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

Equations

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

source

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

has_vadd N α

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

Equations

has_vadd.comp α g = {vadd := has_vadd.comp.vadd g}

source

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

has_scalar N α

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

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

Equations

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

source

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

is_scalar_tower N α β

Given a tower of scalar actions M → α → β, if we use has_scalar.comp to pull back both of M's actions by a map g : N → M, then we obtain a new tower of scalar actions N → α → β.

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

source

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

smul_comm_class N β α

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

source

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

smul_comm_class β N α

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

source

theorem add_vadd_comm {α : Type u_6} {β : Type u_7} [has_add β] [has_vadd α β] [vadd_comm_class α β β] (s : α) (x y : β) :

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

source

theorem mul_smul_comm {α : Type u_6} {β : Type u_7} [has_mul β] [has_scalar α β] [smul_comm_class α β β] (s : α) (x y : β) :

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

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

source

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

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

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

source

theorem smul_smul_smul_comm {α : Type u_6} {β : Type u_7} {γ : Type u_8} {δ : Type u_9} [has_scalar α β] [has_scalar α γ] [has_scalar β δ] [has_scalar α δ] [has_scalar γ δ] [is_scalar_tower α β δ] [is_scalar_tower α γ δ] [smul_comm_class β γ δ] (a : α) (b : β) (c : γ) (d : δ) :

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

source

theorem commute.smul_right {M : Type u_1} {α : Type u_6} [has_scalar M α] [has_mul α] [smul_comm_class M α α] [is_scalar_tower M α α] {a b : α} (h : commute a b) (r : M) :

commute a (r • b)

source

theorem commute.smul_left {M : Type u_1} {α : Type u_6} [has_scalar M α] [has_mul α] [smul_comm_class M α α] [is_scalar_tower M α α] {a b : α} (h : commute a b) (r : M) :

commute (r • a) b

source

theorem ite_smul {M : Type u_1} {α : Type u_6} [has_scalar M α] (p : Prop) [decidable p] (a₁ a₂ : M) (b : α) :

ite p a₁ a₂ • b = ite p (a₁ • b) (a₂ • b)

source

theorem ite_vadd {M : Type u_1} {α : Type u_6} [has_vadd M α] (p : Prop) [decidable p] (a₁ a₂ : M) (b : α) :

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

source

theorem smul_ite {M : Type u_1} {α : Type u_6} [has_scalar M α] (p : Prop) [decidable p] (a : M) (b₁ b₂ : α) :

a • ite p b₁ b₂ = ite p (a • b₁) (a • b₂)

source

theorem vadd_ite {M : Type u_1} {α : Type u_6} [has_vadd M α] (p : Prop) [decidable p] (a : M) (b₁ b₂ : α) :

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

source

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

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

source

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

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

source

@[simp]

theorem one_smul (M : Type u_1) {α : Type u_6} [monoid M] [mul_action M α] (b : α) :

1 • b = b

source

@[simp]

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

0 +ᵥ b = b

source

theorem one_smul_eq_id (M : Type u_1) {α : Type u_6} [monoid M] [mul_action M α] :

has_scalar.smul 1 = id

has_scalar version of one_mul_eq_id

source

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

has_vadd.vadd 0 = id

source

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

has_scalar.smul a₁ ∘ has_scalar.smul a₂ = has_scalar.smul (a₁ * a₂)

has_scalar version of comp_mul_left

source

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

has_vadd.vadd a₁ ∘ has_vadd.vadd a₂ = has_vadd.vadd (a₁ + a₂)

source

@[protected]

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

mul_action M β

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

Equations

function.injective.mul_action f hf smul = {to_has_scalar := {smul := has_scalar.smul _inst_3}, one_smul := _, mul_smul := _}

source

@[protected]

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

add_action M β

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

Equations

function.injective.add_action f hf smul = {to_has_vadd := {vadd := has_vadd.vadd _inst_3}, zero_vadd := _, add_vadd := _}

source

@[protected]

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

add_action M β

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

Equations

function.surjective.add_action f hf smul = {to_has_vadd := {vadd := has_vadd.vadd _inst_3}, zero_vadd := _, add_vadd := _}

source

@[protected]

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

mul_action M β

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

Equations

function.surjective.mul_action f hf smul = {to_has_scalar := {smul := has_scalar.smul _inst_3}, one_smul := _, mul_smul := _}

source

def function.surjective.mul_action_left {R : Type u_1} {S : Type u_2} {M : Type u_3} [monoid R] [mul_action R M] [monoid S] [has_scalar S M] (f : R →* S) (hf : function.surjective ⇑f) (hsmul : ∀ (c : R) (x : M), ⇑f c • x = c • x) :

mul_action S M

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

Equations

function.surjective.mul_action_left f hf hsmul = {to_has_scalar := {smul := has_scalar.smul _inst_6}, one_smul := _, mul_smul := _}

source

def function.surjective.add_action_left {R : Type u_1} {S : Type u_2} {M : Type u_3} [add_monoid R] [add_action R M] [add_monoid S] [has_vadd S M] (f : R →+ S) (hf : function.surjective ⇑f) (hsmul : ∀ (c : R) (x : M), ⇑f c +ᵥ x = c +ᵥ x) :

add_action S M

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

Equations

function.surjective.add_action_left f hf hsmul = {to_has_vadd := {vadd := has_vadd.vadd _inst_6}, zero_vadd := _, add_vadd := _}

source

@[protected, instance]

def monoid.to_mul_action (M : Type u_1) [monoid M] :

mul_action M M

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

This is promoted to a module by semiring.to_module.

Equations

monoid.to_mul_action M = {to_has_scalar := {smul := has_mul.mul (mul_one_class.to_has_mul M)}, one_smul := _, mul_smul := _}

source

@[protected, instance]

def add_monoid.to_add_action (M : Type u_1) [add_monoid M] :

add_action M M

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

This is promoted to an add_torsor by add_group_is_add_torsor.

Equations

add_monoid.to_add_action M = {to_has_vadd := {vadd := has_add.add (add_zero_class.to_has_add M)}, zero_vadd := _, add_vadd := _}

source

@[protected, instance]

def is_scalar_tower.left (M : Type u_1) {α : Type u_6} [monoid M] [mul_action M α] :

is_scalar_tower M M α

source

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

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

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

source

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

α ↪ M → α

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

Equations

mul_action.to_fun M α = {to_fun := λ (y : α) (x : M), x • y, inj' := _}

source

def add_action.to_fun (M : Type u_1) (α : Type u_6) [add_monoid M] [add_action M α] :

α ↪ M → α

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

Equations

add_action.to_fun M α = {to_fun := λ (y : α) (x : M), x +ᵥ y, inj' := _}

source

@[simp]

theorem mul_action.to_fun_apply {M : Type u_1} {α : Type u_6} [monoid M] [mul_action M α] (x : M) (y : α) :

⇑(mul_action.to_fun M α) y x = x • y

source

@[simp]

theorem add_action.to_fun_apply {M : Type u_1} {α : Type u_6} [add_monoid M] [add_action M α] (x : M) (y : α) :

⇑(add_action.to_fun M α) y x = x +ᵥ y

source

def mul_action.comp_hom {M : Type u_1} {N : Type u_2} (α : Type u_6) [monoid M] [mul_action M α] [monoid N] (g : N →* M) :

mul_action N α

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

See note [reducible non-instances].

Equations

mul_action.comp_hom α g = {to_has_scalar := {smul := has_scalar.comp.smul ⇑g}, one_smul := _, mul_smul := _}

source

def add_action.comp_hom {M : Type u_1} {N : Type u_2} (α : Type u_6) [add_monoid M] [add_action M α] [add_monoid N] (g : N →+ M) :

add_action N α

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

See note [reducible non-instances].

Equations

add_action.comp_hom α g = {to_has_vadd := {vadd := has_vadd.comp.vadd ⇑g}, zero_vadd := _, add_vadd := _}

source

@[simp]

theorem smul_one_smul {α : Type u_6} {M : Type u_1} (N : Type u_2) [monoid N] [has_scalar M N] [mul_action N α] [has_scalar M α] [is_scalar_tower M N α] (x : M) (y : α) :

(x • 1) • y = x • y

source

@[simp]

theorem smul_one_mul {M : Type u_1} {N : Type u_2} [monoid N] [has_scalar M N] [is_scalar_tower M N N] (x : M) (y : N) :

x • 1 * y = x • y

source

@[simp]

theorem add_vadd_zero {M : Type u_1} {N : Type u_2} [add_zero_class N] [has_vadd M N] [vadd_comm_class M N N] (x : M) (y : N) :

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

source

@[simp]

theorem mul_smul_one {M : Type u_1} {N : Type u_2} [mul_one_class N] [has_scalar M N] [smul_comm_class M N N] (x : M) (y : N) :

y * x • 1 = x • y

source

theorem is_scalar_tower.of_smul_one_mul {M : Type u_1} {N : Type u_2} [monoid N] [has_scalar M N] (h : ∀ (x : M) (y : N), x • 1 * y = x • y) :

is_scalar_tower M N N

source

theorem smul_comm_class.of_mul_smul_one {M : Type u_1} {N : Type u_2} [monoid N] [has_scalar M N] (H : ∀ (x : M) (y : N), y * x • 1 = x • y) :

smul_comm_class M N N

source

theorem vadd_comm_class.of_add_vadd_zero {M : Type u_1} {N : Type u_2} [add_monoid N] [has_vadd M N] (H : ∀ (x : M) (y : N), y + (x +ᵥ 0) = x +ᵥ y) :

vadd_comm_class M N N

source

theorem distrib_mul_action.ext {M : Type u_10} {A : Type u_11} {_inst_1 : monoid M} {_inst_2 : add_monoid A} (x y : distrib_mul_action M A) (h : distrib_mul_action.to_mul_action = distrib_mul_action.to_mul_action) :

x = y

source

@[ext, class]

structure distrib_mul_action (M : Type u_10) (A : Type u_11) [monoid M] [add_monoid A] :

Type (max u_10 u_11)

to_mul_action : mul_action M A
smul_add : ∀ (r : M) (x y : A), r • (x + y) = r • x + r • y
smul_zero : ∀ (r : M), r • 0 = 0

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

Instances of this typeclass

Instances of other typeclasses for distrib_mul_action

distrib_mul_action.has_sizeof_inst

source

theorem distrib_mul_action.ext_iff {M : Type u_10} {A : Type u_11} {_inst_1 : monoid M} {_inst_2 : add_monoid A} (x y : distrib_mul_action M A) :

x = y ↔ distrib_mul_action.to_mul_action = distrib_mul_action.to_mul_action

source

@[simp]

theorem smul_add {M : Type u_1} {A : Type u_4} [monoid M] [add_monoid A] [distrib_mul_action M A] (a : M) (b₁ b₂ : A) :

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

source

@[simp]

theorem smul_zero {M : Type u_1} {A : Type u_4} [monoid M] [add_monoid A] [distrib_mul_action M A] (a : M) :

a • 0 = 0

source

@[protected]

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

distrib_mul_action M B

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

Equations

function.injective.distrib_mul_action f hf smul = {to_mul_action := {to_has_scalar := {smul := has_scalar.smul _inst_5}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}

source

@[protected]

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

distrib_mul_action M B

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

Equations

function.surjective.distrib_mul_action f hf smul = {to_mul_action := {to_has_scalar := {smul := has_scalar.smul _inst_5}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}

source

def function.surjective.distrib_mul_action_left {R : Type u_1} {S : Type u_2} {M : Type u_3} [monoid R] [add_monoid M] [distrib_mul_action R M] [monoid S] [has_scalar S M] (f : R →* S) (hf : function.surjective ⇑f) (hsmul : ∀ (c : R) (x : M), ⇑f c • x = c • x) :

distrib_mul_action S M

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

Equations

function.surjective.distrib_mul_action_left f hf hsmul = {to_mul_action := {to_has_scalar := {smul := has_scalar.smul _inst_8}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}

source

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

distrib_mul_action N A

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

Equations

distrib_mul_action.comp_hom A f = {to_mul_action := {to_has_scalar := {smul := has_scalar.comp.smul ⇑f}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}

source

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

A →+ A

Each element of the monoid defines a additive monoid homomorphism.

Equations

distrib_mul_action.to_add_monoid_hom A x = {to_fun := has_scalar.smul x, map_zero' := _, map_add' := _}

source

@[simp]

theorem distrib_mul_action.to_add_monoid_hom_apply {M : Type u_1} (A : Type u_4) [monoid M] [add_monoid A] [distrib_mul_action M A] (x : M) (ᾰ : A) :

⇑(distrib_mul_action.to_add_monoid_hom A x) ᾰ = x • ᾰ

source

@[simp]

theorem distrib_mul_action.to_add_monoid_End_apply (M : Type u_1) (A : Type u_4) [monoid M] [add_monoid A] [distrib_mul_action M A] (x : M) :

⇑(distrib_mul_action.to_add_monoid_End M A) x = distrib_mul_action.to_add_monoid_hom A x

source

def distrib_mul_action.to_add_monoid_End (M : Type u_1) (A : Type u_4) [monoid M] [add_monoid A] [distrib_mul_action M A] :

M →* add_monoid.End A

Each element of the monoid defines an additive monoid homomorphism.

Equations

distrib_mul_action.to_add_monoid_End M A = {to_fun := distrib_mul_action.to_add_monoid_hom A _inst_3, map_one' := _, map_mul' := _}

source

@[protected, instance]

def add_monoid.nat_smul_comm_class (M : Type u_1) (A : Type u_4) [monoid M] [add_monoid A] [distrib_mul_action M A] :

smul_comm_class ℕ M A

source

@[protected, instance]

def add_monoid.nat_smul_comm_class' (M : Type u_1) (A : Type u_4) [monoid M] [add_monoid A] [distrib_mul_action M A] :

smul_comm_class M ℕ A

source

@[protected, instance]

def add_group.int_smul_comm_class {M : Type u_1} {A : Type u_4} [monoid M] [add_group A] [distrib_mul_action M A] :

smul_comm_class ℤ M A

source

@[protected, instance]

def add_group.int_smul_comm_class' {M : Type u_1} {A : Type u_4} [monoid M] [add_group A] [distrib_mul_action M A] :

smul_comm_class M ℤ A

source

@[simp]

theorem smul_neg {M : Type u_1} {A : Type u_4} [monoid M] [add_group A] [distrib_mul_action M A] (r : M) (x : A) :

r • -x = -(r • x)

source

theorem smul_sub {M : Type u_1} {A : Type u_4} [monoid M] [add_group A] [distrib_mul_action M A] (r : M) (x y : A) :

r • (x - y) = r • x - r • y

source

theorem mul_distrib_mul_action.ext {M : Type u_10} {A : Type u_11} {_inst_1 : monoid M} {_inst_2 : monoid A} (x y : mul_distrib_mul_action M A) (h : mul_distrib_mul_action.to_mul_action = mul_distrib_mul_action.to_mul_action) :

x = y

source

theorem mul_distrib_mul_action.ext_iff {M : Type u_10} {A : Type u_11} {_inst_1 : monoid M} {_inst_2 : monoid A} (x y : mul_distrib_mul_action M A) :

x = y ↔ mul_distrib_mul_action.to_mul_action = mul_distrib_mul_action.to_mul_action

source

@[ext, class]

structure mul_distrib_mul_action (M : Type u_10) (A : Type u_11) [monoid M] [monoid A] :

Type (max u_10 u_11)

to_mul_action : mul_action M A
smul_mul : ∀ (r : M) (x y : A), r • (x * y) = r • x * r • y
smul_one : ∀ (r : M), r • 1 = 1

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

Instances of this typeclass

Instances of other typeclasses for mul_distrib_mul_action

mul_distrib_mul_action.has_sizeof_inst

source

@[simp]

theorem smul_mul' {M : Type u_1} {A : Type u_4} [monoid M] [monoid A] [mul_distrib_mul_action M A] (a : M) (b₁ b₂ : A) :

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

source

@[protected]

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

mul_distrib_mul_action M B

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

Equations

function.injective.mul_distrib_mul_action f hf smul = {to_mul_action := {to_has_scalar := {smul := has_scalar.smul _inst_5}, one_smul := _, mul_smul := _}, smul_mul := _, smul_one := _}

source

@[protected]

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

mul_distrib_mul_action M B

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

Equations

function.surjective.mul_distrib_mul_action f hf smul = {to_mul_action := {to_has_scalar := {smul := has_scalar.smul _inst_5}, one_smul := _, mul_smul := _}, smul_mul := _, smul_one := _}

source

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

mul_distrib_mul_action N A

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

Equations