Sigma 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 arbitrary sum of additive and multiplicative actions.

See also #

group_theory.group_action.pi
group_theory.group_action.prod
group_theory.group_action.sum

source

@[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)}

source

@[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)}

source

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

source

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

source

@[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⟩

source

@[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⟩

source

@[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)

source

@[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)

source

@[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)

source

@[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)

source

@[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)

source

@[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)

source

@[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.

source

@[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.

source

@[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)

source

@[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)

source

@[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 := _}

source

@[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 := _}