\import Algebra.Group
\import Algebra.Group.Representation
\import Algebra.Group.Representation.InterwiningMap
\import Algebra.Group.Representation.SubLRepres
\import Algebra.Group.SubGroup
\import Algebra.Ring
\import Equiv
\import Function.Meta
\import Logic

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

\lemma SchurLemma {R : Ring} {G : Group} {A B : LinRepres R G} (p : IsIrreducible A) (q : IsIrreducible B) (f : InterwiningMap A B) : f.IsZero || IsEquiv f
  => \case q (ImageLRepres f) \with {
    | byLeft iz => byLeft \lam x => iz $ inP (x, idp)
    | byRight if => \case p (KernelLRepres f) \with {
      | byLeft kz => byRight $ IsEquiv.fromInjSurj (AddKernel-trivial-char. kz) if
      | byRight kf => byLeft kf
    }
  }