\import Algebra.Group
\import Algebra.Group.Category
\import Algebra.Monoid
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.Lattice
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Set.Subset
\import Topology.CoverSpace
\import Topology.TopSpace
\import Topology.TopSpace.Product
\import Topology.UniformSpace
\open Bounded(top)

\class TopAbGroup \extends TopSpace, AbGroup, UniformSpace {
  | +-cont : ContMap (ProductTopSpace \this \this) \this \lam s => s. + s.
  | negative-cont : ContMap \this \this negative
  | neighborhood-uniform {C : Set (Set E)} : isUniform C <-> ∃ (U : isOpen) (U ) ∀ x ∃ (V : C) ∀ {y} (U (x - y) -> V y)
  | uniform-cover Cu x => \case neighborhood-uniform. Cu \with {
    | inP (U,Uo,U0,h) => \case h x \with {
      | inP (V,CV,g) => inP (V, CV, g $ transportInv U negative-right U0)
    }
  }
  | uniform-top => neighborhood-uniform. $ inP (top, open-top, (), \lam x => inP (top, idp, \lam _ => ()))
  | uniform-refine Cu e => \case neighborhood-uniform. Cu \with {
    | inP (U,Uo,U0,h) => neighborhood-uniform. $ inP (U, Uo, U0, \lam x => \case h x \with {
      | inP (V,CV,g) => \case e CV \with {
        | inP (W,DW,V<=W) => inP (W, DW, \lam u => V<=W $ g u)
      }
    })
  }
  | uniform-inter Cu Du => \case neighborhood-uniform. Cu, neighborhood-uniform. Du \with {
    | inP (U,Uo,U0,g), inP (V,Vo,V0,h) => neighborhood-uniform. $ inP (U ∧ V, open-inter Uo Vo, (U0,V0), \lam x => \case g x, h x \with {
      | inP (W,CW,f), inP (W',DW',f') => inP (W ∧ W', inP $ later (W, CW, W', DW', idp), \lam (u,u') => (f u, f' u'))
    })
  }
  | uniform-star Cu => \case neighborhood-uniform. Cu \with {
    | inP (U,Uo,U0,g) => \case shrink' +-cont negative-cont Uo U0 \with {
      | inP (V',V'o,V'0,h') => \case shrink' +-cont negative-cont V'o V'0 \with {
        | inP (V,Vo,V0,h) => inP (\lam W => ∃ (x : E) (W = \lam y => V (x - y)), neighborhood-uniform. $ inP (V, Vo, V0, \lam x => inP (\lam y => V (x - y), inP $ later (x, idp), \lam v => v)),
                                  \lam {_} (inP (x,idp)) => \case g x \with {
                                    | inP (U',CU',g') => inP (U', CU', \lam {_} (inP (x',idp)) (y,(Wy,W'y)) {z} W'z => g' $ simplify in h' (h Wy W'y) (h V0 W'z))
                                  })
      }
    }
  }

  \default cauchy-open {S} => (\lam So {x} Sx => uniform-cauchy. $ ClosurePrecoverSpace.closure $ neighborhood-uniform. \case shrink' +-cont negative-cont (func-cont {+-cont ∘ tuple id (const x)} So) (transportInv S zro-left Sx) \with {
    | inP (U',U'o,U'0,h') => \case shrink' +-cont negative-cont U'o U'0 \with {
      | inP (U,Uo,U0,h) => inP (U, Uo, U0, \lam y => inP (\lam z => U (y - z), later \lam Uyx {z} Uyz => simplify in h' (h U0 Uyz) (h U0 Uyx), \lam u => u))
    }
  }, \lam f => cover-open \lam {x} Sx => \case ClosurePrecoverSpace.closure-filter (NFilter x) (\lam Cu => \case neighborhood-uniform. Cu \with {
    | inP (U,Uo,U0,h) => \case h x \with {
      | inP (V,CV,g) => inP (V, CV, inP (\lam y => U (x - y), func-cont {+-cont ∘ prod (const x) negative-cont ∘ tuple id id} Uo, transportInv U negative-right U0, g __))
    }
  }) $ uniform-cauchy. $ f Sx \with {
    | inP (U, e, inP (V,Vo,Vx,V<=U)) => inP (V, Vo, Vx, V<=U <=∘ e (V<=U Vx))
  })

  \default isUniform C : \Prop => ∃ (U : isOpen) (U ) ∀ x ∃ (V : C) ∀ {y} (U (x - y) -> V y)
  \default neighborhood-uniform \as neighborhood-uniform-impl {C} : _ <-> _ => <->refl {isUniform C}

  \lemma properUniform : IsProperUniform
    => \lam Cu => \case neighborhood-uniform. Cu \with {
      | inP (U,Uo,U0,h) => neighborhood-uniform. $ inP (U, Uo, U0, \lam x => \case h x \with {
        | inP (V,CV,g) => inP (V, later (CV, inP (x, g $ transportInv U negative-right U0)), g)
      })
    }

  \func makeUniform {U : Set E} (Uo : isOpen U) (U0 : U ) : UniformSpace.isUniform \lam V => ∃ (x : E) (V = \lam y => U (x - y))
    => neighborhood-uniform. $ inP (U, Uo, U0, \lam x => inP (_, inP $ later (x, idp), \lam u => u))

  \lemma shrink {U : Set E} (Uo : isOpen U) (U0 : U ) : ∃ (V : isOpen) (V ) (V <=<ta U)
    => shrink' +-cont negative-cont Uo U0

  \func UBall (U : Set E) (x : E) : Set E => \lam x' => U (x - x')

  \lemma UBall-open {U : Set E} (Uo : isOpen U) {x : E} : isOpen (UBall U x)
    => func-cont {+-cont ∘ tuple (const x) negative-cont} Uo

  \lemma UBall-center {U : Set E} (U0 : U ) {x : E} : UBall U x x
    => transportInv U negative-right U0
} \where {
  \open ContMap
  \open ProductTopSpace

  \private \lemma shrink' {X : TopSpace} {A : AddGroup X} (+-cont : ContMap (ProductTopSpace X X) X \lam s => s. + s.) (negative-cont : ContMap X X negative)
                          {U : Set X} (Uo : isOpen U) (U0 : U ) : ∃ (V : isOpen) (V ) ∀ {x y : V} (U (x - y))
    => \case func-cont {+-cont ∘ prod id negative-cont} Uo {,} (transportInv U negative-right U0) \with {
      | inP (V,Vo,V0,W,Wo,W0,h) => inP (V ∧ W, open-inter Vo Wo, (V0,W0), \lam (Vx,_) (_,Wy) => h Vx Wy)
    }
}

