Sigma instances for additive and multiplicative actions #
This file defines instances for arbitrary sum of additive and multiplicative actions.
See also #
group_theory.group_action.pi
group_theory.group_action.prod
group_theory.group_action.sum
@[protected, instance]
def
sigma.has_smul
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_4}
[Π (i : ι), has_smul M (α i)] :
has_smul M (Σ (i : ι), α i)
Equations
- sigma.has_smul = {smul := λ (a : M), sigma.map id (λ (i : ι), has_smul.smul a)}
@[protected, instance]
def
sigma.has_vadd
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_4}
[Π (i : ι), has_vadd M (α i)] :
has_vadd M (Σ (i : ι), α i)
Equations
- sigma.has_vadd = {vadd := λ (a : M), sigma.map id (λ (i : ι), has_vadd.vadd a)}
theorem
sigma.smul_def
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_4}
[Π (i : ι), has_smul M (α i)]
(a : M)
(x : Σ (i : ι), α i) :
a • x = sigma.map id (λ (i : ι), has_smul.smul a) x
theorem
sigma.vadd_def
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_4}
[Π (i : ι), has_vadd M (α i)]
(a : M)
(x : Σ (i : ι), α i) :
a +ᵥ x = sigma.map id (λ (i : ι), has_vadd.vadd a) x
@[protected, instance]
def
sigma.is_scalar_tower
{ι : Type u_1}
{M : Type u_2}
{N : Type u_3}
{α : ι → Type u_4}
[Π (i : ι), has_smul M (α i)]
[Π (i : ι), has_smul N (α i)]
[has_smul M N]
[∀ (i : ι), is_scalar_tower M N (α i)] :
is_scalar_tower M N (Σ (i : ι), α i)
@[protected, instance]
def
sigma.smul_comm_class
{ι : Type u_1}
{M : Type u_2}
{N : Type u_3}
{α : ι → Type u_4}
[Π (i : ι), has_smul M (α i)]
[Π (i : ι), has_smul N (α i)]
[∀ (i : ι), smul_comm_class M N (α i)] :
smul_comm_class M N (Σ (i : ι), α i)
@[protected, instance]
def
sigma.vadd_comm_class
{ι : Type u_1}
{M : Type u_2}
{N : Type u_3}
{α : ι → Type u_4}
[Π (i : ι), has_vadd M (α i)]
[Π (i : ι), has_vadd N (α i)]
[∀ (i : ι), vadd_comm_class M N (α i)] :
vadd_comm_class M N (Σ (i : ι), α i)
@[protected, instance]
def
sigma.is_central_scalar
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_4}
[Π (i : ι), has_smul M (α i)]
[Π (i : ι), has_smul Mᵐᵒᵖ (α i)]
[∀ (i : ι), is_central_scalar M (α i)] :
is_central_scalar M (Σ (i : ι), α i)
@[protected]
theorem
sigma.has_faithful_vadd'
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_4}
[Π (i : ι), has_vadd M (α i)]
(i : ι)
[has_faithful_vadd M (α i)] :
has_faithful_vadd M (Σ (i : ι), α i)
This is not an instance because i
becomes a metavariable.
@[protected]
theorem
sigma.has_faithful_smul'
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_4}
[Π (i : ι), has_smul M (α i)]
(i : ι)
[has_faithful_smul M (α i)] :
has_faithful_smul M (Σ (i : ι), α i)
This is not an instance because i
becomes a metavariable.
@[protected, instance]
def
sigma.has_faithful_smul
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_4}
[Π (i : ι), has_smul M (α i)]
[nonempty ι]
[∀ (i : ι), has_faithful_smul M (α i)] :
has_faithful_smul M (Σ (i : ι), α i)
@[protected, instance]
def
sigma.has_faithful_vadd
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_4}
[Π (i : ι), has_vadd M (α i)]
[nonempty ι]
[∀ (i : ι), has_faithful_vadd M (α i)] :
has_faithful_vadd M (Σ (i : ι), α i)
@[protected, instance]
def
sigma.add_action
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_4}
{m : add_monoid M}
[Π (i : ι), add_action M (α i)] :
add_action M (Σ (i : ι), α i)
Equations
- sigma.add_action = {to_has_vadd := sigma.has_vadd (λ (i : ι), add_action.to_has_vadd), zero_vadd := _, add_vadd := _}
@[protected, instance]
def
sigma.mul_action
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_4}
{m : monoid M}
[Π (i : ι), mul_action M (α i)] :
mul_action M (Σ (i : ι), α i)
Equations
- sigma.mul_action = {to_has_smul := sigma.has_smul (λ (i : ι), mul_action.to_has_smul), one_smul := _, mul_smul := _}