-- | An equivalence between the category of saturated scheme sites and the category of schemes.

\import AG.RingedLocale.RingedLocaleCat
\import AG.Scheme
\import AG.SchemeSite
\import AG.SchemeSite.LRLSchemeSiteHom
\import AG.SchemeSite.SchemeSiteHom
\import AG.SchemeSite.SchemeSitePrecat
\import Algebra.Monoid
\import Algebra.Monoid.Localization
\import Algebra.Monoid.MonoidHom
\import Algebra.Monoid.SubMonoid
\import Algebra.Pointed
\import Algebra.Ring.Ideal
\import Category.Functor
\import Equiv
\import Function.Meta
\import Logic
\import Meta
\import Order.Lattice
\import Order.Lattice.CompleteLattice
\import Order.PartialOrder
\import Paths
\import Relation.Equivalence
\import Topology.Locale.PreorderSite
\open LRLSchemeSiteHom

\func SchemeSiteFunctor.{u} : FullyFaithfulFunctor SatSchemeSitePrecat.{u} LocallyRingedLocaleCat.{u} \cowith
  | F S => S.toScheme
  | Func f => (fromSchemeSiteHom f).toLRLHom
  | Func-id => later (path \lam i => (id_toLRL i).toLRLHom) *> LRL-equiv.f_ret _
  | Func-o {X} {Y} {Z} {g} {f} => path (\lam i => (fromSchemeSiteHom-natural {X} {Y} {Z} i).toLRLHom)
    *> inv (path \lam i => (fromSchemeSiteHom_toLRLHom {_} {_} {Z} {fromSchemeSiteHom f} i).toLRLHom)
    *> inv (toLRLHom-natural {_} {_} {_} {(fromSchemeSiteHom f).toLRLHom} {fromSchemeSiteHom g})
  | isFullyFaithful => IsEquiv.trans (inP SchemeSiteHom-equiv) (inP LRL-equiv)

\func LRL->SchemeSiteHom.{u} {S : Scheme.{u}} : LRLSchemeSiteHom S (maxSchemeSite S) \cowith
  | f* => LRL->SchemeSite.embedding {S} {S.IsAffineOpen} {\lam p => p}
  | f# => NatTrans.id
  | isLRLSchemeSiteHom-top => isLocallyAffine <=∘ Join-univ \lam {a} aff => S.L.IJoin-cond (later (a,aff))
  | isLRLSchemeSiteHom-meet {a} {b} => meet-univ (a.. meet-left) (b.. meet-right) <=∘ S.L.Join-distr>= <=∘ S.L.SJoin-univ
    (later \lam {c} ((c1<=ab, inP (x,xp)), (c2<=ab, inP (y,yp))) =>
      \have | (inP ca) => S.principal-o a. {meet-left} {S.R.F.Func (c1<=ab <=∘ meet-right) y} (S.principal_meet-left _ _ yp) xp
            | cb => S.principal-o b. {meet-right} {S.R.F.Func (c2<=ab <=∘ meet-left) x} (S.principal_meet-right _ xp _) yp
      \in S.L.SJoin-conde (later (c. ∧ c., S.principal-affine a. ca.)) $ later
            ((meet-left <=∘ c1<=ab <=∘ meet-left, inP ca), (meet-right <=∘ c2<=ab <=∘ meet-right, cb)))
  | isLRLSchemeSiteHom-loc {a} (ba, inP (y,yp)) {x} xp ca xi => yp. ca $
    transport Monoid.Inv (pmap (\lam r => Localization.liftHom1 xp _ xi (S.R.F.Func r y)) prop-pi *> xp.lift_inL) $
    (Localization.liftHom1 xp (S.R.F.Func ca) xi).func-Inv $ (S.principal-localization a. yp).localization-inv SubMonoid.powers-id
  \where {
    \lemma isIso : LRL->SchemeSiteHom.toLRLHom.IsIso
      => LRL->SchemeSiteHom.toLRLHom-iso
          (\lam {a} {U} U<=a a<=U => Cover.cover-basic {(maxSchemeSite S).toSite} $ Ideal.radical_ide {Ideal.sclosure _} $ Ideal.sclosure-univ {_} {_} {(Ideal.sclosure _).radical}
            (later \lam {y} (inP (_, inP ((d,Ud),idp), c, cd, ca, cl)) => \case U<=a Ud \with {
              | (da, inP (z,dp)) => \case cl.inv-char. $ transportInv Monoid.Inv (path \lam i => S.R.F.Func-o i z) $ (S.R.F.Func cd).func-Inv dp. \with {
                | inP (w, inP (k,y^k=zw)) => inP (k, transportInv (Ideal.sclosure _) y^k=zw $ ideal-right $ Ideal.sclosure-superset $ inP $ later
                  (d, d, (<=-refl, inP (, S.principal-id)), Ud, (da, inP (z,dp)), transport (\lam r => Localization _ _ (S.R.F.Func r)) prop-pi $ S.principal-localization a. dp))
              }
            }) $ Ideal.radical_ide $ a.. <=-refl  S.principal-id a<=U)
          (\lam b => inP (\lam c => c. <= b, <=-antisymmetric (meet-univ <=-refl (top-univ <=∘ isLocallyAffine) <=∘
            S.L.Join-ldistr>= <=∘ S.L.SJoin-univ \lam {c} aff => later $ aff. meet-right <=∘ Join-univ \lam {d} (d<=bc, inP (x,dp)) =>
            S.L.SJoin-conde (later (d, S.principal-affine aff dp)) (d<=bc <=∘ meet-left)) $ S.L.SJoin-univ \lam p => p))
          (\lam a => inP idEquiv)
  }