mathlib documentation

group_theory.group_action.prod

Prod instances for additive and multiplicative actions #

This file defines instances for binary product of additive and multiplicative actions and provides scalar multiplication as a homomorphism from α × β to β.

Main declarations #

source
@[protected, instance]
def prod.has_scalar {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_scalar M α] [has_scalar M β] :
has_scalar M (α × β)
Equations
source
@[protected, instance]
def prod.has_vadd {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_vadd M α] [has_vadd M β] :
has_vadd M (α × β)
Equations
source
@[simp]
theorem prod.vadd_fst {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_vadd M α] [has_vadd M β] (a : M) (x : α × β) :
(a +ᵥ x).fst = a +ᵥ x.fst
source
@[simp]
theorem prod.smul_fst {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_scalar M α] [has_scalar M β] (a : M) (x : α × β) :
(a • x).fst = a • x.fst
source
@[simp]
theorem prod.smul_snd {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_scalar M α] [has_scalar M β] (a : M) (x : α × β) :
(a • x).snd = a • x.snd
source
@[simp]
theorem prod.vadd_snd {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_vadd M α] [has_vadd M β] (a : M) (x : α × β) :
(a +ᵥ x).snd = a +ᵥ x.snd
source
@[simp]
theorem prod.smul_mk {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_scalar M α] [has_scalar M β] (a : M) (b : α) (c : β) :
a • (b, c) = (a • b, a • c)
source
@[simp]
theorem prod.vadd_mk {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_vadd M α] [has_vadd M β] (a : M) (b : α) (c : β) :
a +ᵥ (b, c) = (a +ᵥ b, a +ᵥ c)
source
theorem prod.vadd_def {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_vadd M α] [has_vadd M β] (a : M) (x : α × β) :
a +ᵥ x = (a +ᵥ x.fst, a +ᵥ x.snd)
source
theorem prod.smul_def {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_scalar M α] [has_scalar M β] (a : M) (x : α × β) :
a • x = (a • x.fst, a • x.snd)
source
@[simp]
theorem prod.vadd_swap {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_vadd M α] [has_vadd M β] (a : M) (x : α × β) :
(a +ᵥ x).swap = a +ᵥ x.swap
source
@[simp]
theorem prod.smul_swap {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_scalar M α] [has_scalar M β] (a : M) (x : α × β) :
(a • x).swap = a • x.swap
source
@[protected, instance]
def prod.is_scalar_tower {M : Type u_1} {N : Type u_2} {α : Type u_4} {β : Type u_5} [has_scalar M α] [has_scalar M β] [has_scalar N α] [has_scalar N β] [has_scalar M N] [is_scalar_tower M N α] [is_scalar_tower M N β] :
is_scalar_tower M N (α × β)
source
@[protected, instance]
def prod.vadd_comm_class {M : Type u_1} {N : Type u_2} {α : Type u_4} {β : Type u_5} [has_vadd M α] [has_vadd M β] [has_vadd N α] [has_vadd N β] [vadd_comm_class M N α] [vadd_comm_class M N β] :
vadd_comm_class M N (α × β)
source
@[protected, instance]
def prod.smul_comm_class {M : Type u_1} {N : Type u_2} {α : Type u_4} {β : Type u_5} [has_scalar M α] [has_scalar M β] [has_scalar N α] [has_scalar N β] [smul_comm_class M N α] [smul_comm_class M N β] :
smul_comm_class M N (α × β)
source
@[protected, instance]
def prod.is_central_scalar {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_scalar M α] [has_scalar M β] [has_scalar Mᵐᵒᵖ α] [has_scalar Mᵐᵒᵖ β] [is_central_scalar M α] [is_central_scalar M β] :
is_central_scalar M (α × β)
source
@[protected, instance]
def prod.has_faithful_scalar_left {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_scalar M α] [has_scalar M β] [has_faithful_scalar M α] [nonempty β] :
has_faithful_scalar M (α × β)
source
@[protected, instance]
def prod.has_faithful_vadd_left {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_vadd M α] [has_vadd M β] [has_faithful_vadd M α] [nonempty β] :
has_faithful_vadd M (α × β)
source
@[protected, instance]
def prod.has_faithful_vadd_right {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_vadd M α] [has_vadd M β] [nonempty α] [has_faithful_vadd M β] :
has_faithful_vadd M (α × β)
source
@[protected, instance]
def prod.has_faithful_scalar_right {M : Type u_1} {α : Type u_4} {β : Type u_5} [has_scalar M α] [has_scalar M β] [nonempty α] [has_faithful_scalar M β] :
has_faithful_scalar M (α × β)
source
@[protected, instance]
def prod.vadd_comm_class_both {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_add N] [has_add P] [has_vadd M N] [has_vadd M P] [vadd_comm_class M N N] [vadd_comm_class M P P] :
vadd_comm_class M (N × P) (N × P)
source
@[protected, instance]
def prod.smul_comm_class_both {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_mul N] [has_mul P] [has_scalar M N] [has_scalar M P] [smul_comm_class M N N] [smul_comm_class M P P] :
smul_comm_class M (N × P) (N × P)
source
@[protected, instance]
def prod.is_scalar_tower_both {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_mul N] [has_mul P] [has_scalar M N] [has_scalar M P] [is_scalar_tower M N N] [is_scalar_tower M P P] :
is_scalar_tower M (N × P) (N × P)
source
@[protected, instance]
def prod.add_action {M : Type u_1} {α : Type u_4} {β : Type u_5} {m : add_monoid M} [add_action M α] [add_action M β] :
add_action M (α × β)
Equations
source
@[protected, instance]
def prod.mul_action {M : Type u_1} {α : Type u_4} {β : Type u_5} {m : monoid M} [mul_action M α] [mul_action M β] :
mul_action M (α × β)
Equations
source
@[protected, instance]
def prod.distrib_mul_action {R : Type u_1} {M : Type u_2} {N : Type u_3} {r : monoid R} [add_monoid M] [add_monoid N] [distrib_mul_action R M] [distrib_mul_action R N] :
distrib_mul_action R (M × N)
Equations
source
@[protected, instance]
def prod.mul_distrib_mul_action {R : Type u_1} {M : Type u_2} {N : Type u_3} {r : monoid R} [monoid M] [monoid N] [mul_distrib_mul_action R M] [mul_distrib_mul_action R N] :
mul_distrib_mul_action R (M × N)
Equations

Scalar multiplication as a homomorphism #

source
@[simp]
theorem smul_mul_hom_apply {α : Type u_4} {β : Type u_5} [monoid α] [has_mul β] [mul_action α β] [is_scalar_tower α β β] [smul_comm_class α β β] (a : α × β) :
⇑smul_mul_hom a = a.fst • a.snd
source
def smul_mul_hom {α : Type u_4} {β : Type u_5} [monoid α] [has_mul β] [mul_action α β] [is_scalar_tower α β β] [smul_comm_class α β β] :
α × β →ₙ* β

Scalar multiplication as a multiplicative homomorphism.

Equations
source
def smul_monoid_hom {α : Type u_4} {β : Type u_5} [monoid α] [mul_one_class β] [mul_action α β] [is_scalar_tower α β β] [smul_comm_class α β β] :
α × β →* β

Scalar multiplication as a monoid homomorphism.

Equations
source
@[simp]
theorem smul_monoid_hom_apply {α : Type u_4} {β : Type u_5} [monoid α] [mul_one_class β] [mul_action α β] [is_scalar_tower α β β] [smul_comm_class α β β] (ᾰ : α × β) :
⇑smul_monoid_hom ᾰ = smul_mul_hom.to_fun ᾰ