Documentation

Mathlib.Algebra.Group.Action.Sigma

Sigma instances for additive and multiplicative actions #

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

See also #

source
instance Sigma.instSMul_mathlib {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [(i : ι) → SMul M (α i)] :
SMul M ((i : ι) × α i)
Equations
    source
    instance Sigma.VAdd {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [(i : ι) → _root_.VAdd M (α i)] :
    _root_.VAdd M ((i : ι) × α i)
    Equations
      source
      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 = map id (fun (x : ι) (x_1 : α x) => a • x_1) x
      source
      theorem Sigma.vadd_def {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [(i : ι) → _root_.VAdd M (α i)] (a : M) (x : (i : ι) × α i) :
      a +ᵥ x = map id (fun (x : ι) (x_1 : α x) => a +ᵥ x_1) x
      source
      @[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⟩
      source
      @[simp]
      theorem Sigma.vadd_mk {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [(i : ι) → _root_.VAdd M (α i)] (a : M) (i : ι) (b : α i) :
      a +ᵥ ⟨i, b⟩ = ⟨i, a +ᵥ b⟩
      source
      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)
      source
      instance Sigma.instVAddAssocClassOfVAdd {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [(i : ι) → _root_.VAdd M (α i)] [(i : ι) → _root_.VAdd N (α i)] [_root_.VAdd M N] [∀ (i : ι), VAddAssocClass M N (α i)] :
      VAddAssocClass M N ((i : ι) × α i)
      source
      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)
      source
      instance Sigma.instVAddCommClass {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [(i : ι) → _root_.VAdd M (α i)] [(i : ι) → _root_.VAdd N (α i)] [∀ (i : ι), VAddCommClass M N (α i)] :
      VAddCommClass M N ((i : ι) × α i)
      source
      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)
      source
      instance Sigma.instIsCentralVAdd {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [(i : ι) → _root_.VAdd M (α i)] [(i : ι) → _root_.VAdd Mᵃᵒᵖ (α i)] [∀ (i : ι), IsCentralVAdd M (α i)] :
      IsCentralVAdd M ((i : ι) × α i)
      source
      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.

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

      This is not an instance because i becomes a metavariable.

      source
      instance Sigma.instFaithfulSMulOfNonempty {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [(i : ι) → SMul M (α i)] [Nonempty ι] [∀ (i : ι), FaithfulSMul M (α i)] :
      FaithfulSMul M ((i : ι) × α i)
      source
      instance Sigma.instFaithfulVAddOfNonempty {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [(i : ι) → _root_.VAdd M (α i)] [Nonempty ι] [∀ (i : ι), FaithfulVAdd M (α i)] :
      FaithfulVAdd M ((i : ι) × α i)
      source
      instance Sigma.instMulAction {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} {m : Monoid M} [(i : ι) → MulAction M (α i)] :
      MulAction M ((i : ι) × α i)
      Equations
        source
        instance Sigma.instAddAction {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} {m : AddMonoid M} [(i : ι) → AddAction M (α i)] :
        AddAction M ((i : ι) × α i)
        Equations