Theorems · Definition · group theory

Representation.IntertwiningMap.tensor

{A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        {U : Type u_5} →
          [inst : CommSemiring A] →
            [inst_1 : Monoid G] →
              [inst_2 : AddCommMonoid V] →
                [inst_3 : AddCommMonoid W] →
                  [inst_4 : AddCommMonoid U] →
                    [inst_5 : Module A V] →
                      [inst_6 : Module A W] →
                        [inst_7 : Module A U] →
                          {ρ : Representation A G V} →
                            {σ : Representation A G W} →
                              {τ : Representation A G U} →
                                {P : Type u_6} →
                                  [inst_8 : AddCommMonoid P] →
                                    [inst_9 : Module A P] →
                                      {π : Representation A G P} →
                                        ρ.IntertwiningMap σ →
                                          τ.IntertwiningMap π → (ρ.tprod τ).IntertwiningMap (σ.tprod π)

The tensor product of intertwining maps induced from tensor product of linear maps.

Defined in

Mathlib.RepresentationTheory.Intertwining

Cited by

10 results in Mathlib

Foundations

Depth 68 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringMonoidAddCommMonoidAddCommMonoidAddCommMonoidModuleModuleModuleAddCommMonoidModule