\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Pointed
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Operations
\import Paths
\import Paths.Meta
\import Set.Filter
\import Set.Subset
\import Topology.CoverSpace
\import Topology.CoverSpace.Complete
\import Topology.CoverSpace.CompletionTools
\import Topology.CoverSpace.Product
\import Topology.TopAbGroup
\import Topology.TopAbGroup.Product
\import Topology.TopSpace
\import Topology.TopSpace.Product
\import Topology.UniformSpace.Complete
\open Completion

\class CompleteTopAbGroup \extends TopAbGroup, CompleteUniformSpace

\func dense-topAb-lift {X Y : TopAbGroup} {Z : CompleteTopAbGroup} (f : TopAbGroupMap X Y) (fd : f.IsDenseTopEmbedding) (g : TopAbGroupMap X Z) : TopAbGroupMap Y Z \cowith
  | ContMap => dense-uniform-lift f (f.embedding->uniformEmbedding fd) g
  | func-+ {y} {y'} =>
    \have | g~ => dense-uniform-lift f (f.embedding->uniformEmbedding fd) g
          | g-char {x} : g~ (f x) = g x => dense-lift-char (fd., f.embedding->coverEmbedding (f.embedding->uniformEmbedding fd).) x
    \in dense-lift-unique (prod f f) (prod.isDense fd. fd.) (g~ ∘ Y.+-cont) (+-cont ∘ prod g~ g~) (\lam (x,x') => pmap g~ (inv f.func-+) *> g-char *> g.func-+ *> inv (pmap2 (+) g-char g-char)) (y,y')
  \where {
    \open ProductTopSpace
    \open ContMap
  }

\instance TopAbGroupCompletion (X : TopAbGroup) : CompleteTopAbGroup
  | CompleteUniformSpace => UniformCompletion X
  | AbGroup => abGroup
  | +-cont => +-cover
  | negative-cont => negative-cover
  | neighborhood-uniform => (\lam (inP (D,Du,g)) => \case neighborhood-uniform. Du \with {
    | inP (U1,U1o,U1_0,h) =>
      \have | (inP (U2,U2o,U2_0,h2)) => X.shrink U1o U1_0
            | (inP (U3,U3o,U3_0,h3)) => X.shrink U2o U2_0
      \in inP (mkSet U3, mkSet-open U3o, PrecoverSpace.open-char. U3o U3_0, \lam F => \case isCauchyFilter {F} (X.makeCauchy $ X.topAbUniform U3o U3_0) \with {
        | inP (_, inP (x,idp), Fx) => \case h x \with {
          | inP (V,DV,d) => \case g DV \with {
            | inP (U',CU',p) => inP (U', CU', \lam {G} q => p \case topAb-neighborhood. $ mkSet_<=<-point. q \with {
              | inP (U'',U''<=<U3,V1,FV1,V2,GV2,h') => filter-mono GV2 \lam {z} V2z => \case isProper (filter-meet Fx FV1) \with {
                | inP (y,(U3xy,V1y)) => d $ simplify in h2 (h3 U3xy U3_0) (h3 U3_0 $ <=<_<= (<=<_<= U''<=<U3 (h' V1y V2z)) idp)
              }
            })
          }
        }
      })
  }, \lam (inP (U1,U1o,U1_0,h1)) => \case <=<-inter $ (PrecoverSpace.open-char {Completion X}). (PrecoverSpace.cauchy-open. U1o) U1_0 \with {
    | inP (U2,U2_0,U2<=<U1) => \case X.shrink (completion.func-cont $ CoverSpace.interior {Completion X}) U2_0 \with {
      | (inP (U3,U3o,U3_0,h3)) => inP (_, X.topAbUniform U3o U3_0, \lam {_} (inP (x,idp)) => \case h1 (pointCF x) \with {
        | inP (V,CV,g) => inP (V, CV, \lam {F} FU3x => g $ <=<_<= (topAb-neighborhood. $
            inP (U2, U2<=<U1, X.UBall U3 x, X.open-char. (X.UBall-open U3o) $ X.UBall-center {U3} U3_0, _, FU3x,
              \lam {y} p {z} q => transport (\lam w => U2 (pointCF w)) X.diff-cancel-left $ <=<_<= (h3 q p) idp)) idp)
      })
    }
  })
  \where {
    \open ProductCoverSpace
    \open CoverMap

    \private \func abGroup : AbGroup (RegularCauchyFilter X) \cowith
      | zro => pointCF 
      | + => +-func
      | zro-left => unique1 (+-cover ∘ tuple (const _) id) id \lam x => +-char *> pmap pointCF zro-left
      | +-assoc => unique3 (+-cover ∘ prod +-cover id) (+-cover ∘ tuple (proj1 ∘ proj1) (+-cover ∘ prod proj2 id))
          \lam x y z => pmap (+-func __ _) +-char *> +-char *> pmap pointCF +-assoc *> inv (pmap (+-func _) +-char *> +-char)
      | negative => negative-cover
      | negative-left => unique1 (+-cover ∘ tuple negative-cover id) (const _) \lam x => pmap (+-func __ _) negative-char *> +-char *> pmap pointCF negative-left
      | +-comm => unique2 +-cover (+-cover ∘ tuple proj2 proj1) \lam x y => +-char *> pmap pointCF +-comm *> inv +-char

    \func subtract-cover : CoverMap (Completion X ⨯ Completion X) (Completion X)
      => lift2 (+-uniform ∘ prod id negative-uniform)

    \lemma subtract_- {F G : RegularCauchyFilter X} : subtract-cover (F,G) = F - {abGroup} G
      => unique2 subtract-cover (+-cover ∘ prod id negative-cover) \lam x y => lift2-char *> inv +-char *> pmap (+-func _) (inv negative-char)

    \sfunc +-cover : CoverMap (Completion X ⨯ Completion X) (Completion X)
      => subtract-cover ∘ prod id negative-cover

    \func +-func (x y : RegularCauchyFilter X) => +-cover (x,y)

    \lemma +-char {x y : X} : +-cover (pointCF x, pointCF y) = pointCF (x + y)
      => rewrite (\peval +-cover) $ pmap (\lam z => subtract-cover (pointCF x, z)) negative-char *> lift2-char *> simplify

    \sfunc negative-cover : CoverMap (Completion X) (Completion X)
      => subtract-cover ∘ tuple (const $ pointCF ) id

    \lemma negative-char {x : X} : negative-cover (pointCF x) = pointCF (negative x)
      => rewrite (\peval negative-cover) $ lift2-char *> simplify

    \lemma topAb-neighborhood {F G : RegularCauchyFilter X} {U : Set (Completion X)} : single (F - {abGroup} G) <=< U <->
      ∃ (U' : Set (Completion X)) (U' <=< U) (V1 : Set X) (F V1) (V2 : Set X) (G V2) ∀ {x : V1} {y : V2} (U' (pointCF (x - y)))
      => rewrite (inv subtract_-, \peval lift2 (+-uniform ∘ prod id negative-uniform)) $ completion-lift-neighborhood2 (completion ∘ +-uniform ∘ prod id negative-uniform) F G U
  }

\func completion-topAb {X : TopAbGroup} : TopAbGroupMap X (TopAbGroupCompletion X) \cowith
  | UniformMap => uniform-completion
  | func-+ => inv TopAbGroupCompletion.+-char