Sum instances for additive and multiplicative actions #

This file defines instances for additive and multiplicative actions on the binary Sum type.

See also #

GroupTheory.GroupAction.Option
GroupTheory.GroupAction.Pi
GroupTheory.GroupAction.Prod
GroupTheory.GroupAction.Sigma

source

ink

instance Sum.hasVAdd {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : VAdd M α] [inst : VAdd M β] :

VAdd M (α ⊕ β)

Equations

Sum.hasVAdd = { vadd := fun a => Sum.map ((fun x x_1 => x +ᵥ x_1) a) ((fun x x_1 => x +ᵥ x_1) a) }

source

ink

instance Sum.instSMulSum {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : SMul M α] [inst : SMul M β] :

SMul M (α ⊕ β)

Equations

Sum.instSMulSum = { smul := fun a => Sum.map ((fun x x_1 => x • x_1) a) ((fun x x_1 => x • x_1) a) }

source

ink

theorem Sum.vadd_def {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : VAdd M α] [inst : VAdd M β] (a : M) (x : α ⊕ β) :

a +ᵥ x = Sum.map ((fun x x_1 => x +ᵥ x_1) a) ((fun x x_1 => x +ᵥ x_1) a) x

source

ink

theorem Sum.smul_def {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : SMul M α] [inst : SMul M β] (a : M) (x : α ⊕ β) :

a • x = Sum.map ((fun x x_1 => x • x_1) a) ((fun x x_1 => x • x_1) a) x

source

ink

@[simp]

theorem Sum.vadd_inl {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : VAdd M α] [inst : VAdd M β] (a : M) (b : α) :

a +ᵥ Sum.inl b = Sum.inl (a +ᵥ b)

source

ink

@[simp]

theorem Sum.smul_inl {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : SMul M α] [inst : SMul M β] (a : M) (b : α) :

a • Sum.inl b = Sum.inl (a • b)

source

ink

@[simp]

theorem Sum.vadd_inr {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : VAdd M α] [inst : VAdd M β] (a : M) (c : β) :

a +ᵥ Sum.inr c = Sum.inr (a +ᵥ c)

source

ink

@[simp]

theorem Sum.smul_inr {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : SMul M α] [inst : SMul M β] (a : M) (c : β) :

a • Sum.inr c = Sum.inr (a • c)

source

ink

@[simp]

theorem Sum.vadd_swap {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : VAdd M α] [inst : VAdd M β] (a : M) (x : α ⊕ β) :

Sum.swap (a +ᵥ x) = a +ᵥ Sum.swap x

source

ink

@[simp]

theorem Sum.smul_swap {M : Type u_3} {α : Type u_1} {β : Type u_2} [inst : SMul M α] [inst : SMul M β] (a : M) (x : α ⊕ β) :

Sum.swap (a • x) = a • Sum.swap x

source

ink

