Definitions of group actions

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

has_scalar α β
mul_action α β
distrib_mul_action α β

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 α
is_scalar_tower M N α

Notation

a • b is used as notation for smul 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.

source

@[class]

structure has_scalar (α : Type u) (γ : Type v) :

Type (max u v)

smul : α → γ → γ

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

Instances

source

@[class]

structure mul_action (α : Type u) (β : Type v) [monoid α] :

Type (max u v)

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

@[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_1) (N : Type u_2) (α : Type u_3) [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} {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 {α : Type u} {β : Type v} [monoid α] [mul_action α β] (a₁ a₂ : α) (b : β) :

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

source

@[simp]

theorem one_smul (α : Type u) {β : Type v} [monoid α] [mul_action α β] (b : β) :

1 • b = b

source

def function.injective.mul_action {α : Type u} {β : Type v} {γ : Type w} [monoid α] [mul_action α β] [has_scalar α γ] (f : γ → β) (hf : function.injective f) (smul : ∀ (c : α) (x : γ), f (c • x) = c • f x) :

mul_action α γ

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.surjective.mul_action {α : Type u} {β : Type v} {γ : Type w} [monoid α] [mul_action α β] [has_scalar α γ] (f : β → γ) (hf : function.surjective f) (smul : ∀ (c : α) (x : β), f (c • x) = c • f x) :

mul_action α γ

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 {α : Type u} {β : Type v} [monoid α] [mul_action α β] (p : Prop) [decidable p] (a₁ a₂ : α) (b : β) :

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

source

theorem smul_ite {α : Type u} {β : Type v} [monoid α] [mul_action α β] (p : Prop) [decidable p] (a : α) (b₁ b₂ : β) :

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

source

def mul_action.regular (α : Type u) [monoid α] :

mul_action α α

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

Equations

mul_action.regular α = {to_has_scalar := {smul := λ (a₁ a₂ : α), a₁ * a₂}, one_smul := _, mul_smul := _}

source

@[instance]

def mul_action.is_scalar_tower.left (α : Type u) {β : Type v} [monoid α] [mul_action α β] :

is_scalar_tower α α β

source

def mul_action.to_fun (α : Type u) (β : Type v) [monoid α] [mul_action α β] :

β ↪ α → β

Embedding induced by action.

Equations

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

source

@[simp]

theorem mul_action.to_fun_apply {α : Type u} {β : Type v} [monoid α] [mul_action α β] (x : α) (y : β) :

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

source

def mul_action.comp_hom {α : Type u} (β : Type v) {γ : Type w} [monoid α] [mul_action α β] [monoid γ] (g : γ →* α) :

mul_action γ β

An action of α on β and a monoid homomorphism γ → α induce an action of γ on β.

Equations

mul_action.comp_hom β g = {to_has_scalar := {smul := λ (x : γ) (b : β), ⇑g x • b}, one_smul := _, mul_smul := _}

source

@[simp]

theorem smul_one_smul {α : Type u} {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 (α : Type u) (β : Type v) [monoid α] [add_monoid β] :

Type (max u v)

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

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

Instances

source

@[simp]

theorem smul_add {α : Type u} {β : Type v} [monoid α] [add_monoid β] [distrib_mul_action α β] (a : α) (b₁ b₂ : β) :

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

source

@[simp]

theorem smul_zero {α : Type u} {β : Type v} [monoid α] [add_monoid β] [distrib_mul_action α β] (a : α) :

a • 0 = 0

source

def function.injective.distrib_mul_action {α : Type u} {β : Type v} {γ : Type w} [monoid α] [add_monoid β] [distrib_mul_action α β] [add_monoid γ] [has_scalar α γ] (f : γ →+ β) (hf : function.injective ⇑f) (smul : ∀ (c : α) (x : γ), ⇑f (c • x) = c • ⇑f x) :

distrib_mul_action α γ

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 {α : Type u} {β : Type v} {γ : Type w} [monoid α] [add_monoid β] [distrib_mul_action α β] [add_monoid γ] [has_scalar α γ] (f : β →+ γ) (hf : function.surjective ⇑f) (smul : ∀ (c : α) (x : β), ⇑f (c • x) = c • ⇑f x) :

distrib_mul_action α γ

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 const_smul_hom {α : Type u} (β : Type v) [monoid α] [add_monoid β] [distrib_mul_action α β] (r : α) :

β →+ β

Scalar multiplication by r as an add_monoid_hom.

Equations

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

source

@[simp]

theorem const_smul_hom_apply {α : Type u} {β : Type v} [monoid α] [add_monoid β] [distrib_mul_action α β] (r : α) (x : β) :

⇑(const_smul_hom β r) x = r • x

source

@[simp]

theorem smul_neg {α : Type u} {β : Type v} [monoid α] [add_group β] [distrib_mul_action α β] (r : α) (x : β) :

r • -x = -(r • x)

source

theorem smul_sub {α : Type u} {β : Type v} [monoid α] [add_group β] [distrib_mul_action α β] (r : α) (x y : β) :

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