# Sigma instances for additive and multiplicative actions #

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

• GroupTheory.GroupAction.Pi
• GroupTheory.GroupAction.Prod
• GroupTheory.GroupAction.Sum
instance Sigma.VAdd {ι : Type u_1} {M : Type u_2} {α : ιType u_4} [(i : ι) → VAdd M (α i)] :
VAdd M ((i : ι) × α i)
Equations
• Sigma.VAdd = { vadd := fun (a : M) => Sigma.map id fun (x : ι) (x_1 : α x) => a +ᵥ x_1 }
instance Sigma.instSMul {ι : Type u_1} {M : Type u_2} {α : ιType u_4} [(i : ι) → SMul M (α i)] :
SMul M ((i : ι) × α i)
Equations
• Sigma.instSMul = { smul := fun (a : M) => Sigma.map id fun (x : ι) (x_1 : α x) => a x_1 }
theorem Sigma.vadd_def {ι : Type u_1} {M : Type u_2} {α : ιType u_4} [(i : ι) → VAdd M (α i)] (a : M) (x : (i : ι) × α i) :
a +ᵥ x = Sigma.map id (fun (x : ι) (x_1 : α x) => a +ᵥ x_1) x
theorem Sigma.smul_def {ι : Type u_1} {M : Type u_2} {α : ιType u_4} [(i : ι) → SMul M (α i)] (a : M) (x : (i : ι) × α i) :
a x = Sigma.map id (fun (x : ι) (x_1 : α x) => a x_1) x
@[simp]
theorem Sigma.vadd_mk {ι : Type u_1} {M : Type u_2} {α : ιType u_4} [(i : ι) → 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 : ι) → SMul M (α i)] (a : M) (i : ι) (b : α i) :
a i, b = i, a b
instance Sigma.instIsScalarTowerOfVAdd {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ιType u_4} [(i : ι) → VAdd M (α i)] [(i : ι) → VAdd N (α i)] [VAdd M N] [∀ (i : ι), VAddAssocClass M N (α i)] :
VAddAssocClass M N ((i : ι) × α i)
Equations
• =
instance Sigma.instIsScalarTowerOfSMul {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ιType u_4} [(i : ι) → SMul M (α i)] [(i : ι) → SMul N (α i)] [SMul M N] [∀ (i : ι), IsScalarTower M N (α i)] :
IsScalarTower M N ((i : ι) × α i)
Equations
• =
instance Sigma.instVAddCommClass {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ιType u_4} [(i : ι) → VAdd M (α i)] [(i : ι) → VAdd N (α i)] [∀ (i : ι), VAddCommClass M N (α i)] :
VAddCommClass M N ((i : ι) × α i)
Equations
• =
instance Sigma.instSMulCommClass {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ιType u_4} [(i : ι) → SMul M (α i)] [(i : ι) → SMul N (α i)] [∀ (i : ι), SMulCommClass M N (α i)] :
SMulCommClass M N ((i : ι) × α i)
Equations
• =
instance Sigma.instIsCentralVAdd {ι : Type u_1} {M : Type u_2} {α : ιType u_4} [(i : ι) → VAdd M (α i)] [(i : ι) → VAdd Mᵃᵒᵖ (α i)] [∀ (i : ι), IsCentralVAdd M (α i)] :
IsCentralVAdd M ((i : ι) × α i)
Equations
• =
instance Sigma.instIsCentralScalar {ι : Type u_1} {M : Type u_2} {α : ιType u_4} [(i : ι) → SMul M (α i)] [(i : ι) → SMul Mᵐᵒᵖ (α i)] [∀ (i : ι), IsCentralScalar M (α i)] :
IsCentralScalar M ((i : ι) × α i)
Equations
• =
theorem Sigma.FaithfulVAdd' {ι : Type u_1} {M : Type u_2} {α : ιType u_4} [(i : ι) → VAdd M (α i)] (i : ι) [FaithfulVAdd M (α i)] :
FaithfulVAdd M ((i : ι) × α i)

This is not an instance because i becomes a metavariable.

theorem Sigma.FaithfulSMul' {ι : Type u_1} {M : Type u_2} {α : ιType u_4} [(i : ι) → SMul M (α i)] (i : ι) [FaithfulSMul M (α i)] :
FaithfulSMul M ((i : ι) × α i)

This is not an instance because i becomes a metavariable.

instance Sigma.instFaithfulVAddOfNonempty {ι : Type u_1} {M : Type u_2} {α : ιType u_4} [(i : ι) → VAdd M (α i)] [] [∀ (i : ι), FaithfulVAdd M (α i)] :
FaithfulVAdd M ((i : ι) × α i)
Equations
• =
instance Sigma.instFaithfulSMulOfNonempty {ι : Type u_1} {M : Type u_2} {α : ιType u_4} [(i : ι) → SMul M (α i)] [] [∀ (i : ι), FaithfulSMul M (α i)] :
FaithfulSMul M ((i : ι) × α i)
Equations
• =
instance Sigma.instAddAction {ι : Type u_1} {M : Type u_2} {α : ιType u_4} {m : } [(i : ι) → AddAction M (α i)] :
AddAction M ((i : ι) × α i)
Equations