\func \infix  <=<ta {X : TopAbGroup} (V U : Set X) : \Prop
  => ∀ {x y : V} (U (x - y))

\lemma <=<ta_<= {X : TopAbGroup} {V U : Set X} (V0 : V ) (p : V <=<ta U) : V ⊆ U
  => \lam Vx => transport U simplify (p Vx V0)

\lemma <=<ta_negative {X : TopAbGroup} {V U : Set X} (p : V <=<ta U) : negative ^-1 V <=<ta negative ^-1 U
  => \lam W-x W-y => simplify $ transport U +-comm $ simplify in p W-x W-y

\lemma <=<ta_<=*-shifted {X : TopAbGroup} {W V U : Set X} (Wo : isOpen W) (W0 : W ) (p : W <=<ta V) (q : V <=<ta U) {x : X} : X.UBall W x <=* X.UBall U x
  => inP (_, X.makeUniform Wo W0, \lam {y} (inP (_, (inP (z,idp), (w,(Wxw,Wzw))), Wzy)) => simplify in q (p Wxw Wzw) (p W0 Wzy))

\lemma <=<ta_<=* {X : TopAbGroup} {W V U : Set X} (Wo : isOpen W) (W0 : W ) (p : W <=<ta V) (q : V <=<ta U) : W <=* U
  => transport2 (<=*) (ext \lam x => simplify) (ext \lam x => simplify) $ <=<ta_<=*-shifted {X} {negative ^-1 W} {negative ^-1 V} {negative ^-1 U}
      (negative-cont.func-cont Wo) (simplify W0) (<=<ta_negative {_} {_} {V} p) (<=<ta_negative {_} {_} {U} q) {}

\record TopAbGroupMap \extends ContMap, AddGroupHom, UniformMap {
  \override Dom : TopAbGroup
  \override Cod : TopAbGroup

  | func-uniform Eu => \case neighborhood-uniform. Eu \with {
    | inP (U,Uo,U0,h) => neighborhood-uniform. $ inP (func ^-1 U, func-cont Uo, transportInv U func-zro U0, \lam x => \case h (func x) \with {
      | inP (V,EV,g) => inP (func ^-1 V, inP $ later (V, EV, idp), \lam u => g $ transport U func-minus u)
    })
  }

  \lemma embedding->uniformEmbedding (e : ContMap.IsDenseEmbedding) : UniformMap.IsDenseEmbedding
    => (e., \lam Cu => \case neighborhood-uniform. Cu \with {
      | inP (U,Uo,U0,h) => \case e. Uo \with {
        | inP (V,Vo,p) => neighborhood-uniform. \case TopAbGroup.shrink Vo $ transport V func-zro $ rewrite p in U0 \with {
          | inP (V',V'o,V'0,g) => inP (V', V'o, V'0, \lam y => inP (\lam y' => V' (y - y'), \case e. (UBall-open V'o {y}) (UBall-center {Cod} {V'} V'0) \with {
            | inP (_, inP (x,idp),V'yfx) => \case h x \with {
              | inP (W,CW,q) => inP $ later (W, CW, \lam {x'} V'yfx' => q $ rewrite p $ transport V (pmap (`- _) +-comm *> simplify +-comm *> inv func-minus) $ g V'yfx' V'yfx)
            }
          }, \lam v => v))
        }
      }
    })
} \where {
  \open TopAbGroup
}