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 #
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
@[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 (α × β)
@[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 (α × β)
@[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 (α × β)
@[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 (α × β)
@[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 (α × β)
@[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 (α × β)
@[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 (α × β)
@[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 (α × β)
@[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)
@[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)
@[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)
@[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 := _}
@[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 := _}
@[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
@[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 #
@[simp]
theorem
smul_mul_hom_apply
{α : Type u_5}
{β : Type u_6}
[monoid α]
[has_mul β]
[mul_action α β]
[is_scalar_tower α β β]
[smul_comm_class α β β]
(a : α × β) :
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.
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' := _}
@[simp]
theorem
smul_monoid_hom_apply
{α : Type u_5}
{β : Type u_6}
[monoid α]
[mul_one_class β]
[mul_action α β]
[is_scalar_tower α β β]
[smul_comm_class α β β]
(ᾰ : α × β) :