instance Sum.instIsScalarTowerSumInstSMulSumInstSMulSum {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [inst : SMul M α] [inst : SMul M β] [inst : SMul N α] [inst : SMul N β] [inst : SMul M N] [inst : IsScalarTower M N α] [inst : IsScalarTower M N β] :

IsScalarTower M N (α ⊕ β)

Equations

@Sum.instIsScalarTowerSumInstSMulSumInstSMulSum = @Sum.instIsScalarTowerSumInstSMulSumInstSMulSum.proof_1

source

ink

instance Sum.instVAddCommClassSumInstVAddSumInstVAddSum {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [inst : VAdd M α] [inst : VAdd M β] [inst : VAdd N α] [inst : VAdd N β] [inst : VAddCommClass M N α] [inst : VAddCommClass M N β] :

VAddCommClass M N (α ⊕ β)

Equations

@Sum.instVAddCommClassSumInstVAddSumInstVAddSum = @Sum.instVAddCommClassSumInstVAddSumInstVAddSum.proof_1

source

ink

def Sum.instVAddCommClassSumInstVAddSumInstVAddSum.proof_1 {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [inst : VAdd M α] [inst : VAdd M β] [inst : VAdd N α] [inst : VAdd N β] [inst : VAddCommClass M N α] [inst : VAddCommClass M N β] :

VAddCommClass M N (α ⊕ β)

Equations

(_ : VAddCommClass M N (α ⊕ β)) = (_ : VAddCommClass M N (α ⊕ β))

source

ink

instance Sum.instSMulCommClassSumInstSMulSumInstSMulSum {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [inst : SMul M α] [inst : SMul M β] [inst : SMul N α] [inst : SMul N β] [inst : SMulCommClass M N α] [inst : SMulCommClass M N β] :

SMulCommClass M N (α ⊕ β)

Equations

@Sum.instSMulCommClassSumInstSMulSumInstSMulSum = @Sum.instSMulCommClassSumInstSMulSumInstSMulSum.proof_1

source

ink

def Sum.instIsCentralVAddSumInstVAddSumAddOpposite.proof_1 {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : VAdd M α] [inst : VAdd M β] [inst : VAdd Mᵃᵒᵖ α] [inst : VAdd Mᵃᵒᵖ β] [inst : IsCentralVAdd M α] [inst : IsCentralVAdd M β] :

IsCentralVAdd M (α ⊕ β)

Equations

(_ : IsCentralVAdd M (α ⊕ β)) = (_ : IsCentralVAdd M (α ⊕ β))

source

ink

instance Sum.instIsCentralVAddSumInstVAddSumAddOpposite {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : VAdd M α] [inst : VAdd M β] [inst : VAdd Mᵃᵒᵖ α] [inst : VAdd Mᵃᵒᵖ β] [inst : IsCentralVAdd M α] [inst : IsCentralVAdd M β] :

IsCentralVAdd M (α ⊕ β)

Equations

@Sum.instIsCentralVAddSumInstVAddSumAddOpposite = @Sum.instIsCentralVAddSumInstVAddSumAddOpposite.proof_1

source

ink

instance Sum.instIsCentralScalarSumInstSMulSumMulOpposite {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : SMul M α] [inst : SMul M β] [inst : SMul Mᵐᵒᵖ α] [inst : SMul Mᵐᵒᵖ β] [inst : IsCentralScalar M α] [inst : IsCentralScalar M β] :

IsCentralScalar M (α ⊕ β)

Equations

@Sum.instIsCentralScalarSumInstSMulSumMulOpposite = @Sum.instIsCentralScalarSumInstSMulSumMulOpposite.proof_1

source

ink

def Sum.FaithfulVAddLeft.proof_1 {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : VAdd M α] [inst : VAdd M β] [inst : FaithfulVAdd M α] :

FaithfulVAdd M (α ⊕ β)

Equations

(_ : FaithfulVAdd M (α ⊕ β)) = (_ : FaithfulVAdd M (α ⊕ β))

source

ink

instance Sum.FaithfulVAddLeft {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : VAdd M α] [inst : VAdd M β] [inst : FaithfulVAdd M α] :

FaithfulVAdd M (α ⊕ β)

Equations

@Sum.FaithfulVAddLeft = @Sum.FaithfulVAddLeft.proof_1

source

ink

instance Sum.FaithfulSMulLeft {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : SMul M α] [inst : SMul M β] [inst : FaithfulSMul M α] :

FaithfulSMul M (α ⊕ β)

Equations

@Sum.FaithfulSMulLeft = @Sum.FaithfulSMulLeft.proof_1

source

ink

instance Sum.FaithfulVAddRight {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : VAdd M α] [inst : VAdd M β] [inst : FaithfulVAdd M β] :

FaithfulVAdd M (α ⊕ β)

Equations

@Sum.FaithfulVAddRight = @Sum.FaithfulVAddRight.proof_1

source

ink

def Sum.FaithfulVAddRight.proof_1 {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : VAdd M α] [inst : VAdd M β] [inst : FaithfulVAdd M β] :

FaithfulVAdd M (α ⊕ β)

Equations

(_ : FaithfulVAdd M (α ⊕ β)) = (_ : FaithfulVAdd M (α ⊕ β))

source

ink

instance Sum.FaithfulSMulRight {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : SMul M α] [inst : SMul M β] [inst : FaithfulSMul M β] :

FaithfulSMul M (α ⊕ β)

Equations

@Sum.FaithfulSMulRight = @Sum.FaithfulSMulRight.proof_1

source

ink

def Sum.instAddActionSum.proof_2 {M : Type u_3} {α : Type u_1} {β : Type u_2} {m : AddMonoid M} [inst : AddAction M α] [inst : AddAction M β] (a : M) (b : M) (x : α ⊕ β) :

a + b +ᵥ x = a +ᵥ (b +ᵥ x)

Equations

(_ : a + b +ᵥ x = a +ᵥ (b +ᵥ x)) = (_ : a + b +ᵥ x = a +ᵥ (b +ᵥ x))

source

ink

def Sum.instAddActionSum.proof_1 {M : Type u_3} {α : Type u_1} {β : Type u_2} {m : AddMonoid M} [inst : AddAction M α] [inst : AddAction M β] (x : α ⊕ β) :

0 +ᵥ x = x

Equations

(_ : 0 +ᵥ x = x) = (_ : 0 +ᵥ x = x)

source

ink

instance Sum.instAddActionSum {M : Type u_1} {α : Type u_2} {β : Type u_3} {m : AddMonoid M} [inst : AddAction M α] [inst : AddAction M β] :

AddAction M (α ⊕ β)

Equations

Sum.instAddActionSum = AddAction.mk (_ : ∀ (x : α ⊕ β), 0 +ᵥ x = x) (_ : ∀ (a b : M) (x : α ⊕ β), a + b +ᵥ x = a +ᵥ (b +ᵥ x))

source

ink

instance Sum.instMulActionSum {M : Type u_1} {α : Type u_2} {β : Type u_3} {m : Monoid M} [inst : MulAction M α] [inst : MulAction M β] :

MulAction M (α ⊕ β)

Equations

Sum.instMulActionSum = MulAction.mk (_ : ∀ (x : α ⊕ β), 1 • x = x) (_ : ∀ (a b : M) (x : α ⊕ β), (a * b) • x = a • b • x)