Prod instances for additive and multiplicative actions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main declarations #

smul_mul_hom/smul_monoid_hom: Scalar multiplication bundled as a multiplicative/monoid homomorphism.

See also #

group_theory.group_action.option
group_theory.group_action.pi
group_theory.group_action.sigma
group_theory.group_action.sum

source

@[protected, instance]

def prod.has_vadd {M : Type u_1} {α : Type u_5} {β : Type u_6} [has_vadd M α] [has_vadd M β] :

has_vadd M (α × β)

Equations

prod.has_vadd = {vadd := λ (a : M) (p : α × β), (a +ᵥ p.fst, a +ᵥ p.snd)}

source

@[protected, instance]

def prod.has_smul {M : Type u_1} {α : Type u_5} {β : Type u_6} [has_smul M α] [has_smul M β] :

has_smul M (α × β)

Equations

prod.has_smul = {smul := λ (a : M) (p : α × β), (a • p.fst, a • p.snd)}

source

@[simp]

theorem prod.vadd_fst {M : Type u_1} {α : Type u_5} {β : Type u_6} [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_5} {β : Type u_6} [has_smul M α] [has_smul M β] (a : M) (x : α × β) :

(a • x).fst = a • x.fst

source

@[simp]

theorem prod.smul_snd {M : Type u_1} {α : Type u_5} {β : Type u_6} [has_smul M α] [has_smul M β] (a : M) (x : α × β) :

(a • x).snd = a • x.snd

source

@[simp]

theorem prod.vadd_snd {M : Type u_1} {α : Type u_5} {β : Type u_6} [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_5} {β : Type u_6} [has_smul M α] [has_smul M β] (a : M) (b : α) (c : β) :

a • (b, c) = (a • b, a • c)

source

@[simp]

theorem prod.vadd_mk {M : Type u_1} {α : Type u_5} {β : Type u_6} [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_5} {β : Type u_6} [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_5} {β : Type u_6} [has_smul M α] [has_smul M β] (a : M) (x : α × β) :

a • x = (a • x.fst, a • x.snd)

source

@[simp]

theorem prod.vadd_swap {M : Type u_1} {α : Type u_5} {β : Type u_6} [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_5} {β : Type u_6} [has_smul M α] [has_smul M β] (a : M) (x : α × β) :

(a • x).swap = a • x.swap

source

theorem prod.smul_zero_mk {M : Type u_1} {β : Type u_6} [has_smul M β] {α : Type u_2} [monoid M] [add_monoid α] [distrib_mul_action M α] (a : M) (c : β) :

a • (0, c) = (0, a • c)

source

theorem prod.smul_mk_zero {M : Type u_1} {α : Type u_5} [has_smul M α] {β : Type u_2} [monoid M] [add_monoid β] [distrib_mul_action M β] (a : M) (b : α) :

a • (b, 0) = (a • b, 0)

source

@[protected, instance]

def prod.has_pow {E : Type u_4} {α : Type u_5} {β : Type u_6} [has_pow α E] [has_pow β E] :

has_pow (α × β) E

Equations

prod.has_pow = {pow := λ (p : α × β) (c : E), (p.fst ^ c, p.snd ^ c)}

source

@[simp]

theorem prod.pow_fst {E : Type u_4} {α : Type u_5} {β : Type u_6} [has_pow α E] [has_pow β E] (p : α × β) (c : E) :

(p ^ c).fst = p.fst ^ c

source

@[simp]

theorem prod.pow_snd {E : Type u_4} {α : Type u_5} {β : Type u_6} [has_pow α E] [has_pow β E] (p : α × β) (c : E) :

(p ^ c).snd = p.snd ^ c

source

@[simp]

theorem prod.pow_mk {E : Type u_4} {α : Type u_5} {β : Type u_6} [has_pow α E] [has_pow β E] (c : E) (a : α) (b : β) :

(a, b) ^ c = (a ^ c, b ^ c)

source

theorem prod.pow_def {E : Type u_4} {α : Type u_5} {β : Type u_6} [has_pow α E] [has_pow β E] (p : α × β) (c : E) :

p ^ c = (p.fst ^ c, p.snd ^ c)

source

@[simp]

theorem prod.pow_swap {E : Type u_4} {α : Type u_5} {β : Type u_6} [has_pow α E] [has_pow β E] (p : α × β) (c : E) :

(p ^ c).swap = p.swap ^ c

source

@[protected, instance]

