Projective

\import AG.AffineScheme
\import AG.Scheme
\import AG.SchemeSite
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Monoid.Localization
\import Algebra.Monoid.MonoidHom
\import Algebra.Monoid.SubMonoid
\import Algebra.Ring.Graded
\import Algebra.Ring.Graded.Localization
\import Algebra.Ring.Localization
\import Algebra.Ring.RingCat
\import Algebra.Ring.RingHom
\import Algebra.Ring.SubRing
\import Arith.Nat
\import Category.Functor
\import Data.Or
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Relation.Equivalence
\open SubMonoid
\open Monoid
\open LocRing(isLocalization \as LR)
\open Localization

\type ProjCarrier (R : GradedCRing) => Given (a : R) ∃ (n : Nat) (isHomogen a (suc n))
  \where {
    \protected \lemma homogen (x : ProjCarrier R) : R.IsHomogen x.1
      => \case x.2 \with {
        | inP (n,h) => inP (suc n, h)
      }
  }

\instance ProjPreorder (R : GradedCRing) : Preorder (ProjCarrier R)
  | <= a b => TruncP (LDiv b.1 a.1)
  | <=-refl => inP LDiv.id-div
  | <=-transitive (inP y|x) (inP z|y) => inP (LDiv.trans z|y y|x)
  \where {
    \func toSpec.{u} {R : GradedCRing.{u}} : PreorderHom (ProjPreorder R) (Spec.satSite R) \cowith
      | func a => ((), a.1)
      | func-<= p => ((), p)
  }

