mathlib documentation

group_theory.group_action.sigma

Sigma instances for additive and multiplicative actions #

This file defines instances for arbitrary sum of additive and multiplicative actions.

See also #

@[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
@[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
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
@[simp]
theorem sigma.vadd_mk {ι : Type u_1} {M : Type u_2} {α : ι Type u_4} [Π (i : ι), has_vadd M (α i)] (a : M) (i : ι) (b : α i) :
a +ᵥ i, b⟩ = i, a +ᵥ b
@[simp]
theorem sigma.smul_mk {ι : Type u_1} {M : Type u_2} {α : ι Type u_4} [Π (i : ι), has_smul M (α i)] (a : M) (i : ι) (b : α i) :
a i, b⟩ = i, a b
@[protected, instance]
def sigma.vadd_assoc_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)] [has_vadd M N] [ (i : ι), vadd_assoc_class M N (α i)] :
vadd_assoc_class M N (Σ (i : ι), α i)
@[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_vadd {ι : Type u_1} {M : Type u_2} {α : ι Type u_4} [Π (i : ι), has_vadd M (α i)] [Π (i : ι), has_vadd Mᵃᵒᵖ (α i)] [ (i : ι), is_central_vadd M (α i)] :
is_central_vadd M (Σ (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
@[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