def prod.vadd_assoc_class {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [has_vadd M α] [has_vadd M β] [has_vadd N α] [has_vadd N β] [has_vadd M N] [vadd_assoc_class M N α] [vadd_assoc_class M N β] :

vadd_assoc_class M N (α × β)

source

@[protected, instance]

def prod.is_scalar_tower {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [has_smul M α] [has_smul M β] [has_smul N α] [has_smul N β] [has_smul 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_5} {β : Type u_6} [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_5} {β : Type u_6} [has_smul M α] [has_smul M β] [has_smul N α] [has_smul N β] [smul_comm_class M N α] [smul_comm_class M N β] :

smul_comm_class M N (α × β)

source

@[protected, instance]

def prod.is_central_vadd {M : Type u_1} {α : Type u_5} {β : Type u_6} [has_vadd M α] [has_vadd M β] [has_vadd Mᵃᵒᵖ α] [has_vadd Mᵃᵒᵖ β] [is_central_vadd M α] [is_central_vadd M β] :

is_central_vadd M (α × β)

source

@[protected, instance]

def prod.is_central_scalar {M : Type u_1} {α : Type u_5} {β : Type u_6} [has_smul M α] [has_smul M β] [has_smul Mᵐᵒᵖ α] [has_smul Mᵐᵒᵖ β] [is_central_scalar M α] [is_central_scalar M β] :

is_central_scalar M (α × β)

source

@[protected, instance]

def prod.has_faithful_vadd_left {M : Type u_1} {α : Type u_5} {β : Type u_6} [has_vadd M α] [has_vadd M β] [has_faithful_vadd M α] [nonempty β] :

has_faithful_vadd M (α × β)

source

@[protected, instance]

def prod.has_faithful_smul_left {M : Type u_1} {α : Type u_5} {β : Type u_6} [has_smul M α] [has_smul M β] [has_faithful_smul M α] [nonempty β] :

has_faithful_smul M (α × β)

source

@[protected, instance]

def prod.has_faithful_vadd_right {M : Type u_1} {α : Type u_5} {β : Type u_6} [has_vadd M α] [has_vadd M β] [nonempty α] [has_faithful_vadd M β] :

has_faithful_vadd M (α × β)

source

@[protected, instance]

def prod.has_faithful_smul_right {M : Type u_1} {α : Type u_5} {β : Type u_6} [has_smul M α] [has_smul M β] [nonempty α] [has_faithful_smul M β] :

has_faithful_smul 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_smul M N] [has_smul 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_smul M N] [has_smul 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_5} {β : Type u_6} {m : add_monoid M} [add_action M α] [add_action M β] :

add_action M (α × β)

Equations

prod.add_action = {to_has_vadd := prod.has_vadd add_action.to_has_vadd, zero_vadd := _, add_vadd := _}

source

@[protected, instance]

def prod.mul_action {M : Type u_1} {α : Type u_5} {β : Type u_6} {m : monoid M} [mul_action M α] [mul_action M β] :

mul_action M (α × β)

Equations

prod.mul_action = {to_has_smul := prod.has_smul mul_action.to_has_smul, one_smul := _, mul_smul := _}

source

@[protected, instance]

def prod.smul_zero_class {R : Type u_1} {M : Type u_2} {N : Type u_3} [has_zero M] [has_zero N] [smul_zero_class R M] [smul_zero_class R N] :

smul_zero_class R (M × N)

Equations

prod.smul_zero_class = {to_has_smul := prod.has_smul smul_zero_class.to_has_smul, smul_zero := _}

source

@[protected, instance]

def prod.distrib_smul {R : Type u_1} {M : Type u_2} {N : Type u_3} [add_zero_class M] [add_zero_class N] [distrib_smul R M] [distrib_smul R N] :

distrib_smul R (M × N)

Equations

prod.distrib_smul = {to_smul_zero_class := prod.smul_zero_class distrib_smul.to_smul_zero_class, smul_add := _}

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

prod.distrib_mul_action = {to_mul_action := prod.mul_action distrib_mul_action.to_mul_action, smul_zero := _, smul_add := _}

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

prod.mul_distrib_mul_action = {to_mul_action := prod.mul_action mul_distrib_mul_action.to_mul_action, smul_mul := _, smul_one := _}

Scalar multiplication as a homomorphism #

source

@[simp]

theorem smul_mul_hom_apply {α : Type u_5} {β : Type u_6} [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_5} {β : Type u_6} [monoid α] [has_mul β] [mul_action α β] [is_scalar_tower α β β] [smul_comm_class α β β] :

α × β →ₙ* β

Scalar multiplication as a multiplicative homomorphism.

Equations

smul_mul_hom = {to_fun := λ (a : α × β), a.fst • a.snd, map_mul' := _}

source

def smul_monoid_hom {α : Type u_5} {β : Type u_6} [monoid α] [mul_one_class β] [mul_action α β] [is_scalar_tower α β β] [smul_comm_class α β β] :

α × β →* β

Scalar multiplication as a monoid homomorphism.

Equations

smul_monoid_hom = {to_fun := smul_mul_hom.to_fun, map_one' := _, map_mul' := _}

source

@[simp]

theorem smul_monoid_hom_apply {α : Type u_5} {β : Type u_6} [monoid α] [mul_one_class β] [mul_action α β] [is_scalar_tower α β β] [smul_comm_class α β β] (ᾰ : α × β) :

⇑smul_monoid_hom ᾰ = smul_mul_hom.to_fun ᾰ