Definitions of group actions #

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

has_scalar M α and its additive version has_vadd G P are notation typeclasses for • and +ᵥ, respectively;
mul_action M α and its additive version add_action G P are typeclasses used for actions of multiplicative and additive monoids and groups;
distrib_mul_action 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 semimodule, defined elsewhere.

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

smul_comm_class M N α and its additive version vadd_comm_class M N α;
is_scalar_tower M N α (no additive version).

Notation #

a • b is used as notation for has_scalar.smul a b.
a +ᵥ b is used as notation for has_vadd.vadd a b.

Implementation details #

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

Tags #

group action

source

@[class]

structure has_vadd (G : Type u_9) (P : Type u_10) :

Type (max u_10 u_9)

vadd : G → P → P

Type class for the +ᵥ notation.

Instances

source

@[class]

structure has_scalar (M : Type u_9) (α : Type u_10) :

Type (max u_10 u_9)

smul : M → α → α

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

Instances

source

@[class]

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

Type (max u_10 u_9)

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

Type class for additive monoid actions.

Instances

source

@[class]

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

Type (max u_10 u_9)

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

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

Instances

source

@[class]

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

Prop

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

source

@[class]

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

Prop

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

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

Instances

source

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

smul_comm_class N M α

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

source

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

vadd_comm_class N M α

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

source

@[instance]

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

vadd_comm_class M M α

source

@[instance]

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

smul_comm_class M M α

source

@[class]

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

Prop

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

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

Instances

source

@[simp]

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

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

source

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

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

source

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

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

source

@[simp]

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

1 • b = b

source

@[simp]

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

0 +ᵥ b = b

source

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

mul_action M β

Pullback a multiplicative action along an injective map respecting •.

Equations

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

source

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

add_action M β

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

source

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

add_action M β

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

source

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

mul_action M β

Pushforward a multiplicative action along a surjective map respecting •.

Equations

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

source

theorem ite_smul {M : Type u_1} {α : Type u_6} [monoid M] [mul_action 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} [add_monoid M] [add_action 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} [monoid M] [mul_action 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} [add_monoid M] [add_action M α] (p : Prop) [decidable p] (a : M) (b₁ b₂ : α) :

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

source

@[instance]

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

mul_action M M

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

This is promoted to a semimodule by semiring.to_semimodule.

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

@[instance]

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

add_action M M

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

This is promoted to an add_torsor by add_group_is_add_torsor.

source

@[simp]

theorem vadd_eq_add (M : Type u_1) [add_monoid M] {a a' : M} :

a +ᵥ a' = a + a'

source

@[simp]

theorem smul_eq_mul (M : Type u_1) [monoid M] {a a' : M} :

a • a' = a * a'

source

@[instance]

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

is_scalar_tower M M α

source

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

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

Equations

mul_action.comp_hom α g = {to_has_scalar := {smul := λ (x : N) (b : α), ⇑g x • b}, 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 α.

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

@[class]

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

Type (max u_10 u_9)

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

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

Instances

source

@[simp]

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

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

source

@[simp]

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

a • 0 = 0

source

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

distrib_mul_action M B

Pullback a distributive multiplicative action along an injective additive monoid homomorphism.

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

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.

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

Equations

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

source

def const_smul_hom {M : Type u_1} (A : Type u_4) [monoid M] [add_monoid A] [distrib_mul_action M A] (r : M) :

A →+ A

Scalar multiplication by r as an add_monoid_hom.

Equations

const_smul_hom A r = {to_fun := has_scalar.smul r, map_zero' := _, map_add' := _}

source

@[simp]

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

⇑(const_smul_hom A r) x = r • x

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