coincident-root-loci-0.2: test/Tests/Pushforward.hs

-- | Tests for the push-forward


{-# LANGUAGE Rank2Types, GADTs, TypeFamilies #-}
module Tests.Pushforward where

--------------------------------------------------------------------------------

import Data.Proxy

import Math.Combinat.Classes
import Math.Combinat.Partitions

import qualified Math.RootLoci.Algebra.FreeMod as ZMod

import Math.RootLoci.Algebra
import Math.RootLoci.Geometry
import Math.RootLoci.Misc

import Math.RootLoci.CSM.Equivariant.PushForward 

import Math.RootLoci.Classic

import Tests.Common

import Test.Tasty
import Test.Tasty.HUnit

--------------------------------------------------------------------------------

all_tests = testGroup "pushforward"
  [ testCase "tau definition"                                    (forList [-1..20] "failed" prop_tau_defin                 ) 
  , testCase "symm breaking pi_* == recursive formula for P_j"   (forAllInt 20 "failed" prop_symmbreaking_vs_ppolys        ) 
  , testCase "affine pi_* == proj pi_* [ gamma -> 0 ] /AB"       (forAllInt 20 "failed" (prop_ppoly_aff_vs_proj ChernRoot ))
  , testCase "affine pi_* == proj pi_* [ gamma -> 0 ] /Chern"    (forAllInt 20 "failed" (prop_ppoly_aff_vs_proj ChernClass))
  ]

prop_symmbreaking_vs_ppolys n = spec3' ChernRoot (piStarTableProj n) == pi_star_table n

prop_ppoly_aff_vs_proj sing n = spec2' sing (piStarTableAff n) == fmap forgetGamma (spec3' sing (piStarTableProj n))

prop_tau_defin n = (tau n * (a - b)) == (apow - bpow) where
  a    = ZMod.generator $ AB  1     0   
  b    = ZMod.generator $ AB  0     1   
  apow = ZMod.generator $ AB (n+1)  0   
  bpow = ZMod.generator $ AB  0    (n+1)

--------------------------------------------------------------------------------