\import Algebra.Module
\import Algebra.Monoid
\import Algebra.Ring
\import Logic
\import Logic.Meta
\import Paths
\import Set.Subset
\import Topology.TopAbGroup
\import Topology.TopModule
\import Topology.TopSpace
\import Topology.TopSpace.Product
\open ContMap
\open ProductTopSpace

\class TopSemigroup \extends TopSpace, Semigroup
  | *-cont : ContMap (ProductTopSpace \this \this) \this \lam s => s. * s.

\class TopMonoid \extends TopSemigroup, Monoid {
  \lemma pow-cont {n : Nat} : IsCont (pow __ n) \elim n
    |  => ContMap.const 
    | suc n => *-cont ∘ tuple pow-cont id
}

\class TopRing \extends TopAbGroup, TopMonoid, Ring

\class NearSkewField \extends TopRing
  | inv-dense : IsDenseSet \lam (x : E) => Monoid.Inv x

\class NearField \extends NearSkewField, CRing

\lemma nearField-map-unique {R : NearSkewField} {Y : HausdorffTopLModule R} {U : Set R} (Uo : isOpen U) (f g : ContMap (TopSub U) Y)
                            (p : \Pi {h : R} (Uh : U h) -> h *c f (h,Uh) = h *c g (h,Uh)) {h : R} (Uh : U h) : f (h,Uh) = g (h,Uh)
  => denseSet-lift-unique (\lam {s} {_} (inP (V,Vo,idp)) Vs => \case inv-dense (open-inter Uo Vo) (s.,Vs) \with {
    | inP (h,hi,(Uh,Vh)) => inP ((h,Uh),hi,Vh)
  }) f g (\lam {s} (si : Monoid.Inv s.) => inv ide_*c *> pmap (`*c _) (inv si.inv-left) *> *c-assoc *> pmap (_ *c) (p s.) *> inv *c-assoc *> pmap (`*c _) si.inv-left *> ide_*c)

\lemma nearField-tmap-unique {R : NearSkewField} {Y : HausdorffTopLModule R} (f g : ContMap R Y)
                             (p : \Pi {h : R} -> h *c f h = h *c g h) {h : R} : f h = g h
  => nearField-map-unique open-top (f ∘ TopTransfer-map __.) (g ∘ TopTransfer-map __.) (\lam _ => p) {h} ()