\import Algebra.Group
\import Algebra.Module
\import Algebra.Monoid
\import Algebra.Pointed
\import Algebra.Semiring
\import Logic
\import Operations
\import Order.Lattice
\import Paths
\import Paths.Meta
\import Set.Subset
\import Topology.TopAbGroup
\import Topology.TopAbGroup.Complete
\import Topology.TopAbGroup.Product
\import Topology.TopRing
\import Topology.TopSpace
\import Topology.TopSpace.Product

\class TopLModule \extends LModule, TopAbGroup {
  \override R : TopRing
  | *c-cont : ContMap (ProductTopSpace R \this) \this \lam s => s. *c s.
  | negative-cont => transport (ContMap \this \this) { -1 *c __} (ext \lam a => neg_ide_*c) (*c-cont ContMap.∘ ProductTopSpace.tuple (ContMap.const -1) ContMap.id)
}

\class HausdorffTopLModule \extends TopLModule, HausdorffTopAbGroup

\class CompleteTopLModule \extends HausdorffTopLModule, CompleteTopAbGroup

\func RingTopLModule (R : TopRing) : TopLModule R R \cowith
  | TopAbGroup => R
  | *c => *
  | *c-assoc => *-assoc
  | *c-ldistr => ldistr
  | *c-rdistr => rdistr
  | ide_*c => ide-left
  | *c-cont => *-cont

\instance ProductTopLModule {R : TopRing} (X Y : TopLModule R) : TopLModule R (\Sigma X Y)
  | TopAbGroup => ProductTopAbGroup X Y
  | *c r (x,y) => (r *c x, r *c y)
  | *c-assoc => ext (*c-assoc,*c-assoc)
  | *c-ldistr => ext (*c-ldistr,*c-ldistr)
  | *c-rdistr => ext (*c-rdistr,*c-rdistr)
  | ide_*c => ext (ide_*c,ide_*c)
  | *c-cont => \new ContMap {
    | func-cont {W} f {(r,s)} Wst => \case f Wst \with {
      | inP (U,Uo,Ust,V,Vo,Vst,g) => \case *c-cont.func-cont Uo {r,s.} Ust, *c-cont.func-cont Vo {r,s.} Vst \with {
        | inP (U1,U1o,U1s1,V1,V1o,V1t1,f1), inP (U2,U2o,U2s2,V2,V2o,V2t2,f2) => inP (U1 ∧ U2, open-inter U1o U2o, (U1s1,U2s2), Set.Prod V1 V2, Prod-open V1o V2o, (V1t1,V2t2), \lam c d => g (f1 c. d.) (f2 c. d.))
      }
    }
  }

\instance TopLModuleHasProduct (R : TopRing) : HasProduct (TopLModule R)
  | Product => ProductTopLModule {R}