\import Algebra.Group
\import Algebra.Group.Representation.Category
\import Algebra.Group.Representation
\import Algebra.Group.Representation.Sub
\import Algebra.Module.ModuleCategory
\import Algebra.Module.LinearMap
\import Algebra.Ring
\import Category
\import Logic

\func Irreducible {R : Ring}{G : Group} (E : LinRepres R G) => \Pi (A : SubLRepres E) -> A.isTrivial

\class Hom-between-Irreducible \noclassifying {R : Ring}{G : Group} {A B : LinRepres R G} (p : Irreducible A) (q : Irreducible B) {
  \func Schur's-Lemma (f : InterwiningMap A B) : IsZeroMap f || Iso f => \case q (ImageSubLRepres f) \with {
    | byLeft zero-image => byLeft (ZeroIm=>Zero-func zero-image)
    | byRight full-image => \case p (KernelSubLRepres f) \with {
      | byLeft zero-ker => byRight (repr+module-iso=>repr-iso (iso<->zeroKer-FullIm. (zero-ker, full-image)))
      | byRight full-ker => byLeft (FullKer=>Zero-func full-ker)
    }
  }
}