\import Algebra.Group
\import Algebra.Group.Representation.Category
\import Algebra.Group.Representation
\import Algebra.Module.ModuleCategory
\import Algebra.Ring
\import Function
\import Logic
\import Paths.Meta

\class SubLRepres {R : Ring} {G : Group} (E : LinRepres R G) (\classifying S : LinRepres R G) {
  | in : InterwiningMap S E
  | in-mono : IsInj in

  \func isTrivial => IsZeroMod S || IsSurj in

  \func \infix  **'in (g : G)(s : S) : S => (LinRepres.** {S}) g s

}

\func KernelSubLRepres{R : Ring} {G : Group} {A B : LinRepres R G} (f : InterwiningMap A B) : SubLRepres A \cowith
  | S => KerLRepres f
  | in => KerLRepresHom f
  | in-mono {a a' : KerLRepres f} => \lam (p : KerLRepresHom f a = KerLRepresHom f a') => exts p

\func ImageSubLRepres {R : Ring} {G : Group} {A B : LinRepres R G} (f : InterwiningMap A B) : SubLRepres B \cowith
  | S => ImageLRepres {R} {G} {A} {B} f
  | in => ImageLRepresRightHom f
  | in-mono {a a' : ImageLRepres f} => \lam (p : ImageLRepresRightHom f a = ImageLRepresRightHom f a') => ext p