--- The total cohomology of Hilbert schemes is the module HILB

mod HILB is

    protecting RAT . --- Cohomology over the rational numbers

    sorts End Surf Part Alg . --- Endomorphims, Surface, Partitions, Algebra
    subsort Nat < Part .

    vars f g h k : End .
    vars a b : Rat .
    vars i j : Nat .
    vars m n : NzNat .
    vars p q : Part .
    vars c d s t u v : Surf .

-------------------
--- basic operators
-------------------

    --- Kronecker Symbol

    op kro(_ _) : Nat Nat -> Nat .

    eq kro (i j) = if i == j then 1 else 0 fi .

    --- Factorial

    op fact(_) : Nat -> Nat [memo].

    eq fact(0) = 1 .
    eq fact(i) = i * fact(i - 1) .

    --- Concatenation of partitions

    op _;_ : Part Part -> Part [assoc comm].

-----------------------------------------------------
--- Algebra of endomorphims over the rational numbers
-----------------------------------------------------

    ---- operations

    op O : -> End [ctor] . --- zero morphism
    op Id : -> End [ctor] . --- identity morphism

    op _+_ : End End -> End [assoc comm ctor prec 35 format (nt d d d)] . --- addition
    op __ : Rat End -> End [ctor prec 33] . --- multiplication by a scalar
    op _._ : End End -> End [ctor assoc prec 30] . --- composition
    op [__] : End End -> End . --- Lie bracket
    op P(__) : End Nat -> End . --- Iterated composition (power)

    --- Axioms for the addition

    eq f + f = 2 f .
    eq O + f = f .

   --- Axioms for the multiplication by a scalar

    eq a f + b f = (a + b) f .
    eq a (f + g) = a f + a g .
    eq a f + f = (a + 1) f .
    eq a (b f) = (a * b) f .
    eq 1 f = f .
    eq 0 f = O .
    eq a O = O .

    --- Axioms for the composition

    eq (a f) . g = a (f . g) .
    eq f . (a g) = a (f . g) .
    eq f . (h + k) = f . h + f . k .
    eq (f + g ) . h = f . h + g . h .
    eq Id . f = f .
    eq f . Id = f .
    eq O . f = O .
    eq f . O = O .

    --- Axioms for the Lie bracket

    eq [ f g ] = f . g + (-1) g . f .

    --- Axiom for iterated composition (power)

    eq P(f 0) = Id .
    eq P(f i) = f . P( f (i - 1) ) .


