\import Algebra.Group
\import Algebra.Monoid
\import Algebra.Ring
\import Algebra.Semiring
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Paths
\import Paths.Meta
\open Monoid(Inv,LInv)

\class LocalRing \extends Ring, NonZeroRing {
| locality (x : E) : Inv x || Inv (x + ide)

\lemma locality_- (x : E) : Inv x || Inv (ide - x)
=> \case locality (negative x) \with {
| byLeft p => byLeft $transport Inv negative-isInv (Ring.negative_inv p) | byRight p => byRight$ transport Inv +-comm p
}

\lemma sum1=>eitherInv {x y : E} (x+y=1 : x + y = ide) : Inv x || Inv y => \case locality (negative x) \with {
| byLeft -x_inv => byLeft (rewriteI negative-isInv (Ring.negative_inv -x_inv))
| byRight [-x+1]_inv => byRight (rewriteEq (pmap (negative x +) x+y=1) [-x+1]_inv)
}

\lemma sumInv=>eitherInv {x y : E} (q : Inv (x + y)) : Inv x || Inv y =>
\case sum1=>eitherInv (inv ldistr *> q.inv-left) \with {
| byLeft s => byLeft (Inv.factor-right (\new LInv q.inv (x + y) q.inv-right) s)
| byRight s => byRight (Inv.factor-right (\new LInv q.inv (x + y) q.inv-right) s)
}

\lemma sumInvArray (l : Array E) (p : Inv (BigSum l)) : ∃ (j : Fin l.len) (Inv (l j)) \elim l
| nil => absurd (NonZeroSemiring.inv-nonZero p idp)
| a :: l => \case sumInv=>eitherInv p \with {
| byLeft r => inP (0, r)
| byRight r => TruncP.map (sumInvArray l r) \lam s => (suc s.1, s.2)
}

\lemma sum1Array (l : Array E) (p : BigSum l = 1) : ∃ (j : Fin l.len) (Inv (l j))
=> sumInvArray l (transportInv Inv p Inv.ide-isInv)

\lemma connected : IsConnected
=> local=>connected locality
} \where {
\lemma local=>connected {R : Ring} (loc : \Pi (a : R) -> Inv a || Inv (a + 1)) : R.IsConnected
=> \lam a p => \have q : a * (negative a + 1) = 0 => ldistr *> +-comm *> pmap (_ +) negative_*-right *> toZero (ide-right *> inv p)
\in \case loc (negative a) \with {
| byLeft (r : Inv) => byRight $inv$ fromZero $+-comm *> inv ide-left *> pmap (* _) (inv r.inv-left) *> *-assoc *> pmap (r.inv *) (negative_*-left *> pmap negative q *> negative_zro) *> zro_*-right | byRight (r : Inv) => byLeft$ inv ide-right *> pmap (a *) (inv r.inv-right) *> inv *-assoc *> pmap (* r.inv) q *> zro_*-left
}
}

\class LocalCRing \extends LocalRing, NonZeroCRing