\import Algebra.Group
\import Algebra.Group.GroupHom
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Pointed
\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.CoverSpace.Complete
\import Topology.TopSpace
\import Topology.TopSpace.Product
\import Topology.UniformSpace

\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 ((+-cont ∘ tuple id (const x)).func-cont 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), (+-cont ∘ prod (const x) negative-cont ∘ tuple id id).func-cont 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 topAbProperUniform : 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 topAbUniform {U : Set E} (Uo : isOpen U) (U0 : U ) : PreuniformSpace.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)
    => (+-cont ∘ tuple (const x) negative-cont).func-cont Uo

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

  \lemma UBall-point {U : Set E} {x : E} (Ux : U x) : UBall U x 
    => transportInv U simplify Ux

  \lemma subtract-cont : ContMap (ProductTopSpace \this \this) \this \lam s => s. - s.
    => +-cont ∘ prod id negative-cont
} \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 (+-cont ∘ prod id negative-cont).func-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-left {X : TopAbGroup} {V U : Set X} (V<=<U : V <=<ta U) {x y z : X} (p : V (x - z)) (q : V (y - z)) : U (x - y)
  => transport U simplify (V<=<U p q)

\lemma <=<ta-right {X : TopAbGroup} {V U : Set X} (V<=<U : V <=<ta U) {x y z : X} (p : V (x - y)) (q : V (x - z)) : U (y - z)
  => transport U (simplify +-comm) (V<=<U q p)

\lemma topAb-sub-contAt {X Y : TopAbGroup} {S : Set X} {f : Set.Total S -> Y} {x : Set.Total S}
  : IsContAt {TopSub S} f x <-> ∀ {V : Y.isOpen} (V ) ∃ (U : X.isOpen) (U ) ∀ {x' : Set.Total S} (U (x. - x'.)) (V (f x - f x'))
  => (\lam fc {V} Vo V0 => \case fc (Y.UBall-open Vo) (Y.UBall-center {V} V0) \with {
    | inP (_, inP (U,Uo,idp), Ux, p) => inP (_, X.UBall-open Uo {x.}, X.UBall-point {U} Ux, \lam u => p $ simplify in u)
  }, \lam fc {V} Vo Vfx => \case fc (Y.UBall-open Vo {f x}) (Y.UBall-point {V} Vfx) \with {
    | inP (U,Uo,U0,g) => inP (_, inP (_, X.UBall-open Uo {x.}, idp), X.UBall-center {U} U0, \lam u => simplify in g u)
  })

\lemma topAb-contAt {X Y : TopAbGroup} {f : X -> Y} {x : X} : IsContAt f x <-> ∀ {V : Y.isOpen} (V ) ∃ (U : X.isOpen) (U ) ∀ {x'} (U (x - x')) (V (f x - f x'))
  => (\lam fc {V} Vo V0 => \case fc (Y.UBall-open Vo) (Y.UBall-center {V} V0) \with {
    | inP (U, Uo, Ux, p) => inP (_, X.UBall-open Uo, X.UBall-point {U} Ux, \lam u => p $ simplify in u)
  }, \lam fc {V} Vo Vfx => \case fc (Y.UBall-open Vo {f x}) (Y.UBall-point {V} Vfx) \with {
    | inP (U,Uo,U0,g) => inP (_, X.UBall-open Uo, X.UBall-center {U} U0, \lam u => simplify in g u)
  })

\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.topAbUniform 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) {}

\class HausdorffTopAbGroup \extends TopAbGroup, HausdorffTopSpace, SeparatedCoverSpace {
  \lemma equals {x y : E} (p : ∀ {U : isOpen} (U ) (U (x - y))) : x = y
    => fromZero $ isHausdorff \lam Uo Vo Ud V0 => inP (x - y, (Ud, p Vo V0))
}

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

  \default 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.IsDenseTopEmbedding) : UniformMap.IsDenseUniformEmbedding
    => (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
}