\func Proj.{u} (R : GradedCRing.{u}) : Scheme
  => (site R).toScheme
  \where {
    \func SpecStructureSheaf.{u} {R : GradedCRing.{u}} : Functor (ProjPreorder R).op CRingCat
      => Comp (Spec.satSite R).R ProjPreorder.toSpec.op

    \lemma homogen-factor {R : GradedCRing} (a b : ProjCarrier R) (b<=a : b <= a) : ∃ (c : R) (k : Nat) (isHomogen c k) (b.1 = a.1 * c) \elim b<=a
      | inP a|b => R.homogen-factor a|b (ProjCarrier.homogen b) (ProjCarrier.homogen a)

    \lemma Func-homogen.{u} {R : GradedCRing.{u}} {a b : ProjCarrier R} (ba : b <= a) {x : LocRing (powers a.1)}
                            (xs : HomogenLocRing.subRing x) : HomogenLocRing.subRing (SpecStructureSheaf.Func ba x) \elim xs
      | inP ((x, _, inP (k,idp)), idp, n, xh, b^kh) => \case homogen-factor a b ba \with {
          | inP (c,cn,ch,a=bc) => inP ((x * pow c k, _, inP (k,idp)), LR.lift-quot-char x (pow a.1 k)
              (later $ inP (k,idp)) (~-lequiv1 simplify) (~-lequiv1 $ equation.cMonoid {pmap (pow __ k) a=bc *> R.pow_*-comm}),
              n + cn * k, homogen-* xh $ R.homogen-pow ch, rewrite (a=bc,R.pow_*-comm) $ homogen-* b^kh $ R.homogen-pow ch)
        }

    \lemma Func-homogen-conv.{u} {R : GradedCRing.{u}} {a b : ProjCarrier R} (ba : b <= a) {x : LocRing (powers a.1)}
                                 (xs : HomogenLocRing.subRing (SpecStructureSheaf.Func ba x))
      : ∃ (y : HomogenLocRing (powers a.1)) (SpecStructureSheaf.Func ba x = SpecStructureSheaf.Func ba y.1) \elim x, xs
      | in~ (x, _, inP (n,idp)), inP ((y, _, inP (k,idp)), yp, yn, y1h, y2h) => \case ~-unlequiv $ inv (pmap (* locR (pow a.1 n)) yp) *> LR.lift_inL-quot (later $ inP (n,idp)) (~-lequiv1 *-assoc) \with {
        | inP (_, inP (m,idp), p) => simplify at p $ \case ProjCarrier.homogen a, ProjCarrier.homogen b, R.homogen-factor (LDiv.make x $ inv $ p *> *-assoc *> *-comm) (R.IsHomogen_* (R.IsHomogen_* (inP (yn,y1h)) $ R.IsHomogen_pow $ ProjCarrier.homogen a) $ R.IsHomogen_pow $ ProjCarrier.homogen b) (R.IsHomogen_* (R.IsHomogen_pow $ ProjCarrier.homogen b) (R.IsHomogen_pow $ ProjCarrier.homogen b)) \with {
          | inP (an,ah), inP (bn,bh), inP (x',x'n,x'h,q) => \case R.degree-unique {y * pow a.1 n * pow b.1 m} {yn + an * n + bn * m} {yn + bn * m + x'n} (homogen-* (homogen-* y1h $ R.homogen-pow ah) $ R.homogen-pow bh) $ transportInv (isHomogen __ _) q $ homogen-* (homogen-* y2h $ R.homogen-pow bh) x'h \with {
            | inl y_=0 => \case ba \with {
              | inP (c,cp) => inP ((HomogenLocRing _).zro, yp *> ~-lequiv _ (later $ inP (n + m, idp)) (simplify $ pmap (y *) (pow_+ *> pmap (* _) (pmap (pow __ n) (inv cp) *> R.pow_*-comm) *> *-assoc *> pmap (_ *) *-comm) *> inv *-assoc *> inv *-assoc *> pmap (* pow c n) y_=0 *> R.zro_*-left) *> inv (SpecStructureSheaf.Func ba).func-zro)
            }
            | inr e => inP ((_, inP ((x', _, inP (n,idp)), idp, x'n, x'h, transport (isHomogen _) (NatSemiring.cancel-left _ $ +-comm *> NatSemiring.cancel-left yn (inv +-assoc *> e *> +-assoc)) $ R.homogen-pow ah)),
                            yp *> inv (LR.lift-quot-char x' _ (later $ inP (n,idp)) (~-lequiv1 simplify) $
                            ~-lequiv _ (later $ inP (m,idp)) $ simplify $ q *> *-comm *> inv *-assoc))
          }
        }
      }

    \func StructureSheaf.{u} {R : GradedCRing.{u}} : Functor (ProjPreorder R).op CRingCat.{u} \cowith
      | F a => HomogenLocRing (powers a.1)
      | Func {b} {a} ba => IRing.corestrict (SpecStructureSheaf.Func (\box ba) RingHom.∘ IRing.embed) $ unfold \lam s => Func-homogen ba s.2
      | Func-id => later $ exts \lam x => ext $ path \lam i => SpecStructureSheaf.Func-id i _
      | Func-o => later $ exts \lam x => ext $ path \lam i => SpecStructureSheaf.Func-o i _

    \lemma StructureSheaf-loc.{u} {R : GradedCRing.{u}} {a b : ProjCarrier R} {ba : b <= a} {x : StructureSheaf a}
                                  (L : Localization (powers x.1) (LocRing (powers b.1)) (SpecStructureSheaf.Func ba))
      : Localization (powers x) (StructureSheaf b) (StructureSheaf.Func ba) \cowith
      | localization-inv {_} (inP (k,idp)) => transportInv Inv (StructureSheaf.Func ba).func-pow $
        Inv.Inv_pow $ HomogenLocRing.homogen-Inv1 (ProjCarrier.homogen b) (L.localization-inv powers-id)
      | localization-inj {y} {z} p => \case L.localization-inj (pmap __.1 p) \with {
        | inP (_, inP (k,idp), q) => inP (_, inP (k,idp), ext $ pmap (_ *) IRing.embed.func-pow *> q *> pmap (_ *) (inv IRing.embed.func-pow))
      }
      | localization-surj z => \case L.localization-surj z.1 \with {
        | inP (y, _, inP (n,idp), p) => \case Func-homogen-conv ba $ transport HomogenLocRing.subRing p $ contains_* z.2 $ Func-homogen ba (HomogenLocRing.subRing.contains_pow x.2) \with {
          | inP (z,z_=y_) => inP (z, _, inP (n,idp), ext $ pmap (_ *) (pmap (SpecStructureSheaf.Func ba) MonoidHom.func-pow) *> p *> z_=y_)
        }
      }

    \func site.{u} (R : GradedCRing.{u}) : SatSchemeSite \cowith
      | P => ProjPreorder R
      | R => StructureSheaf
      | loc-exists {a} (in~ (x, y, inP (n,p)), inP (z,xyz,k,z1h,z2h)) => inP ((a.1 * z.1, \case a.2 \with {
        | inP (an,ah) => inP (an + k, homogen-* ah z1h)
      }), inP $ LDiv.make z.1 idp, StructureSheaf-loc $ transportInv (\lam r => Localization (powers r) _ _) xyz \case z.3 \with {
        | inP (n,p) => transportSubMonoid1 (later $ factor-right1 LR LR \lam x => LR.lift_inL)
          (inP (1, LDiv.make (locR (a.1 * z.2)) $ unfold $ ~-lequiv1 equation.cMonoid))
          \let ai => (LR {_} {powers a.1}).localization-inv $ inP (suc n, idp)
          \in inP (1, LDiv.make ai.inv $ inv $ ai.rotate-inv-right $ unfold $ ~-lequiv1 $ equation.cMonoid {p})
      })
      | loc-stable {a'} {a} {b} (inP a|a') (inP a|b) => \case a.2, R.homogen-factor a|a' (ProjCarrier.homogen a') (ProjCarrier.homogen a), R.homogen-factor a|b (ProjCarrier.homogen b) (ProjCarrier.homogen a) \with {
        | inP (an,ah), inP (c,cn,ch,a'=ac), inP (d,dn,dh,b=ad) => inP ((a.1 * (c * d), inP (an + (cn + dn), homogen-* ah $ homogen-* ch dh)),
          inP $ LDiv.make d $ pmap (* d) a'=ac *> *-assoc,
          inP $ LDiv.make c $ pmap (* _) b=ad *> *-assoc *> pmap (_ *) *-comm,
          (_, \box inP ((pow d (suc an), _, inP (dn,idp)), idp, dn * suc an, R.homogen-pow dh {suc an}, transport (isHomogen _) *-comm $ R.homogen-pow ah)),
          StructureSheaf-loc $ transportSubMonoid1 (factor-right1 LR LR \lam x => later LR.lift_inL)
            (inP (suc an, LDiv.make (locR (pow a.1 (suc an) * pow a.1 dn)) $ later (~-lequiv1 $ equation.cMonoid {b=ad, pmap (pow __ an) b=ad *> R.pow_*-comm}) *> pmap (* _) locR.func-pow))
            (inP (1, LDiv.make (inl~ (pow d an, _, later $ inP (suc dn, idp))) $ unfold $ ~-lequiv1 $ equation.cMonoid {b=ad})),
          StructureSheaf-loc $ transportSubMonoid1 (factor-right1 LR LR \lam x => later LR.lift_inL)
            (inP (suc an, LDiv.make (locR (pow a.1 dn) * locR (pow a'.1 (suc an))) $ inv (*-assoc {_} {_} {locR _} {locR _}) *>
                          pmap (* _) (LR.lift_inL-quot (later $ inP (dn,idp)) {pow d (suc an)} $ ~-lequiv1 simplify) *>
                          later (~-lequiv1 $ simplify $ inv (R.pow_*-comm {_} {_} {suc an}) *> pmap (pow __ (suc an))
                            (*-comm *> pmap (* d) a'=ac *> *-assoc)) *> pmap (* _) locR.func-pow))
            (inP (1, LDiv.make (inl~ (pow d an * pow c dn, _, later $ inP (suc dn, idp))) $ inv $ ide-left *>
              LR.lift-quot-char (pow d (suc an)) _ (later $ inP (dn,idp)) (~-lequiv1 simplify)
                (later $ ~-lequiv1 $ simplify $ equation.cMonoid {a'=ac, pmap (pow __ dn) a'=ac *> R.pow_*-comm}))))
      }
  }