Sigma instances for additive and multiplicative actions

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

See also

• GroupTheory.GroupAction.Pi
• GroupTheory.GroupAction.Prod
• GroupTheory.GroupAction.Sum

ink

instance Sigma.VAdd {ι : Type u_1} {M : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → VAdd M (α i)] : VAdd M ((i : ι) × α i)

Equations

• Sigma.VAdd = { vadd := fun a => Sigma.map id fun x => (fun x_1 x_2 => x_1 +ᵥ x_2) a }

ink

instance Sigma.instSMulSigma {ι : Type u_1} {M : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → SMul M (α i)] : SMul M ((i : ι) × α i)

Equations

• Sigma.instSMulSigma = { smul := fun a => Sigma.map id fun x => (fun x_1 x_2 => x_1 • x_2) a }

ink

theorem Sigma.vadd_def {ι : Type u_1} {M : Type u_3} {α : ι → Type u_2} [inst : (i : ι) → VAdd M (α i)] (a : M) (x : (i : ι) × α i) : a +ᵥ x = Sigma.map id (fun x => (fun x_1 x_2 => x_1 +ᵥ x_2) a) x

ink

theorem Sigma.smul_def {ι : Type u_1} {M : Type u_3} {α : ι → Type u_2} [inst : (i : ι) → SMul M (α i)] (a : M) (x : (i : ι) × α i) : a • x = Sigma.map id (fun x => (fun x_1 x_2 => x_1 • x_2) a) x

ink

@[simp]

theorem Sigma.vadd_mk {ι : Type u_1} {M : Type u_3} {α : ι → Type u_2} [inst : (i : ι) → VAdd M (α i)] (a : M) (i : ι) (b : α i) : a +ᵥ { fst := i, snd := b } = { fst := i, snd := a +ᵥ b }

ink

@[simp]

theorem Sigma.smul_mk {ι : Type u_1} {M : Type u_3} {α : ι → Type u_2} [inst : (i : ι) → SMul M (α i)] (a : M) (i : ι) (b : α i) : a • { fst := i, snd := b } = { fst := i, snd := a • b }

ink

def Sigma.instIsScalarTowerSigmaInstVAddSigmaInstVAddSigma.proof_1 {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → VAdd M (α i)] [inst : (i : ι) → VAdd N (α i)] [inst : VAdd M N] [inst : ∀ (i : ι), VAddAssocClass M N (α i)] : VAddAssocClass M N ((i : ι) × α i)

Equations

• (_ : VAddAssocClass M N ((i : ι) × α i)) = (_ : VAddAssocClass M N ((i : ι) × α i))

ink

instance Sigma.instIsScalarTowerSigmaInstVAddSigmaInstVAddSigma {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → VAdd M (α i)] [inst : (i : ι) → VAdd N (α i)] [inst : VAdd M N] [inst : ∀ (i : ι), VAddAssocClass M N (α i)] : VAddAssocClass M N ((i : ι) × α i)

Equations

• @Sigma.instIsScalarTowerSigmaInstVAddSigmaInstVAddSigma = @Sigma.instIsScalarTowerSigmaInstVAddSigmaInstVAddSigma.proof_1

ink

instance Sigma.instIsScalarTowerSigmaInstSMulSigmaInstSMulSigma {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → SMul M (α i)] [inst : (i : ι) → SMul N (α i)] [inst : SMul M N] [inst : ∀ (i : ι), IsScalarTower M N (α i)] : IsScalarTower M N ((i : ι) × α i)

Equations

• @Sigma.instIsScalarTowerSigmaInstSMulSigmaInstSMulSigma = @Sigma.instIsScalarTowerSigmaInstSMulSigmaInstSMulSigma.proof_1

ink

instance Sigma.instVAddCommClassSigmaInstVAddSigmaInstVAddSigma {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → VAdd M (α i)] [inst : (i : ι) → VAdd N (α i)] [inst : ∀ (i : ι), VAddCommClass M N (α i)] : VAddCommClass M N ((i : ι) × α i)

Equations

• @Sigma.instVAddCommClassSigmaInstVAddSigmaInstVAddSigma = @Sigma.instVAddCommClassSigmaInstVAddSigmaInstVAddSigma.proof_1

ink

def Sigma.instVAddCommClassSigmaInstVAddSigmaInstVAddSigma.proof_1 {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → VAdd M (α i)] [inst : (i : ι) → VAdd N (α i)] [inst : ∀ (i : ι), VAddCommClass M N (α i)] : VAddCommClass M N ((i : ι) × α i)

Equations

• (_ : VAddCommClass M N ((i : ι) × α i)) = (_ : VAddCommClass M N ((i : ι) × α i))

ink

instance Sigma.instSMulCommClassSigmaInstSMulSigmaInstSMulSigma {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → SMul M (α i)] [inst : (i : ι) → SMul N (α i)] [inst : ∀ (i : ι), SMulCommClass M N (α i)] : SMulCommClass M N ((i : ι) × α i)

Equations

• @Sigma.instSMulCommClassSigmaInstSMulSigmaInstSMulSigma = @Sigma.instSMulCommClassSigmaInstSMulSigmaInstSMulSigma.proof_1