--------------------------------------------
--- Rational cohomology algebra of a surface
--------------------------------------------

   --- Usual classes

   op o : -> Surf [ctor] . --- zero class
   op I : -> Surf [ctor] . --- unit class
   op K : -> Surf [ctor] . --- canonical class
   op e : -> Surf [ctor] . --- Euler class
   op C : -> Surf . --- a degree 2 class (first Chern class)
   op D : -> Surf . --- a degree 4 class (second Chern class)

   --- Operations

   op _+_ : Surf Surf -> Surf [assoc comm ctor prec 35] . --- addition
   op __ : Rat Surf -> Surf [ctor prec 33] . --- external law
   op _._ : Surf Surf -> Surf [ctor assoc comm prec 30] . --- cup product
   op int(__) : Surf Surf -> Rat [comm] . --- intersection product
   op [_'] : Surf -> Surf . --- simulation of Kuenneth decomposition

   --- Axioms for the addition

    eq s + s = 2 s .
    eq o + s = s .

   --- Axioms for the external law

    eq a s + b s = (a + b) s .
    eq a (s + t) = a s + a t .
    eq a s + s = (a + 1) s .
    eq a (b s) = (a * b) s .
    eq 1 s = s .
    eq 0 s = o .
    eq a o = o .

    --- Axioms for the cup product

    eq (a s) . t = a (s . t) .
    eq s . (a t) = a (s . t) .
    eq s . (t + u) = s . t + s . u .
    eq (s + t) . u = s . u + t . u .
    eq I . s = s .
    eq o . s = o .

   --- special cases (for K3 or abelian surface)

    --- eq K = o .
    --- eq e = o .

   --- universal relations

   eq K . K . K = o .
   eq e . e = o .
   eq e . K = o .
   eq C . C . C = o .
   eq C . C . K = o .
   eq C . K . K = o .
   eq C . e = o .
   eq C . D = o .
   eq D . D = o .
   eq D . K = o .
   eq D . e = o .

--------------------
--- Vertex operators
--------------------

   op |> : -> End [ctor]. --- the vaccum, considered as an operator for simplicity
   op d : -> End . --- boundary operator
   op q(___) : Nat Surf NzNat -> End . --- derived Nakajima operator
   op <__> : Surf NzNat -> End . --- non-derived Nakajima operator
   op <<__>> : Surf Part -> End . --- Nakajima operator for a partition
   op L(__) : Surf NzNat -> End . --- Virasoro operator
   op Rec(___) : Surf NzNat NzNat -> End . --- recursive computation of L(__).|>
   op CH(__) : Surf Nat -> End [memo]. --- Chern character of a tautological class
   op Rec2(___) : Surf Nat Nat -> End . --- recursive computation of CH(__).|>
   op CHv(__) : Surf Nat -> End [memo]. --- Chern character of a dual tautological class
   op Rec2v(___) : Surf Nat Nat -> End . --- recursive computation of CHv(__).|>
   op C1(__) : Surf Nat -> End [memo]. --- Chern class of a tautological rank 1 bundle
   op C2(___) : Surf Surf Nat -> End [memo]. --- Chern class of a tautological rank 2 bundle
   op C2t(_) : Nat -> End [memo]. --- Chern class of a tautological rank 2 trivial bundle
   op C3t(_) : Nat -> End [memo]. --- Chern class of a tautological rank 3 trivial bundle
   op C4t(_) : Nat -> End [memo]. --- Chern class of a tautological rank 4 trivial bundle
   op C5t(_) : Nat -> End [memo]. --- Chern class of a tautological rank 5 trivial bundle
   op CHT(_) : Nat -> End [memo]. --- Chern character of the tangent bundle
   op Rec3(___) : Nat Nat NzNat -> End . --- recursive computation of CHT(_).|>
   --- Basics

   eq d . |> = O .
   eq < o n > = O .
   eq << o p >> = O .

   --- Derived Nakajima operators

   eq q(0 u n) = < u n > .
   eq q(i u n) = [ d  q( (i - 1) u n ) ] .
   eq d . < u n > = < u n > . d + n L( u n ) + ( n * (n - 1)) / 2 < (K . u) n > .

   --- Virasoro operators

   eq L(u n) . < v m > = < v m > . L(u n) + (-1) * m < (u . v) (n + m) > .
   eq L(u n) . |> = Rec(u n 1) .
   eq Rec(u n n) = O .
   eq Rec(u n m) = (1 / 2) < [ u '] m > . < [ u '] (n - m) > . |> + Rec(u n (m + 1)) .

   --- Chern character of a tautological class

   eq CH(c 0) = O .
   eq CH(c n) = (1 / n) < I 1 > . CH( c (n - 1) )
                + (1 / fact(n) ) Rec2(c 0 ( (2 * n) ) ) . P( < I 1 > (n - 1) ) . |> .

   eq Rec2(c j j) = (1 / fact(j) ) q(j c 1) .
   eq Rec2(c i j) = (1 / fact(i) ) q(i c 1) + Rec2(c (i + 1) j) .

   --- Chern character of a dual tautological class

   eq CHv(c 0) = O .
   eq CHv(c n) = (1 / n) < I 1 > . CHv( c (n - 1) )
                 + (1 / fact(n) ) Rec2v(c 0 ( (2 * n) ) ) . P( < I 1 > (n - 1) ) . |> .

   eq Rec2v(c j j) = ( ( (-1) ^ j ) / fact(j) ) q(j c 1) .
   eq Rec2v(c i j) = ( ( (-1) ^ i ) / fact(i) ) q(i c 1) + Rec2v(c (i + 1) j) .

   --- Chern class of a tautological bundle

       --- Rank 1: c is the first Chern class of a line bundle
   eq C1(c 0) = |> .
   eq C1(c i) = (1 / i) (< c 1 > + q(1 I 1)) . C1(c (i - 1)) .

       --- Rank 2: c is the first Chern class, d the second Chern class
   eq C2(c d 0) = |> .
   eq C2(c d i) = (1 / i) (< I 1 > + < c 1 > + < d 1 > + 2 q(1 I 1)
                  + q(1 c 1) + q(2 I 1) ) . C2(c d (i - 1)) .

       --- special cases: trivial bundles of ranks 2,3,4,5
   eq C2t(0) = |> .
   eq C2t(i) = (1 / i) (< I 1 > + 2 q(1 I 1) + q(2 I 1) ) . C2t((i - 1)) .

   eq C3t(0) = |> .
   eq C3t(i) = (1 / i) ( < I 1 > + 3 q(1 I 1) + 3 q(2 I 1) + q(3 I 1) ) . C3t((i - 1)) .

   eq C4t(0) = |> .
   eq C4t(i) = (1 / i) ( < I 1 > + 4 q(1 I 1) + 6 q(2 I 1) + 4 q(3 I 1)
               + q(4 I 1)) . C4t((i - 1)) .

   eq C5t(0) = |> .
   eq C5t(i) = (1 / i) ( < I 1 > + 5 q(1 I 1) + 10 q(2 I 1) + 10 q(3 I 1)
               + 5 q(4 I 1) + q(5 I 1)) . C5t((i - 1)) .

   --- Chern character of the tangent bundle

   eq CHT(0) = O .
   eq CHT(n) = (1 / n) < I 1 > . CHT((n - 1))
               + ((-1) / fact(n)) < e 1 > . P( < I 1 > (n - 1) ) . |>
               + (1 / fact(n) ) Rec3( 0 (2 * n) n) .

   eq Rec3(j j n) = (1 / fact(j)) ( q(j I 1) . P( < I 1 > (n - 1) ) . |>
          + (-1) fact(n - 1) q(j [ I '] 1) . CHv( [ I '] (n - 1) )
          + ((-1) / 2) fact(n - 1) q(j [ K '] 1) . CHv( [ K '] (n - 1))
          + ((-1) / 6) fact (n - 1) q(j [ (K . K) '] 1) . CHv([ (K . K) '] (n - 1) )
          + (1 / 12) fact(n - 1) q(j [ e '] 1) . CHv( [ e '] (n - 1) )
          + ((-1) ^ j) q(j I 1) . P( < I 1 > (n - 1) ) . |>
          + ((-1) ^ (j + 1)) q(j K 1) . P( < I 1 > (n - 1) ) . |>
          + (((-1) ^ j) / 2) q(j (K . K) 1) . P( < I 1 > (n - 1) ) . |>
          + ((-1) ^ (j + 1)) fact(n - 1) q(j [ I '] 1) . CH( [ I '] (n - 1))
          + (((-1) ^ j) / 2) fact(n - 1) q(j [ K '] 1) . CH( [ K '] (n - 1))
          + (((-1) ^ (j + 1)) / 6) fact(n - 1) q(j [ (K . K) '] 1) . CH( [ (K . K) '] (n - 1))
          + (((-1) ^ j) / 12) fact(n - 1) q(j [ e '] 1) . CH( [ e '] (n - 1)) ) .
   eq Rec3(i j n) = (1 / fact(i)) ( q(i I 1) . P( < I 1 > (n - 1) ) . |>
          + (-1) fact(n - 1) q(i [ I '] 1) . CHv( [ I '] (n - 1))
          + ((-1) / 2) fact(n - 1) q(i [ K '] 1) . CHv( [ K '] (n - 1))
          + ((-1) / 6) fact(n - 1) q(i [ (K . K) '] 1) . CHv( [ (K . K) '](n - 1))
          + (1 / 12) fact(n - 1) q(i [ e '] 1) . CHv( [ e '] (n - 1))
          + ((-1) ^ i) q(i I 1) . P( < I 1 > (n - 1) ) . |>
          + ((-1) ^ (i + 1)) q(i K 1) . P( < I 1 > (n - 1) ) . |>
          + (((-1) ^ i) / 2) q(i (K . K) 1) . P( < I 1 > (n - 1) ) . |>
          + ((-1) ^ (i + 1)) fact(n - 1) q(i [ I '] 1) . CH( [ I '] (n - 1))
          + (((-1) ^ i) / 2) fact(n - 1) q(i [ K '] 1) . CH( [ K '] (n - 1))
          + (((-1) ^ (i + 1)) / 6) fact(n - 1) q(i [ (K . K) '] 1) . CH( [ (K . K) '] (n - 1))
          + (((-1) ^ i) / 12) fact(n - 1) q(i [ e '] 1) . CH( [ e '] (n - 1)) )
          + Rec3( (i + 1) j n) .

   --- Rules for the final simplifications of Kuenneth decompositions

   rl [1] : < [ u ']  n > . < [ u '] m > => << u (n ; m) >> .
   rl [2] : < ( s . [ u '] )  n > . < [ u '] m > => << ( s . u ) (n ; m) >> .
   rl [3] : < [ u ']  n > . < ( t . [ u '] ) m > => << ( t . u ) (n ; m) >> .
   rl [4] : < ( s . [ u '] )  n > . < ( t . [ u '] ) m > => << ( s . t . u ) (n ; m) >> .

   rl [5] : <<  [ u ']  p >> . << [ u ']  q >> => <<  u  (p ; q) >> .
   rl [6] : << ( s . [ u '] )  p >> . << [ u ']  q >> => << ( s . u ) (p ; q) >> .
   rl [7] : << [ u ']  p >> . << ( t . [ u '] ) q >> => << ( t . u ) (p ; q) >> .
   rl [8] : << ( s . [ u '] )  p >> . << ( t . [ u '] ) q >> => << ( s . t . u ) (p ; q) >> .

   rl [9] : <<  [ u ']  p >> . < [ u ']  m > => <<  u  (p ; m) >> .
   rl [10] : << ( s . [ u '] )  p >> . < [ u ']  m > => << ( s . u ) (p ; m) >> .
   rl [11] : << [ u ']  p >> . < ( t . [ u '] ) m > => << ( t . u ) (p ; m) >> .
   rl [12] : << ( s . [ u '] )  p >> . < ( t . [ u '] ) m > => << ( s . t . u ) (p ; m) >> .

   rl [13] : < [ u ']   n > . << [ u ']  q >> => <<  u  (n ; q) >> .
   rl [14] : < ( s . [ u '] )  n > . << [ u ']  q >> => << ( s . u ) (n ; q) >> .
   rl [15] : < [ u ']  n > . << ( t . [ u '] ) q >> => << ( t . u ) (n ; q) >> .
   rl [16] : < ( s . [ u '] )  n > . << ( t . [ u '] ) q >> => << ( s . t . u ) (n ; q) >> .

   rl [17] : < ([u '] . [u ']) n > => < (e . u) n > .
   rl [18] : << ([u '] . [u ']) p >> => << (e . u) p >> .

   rl [19] : < (s . [u '] . [u ']) n > => < (s . e . u) n > .
   rl [20] : << (s . [u '] . [u ']) p >> => << (s . e . u) p >> .


   rl [1b] : <  [ u ']  n > . f . < [ u ']  m > =>  f . <<  u  (n ; m) >> .
   rl [2b] : < ( s . [ u '] )  n > . f . < [ u ']  m > => f . << ( s . u ) (n ; m) >> .
   rl [3b] : < [ u ']  n > . f . < ( t . [ u '] ) m > => f . << ( t . u ) (n ; m) >> .
   rl [4b] : < ( s . [ u '] )  n > . f . < ( t . [ u '] ) m > => f . << ( s . t . u ) (n ; m) >> .

   rl [5b] : <<  [ u ']  p >> . f . << [ u ']  q >> => f . <<  u  (p ; q) >> .
   rl [6b] : << ( s . [ u '] )  p >> . f . << [ u ']  q >> => f . << ( s . u ) (p ; q) >> .
   rl [7b] : << [ u ']   p >> . f . << ( t . [ u '] ) q >> => f . << ( t . u ) (p ; q) >> .
   rl [8b] : << ( s . [ u '] )  p >> . f . << ( t . [ u '] ) q >>
             => f . << ( s . t . u ) (p ; q) >> .

   rl [9b] : << [ u ']   p >> . f . < [ u ']  m > => f . <<  u  (p ; m) >> .
   rl [10b] : << ( s . [ u '] )  p >> . f . < [ u ']  m > => f . << ( s . u ) (p ; m) >> .
   rl [11b] : << [ u ']  p >> . f . < ( t . [ u '] ) m > => f . << ( t . u ) (p ; m) >> .
   rl [12b] : << ( s . [ u '] )  p >> . f . < ( t . [ u '] ) m >
              => f . << ( s . t . u ) (p ; m) >> .

   rl [13b] : <  [ u ']   n > . f . << [ u ']  q >> => f . <<  u  (n ; q) >> .
   rl [14b] : < ( s . [ u '] )  n > . f . << [ u ']  q >> => f . << ( s . u ) (n ; q) >> .
   rl [15b] : < [ u ']  n > . f . << ( t . [ u '] ) q >> => f . << ( t . u ) (n ; q) >> .
   rl [16b] : < ( s . [ u '] )  n > . f . << ( t . [ u '] ) q >>
              => f . << ( s . t . u ) (n ; q) >> .

endm

------------
--- Examples
------------

   --- Chern class of a tautological rank 2 bundle
   rew C2(c d 1) .
   rew C2(c d 2) .
   rew C2(c d 3) .

   --- Chern character of the tangent bundle
   rew CHT(1) .
   rew CHT(2) .
   rew CHT(3) .