mmarco/kenzo
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Extracted tests from serre.lisp.

Browse Source
This commit is contained in:
Gerd Heber 2015-07-28 06:47:14 -05:00
parent cb8a3d582c
commit 5dceced785
4 changed files with 248 additions and 225 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
kenzo-test.asd
View File

@ -35,6 +35,7 @@
(:file "loop-spaces-test") (:file "loop-spaces-test")
(:file "ls-twisted-products-test") (:file "ls-twisted-products-test")
(:file "searching-homology-test") (:file "searching-homology-test")
(:file "serre-test")
(:file "simplicial-groups-test") (:file "simplicial-groups-test")
(:file "simplicial-mrphs-test") (:file "simplicial-mrphs-test")
(:file "simplicial-sets-test") (:file "simplicial-sets-test")

3
package.lisp
View File

@ -415,6 +415,9 @@
;; serre.lisp ;; serre.lisp
BROWN-REDUCTION BROWN-REDUCTION
FIBRATION-DTAU-D
FIBRATION-DTAU-D-INTR
RIGHT-SERRE-EFHM
;; simplicial-mrphs.lisp ;; simplicial-mrphs.lisp

339
src/serre.lisp
View File

@ -7,116 +7,85 @@
(PROVIDE "serre") (PROVIDE "serre")
(DEFUN FIBRATION-DTAU-D-INTR (DEFUN FIBRATION-DTAU-D-INTR
(fibration &aux (base (sorc fibration)) (fibration &aux (base (sorc fibration))
(bface (face base)) (bface (face base))
(fibre (trgt fibration)) (fibre (trgt fibration))
(fface (face fibre)) (fface (face fibre))
(sintr-grml (sintr (grml fibre))) (sintr-grml (sintr (grml fibre)))
(fbspn (bspn fibre)) (fbspn (bspn fibre))
(sintr-twist (sintr fibration)) (sintr-twist (sintr fibration))
(total (fibration-total fibration)) (total (fibration-total fibration))
(total-cmpr (cmpr total))) (total-cmpr (cmpr total)))
(declare (declare
(type fibration fibration) (type fibration fibration)
(type simplicial-set base total) (type simplicial-set base total)
(type face bface fface) (type face bface fface)
(type simplicial-group fibre) (type simplicial-group fibre)
(type gmsm fbspn) (type gmsm fbspn)
(type sintr sintr-grml sintr-twist) (type sintr sintr-grml sintr-twist)
(type cmprf total-cmpr)) (type cmprf total-cmpr))
(flet ((rslt (dmns crpr (flet ((rslt (dmns crpr
&aux (dmns-1 (1- dmns))) &aux (dmns-1 (1- dmns)))
(declare (declare
(fixnum dmns dmns-1) (fixnum dmns dmns-1)
(type crpr crpr)) (type crpr crpr))
(unless (plusp dmns) (unless (plusp dmns)
(return-from rslt (return-from rslt
(zero-cmbn dmns-1))) (zero-cmbn dmns-1)))
(with-crpr (b-absm f-absm) crpr (with-crpr
(let ((tau-b (b-absm f-absm) crpr
(tw-a-sintr3 sintr-twist dmns (let ((tau-b
b-absm fbspn))) (tw-a-sintr3 sintr-twist dmns
(declare (type absm tau-b)) b-absm fbspn)))
(when (= (dgop tau-b) (mask dmns-1)) (declare (type absm tau-b))
(return-from rslt (when (= (dgop tau-b) (mask dmns-1))
(zero-cmbn dmns-1))) (return-from rslt
(let ((deln-b (zero-cmbn dmns-1)))
(a-face4 bface dmns dmns (let ((deln-b
b-absm)) (a-face4 bface dmns dmns
(deln-f b-absm))
(a-face4 fface dmns dmns (deln-f
f-absm))) (a-face4 fface dmns dmns
(declare f-absm)))
(type absm deln-b deln-f tau-b)) (declare
(let ((acrpr1 (2absm-acrpr deln-b deln-f)) (type absm deln-b deln-f tau-b))
(acrpr2 (let ((acrpr1 (2absm-acrpr deln-b deln-f))
(2absm-acrpr (acrpr2
deln-b (2absm-acrpr
(a-grml4 sintr-grml (1- dmns) deln-b
tau-b deln-f)))) (a-grml4 sintr-grml (1- dmns)
(declare (type absm acrpr1 acrpr2)) tau-b deln-f))))
(with-absm (dgop1 crpr1) acrpr1 (declare (type absm acrpr1 acrpr2))
(with-absm (dgop2 crpr2) acrpr2 (with-absm
(if (zerop dgop1) (dgop1 crpr1) acrpr1
(if (zerop dgop2) (with-absm
(dstr-add-term-to-cmbn (dgop2 crpr2) acrpr2
total-cmpr (if (zerop dgop1)
(-1-expt-n+1 dmns) crpr1 (if (zerop dgop2)
(term-cmbn dmns-1 (dstr-add-term-to-cmbn
(-1-expt-n dmns) total-cmpr
crpr2)) (-1-expt-n+1 dmns) crpr1
(term-cmbn dmns-1 (term-cmbn dmns-1
(-1-expt-n+1 dmns) (-1-expt-n dmns)
crpr1)) crpr2))
(if (zerop dgop2) (term-cmbn dmns-1
(term-cmbn dmns-1 (-1-expt-n+1 dmns)
(-1-expt-n dmns) crpr1))
crpr2) (if (zerop dgop2)
(zero-cmbn dmns-1))))))))))) (term-cmbn dmns-1
(the intr-mrph #'rslt))) (-1-expt-n dmns)
crpr2)
(zero-cmbn dmns-1)))))))))))
(the intr-mrph #'rslt)))
#|
(cat-init)
(setf s2 (sphere 2))
(setf k (k-z2-1))
(setf tw (build-smmr
:sorc s2
:trgt k
:degr -1
:sintr #'(lambda (dmns gmsm)
(absm 0 1))
:orgn '(s2-tw-kz2)))
(setf dt-d (fibration-dtau-d-intr tw))
(funcall dt-d 0 (crpr 0 '* 0 0))
(funcall dt-d 3 (crpr 4 's2 0 3))
(funcall dt-d 3 (crpr 2 's2 0 3))
(funcall dt-d 3 (crpr 2 's2 5 1))
(funcall dt-d 2 (crpr 0 's2 0 2))
(cat-init)
(setf s2 (sphere 2))
(setf k (k-z-1))
(setf tw (build-smmr
:sorc s2
:trgt k
:degr -1
:sintr #'(lambda (dmns gmsm)
(absm 0 (list 1)))
:orgn '(s2-tw-kz)))
(setf dt-d (fibration-dtau-d-intr tw))
(funcall dt-d 0 (crpr 0 '* 0 nil))
(funcall dt-d 3 (crpr 4 's2 0 '(2 3 4)))
(funcall dt-d 3 (crpr 2 's2 0 '(2 3 4)))
(funcall dt-d 3 (crpr 2 's2 5 '(5)))
(funcall dt-d 2 (crpr 0 's2 0 '(3 -2)))
|#
(DEFUN FIBRATION-DTAU-D (fibration (DEFUN FIBRATION-DTAU-D (fibration
&aux (base (sorc fibration)) &aux (base (sorc fibration))
(fibre (trgt fibration)) (fibre (trgt fibration))
(utotal (crts-prdc base fibre))) (utotal (crts-prdc base fibre)))
(declare (type fibration fibration)) (declare (type fibration fibration))
(the morphism (the morphism
(build-mrph (build-mrph
:sorc utotal :sorc utotal
:trgt utotal :trgt utotal
:degr -1 :degr -1
@ -124,135 +93,73 @@
:strt :gnrt :strt :gnrt
:orgn `(fibration-dtau-d ,fibration)))) :orgn `(fibration-dtau-d ,fibration))))
#|
(cat-init)
(setf s2 (sphere 2))
(setf k (k-z-1))
(setf tw (build-smmr
:sorc s2
:trgt k
:degr -1
:sintr #'(lambda (dmns gmsm)
(absm 0 (list 1)))
:orgn '(s2-tw-kz)))
(setf dt-d (fibration-dtau-d tw))
(? dt-d 0 (crpr 0 '* 0 nil))
(? dt-d 3 (crpr 4 's2 0 '(2 3 4)))
(? dt-d 3 (crpr 2 's2 0 '(2 3 4)))
(? dt-d 3 (crpr 2 's2 5 '(5)))
(? dt-d 2 (crpr 0 's2 0 '(3 -2)))
|#
(DEFUN BROWN-REDUCTION (fibration (DEFUN BROWN-REDUCTION (fibration
&aux (base (sorc fibration)) &aux (base (sorc fibration))
(fibre (trgt fibration)) (fibre (trgt fibration))
(total (fibration-total fibration)) (total (fibration-total fibration))
(ez (eilenberg-zilber base fibre)) (ez (eilenberg-zilber base fibre))
(t-perturbation (fibration-dtau-d fibration))) (t-perturbation (fibration-dtau-d fibration)))
(declare (declare
(type fibration fibration) (type fibration fibration)
(type simplicial-set base fibre total) (type simplicial-set base fibre total)
(type reduction ez) (type reduction ez)
(type morphism t-perturbation)) (type morphism t-perturbation))
(the (values reduction morphism) (the (values reduction morphism)
(multiple-value-bind (rslt b-perturbation) (add ez t-perturbation) (multiple-value-bind (rslt b-perturbation) (add ez t-perturbation)
(declare (declare
(type reduction rslt) (type reduction rslt)
(type morphism b-perturbation)) (type morphism b-perturbation))
(with-slots (f g h tcc) rslt (with-slots (f g h tcc) rslt
(setf tcc total) (setf tcc total)
(dstr-change-sorc-trgt f :new-sorc total) (dstr-change-sorc-trgt f :new-sorc total)
(dstr-change-sorc-trgt g :new-trgt total) (dstr-change-sorc-trgt g :new-trgt total)
(dstr-change-sorc-trgt h :new-sorc total :new-trgt total) (dstr-change-sorc-trgt h :new-sorc total :new-trgt total)
(values rslt b-perturbation))))) (values rslt b-perturbation)))))
#|
(cat-init)
(setf s2 (sphere 2))
(setf k (k-z2-1))
(setf tw (build-smmr
:sorc s2
:trgt k
:degr -1
:sintr #'(lambda (dmns gmsm)
(absm 0 1))
:orgn '(s2-tw-kz2)))
(setf brown (brown-reduction tw))
(setf tcc (tcc brown) bcc (bcc brown))
(homology bcc 3)
(homology tcc 1 8)
(homology bcc 1 8)
(cat-init)
(setf s2 (sphere 2))
(setf k (k-z-1))
(setf tw (build-smmr
:sorc s2
:trgt k
:degr -1
:sintr #'(lambda (dmns gmsm)
(absm 0 (list 1)))
:orgn '(s2-tw-kz1)))
(setf brown (brown-reduction tw))
(homology (tcc brown) 1 5)
(homology (bcc brown) 1 5)
|#
(DEFUN LEFT-SERRE-EFHM (fibration) (DEFUN LEFT-SERRE-EFHM (fibration)
(declare (type fibration fibration)) (declare (type fibration fibration))
(the homotopy-equivalence (the homotopy-equivalence
(build-hmeq (build-hmeq
:lrdct (trivial-rdct (fibration-total fibration)) :lrdct (trivial-rdct (fibration-total fibration))
:rrdct (brown-reduction fibration)))) :rrdct (brown-reduction fibration))))
(DEFUN RIGHT-SERRE-EFHM (fibration (DEFUN RIGHT-SERRE-EFHM (fibration
&aux (base (sorc fibration)) &aux (base (sorc fibration))
(fibre (trgt fibration)) (fibre (trgt fibration))
(base-efhm (efhm base)) (base-efhm (efhm base))
(fibre-efhm (efhm fibre)) (fibre-efhm (efhm fibre))
(uprdc-efhm (tnsr-prdc base-efhm fibre-efhm))) (uprdc-efhm (tnsr-prdc base-efhm fibre-efhm)))
(declare (declare
(type fibration fibration) (type fibration fibration)
(type simplicial-set base fibre) (type simplicial-set base fibre)
(type homotopy-equivalence base-efhm fibre-efhm uprdc-efhm)) (type homotopy-equivalence base-efhm fibre-efhm uprdc-efhm))
(the homotopy-equivalence (the homotopy-equivalence
(multiple-value-bind (brown b-perturbation) (brown-reduction fibration) (multiple-value-bind (brown b-perturbation) (brown-reduction fibration)
(declare (declare
(type reduction brown) (type reduction brown)
(type morphism b-perturbation)) (type morphism b-perturbation))
(let ((rslt (add uprdc-efhm b-perturbation))) (let ((rslt (add uprdc-efhm b-perturbation)))
(declare (type homotopy-equivalence rslt)) (declare (type homotopy-equivalence rslt))
(with-slots (lbcc lf lg lrdct) rslt (with-slots (lbcc lf lg lrdct) rslt
(declare (declare
(type chain-complex lbcc) (type chain-complex lbcc)
(type morphism lf lg) (type morphism lf lg)
(type reduction lrdct)) (type reduction lrdct))
(setf lbcc (bcc brown)) (setf lbcc (bcc brown))
(dstr-change-sorc-trgt lf :new-trgt lbcc) (dstr-change-sorc-trgt lf :new-trgt lbcc)
(dstr-change-sorc-trgt lg :new-sorc lbcc) (dstr-change-sorc-trgt lg :new-sorc lbcc)
(with-slots (bcc f g) lrdct (with-slots (bcc f g) lrdct
(declare (declare
(type chain-complex bcc) (type chain-complex bcc)
(type morphism f g)) (type morphism f g))
(setf bcc lbcc) (setf bcc lbcc)
(dstr-change-sorc-trgt f :new-trgt lbcc) (dstr-change-sorc-trgt f :new-trgt lbcc)
(dstr-change-sorc-trgt g :new-sorc lbcc))) (dstr-change-sorc-trgt g :new-sorc lbcc)))
rslt)))) rslt))))
#|
(cat-init)
(setf s2 (sphere 2))
(setf k (k-z-1))
(setf tw (build-smmr
:sorc s2
:trgt k
:degr -1
:sintr #'(lambda (dmns gmsm)
(absm 0 (list 1)))
:orgn '(s2-tw-kz1)))
(setf rh (right-serre-efhm tw))
(setf rbcc (rbcc rh))
(homology rbcc 0 5)
|#
(DEFUN FIBRATION-TOTAL-EFHM (fibration) (DEFUN FIBRATION-TOTAL-EFHM (fibration)
(declare (type fibration fibration)) (declare (type fibration fibration))
@ -260,27 +167,9 @@
(cmps (left-serre-efhm fibration) (cmps (left-serre-efhm fibration)
(right-serre-efhm fibration)))) (right-serre-efhm fibration))))
(DEFMETHOD SEARCH-EFHM (smst (orgn (eql 'fibration-total))) (DEFMETHOD SEARCH-EFHM (smst (orgn (eql 'fibration-total)))
(declare (declare
(type simplicial-set smst)) (type simplicial-set smst))
(the homotopy-equivalence (the homotopy-equivalence
(fibration-total-efhm (second (orgn smst))))) (fibration-total-efhm (second (orgn smst)))))
#|
(cat-init)
(setf s2 (sphere 2))
(setf k (k-z-1))
(setf tw (build-smmr
:sorc s2
:trgt k
:degr -1
:sintr #'(lambda (dmns gmsm)
(absm 0 (list 2)))
:orgn '(s2-tw-kz1)))
(setf p3r (fibration-total tw))
(homology p3r 1 )
|#

130
test/serre-test.lisp Normal file
View File

@ -0,0 +1,130 @@
(in-package :kenzo-test)
(in-suite :kenzo)
(test fibration-dtau-d-intr
(cat:cat-init)
(let* ((s2 (cat:sphere 2))
(k (cat:k-z2-1))
(tw (cat:build-smmr
:sorc s2
:trgt k
:degr -1
:sintr #'(lambda (dmns gmsm)
(cat:absm 0 1))
:orgn '(s2-tw-kz2)))
(dt-d (cat:fibration-dtau-d-intr tw)))
(funcall dt-d 0 (cat:crpr 0 '* 0 0))
(funcall dt-d 3 (cat:crpr 4 's2 0 3))
(funcall dt-d 3 (cat:crpr 2 's2 0 3))
(funcall dt-d 3 (cat:crpr 2 's2 5 1))
(funcall dt-d 2 (cat:crpr 0 's2 0 2))))
(test fibration-dtau-d-intr1
(cat:cat-init)
(let* ((s2 (cat:sphere 2))
(k (cat:k-z-1))
(tw (cat:build-smmr
:sorc s2
:trgt k
:degr -1
:sintr #'(lambda (dmns gmsm)
(cat:absm 0 (list 1)))
:orgn '(s2-tw-kz)))
(dt-d (cat:fibration-dtau-d-intr tw)))
(funcall dt-d 0 (cat:crpr 0 '* 0 nil))
(funcall dt-d 3 (cat:crpr 4 's2 0 '(2 3 4)))
(funcall dt-d 3 (cat:crpr 2 's2 0 '(2 3 4)))
(funcall dt-d 3 (cat:crpr 2 's2 5 '(5)))
(funcall dt-d 2 (cat:crpr 0 's2 0 '(3 -2)))))
(test fibration-dtau-d
(cat:cat-init)
(let* ((s2 (cat:sphere 2))
(k (cat:k-z-1))
(tw (cat:build-smmr
:sorc s2
:trgt k
:degr -1
:sintr #'(lambda (dmns gmsm)
(cat:absm 0 (list 1)))
:orgn '(s2-tw-kz)))
(dt-d (cat:fibration-dtau-d tw)))
(cat:? dt-d 0 (cat:crpr 0 '* 0 nil))
(cat:? dt-d 3 (cat:crpr 4 's2 0 '(2 3 4)))
(cat:? dt-d 3 (cat:crpr 2 's2 0 '(2 3 4)))
(cat:? dt-d 3 (cat:crpr 2 's2 5 '(5)))
(cat:? dt-d 2 (cat:crpr 0 's2 0 '(3 -2)))))
(test brown-reduction
(cat:cat-init)
(let* ((s2 (cat:sphere 2))
(k (cat:k-z2-1))
(tw (cat:build-smmr
:sorc s2
:trgt k
:degr -1
:sintr #'(lambda (dmns gmsm)
(cat:absm 0 1))
:orgn '(s2-tw-kz2)))
(brown (cat:brown-reduction tw))
(tcc (cat:tcc brown))
(bcc (cat:bcc brown)))
(cat:homology bcc 3)
(cat:homology tcc 1 8)
(cat:homology bcc 1 8)))
#|
(test brown-reduction1
(cat:cat-init)
(let* ((s2 (cat:sphere 2))
(k (cat:k-z-1))
(tw (cat:build-smmr
:sorc s2
:trgt k
:degr -1
:sintr #'(lambda (dmns gmsm)
(cat:absm 0 (list 1)))
:orgn '(s2-tw-kz)))
(brown (cat:brown-reduction tw)))
(cat:homology (cat:tcc brown) 1 5)
(cat:homology (cat:bcc brown) 1 5)))
|#
(test right-serre-efhm
(cat:cat-init)
(let* ((s2 (cat:sphere 2))
(k (cat:k-z-1))
(tw (cat:build-smmr
:sorc s2
:trgt k
:degr -1
:sintr #'(lambda (dmns gmsm)
(cat:absm 0 (list 1)))
:orgn '(s2-tw-kz1)))
(rh (cat:right-serre-efhm tw))
(rbcc (cat:rbcc rh)))
(cat:homology rbcc 0 5)))
(test fibration-total
(cat:cat-init)
(let* ((s2 (cat:sphere 2))
(k (cat:k-z-1))
(tw (cat:build-smmr
:sorc s2
:trgt k
:degr -1
:sintr #'(lambda (dmns gmsm)
(cat:absm 0 (list 1)))
:orgn '(s2-tw-kz1)))
(p3r (cat:fibration-total tw)))
(cat:homology p3r 1)))
(test dummy
(is (not (null t))))