ink

def Sigma.instIsCentralVAddSigmaInstVAddSigmaAddOpposite.proof_1 {ι : Type u_1} {M : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → VAdd M (α i)] [inst : (i : ι) → VAdd Mᵃᵒᵖ (α i)] [inst : ∀ (i : ι), IsCentralVAdd M (α i)] : IsCentralVAdd M ((i : ι) × α i)

Equations

• (_ : IsCentralVAdd M ((i : ι) × α i)) = (_ : IsCentralVAdd M ((i : ι) × α i))

ink

instance Sigma.instIsCentralVAddSigmaInstVAddSigmaAddOpposite {ι : Type u_1} {M : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → VAdd M (α i)] [inst : (i : ι) → VAdd Mᵃᵒᵖ (α i)] [inst : ∀ (i : ι), IsCentralVAdd M (α i)] : IsCentralVAdd M ((i : ι) × α i)

Equations

• @Sigma.instIsCentralVAddSigmaInstVAddSigmaAddOpposite = @Sigma.instIsCentralVAddSigmaInstVAddSigmaAddOpposite.proof_1

ink

instance Sigma.instIsCentralScalarSigmaInstSMulSigmaMulOpposite {ι : Type u_1} {M : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → SMul M (α i)] [inst : (i : ι) → SMul Mᵐᵒᵖ (α i)] [inst : ∀ (i : ι), IsCentralScalar M (α i)] : IsCentralScalar M ((i : ι) × α i)

Equations

• @Sigma.instIsCentralScalarSigmaInstSMulSigmaMulOpposite = @Sigma.instIsCentralScalarSigmaInstSMulSigmaMulOpposite.proof_1

ink

theorem Sigma.FaithfulVAdd' {ι : Type u_3} {M : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → VAdd M (α i)] (i : ι) [inst : FaithfulVAdd M (α i)] : FaithfulVAdd M ((i : ι) × α i)

This is not an instance because i becomes a metavariable.

ink

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

This is not an instance because i becomes a metavariable.

ink

instance Sigma.instFaithfulVAddSigmaInstVAddSigma {ι : Type u_1} {M : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → VAdd M (α i)] [inst : Nonempty ι] [inst : ∀ (i : ι), FaithfulVAdd M (α i)] : FaithfulVAdd M ((i : ι) × α i)

Equations

• @Sigma.instFaithfulVAddSigmaInstVAddSigma = @Sigma.instFaithfulVAddSigmaInstVAddSigma.proof_1

ink

def Sigma.instFaithfulVAddSigmaInstVAddSigma.proof_1 {ι : Type u_1} {M : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → VAdd M (α i)] [inst : Nonempty ι] [inst : ∀ (i : ι), FaithfulVAdd M (α i)] : FaithfulVAdd M ((i : ι) × α i)

Equations

• (_ : FaithfulVAdd M ((i : ι) × α i)) = (_ : FaithfulVAdd M ((i : ι) × α i))

ink

instance Sigma.instFaithfulSMulSigmaInstSMulSigma {ι : Type u_1} {M : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → SMul M (α i)] [inst : Nonempty ι] [inst : ∀ (i : ι), FaithfulSMul M (α i)] : FaithfulSMul M ((i : ι) × α i)

Equations

• @Sigma.instFaithfulSMulSigmaInstSMulSigma = @Sigma.instFaithfulSMulSigmaInstSMulSigma.proof_1

ink

instance Sigma.instAddActionSigma {ι : Type u_1} {M : Type u_2} {α : ι → Type u_3} {m : AddMonoid M} [inst : (i : ι) → AddAction M (α i)] : AddAction M ((i : ι) × α i)

Equations

• Sigma.instAddActionSigma = AddAction.mk (_ : ∀ (x : (i : ι) × α i), 0 +ᵥ x = x) (_ : ∀ (a b : M) (x : (i : ι) × α i), a + b +ᵥ x = a +ᵥ (b +ᵥ x))

ink

def Sigma.instAddActionSigma.proof_1 {ι : Type u_1} {M : Type u_3} {α : ι → Type u_2} {m : AddMonoid M} [inst : (i : ι) → AddAction M (α i)] (x : (i : ι) × α i) : 0 +ᵥ x = x

Equations

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

ink

def Sigma.instAddActionSigma.proof_2 {ι : Type u_1} {M : Type u_3} {α : ι → Type u_2} {m : AddMonoid M} [inst : (i : ι) → AddAction M (α i)] (a : M) (b : M) (x : (i : ι) × α i) : a + b +ᵥ x = a +ᵥ (b +ᵥ x)

Equations

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

ink

instance Sigma.instMulActionSigma {ι : Type u_1} {M : Type u_2} {α : ι → Type u_3} {m : Monoid M} [inst : (i : ι) → MulAction M (α i)] : MulAction M ((i : ι) × α i)

Equations

• Sigma.instMulActionSigma = MulAction.mk (_ : ∀ (x : (i : ι) × α i), 1 • x = x) (_ : ∀ (a b : M) (x : (i : ι) × α i), (a * b) • x = a • b • x)