From 0f614d77ea8fda22fdc17a1959ff169d01684e18 Mon Sep 17 00:00:00 2001 From: jodivaso Date: Mon, 2 Sep 2019 12:01:10 +0200 Subject: [PATCH] added pushouts --- kenzo.asd | 30 +- src/pushout/AiBjC-rdct.lisp | 95 +++++ src/pushout/Examples.lisp | 642 +++++++++++++++++++++++++++++++++ src/pushout/Pushout.lisp | 377 +++++++++++++++++++ src/pushout/cones2.lisp | 210 +++++++++++ src/pushout/direct-sum.lisp | 210 +++++++++++ src/pushout/remove-covers.lisp | 150 ++++++++ src/pushout/suspension2.lisp | 138 +++++++ src/special-smsts.lisp | 2 +- 9 files changed, 1842 insertions(+), 12 deletions(-) create mode 100644 src/pushout/AiBjC-rdct.lisp create mode 100644 src/pushout/Examples.lisp create mode 100644 src/pushout/Pushout.lisp create mode 100644 src/pushout/cones2.lisp create mode 100644 src/pushout/direct-sum.lisp create mode 100644 src/pushout/remove-covers.lisp create mode 100644 src/pushout/suspension2.lisp diff --git a/kenzo.asd b/kenzo.asd index 007a699..4a722b0 100644 --- a/kenzo.asd +++ b/kenzo.asd @@ -17,8 +17,7 @@ ((:file "package") (:module "src" :components - ( - (:file "kenzo") + ((:file "kenzo") (:file "abbreviations") (:file "macros") (:file "various") @@ -57,17 +56,26 @@ (:file "cl-space-efhm") (:file "whitehead") (:file "smith") - (:file "vf-order") (:file "sage-interface") - (:file "finite-topological-spaces") + (:module "anromero" :components - ((:file "resolutions") - (:file "cylinders") - (:file "fundamental-classes") - (:file "homotopy") - (:file "bicomplexes") + ((:file "bicomplexes") (:file "filtered-complexes") (:file "spectral-sequences") - (:file "persistent-homology") - )))))) + (:file "resolutions") + (:file "cylinders") + (:file "fundamental-classes") + (:file "homotopy"))) + + (:module "pushout" + :components + ((:file "AiBjC-rdct") + (:file "cones2") + (:file "direct-sum") + (:file "remove-covers") + (:file "suspension2") + (:file "Pushout"))) + + + )))) diff --git a/src/pushout/AiBjC-rdct.lisp b/src/pushout/AiBjC-rdct.lisp new file mode 100644 index 0000000..c7fe759 --- /dev/null +++ b/src/pushout/AiBjC-rdct.lisp @@ -0,0 +1,95 @@ +;;;============================================================================ +;;; +;;; Subject: AiBjC reduction +;;; +;;; +;;;---------------------------------------------------------------------------- +;;; +;;; Author: Jónathan Heras Vicente +;;; Extracted from Cones of GiftQ program of Francis Sergeraert +;;; 13/10/09 +;;; +;;;============================================================================ + +;;; Adapted by Julián Cuevas, Jose Divasón, Miguel Marco Buzunariz and Ana Romero. +;;; August 2019 + +(in-package #:cat) +(provide "AiBjC-rdct") + +(DEFUN AiBjC-RDCT-F-IMPL (j) + (declare (type morphism j)) + #'(lambda (cmbn) + (declare (type cmbn cmbn)) + (the cmbn + (multiple-value-bind (cmbnB cmbnA) + (cone-cmbn-split cmbn) + (declare (type cmbn cmbnB) (ignore cmbnA)) + (? j cmbnB))))) + + +(DEFUN AiBjC-RDCT-F (A i rho B j sigma C) + (declare (type chain-complex A B C) (type morphism i rho j sigma)) + (the morphism + (build-mrph + :sorc (cone i) + :trgt C + :degr 0 + :intr (AiBjC-RDCT-F-IMPL j) + :strt :cmbn + :orgn `(AiBjC-rdct-f ,A ,i ,rho ,B ,j ,sigma ,C)))) + + +(DEFUN AiBjC-RDCT-G-IMPL (rho B sigma) + (declare (type morphism sigma) (type chain-complex B)) + + #'(lambda (cmbn) + (declare (type cmbn cmbn)) + (the cmbn + (let ((cmbn-sigma (? sigma cmbn))) + (declare (type cmbn cmbn-sigma)) + (cone-2cmbn-append + cmbn-sigma + (n-cmbn -1 (? rho (? B cmbn-sigma)))))))) + + +(DEFUN AiBjC-RDCT-G (A i rho B j sigma C) + (declare (type chain-complex A B C) (type morphism i rho j sigma)) + (the morphism + (build-mrph + :sorc C :trgt (cone i) :degr 0 + :intr (Aibjc-rdct-g-impl rho B sigma) + :strt :cmbn + :orgn `(Aibjc-rdct-g ,A ,i ,rho ,B ,j ,sigma ,C)))) + + +(DEFUN AiBjC-RDCT-H-IMPL (rho) + (declare (type morphism)) + #'(lambda (cmbn) + (declare (type cmbn cmbn)) + (the cmbn + (multiple-value-bind (cmbn0 cmbn1) + (cone-cmbn-split cmbn) + (declare (type cmbn cmbn0) (ignore cmbn1)) + (cone-2cmbn-append + (zero-cmbn (1+ (cmbn-degr cmbn))) + (? rho cmbn0)))))) + + +(DEFUN AiBjC-RDCT-H (A i rho B j sigma C) + (declare (type chain-complex A B C) (type morphism i rho j sigma)) + (the morphism + (build-mrph + :sorc (cone i) :trgt (cone i) :degr +1 + :intr (AiBjC-rdct-h-impl rho) :strt :cmbn + :orgn `(AiBjC-RDCT-H ,A ,i ,rho ,B ,j ,sigma ,C)))) + + +(DEFUN AiBjC-RDCT (A i rho B j sigma C) + (declare (type chain-complex A B C) (type morphism i rho j sigma)) + (the reduction + (build-rdct + :f (AiBjC-rdct-f A i rho B j sigma C) + :g (AiBjC-rdct-g A i rho B j sigma C) + :h (AiBjC-rdct-h A i rho B j sigma C) + :orgn `(AiBjC-rdct ,A ,i ,rho ,B ,j ,sigma ,C)))) diff --git a/src/pushout/Examples.lisp b/src/pushout/Examples.lisp new file mode 100644 index 0000000..9552983 --- /dev/null +++ b/src/pushout/Examples.lisp @@ -0,0 +1,642 @@ +;;;============================================================================ +;;; +;;; Subject: Examples to test the pushout +;;; +;;; +;;;---------------------------------------------------------------------------- +;;; +;;; Author: Jónathan Heras Vicente +;;; +;;; 13/10/09 +;;; +;;;============================================================================ + + +;;; Adapted by Julián Cuevas, Jose Divasón, Miguel Marco Buzunariz and Ana Romero. +;; August 2019 +;;; Most of the examples have been collected from the rest of the development +;;; and unified in this file. + +;; ==================================== +;; Examples cones2.lisp +;; ==================================== + +#| +() +(setf basis (cone-basis2 + #'(lambda (n) (list n)) + #'(lambda (n) (list n)))) +(funcall basis 4) +|# + +#| +() +(cone-cmbn-split2 + (cmbn 3 4 (con0 'a) 5 (con1 'b))) +(cone-cmbn-split2 (cmbn 3 4 (con0 'a))) +(cone-cmbn-split2 (cmbn 3 4 (con1 'a))) +|# + +#| +() +(cmbn-con02 (cmbn 3 1 'a 2 'b)) +|# + +#| +() +(setf mrph (dffr (delta 4))) +(setf rslt (cone-2mrph-diag-impl2 mrph mrph)) +(funcall rslt (cmbn 3 4 (con0 15) 5 (con1 7))) +|# + + +#| +() +(setf rslt (cone-3mrph-triangle-impl2 #'f-cmpr + (dffr (delta 4)) + (dffr (delta 4)) + (idnt-mrph (delta 4)))) +(funcall rslt 4 (con0 '31)) +(funcall rslt 5 (con1 '31)) +(funcall rslt 4 (con1 '15)) +; (funcall rslt (cmbn 4 1 (con0 '31) 1 (con1 '15))) +|# + + +#| +() +(cat-init) +(setf k (k-z 1)) +(setf u (idnt-mrph k)) +(setf c (cone2 u)) +(setf *tc* (cmbn 3 1 (con0 '(1 2 3 4)))) +(? c 3 (con0 '(1 2 3 4))) +(? c *tc*) +|# + + +#| +() +(setf idnt (idnt-mrph (delta 4))) +(setf cone (cone2 idnt)) +(setf ff (cone-2mrph-diag2 cone cone idnt idnt)) +(? ff (cmbn 4 1 (con0 '31) 10 (con1 '15))) +|# + +#| +() +(cat-init) +(setf d (delta 4)) +(setf df (dffr (delta 4))) +(setf n (idnt-mrph d)) +(setf c (cone n)) +(setf z (sbtr (dffr c) + (cone-3mrph-triangle c c df (n-mrph -1 df) n))) +(? z 0 (con0 '1)) +(? z 1 (con1 '1)) +(? z 1 (con0 '3)) +(? z 2 (con1 '3)) +(? z 4 (con0 '31)) +(? z 5 (con1 '31)) +|# + + +;; ==================================== +;; Examples direct-sum.lisp +;; ==================================== + + +#| +() +(direct-sum-gsm 0 'a) +(direct-sum-gsm 1 'b) +|# + +#| +() +(setf cmpr (direct-sum-cmpr #'s-cmpr #'f-cmpr)) +(funcall cmpr (direct-sum-gsm 0 'a) (direct-sum-gsm 0 'b)) +(funcall cmpr (direct-sum-gsm 0 'b) (direct-sum-gsm 0 'b)) +(funcall cmpr (direct-sum-gsm 0 'b) (direct-sum-gsm 0 'a)) +(funcall cmpr (direct-sum-gsm 0 'b) (direct-sum-gsm 1 '2)) +(funcall cmpr (direct-sum-gsm 1 '2) (direct-sum-gsm 0 'b)) +(funcall cmpr (direct-sum-gsm 1 '1) (direct-sum-gsm 1 '2)) +(funcall cmpr (direct-sum-gsm 1 '2) (direct-sum-gsm 1 '2)) +(funcall cmpr (direct-sum-gsm 1 '2) (direct-sum-gsm 1 '1)) +|# + + +#| +(setf basis (direct-sum-basis + #'(lambda (n) (list n)) + #'(lambda (n) (list n)))) +(funcall basis 4) +|# + + +#| +() +(TERM-d-sum-0 (term 2 'a)) +(TERM-d-sum-1 (term 2 'a)) +|# + +#| +() +(direct-sum-cmbn-split + (cmbn 3 4 (direct-sum-gsm 0 'a) 5 (direct-sum-gsm 1 'b))) +(cone-cmbn-split (cmbn 3 4 (direct-sum-gsm 0 'a))) +(cone-cmbn-split (cmbn 3 4 (direct-sum-gsm 1 'a))) +|# + +#| +() +(direct-sum-2cmbn-append (cmbn 3 4 'a) (cmbn 2 5 'b)) +|# + + +#| +() +(setf mrph (dffr (delta 4))) +(setf rslt (direct-sum-dffr mrph mrph)) +(funcall rslt (cmbn 3 4 (direct-sum-gsm 0 15) 5 (direct-sum-gsm 1 7))) +|# + +#| +() +(setf s3 (sphere 3)) +(setf s3+s3 (direct-sum s3 s3)) + +|# + + +#| + +(cat-init) +(setf s3xs3 (crts-prdc (sphere 3) (sphere 3))) +(setf s3xs3+s3xs3-efhm (direct-sum-efhm s3xs3 s3xs3)) +(setf lrdct (lrdct s3xs3+s3xs3-efhm)) + +(pre-check-rdct lrdct) +(setf *tc* (cmbn 3 1 (first (basis (k 40) 3)) -2 (second (basis (k 40) 3)) 3 (third (basis (k 40) 3)))) +(setf *bc* (cmbn 4 -1 (first (basis (k 38) 4)) -5 (second (basis (k 38) 4)) 7 (third (basis (k 38) 4)) -4 (fourth (basis (k 38) 4)))) +(check-rdct) + +(setf rrdct (rrdct s3xs3+s3xs3-efhm)) + +(pre-check-rdct rrdct) +(setf *tc* (cmbn 2 1 (first (basis (k 40) 2)) -2 (second (basis (k 40) 2)) 3 (third (basis (k 40) 2)))) +(setf *bc* (cmbn 3 -1 (first (basis (k 42) 3)) -5 (second (basis (k 42) 3)) 7 (third (basis (k 42) 3)) -4 (fourth (basis (k 42) 3)))) +(check-rdct) + +|# + +#| +() +(setf ls3 (loop-space (sphere 3))) +(setf s3 (sphere 3)) +(setf ls3+s3 (direct-sum ls3 s3)) + +(homology ls3+s3 0 6) + +|# + + + +;; ==================================== +;; Examples remove-covers.lisp +;; ==================================== + +#| +(setf s3xI (crts-prdc (sphere 3) (delta 1))) + +(setf basis (remove-covers-basis + (basis s3xI))) +(funcall basis 4) +|# + +#| + + +(setf rcs3 (remove-covers (sphere 3))) + +(homology rcs3 0 6) + +|# + + +#| + +(cat-init) +(setf s3xs3 (crts-prdc (sphere 3) (sphere 3))) +(setf rcs3xs3-efhm (remove-covers-efhm (remove-covers s3xs3))) +(setf lrdct (lrdct rcs3xs3-efhm)) + +(pre-check-rdct lrdct) +(setf *tc* (cmbn 3 1 (first (basis (k 117) 3)) -2 (second (basis (k 117) 3)) 4 (third (basis (k 117) 3)))) +(setf *bc* (cmbn 4 -1 (first (basis (k 21) 4)) -5 (second (basis (k 21) 4)) 7 (third (basis (k 21) 4)))) +(check-rdct) + +(setf rrdct (rrdct rcs3xs3-efhm)) + +(pre-check-rdct rrdct) +(setf *tc* (cmbn 3 1 (first (basis (k 117) 3)) -2 (second (basis (k 117) 3)) 4 (third (basis (k 117) 3)))) +(setf *bc* (cmbn 4 -1 (first (basis (k 120) 4)) -5 (second (basis (k 120) 4)) 3 (car (last (basis (k 120) 4))))) +(check-rdct) + +|# + + +#| + +(setf rcls3 (remove-covers (loop-space (sphere 3)))) + +(homology rcls3 0 6) + +|# + + + +;; ==================================== +;; Examples suspension2.lisp +;; ==================================== + + + +#| + (setf cc (sphere 2)) + (setf basis (suspension2-basis (basis cc))) + (dotimes (i 6) + (print (funcall basis i))) + (suspension-basis :locally-effective) +|# + +#| + (setf cc (deltab)) + (setf intr (suspension2-intr-dffr (dffr cc))) + (funcall intr (cmbn 3 66 7)) +|# + + +#| + (cat-init) + (setf cc (deltab)) + (setf scc (suspension2 cc)) + (cmpr scc 7 11) + (basis scc 3) ;; error + (bsgn scc) + (? scc 3 11) +|# + +#| + (setf f (idnt-mrph (deltab))) + (setf sf (suspension2-intr f)) + (funcall sf (cmbn 2 4 3)) + (setf d (dffr (deltab))) + (setf sd (suspension2-intr d)) + (funcall sd (cmbn 2 4 3)) + (funcall sd (cmbn 3 4 7)) +|# + +#| + (setf f (idnt-mrph (deltab))) + (setf sf (suspension2 f)) + (? sf (cmbn 2 4 3)) + (setf d (dffr (deltab))) + (setf sd (suspension2 d)) + (? sd (cmbn 2 4 3)) + (? sd (cmbn 3 4 7)) +|# + + +#| + +(cat-init) +(setf s3xs3 (crts-prdc (sphere 3) (sphere 3))) +(setf s3xs3-efhm (efhm s3xs3)) +(setf s_2-s3xs3-efhm (suspension2 s3xs3-efhm)) +(setf lrdct (lrdct s_2-s3xs3-efhm)) + +(pre-check-rdct lrdct) +(setf *tc* (cmbn 3 1 (first (basis (k 38) 3)) -2 (second (basis (k 38) 3)))) +(setf *bc* (cmbn 4 -1 (first (basis (k 40) 4)) -5 (second (basis (k 40) 4)) 7 (third (basis (k 40) 4)))) +(check-rdct) + +(setf rrdct (rrdct s_2-s3xs3-efhm)) + +(pre-check-rdct rrdct) +(setf *tc* (cmbn 3 1 (first (basis (k 38) 3)) -2 (second (basis (k 38) 3)))) +(setf *bc* (cmbn 4 -1 (first (basis (k 46) 4)) -5 (second (basis (k 46) 4)))) +(check-rdct) + +|# + + + +#| + (setf sk (suspension2 (k-z 2))) + (homology sk 0 10) +|# + + + +;; ==================================== +;; Examples Pushout.lisp +;; ==================================== + + + + +#| +(setf s3 (sphere 3)) +(setf s3xs3 (crts-prdc (sphere 3) (sphere 3))) + +(setf f (build-smmr :sorc s3xs3 :trgt s3 :degr 0 + :sintr #'(lambda (dmns gmsm) + (absm (dgop1 gmsm) (gmsm1 gmsm))) + :orgn `(first ,s3xs3))) + +(setf g (build-smmr :sorc s3xs3 :trgt s3 :degr 0 + :sintr #'(lambda (dmns gmsm) + (absm (dgop2 gmsm) (gmsm2 gmsm))) + :orgn `(second ,s3xs3))) + + +(setf p (pushout-cmpr (cmpr (crts-prdc s3xs3 (delta 1))) + (cmpr s3) + (cmpr s3))) + +;;;JJJ Coherent examples. + +(funcall p (pushout-gsm 0 (crpr 0 (crpr 0 's3 7 '*) 7 1)) + (pushout-gsm 0 (crpr 0 (crpr 0 's3 7 '*) 7 1))) +(funcall p (pushout-gsm 0 (crpr 0 (crpr 0 's3 7 '*) 7 1)) + (pushout-gsm 0 (crpr 0 (crpr 7 '* 0 's3) 7 1))) +(funcall p (pushout-gsm 0 (crpr 0 (crpr 7 '* 0 's3) 7 1)) + (pushout-gsm 0 (crpr 0 (crpr 0 's3 7 '*) 7 1))) +(funcall p (pushout-gsm 0 (crpr 0 (crpr 0 's3 7 '*) 7 1)) + (pushout-gsm 1 's3)) +(funcall p (pushout-gsm 1 's3) (pushout-gsm 1 's3)) +(funcall p (pushout-gsm 1 's3) (pushout-gsm 2 's3)) +(funcall p (pushout-gsm 2 's3) (pushout-gsm 1 's3)) +|# + + +#| +(setf s3 (sphere 3)) +(setf s3xs3 (crts-prdc (sphere 3) (sphere 3))) + +(setf f (build-smmr :sorc s3xs3 :trgt s3 :degr 0 + :sintr #'(lambda (dmns gmsm) + (absm (dgop1 gmsm) (gmsm1 gmsm))) + :orgn `(first ,s3xs3))) + +(setf g (build-smmr :sorc s3xs3 :trgt s3 :degr 0 + :sintr #'(lambda (dmns gmsm) + (absm (dgop2 gmsm) (gmsm2 gmsm))) + :orgn `(second ,s3xs3))) + + +(setf p-basis (pushout-basis (basis (crts-prdc s3xs3 (delta 1))) + (basis s3) + (basis s3))) + +(dolist (item (funcall p-basis 3)) + (print item)) + + +|# + + +#| +(setf s3 (sphere 3)) +(setf s3xs3 (crts-prdc (sphere 3) (sphere 3))) + +(setf f (build-smmr :sorc s3xs3 :trgt s3 :degr 0 + :sintr #'(lambda (dmns gmsm) + (absm (dgop1 gmsm) (gmsm1 gmsm))) + :orgn `(first ,s3xs3))) + +(setf g (build-smmr :sorc s3xs3 :trgt s3 :degr 0 + :sintr #'(lambda (dmns gmsm) + (absm (dgop2 gmsm) (gmsm2 gmsm))) + :orgn `(second ,s3xs3))) + + +(setf p-face (pushout-face (face (crts-prdc s3xs3 (delta 1))) + (face s3) + (face s3) f g)) + +(setf p-basis (pushout-basis (basis (crts-prdc s3xs3 (delta 1))) + (basis s3) (basis s3))) + +(map nil #'print (funcall p-basis 3)) + +(dolist (item (funcall p-basis 3)) + (terpri) + (print item) + (dotimes (i 4) + (print (funcall p-face i 3 item)))) + +|# + + +#| +(cat-init) +(setf s3 (sphere 3)) +(setf s3xs3 (crts-prdc (sphere 3) (sphere 3))) + +(setf f (build-smmr :sorc s3xs3 :trgt s3 :degr 0 + :sintr #'(lambda (dmns gmsm) + (absm (dgop1 gmsm) (gmsm1 gmsm))) + :orgn `(first ,s3xs3))) + +(setf g (build-smmr :sorc s3xs3 :trgt s3 :degr 0 + :sintr #'(lambda (dmns gmsm) + (absm (dgop2 gmsm) (gmsm2 gmsm))) + :orgn `(second ,s3xs3))) +(setf p (pushout f g)) + + +;;;JJJ Very useful: several bugs so discovered. + +(check-smst p 0 8) + +|# + + +#| +() +(cat-init) +(setf unipunctual (build-finite-ss '(x))) +(setf k-z (k-z 1)) + + +(setf f (build-smmr :sorc unipunctual :trgt k-z :degr 0 + :sintr #'(lambda (dmns gmsm) + (if (= dmns 0) + (absm 0 (bspn k-z)) + nil + )) + :orgn `(triv ,unipunctual ,k-z))) + + +(setf p (pushout f f)) + +(homology p 0 3) + +|# + + +#| + + (setf wkk (wedge (k-z 2) (k-z 2))) + (homology wkk 0 10) + (setf wedge-loop (wedge (loop-space (sphere 3)) (loop-space (sphere 3)))) + (homology wedge-loop 0 10) + +|# + + + +#| + (cat-init) + (setf s3*s4 (join (sphere 3) (sphere 4))) + (homology s3*s4 0 9) + (setf k-z2*k-z2 (join (k-z2 1) (k-z2 1))) + (homology k-z2*k-z2 0 10) + +|# + + + +#| + (cat-init) + (setf s3*s4 (join (sphere 3) (sphere 4))) + (setf hom-equ (efhm s3*s4)) + (setf lrdct (lrdct hom-equ)) + (pre-check-rdct lrdct) + (setf *bc* (CMBN 3 2 (CAR (basis (k 28) 3)) -8 (CADR (basis (k 28) 3)) 7 (CADDR (basis (k 28) 3)))) + (SETF *tc* (CMBN 2 -1 (CAR (basis (k 195) 2)) 4 (CADR (basis (k 195) 2)) -5 (CADDR (basis (k 195) 2)))) + (check-rdct) + + (setf rrdct (rrdct hom-equ)) + (pre-check-rdct rrdct) + (setf *bc* (CMBN 3 2 (CAR (basis (k 198) 3)) -8 (CADR (basis (k 198) 3)) 7 (CADDR (basis (k 198) 3)))) + (SETF *tc* (CMBN 2 -1 (CAR (basis (k 195) 2)) 4 (CADR (basis (k 195) 2)) -5 (CADDR (basis (k 195) 2)))) + (check-rdct) +|# + + +;;;---------------------------------------------------------------------------- +;;; +;;; Subject: Disjoint Union (Direct Sum) +;;; +;;; X = \emptyset +;;; +;;;---------------------------------------------------------------------------- + + +(IN-PACKAGE #:cat) +(setf s3 (sphere 3)) +(setf s4 (sphere 4)) +(setf nil-ss (build-finite-ss nil)) + +(setf f (build-smmr :sorc nil-ss :trgt s3 :degr 0 + :sintr #'(lambda (dmns gmsm) + nil) + :orgn `(triv ,nil-ss ,s3))) + +(setf g (build-smmr :sorc nil-ss :trgt s4 :degr 0 + :sintr #'(lambda (dmns gmsm) + nil) + :orgn `(triv ,nil-ss ,s4))) + +(setf p (pushout f g)) + +(homology p 0 6) + +(cat-init) +(setf l2s3 (loop-space (sphere 3) 2)) +(setf l3s4 (loop-space (sphere 4) 3)) +(setf nil-ss (build-finite-ss nil)) + +(setf f (build-smmr :sorc nil-ss :trgt l2s3 :degr 0 + :sintr #'(lambda (dmns gmsm) + nil) + :orgn `(triv ,nil-ss ,l2s3))) + +(setf g (build-smmr :sorc nil-ss :trgt l3s4 :degr 0 + :sintr #'(lambda (dmns gmsm) + nil) + :orgn `(triv ,nil-ss ,l3s4))) + +(setf p (pushout f g)) +(setf ds (direct-sum l2s3 l3s4)) + +(homology p 0 6) +(homology ds 0 6) + + + +;;;---------------------------------------------------------------------------- +;;; +;;; Subject: Suspension +;;; +;;; Arbitrary X, Y=Z={*} +;;; +;;;---------------------------------------------------------------------------- + +(cat-init) +(setf ls3 (loop-space (sphere 3))) +(setf unipunctual (build-finite-ss '(x))) + +(setf f (build-smmr :sorc ls3 :trgt unipunctual :degr 0 + :sintr #'(lambda (dmns gmsm) + (if (and (equal dmns 0) + (equal gmsm (bsgn ls3))) + 'x + nil)) + :orgn `(triv ,ls3 ,unipunctual))) + +(setf p (pushout f f)) + +(homology p 0 6) + +(homology (suspension2 (loop-space (sphere 3))) 0 6) + + +;;;---------------------------------------------------------------------------- +;;; +;;; Subject: P^2(C) +;;; +;;; X = X3, Y = S^2, Z = {x} +;;; +;;; Homology groups of P^2(C) -> (Z,0,Z,0,Z) +;;; +;;;---------------------------------------------------------------------------- + +(cat-init) +(setf s2 (sphere 2)) +(setf ch2 ( chml-clss s2 2)) +(setf f2 (z-whitehead s2 ch2)) +(setf x3 (fibration-total f2)) +(setf unipunctual (build-finite-ss '(x))) + +(setf f (build-smmr :sorc x3 :trgt s2 :degr 0 + :sintr #'(lambda (dmns gmsm) + (declare (ignore dmns)) + (absm (dgop1 gmsm) (gmsm1 gmsm))) + :orgn `(proj ,x3 ,s2))) + +(setf g (build-smmr :sorc x3 :trgt unipunctual :degr 0 + :sintr #'(lambda (dmns gmsm) + (if (and (equal dmns 0) + (equal gmsm (bsgn x3))) + 'x + nil)) + :orgn `(proj ,x3 ,unipunctual))) + +(setf p (pushout f g)) + +(homology p 0 10) + diff --git a/src/pushout/Pushout.lisp b/src/pushout/Pushout.lisp new file mode 100644 index 0000000..cfa64cf --- /dev/null +++ b/src/pushout/Pushout.lisp @@ -0,0 +1,377 @@ +;;;============================================================================ +;;; +;;; Subject: Pushout +;;; +;;; +;;;---------------------------------------------------------------------------- +;;; +;;; Author: Jónathan Heras Vicente +;;; +;;; 13/10/09 +;;; +;;;============================================================================ + +;;; Adapted by Julián Cuevas, Jose Divasón, Miguel Marco Buzunariz and Ana Romero. +;;; August 2019 + + +(in-package #:cat) + +(provide "pushout") + + +;;; +;;; Struct +;;; + + +(DEFSTRUCT (pushout-gsm (:print-function pushout-gsm-print) (:conc-name nil)) + (p-ind #+allegro :type #+allegro (member :undefined 0 1 2)) + ;;;JJJ Why the possible value ":undefined" ??? + (p-old #+allegro :type #+allegro gmsm)) + +;;; +;;; MACROS +;;; + + +(defmacro pushout-gsm (p-ind p-old) + `(make-pushout-gsm :p-ind ,p-ind :p-old ,p-old) + ) + + +(DEFMACRO WITH-pushout-gsm (&rest rest) + (ecase (length (first rest)) + (2 `(with-pushout-gsm-2 ,@rest)) + )) + +;;;JJJ Why these two macros which in fact are the same ? +;;;JJJ In fact only the with-pushout-gsm-2 can be used. + + +(DEFMACRO with-pushout-gsm-2 ((p-ind p-old) pushout-gsm . body) + `(let ((,p-ind (p-ind ,pushout-gsm)) + (,p-old (p-old ,pushout-gsm))) + (declare (fixnum ,p-ind) (type gmsm ,p-old)) + ,@body)) + +(defun pushout-gsm-print (pushout-gsm stream depth) + (declare + (type pushout-gsm pushout-gsm) + (stream stream) + (ignore depth)) + (with-pushout-gsm (p-ind p-old) pushout-gsm + (format stream "" + p-ind + p-old) + pushout-gsm)) + + +;;; Pushout Pushout Pushout Pushout Pushout Pushout Pushout Pushout Pushout Pushout +;;; Pushout Pushout Pushout Pushout Pushout Pushout Pushout Pushout Pushout Pushout +;;; Pushout Pushout Pushout Pushout Pushout Pushout Pushout Pushout Pushout Pushout + +#| +(defun pushout-cmpr (cmpr1 cmpr2 cmpr3) + (declare (type cmprf cmpr1 cmpr2 cmpr3)) + (flet ((rslt (pushout-gsm1 pushout-gsm2) + (case (p-ind pushout-gsm1) + (0 (lexico (f-cmpr (p-ind pushout-gsm1) (p-ind pushout-gsm2)) + (funcall cmpr1 (p-old pushout-gsm1) (p-old pushout-gsm2)))) + (1 (lexico (f-cmpr (p-ind pushout-gsm1) (p-ind pushout-gsm2)) + (funcall cmpr2 (p-old pushout-gsm1) (p-old pushout-gsm2)))) + (2 (lexico (f-cmpr (p-ind pushout-gsm1) (p-ind pushout-gsm2)) + (funcall cmpr3 (p-old pushout-gsm1) (p-old pushout-gsm2)))) + ) + )) + (the cmprf #'rslt))) +|# + +;;;JJJ For the fun... + +(defun pushout-cmpr (cmpr1 cmpr2 cmpr3) + (declare (type cmprf cmpr1 cmpr2 cmpr3)) + (flet ((rslt (pushout-gsm1 pushout-gsm2) + (ecase (+ (* 10 (p-ind pushout-gsm1)) (p-ind pushout-gsm2)) + ((01 02 12) :less) + ((10 20 21) :greater) + (00 (funcall cmpr1 (p-old pushout-gsm1) (p-old pushout-gsm2))) + (11 (funcall cmpr2 (p-old pushout-gsm1) (p-old pushout-gsm2))) + (22 (funcall cmpr3 (p-old pushout-gsm1) (p-old pushout-gsm2)))))) + (the cmprf #'rslt))) + + + +(defun pushout-basis (basis1 basis2 basis3) + (declare (type basis basis1 basis2 basis3)) + (when (or (eq basis1 :locally-effective) + (eq basis2 :locally-effective) + (eq basis3 :locally-effective)) + (return-from pushout-basis :locally-effective)) + (flet ((rslt (dmns) + (declare (fixnum dmns)) + (let ((basis-from-1 (remove-if #'(lambda (item) + (member item '(1 2))) + (funcall basis1 dmns) :key #'gmsm2))) + (append (mapcar #'(lambda (old) + (declare (type gmsm old)) + (pushout-gsm 0 old)) + basis-from-1) + (mapcar #'(lambda (old) + (declare (type gmsm old)) + (pushout-gsm 1 old)) + (funcall basis2 dmns)) + (mapcar #'(lambda (old) + (declare (type gmsm old)) + (pushout-gsm 2 old)) + (funcall basis3 dmns)))))) + (the basis #'rslt))) + + + +(defun pushout-face (face1 face2 face3 f g) + (declare (type face face1 face2 face3)) + (flet ((rslt (indx dmns gmsm) + (declare (fixnum indx dmns) (type pushout-gsm gmsm)) + (with-pushout-gsm (ind old) gmsm + (ecase ind + (0 (with-absm (dgop crpr) + (funcall face1 indx dmns old) + (with-crpr (dgop1 gmsm1 dgop2 gmsm2) crpr + (declare (ignore dgop1 dgop2)) + (ecase gmsm2 + (1 (with-absm (dgop gmsm) (? f (1- dmns) (absm dgop gmsm1)) + (absm dgop (pushout-gsm 1 gmsm)))) + (2 (with-absm (dgop gmsm) (? g (1- dmns) (absm dgop gmsm1)) + (absm dgop (pushout-gsm 2 gmsm)))) + (3 (absm dgop (pushout-gsm 0 crpr))))))) + (1 (with-absm (dgop gmsm) (funcall face2 indx dmns gmsm) + (absm dgop (pushout-gsm 1 gmsm)))) + (2 (with-absm (dgop gmsm) (funcall face3 indx dmns gmsm) + (absm dgop (pushout-gsm 2 gmsm)))))))) + (the face #'rslt))) + + + +(defmethod pushout ((f morphism) (g morphism)) + (if (equal (sorc f) (sorc g)) + (let* ((X (sorc f)) + (XxI (crts-prdc X (delta 1))) + (Y (trgt f)) + (Z (trgt g))) + (the simplicial-set + (let ((rslt (build-smst + :cmpr (pushout-cmpr (cmpr XxI) (cmpr Y) (cmpr Z)) + :basis (pushout-basis (basis XxI) (basis Y) (basis Z)) + ;;;JJJ :bspn nil + :bspn (pushout-gsm 1 (bspn Y)) + :face (pushout-face (face XxI) (face Y) (face Z) f g) + :orgn `(pushout ,f ,g)))) + (declare (type simplicial-set rslt)) + rslt))) + (error "The source of f and g must be the same"))) + + + +(defun pushout-efhm (f g) + (declare (morphism f g)) + (if (equal (sorc f) (sorc g)) + (let* ((sorc (sorc f)) + (trgt-f (trgt f)) + (trgt-g (trgt g)) + (rc (remove-covers sorc)) + (ds (direct-sum trgt-f trgt-g)) + (sds (suspension2 ds)) + (p (pushout f g)) + (sigma + (build-mrph + :sorc rc :trgt p :degr 0 + :intr + #'(lambda (cmbn) + (with-cmbn (degr list) cmbn + (make-cmbn + :degr degr + :list (mapcar + #'(lambda (term) + (declare (type term term)) + (the term + (with-term (cffc gnrt) term + (term + cffc + (pushout-gsm 0 gnrt))))) + list))) + ) + :strt :cmbn + :orgn `(sigma ,rc -> ,p))) + (rho (build-mrph + :sorc p :trgt ds :degr 0 + :intr + #'(lambda (cmbn) + (with-cmbn (degr list) cmbn + (make-cmbn + :degr degr + :list (mapcar + #'(lambda (term) + (declare (type term term)) + (the term + (with-term (cffc gnrt) term + (ecase (p-ind gnrt) + (1 (term + cffc + (direct-sum-gsm 0 (p-old gnrt))) + ) + (2 (term + cffc + (direct-sum-gsm 1 (p-old gnrt)))) + ) + ))) + (remove-if #'(lambda (item) + (equal (p-ind (gnrt item)) 0)) + list)))) + ) + :strt :cmbn + :orgn `(rho ,p -> ,ds))) + (shift (build-mrph + :sorc ds :trgt sds :degr 1 + :intr + #'(lambda (cmbn) + (with-cmbn (degr list) cmbn + (make-cmbn + :degr (1+ degr) + :list list)) + ) + :strt :cmbn + :orgn `(shift ,ds -> ,sds))) + (chi (build-mrph + :sorc rc :trgt sds :degr 0 + :intr + #'(lambda (cmbn) + (with-cmbn (degr list) (? (cmps shift (cmps rho (cmps p sigma))) cmbn) + (make-cmbn + :degr degr + :list list)) + ) + :strt :cmbn + :orgn `(chi ,rc -> ,sds))) + (cone2 (cone2 chi)) + (f-isom (build-mrph :sorc cone2 :trgt p :degr 0 :intr + #'(lambda (cmbn) + (with-cmbn (degr list) + cmbn + (make-cmbn :degr degr :list + (mapcar #'(lambda (term) + (declare (type term term)) + (ecase (conx (gnrt term)) + (0 + (term (cffc term) + (if(= + (d-sum-ind (icon (gnrt term))) + 0) + (pushout-gsm 1 (d-sum-old (icon (gnrt term)))) + (pushout-gsm + 2 + (d-sum-old (icon (gnrt term))))))) + (1 + (term (cffc term) + (pushout-gsm + 0 + (icon (gnrt term))))))) + list)))) + :strt :cmbn :orgn `(f-isom ,cone2 -> ,p))) + (g-isom + (build-mrph :sorc p :trgt cone2 :degr 0 :intr + #'(lambda (cmbn) + (with-cmbn (degr list) + cmbn + (make-cmbn :degr degr :list + (mapcar #'(lambda (term) + (declare (type term term)) + (ecase (p-ind (gnrt term)) + (0 + (term (cffc term) + (con1 (p-old (gnrt term))))) + (1 + (term (cffc term) + (con0 + (direct-sum-gsm + 0 + (p-old (gnrt term)))))) + (2 + (term (cffc term) + (con0 + (direct-sum-gsm + 1 + (p-old (gnrt term)))))))) + list)))) + :strt :cmbn :orgn `(g-isom ,p -> ,cone2))) + (cone2-efhm (efhm cone2)) + ) + (the homotopy-equivalence + (build-hmeq :lf (cmps f-isom (lf cone2-efhm)) + :lg (cmps (lg cone2-efhm) g-isom) + :lh (lh cone2-efhm) + :rf (rf cone2-efhm) :rg (rg cone2-efhm) + :rh (rh cone2-efhm)) + ) + ) + (error "The source of f and g must be the same"))) + + +(DEFMETHOD SEARCH-EFHM (pushout (orgn (eql 'pushout))) + (declare (type chain-complex pushout)) + (the homotopy-equivalence + (pushout-efhm (second (orgn pushout)) + (third (orgn pushout)) + ))) + + + +;;; Wedge + + +(defun wedge (smst1 smst2) + (declare (simplicial-set smst1 smst2)) + (let* ((unipunctual (build-finite-ss '(x))) + (f (build-smmr :sorc unipunctual :trgt smst1 :degr 0 + :sintr #'(lambda (dmns gmsm) + (declare (ignore gmsm)) + (if (= dmns 0) + (absm 0 (bspn smst1)) + nil + )) + :orgn `(triv ,unipunctual ,smst1))) + (g (build-smmr :sorc unipunctual :trgt smst2 :degr 0 + :sintr #'(lambda (dmns gmsm) + (declare (ignore gmsm)) + (if (= dmns 0) + (absm 0 (bspn smst2)) + nil + )) + :orgn `(triv ,unipunctual ,smst2)))) + (pushout f g) + )) + + + +;;; Join + + +(defun join (smst1 smst2) + (declare (simplicial-set smst1 smst2)) + (let* ((smst1xsmst2 (crts-prdc smst1 smst2)) + (f (build-smmr :sorc smst1xsmst2 :trgt smst1 :degr 0 + :sintr #'(lambda (dmns gmsm) + (declare (ignore dmns)) + (absm (dgop1 gmsm) (gmsm1 gmsm))) + :orgn `(projection ,smst1xsmst2 ,smst1))) + (g (build-smmr :sorc smst1xsmst2 :trgt smst2 :degr 0 + :sintr #'(lambda (dmns gmsm) + (declare (ignore dmns)) + (absm (dgop2 gmsm) (gmsm2 gmsm))) + :orgn `(projection ,smst1xsmst2 ,smst2)))) + (pushout f g) + )) + + + + diff --git a/src/pushout/cones2.lisp b/src/pushout/cones2.lisp new file mode 100644 index 0000000..701c689 --- /dev/null +++ b/src/pushout/cones2.lisp @@ -0,0 +1,210 @@ +;;;============================================================================ +;;; +;;; Subject: Cones 2nd definition +;;; +;;; +;;;---------------------------------------------------------------------------- +;;; +;;; Author: Jónathan Heras Vicente +;;; +;;; 13/10/09 +;;; +;;;============================================================================ + +;;; Adapted by Julián Cuevas, Jose Divasón, Miguel Marco Buzunariz and Ana Romero. +;;; August 2019 + +(in-package #:cat) + +(provide "cones2") + + +(DEFUN CONE-BASIS2 (basis0 basis1) + (declare (type basis basis0 basis1)) + (the basis + (progn + (when (or (eq basis0 :locally-effective) + (eq basis1 :locally-effective)) + (return-from cone-basis2 :locally-effective)) + (flet ((rslt (degr) + (declare (type fixnum degr)) + (the list + (append + (mapcar #'(lambda (item) (con0 item)) + (funcall basis0 (1+ degr))) + (mapcar #'(lambda (item) (con1 item)) + (funcall basis1 degr)))))) + (declare (ftype (function (fixnum) list) rslt)) + #'rslt)))) + + +(DEFUN CONE-CMBN-SPLIT2 (cmbn) + (declare (type cmbn cmbn)) + (the (values cmbn cmbn) + (with-cmbn (degr list) cmbn + (let ((list0 +empty-list+) + (list1 +empty-list+)) + (declare (type list list0 list1)) + (do ((mark list (cdr mark))) + ((endp mark) + (setf list0 (nreverse list0) + list1 +empty-list+)) + (declare (type list mark)) + (when (eql 1 (conx (cdar mark))) + (setf list0 (nreverse list0) + list1 (mapcar #'term-uncon mark)) + (return)) + (push (term-uncon (car mark)) list0)) + (values (make-cmbn :degr (1+ degr) :list list0) + (make-cmbn :degr degr :list list1)))))) + + + +(DEFUN CMBN-CON02 (cmbn) + (declare (type cmbn cmbn)) + (the cmbn + (make-cmbn + :degr (1- (cmbn-degr cmbn)) + :list (mapcar #'term-con0 (cmbn-list cmbn))))) + + +(DEFUN CONE-2CMBN-APPEND2 (cmbn0 cmbn1) + (declare (type cmbn cmbn0 cmbn1)) + (the cmbn + (make-cmbn + :degr (cmbn-degr cmbn1) + :list (append (mapcar #'term-con0 (cmbn-list cmbn0)) + (mapcar #'term-con1 (cmbn-list cmbn1)))))) + +(DEFUN CONE-2MRPH-DIAG-IMPL2 (mrph0 mrph1) + (declare (type morphism mrph0 mrph1)) + (the intr-mrph + (flet ((rslt (cmbn) + (declare (type cmbn cmbn)) + (the cmbn + (multiple-value-bind (cmbn0 cmbn1) + (cone-cmbn-split2 cmbn) + (declare (type cmbn cmbn0 cmbn1)) + (cone-2cmbn-append2 (? mrph0 cmbn0) + (? mrph1 cmbn1)))))) + #'rslt))) + + + +(DEFUN cone-3mrph-triangle-impl2 (cmpr0 mrph0 mrph1 phi) + (declare (ignore cmpr0) (type morphism mrph0 mrph1 phi)) + (the intr-mrph + (flet ((rslt (degr gnrt) + (declare (type fixnum degr) (type gnrt gnrt)) + (the cmbn + (ecase (conx gnrt) + (0 (cmbn-con02 (? mrph0 (1+ degr) (icon gnrt)))) + (1 + (let ((gnrt (icon gnrt))) + (declare (type gnrt gnrt)) + (cone-2cmbn-append2 + (? phi degr gnrt) + (? mrph1 degr gnrt))))) + ))) + #'rslt))) + + +(DEFUN CONE2 (mrph) + (declare (type morphism mrph)) + (the chain-complex + (let ((chcm0 (trgt mrph)) + (chcm1 (sorc mrph))) + (declare (type chain-complex chcm0 chcm1)) + (build-chcm + :cmpr (cone-cmpr (cmpr chcm0) (cmpr chcm1)) + :basis (cone-basis2 (basis chcm0) (basis chcm1)) + :bsgn (con0 (bsgn chcm0)) + :intr-dffr (cone-3mrph-triangle-impl2 (cmpr chcm0) + (dffr chcm0) + (n-mrph -1 (dffr chcm1)) + mrph) + :strt :gnrt + :orgn `(cone2 ,mrph))))) + + + + +(DEFUN CONE-2MRPH-DIAG2 (sorc-cone trgt-cone mrph0 mrph1) + (declare + (type chain-complex sorc-cone trgt-cone) + (type morphism mrph0 mrph1)) + (the morphism + (progn + (unless (= (degr mrph0) (degr mrph1)) + (error "Non-coherent degrees in CONE-2MRPH-DIAG2.")) + (build-mrph + :sorc sorc-cone + :trgt trgt-cone + :degr (degr mrph0) + :intr (cone-2mrph-diag-impl2 mrph0 mrph1) + :strt :cmbn + :orgn `(cone-2mrph-diag2 ,sorc-cone ,trgt-cone ,mrph0 ,mrph1))))) + + + +(DEFUN CONE-3MRPH-TRIANGLE2 (sorc-cone trgt-cone mrph0 mrph1 phi) + (declare + (type chain-complex sorc-cone trgt-cone) + (type morphism mrph0 mrph1 phi)) + (the morphism + (progn + (unless (= (degr mrph0) (degr mrph1)) + (error "Non-coherent degrees in CONE-3MRPH-TRIANGLE.")) + (unless (= (1+ (degr mrph0)) (degr phi)) + (error "Non-coherent-degrees in CONE-3MRPH-TRIANGLE.")) + (build-mrph + :sorc sorc-cone + :trgt trgt-cone + :degr (degr mrph0) + :intr (cone-3mrph-triangle-impl2 + (cmpr (trgt phi)) + mrph0 mrph1 phi) + :strt :gnrt + :orgn `(cone-3mrph-triangle2 ,sorc-cone ,trgt-cone + ,mrph0 ,mrph1 ,phi))))) + + +(DEFUN CONE2-EFHM (cone) + (declare (type chain-complex cone)) + (the homotopy-equivalence + (let* ((phi (second (orgn cone))) + (chcm0 (trgt phi)) (chcm1 (sorc phi)) + (efhm0 (efhm chcm0)) (efhm1 (efhm chcm1)) + (lf0 (lf efhm0)) (lg0 (lg efhm0)) (lh0 (lh efhm0)) + (rf0 (rf efhm0)) (rg0 (rg efhm0)) (rh0 (rh efhm0)) + (lf1 (lf efhm1)) (lg1 (lg efhm1)) (lh1 (lh efhm1)) + (rf1 (rf efhm1)) (rg1 (rg efhm1)) (rh1 (rh efhm1)) + (hphi (cmps lg0 (cmps phi lf1))) + (ephi (cmps rf0 (cmps hphi rg1))) + (hcone (cone2 hphi)) + (econe (cone2 ephi)) + (LF (cone-2mrph-diag2 hcone cone lf0 lf1)) + (LG (cone-2mrph-diag2 cone hcone lg0 lg1)) + (LH (cone-2mrph-diag2 hcone hcone lh0 (n-mrph -1 lh1))) + (RF (cone-3mrph-triangle2 hcone econe rf0 rf1 + (cmps rf0 (cmps hphi rh1)))) + (RG (cone-3mrph-triangle2 econe hcone rg0 rg1 + (n-mrph -1 (cmps rh0 (cmps hphi rg1))))) + (RH (cone-3mrph-triangle2 hcone hcone rh0 (n-mrph -1 rh1) + (cmps rh0 (cmps hphi rh1))))) + (declare + (type chain-complex chcm0 chcm1 hcone econe) + (type morphism phi lf0 lg0 lh0 rf0 rg0 rh0 lf1 lg1 lh1 rf1 rg1 rh1 + hphi ephi LF LG LH RF RG RH)) + (build-hmeq + :lrdct (build-rdct :f LF :g LG :h LH + :orgn `(cone2-efhm ,cone lrdct)) + :rrdct (build-rdct :f RF :g RG :h RH + :orgn `(cone2-efhm ,cone rrdct)) + :orgn `(cone2-efhm ,cone))))) + +(DEFMETHOD SEARCH-EFHM (chcm (orgn (eql 'cone2))) + (declare (type chain-complex chcm)) + (the homotopy-equivalence + (cone2-efhm chcm))) + diff --git a/src/pushout/direct-sum.lisp b/src/pushout/direct-sum.lisp new file mode 100644 index 0000000..389cbb5 --- /dev/null +++ b/src/pushout/direct-sum.lisp @@ -0,0 +1,210 @@ +;;;============================================================================ +;;; +;;; Subject: Direct Sum +;;; +;;; +;;;---------------------------------------------------------------------------- +;;; +;;; Author: Jónathan Heras Vicente +;;; 13/10/09 +;;; +;;;============================================================================ + +;;; Adapted by Julián Cuevas, Jose Divasón, Miguel Marco Buzunariz and Ana Romero. +;;; August 2019 + +(in-package #:cat) + +(provide "direct-sum") + +(DEFSTRUCT (direct-sum-gsm (:print-function direct-sum-gsm-print) (:conc-name nil)) + (d-sum-ind #+allegro :type #+allegro (member :undefined 0 1)) + (d-sum-old #+allegro :type #+allegro gmsm)) + +(defmacro direct-sum-gsm (d-sum-ind d-sum-old) + `(make-direct-sum-gsm :d-sum-ind ,d-sum-ind :d-sum-old ,d-sum-old) + ) + +(DEFMACRO WITH-direct-sum-gsm-2 ((d-sum-ind d-sum-old) direct-sum-gsm . body) + `(let ((,d-sum-ind (d-sum-ind ,direct-sum-gsm)) + (,d-sum-old (d-sum-old ,direct-sum-gsm))) + (declare (fixnum ,d-sum-ind) (type gmsm ,d-sum-old)) + ,@body)) + +(DEFMACRO WITH-direct-sum-gsm (&rest rest) + (ecase (length (first rest)) + (2 `(WITH-direct-sum-gsm-2 ,@rest)) + )) + + + +(defun direct-sum-gsm-print (direct-sum-gsm stream depth) + (declare + (type direct-sum-gsm direct-sum-gsm) + (stream stream) + (ignore depth)) + (with-direct-sum-gsm (d-sum-ind d-sum-old) direct-sum-gsm + (format stream "" + d-sum-ind + d-sum-old) + direct-sum-gsm)) + + + +(defun direct-sum-cmpr (cmpr1 cmpr2) + (declare (type cmprf cmpr1 cmpr2)) + (flet ((rslt (direct-sum-gsm1 direct-sum-gsm2) + (ecase (d-sum-ind direct-sum-gsm1) + (0 (if (equal 0 (d-sum-ind direct-sum-gsm2)) + (funcall cmpr1 (d-sum-old direct-sum-gsm1) (d-sum-old direct-sum-gsm2)) + :less + )) + (1 (if (equal 0 (d-sum-ind direct-sum-gsm2)) + :greater + (funcall cmpr2 (d-sum-old direct-sum-gsm1) (d-sum-old direct-sum-gsm2)))) + ))) + (the cmprf #'rslt))) + + + +(defun direct-sum-basis (basis1 basis2) + (declare (type basis basis1 basis2)) + (when (or (eq basis1 :locally-effective) + (eq basis2 :locally-effective) + ) + (return-from direct-sum-basis :locally-effective)) + (flet ((rslt (dmns) + (declare (fixnum dmns)) + (append (mapcar #'(lambda (old) + (declare (type gmsm old)) + (direct-sum-gsm 0 old)) + (funcall basis1 dmns)) + (mapcar #'(lambda (old) + (declare (type gmsm old)) + (direct-sum-gsm 1 old)) + (funcall basis2 dmns))))) + (the basis #'rslt))) + + +(DEFUN TERM-d-sum-0 (term) + (declare (type term term)) + (the term + (term (cffc term) + (direct-sum-gsm 0 (gnrt term))))) + +(DEFUN TERM-d-sum-1 (term) + (declare (type term term)) + (the term + (term (cffc term) + (direct-sum-gsm 1 (gnrt term))))) + + +(DEFUN direct-sum-cmbn-split (cmbn) + (declare (type cmbn cmbn)) + (the (values cmbn cmbn) + (with-cmbn (degr list) cmbn + (let ((list0 +empty-list+) + (list1 +empty-list+)) + (declare (type list list0 list1)) + (do ((mark list (cdr mark))) + ((endp mark) + (setf list0 (nreverse list0) + list1 (nreverse list1))) + (declare (type list mark)) + (if (equal 0 (d-sum-ind (cdar mark))) + (push (term (caar mark) (d-sum-old (cdar mark))) list0) + (push (term (caar mark) (d-sum-old (cdar mark))) list1))) + (values (make-cmbn :degr degr :list list0) + (make-cmbn :degr degr :list list1)))))) + + + +(DEFUN direct-sum-2cmbn-append (cmbn0 cmbn1) + (declare (type cmbn cmbn0 cmbn1)) + (the cmbn + (make-cmbn + :degr (cmbn-degr cmbn0) + :list (append (mapcar #'term-d-sum-0 (cmbn-list cmbn0)) + (mapcar #'term-d-sum-1 (cmbn-list cmbn1)))))) + + + +(defun direct-sum-dffr (dffr1 dffr2) + (declare (type morphism dffr1 dffr2)) + (flet ((rslt (cmbn) + (declare (type cmbn cmbn)) + (multiple-value-bind (cmbn0 cmbn1) + (direct-sum-cmbn-split cmbn) + (declare (type cmbn cmbn0 cmbn1)) + (direct-sum-2cmbn-append (? dffr1 cmbn0) + (? dffr2 cmbn1))) + )) + (the intr-mrph #'rslt))) + + + + +(defun direct-sum (chcm1 chcm2) + (declare (type chain-complex chcm1 chcm2)) + (the chain-complex + (build-chcm + :cmpr (direct-sum-cmpr (cmpr chcm1) (cmpr chcm2)) + :basis (direct-sum-basis (basis chcm1) (basis chcm2)) + :bsgn (direct-sum-gsm 0 (bsgn chcm1)) + :intr-dffr (direct-sum-dffr (dffr chcm1) (dffr chcm2)) + :strt :cmbn + :orgn `(direct-sum ,chcm1 ,chcm2)))) + + +(defun direct-sum-mrph (sorc trgt mrph1 mrph2) + (declare (type morphism mrph1 mrph2)) + (the morphism + (progn + (unless (= (degr mrph1) (degr mrph2)) + (error "Non-coherent degrees in direct-sum-mrph")) + (build-mrph + :sorc sorc + :trgt trgt + :degr (degr mrph1) + :intr (direct-sum-dffr mrph1 mrph2) + :strt :cmbn + :orgn `(direct-sum-mrph ,sorc ,trgt ,mrph1 ,mrph2))))) + +(DEFUN direct-sum-efhm (chcm1 chcm2) + (declare (type chain-complex chcm1 chcm2)) + (the homotopy-equivalence + (let* ((efhm1 (efhm chcm1)) (efhm2 (efhm chcm2)) + (lf1 (lf efhm1)) (lg1 (lg efhm1)) (lh1 (lh efhm1)) + (rf1 (rf efhm1)) (rg1 (rg efhm1)) (rh1 (rh efhm1)) + (lf2 (lf efhm2)) (lg2 (lg efhm2)) (lh2 (lh efhm2)) + (rf2 (rf efhm2)) (rg2 (rg efhm2)) (rh2 (rh efhm2)) + (tcc1 (tcc efhm1)) + (tcc2 (tcc efhm2)) + (rbcc1 (rbcc efhm1)) + (rbcc2 (rbcc efhm2)) + (lbcc (direct-sum chcm1 chcm2)) + (tcc (direct-sum tcc1 tcc2)) + (rbcc (direct-sum rbcc1 rbcc2)) + (LF (direct-sum-mrph tcc lbcc lf1 lf2)) + (LG (direct-sum-mrph lbcc tcc lg1 lg2)) + (LH (direct-sum-mrph tcc tcc lh1 lh2)) + (RF (direct-sum-mrph tcc rbcc rf1 rf2)) + (RG (direct-sum-mrph rbcc tcc rg1 rg2)) + (RH (direct-sum-mrph tcc tcc rh1 rh2))) + (build-hmeq + :lrdct (build-rdct :f LF :g LG :h LH + :orgn `(direct-sum-efhm ,chcm1 ,chcm2 lrdct)) + :rrdct (build-rdct :f RF :g RG :h RH + :orgn `(direct-sum-efhm ,chcm1 ,chcm2 rrdct)) + :orgn `(direct-sum-efhm ,chcm1 ,chcm2))))) + + + + +(DEFMETHOD SEARCH-EFHM (direct-sum (orgn (eql 'direct-sum))) + (declare (type chain-complex direct-sum)) + (the homotopy-equivalence + (direct-sum-efhm (second (orgn direct-sum)) + (third (orgn direct-sum))))) + + diff --git a/src/pushout/remove-covers.lisp b/src/pushout/remove-covers.lisp new file mode 100644 index 0000000..9a5c70b --- /dev/null +++ b/src/pushout/remove-covers.lisp @@ -0,0 +1,150 @@ +;;;============================================================================ +;;; +;;; Subject: Remove Covers +;;; +;;; +;;;---------------------------------------------------------------------------- +;;; +;;; Author: Jónathan Heras Vicente +;;; 13/10/09 +;;; +;;;============================================================================ + +;;; Adapted by Julián Cuevas, Jose Divasón, Miguel Marco Buzunariz and Ana Romero. +;;; August 2019 + +(in-package #:cat) + +(provide "remove-covers") + +(defun remove-covers-basis (basis1) + (declare (type basis basis1)) + (when (eq basis1 :locally-effective) + (return-from remove-covers-basis :locally-effective)) + (flet ((rslt (dmns) + (remove-if #'(lambda (item) + (member item '(1 2))) + (funcall basis1 dmns) :key #'gmsm2) + )) + (the basis #'rslt))) + + + +(defun remove-covers-dffr (dffr1) + (declare (type morphism dffr1)) + (flet ((rslt (cmbn) + (declare (type cmbn cmbn)) + (with-cmbn (degr list) cmbn + (declare (ignore list)) + (make-cmbn :degr (1- degr) + :list (remove-if #'(lambda (item) + (member (gnrt2 (gnrt item)) '(1 2))) + (cmbn-list (? dffr1 cmbn)))) + ) + )) + (the intr-mrph #'rslt))) + + + +(defun remove-covers (chcm1) + (declare (type simplicial-set chcm1)) + (let ((XxI (crts-prdc chcm1 (delta 1)))) + (the chain-complex + (build-chcm + :cmpr (cmpr XxI) + :basis (remove-covers-basis (basis XxI)) + :bsgn nil + :intr-dffr (remove-covers-dffr (dffr XxI)) + :strt :cmbn + :orgn `(remove-covers ,chcm1))))) + + + + + + +(DEFUN remove-covers-efhm (chcm) + (let* ((A (direct-sum (second (orgn chcm)) (second (orgn chcm)))) + (B (crts-prdc (second (orgn chcm)) (delta 1))) + (C chcm) + (i (build-mrph + :sorc A :trgt B :degr 0 + :intr + #'(lambda (cmbn) + (with-cmbn (degr list) cmbn + (make-cmbn + :degr degr + :list (mapcar + #'(lambda (term) + (with-term (cffc gnrt) term + (if (= (d-sum-ind gnrt) 0) + (term cffc + (crpr 0 (d-sum-old gnrt) (mask degr) 1)) + (term cffc + (crpr 0 (d-sum-old gnrt) (mask degr) 2))))) + list)))) + :strt :cmbn + :orgn `(,A -> ,B))) + (rho (build-mrph + :sorc B :trgt A :degr 0 + :intr + #'(lambda (cmbn) + (with-cmbn (degr list) cmbn + (make-cmbn + :degr degr + :list (mapcar #'(lambda (mnm) + (if (equal (gmsm2 (gnrt mnm)) 1) + (term (cffc mnm) + (direct-sum-gsm 0 (gmsm1 (gnrt mnm))) + ) + (term (cffc mnm) + (direct-sum-gsm 1 (gmsm1 (gnrt mnm)))))) + (remove-if #'(lambda (item) + (member (gmsm2 (gnrt item)) '(3))) + list))))) + :strt :cmbn + :orgn `(,B -> ,A))) + (sigma (build-mrph + :sorc C :trgt B :degr 0 + :intr + #'(lambda (cmbn) + (with-cmbn (degr list) cmbn + (make-cmbn + :degr degr + :list list))) + :strt :cmbn + :orgn `(,C -> ,B))) + (j (build-mrph + :sorc B :trgt C :degr 0 + :intr + #'(lambda (cmbn) + (with-cmbn (degr list) cmbn + (make-cmbn + :degr degr + :list (remove-if #'(lambda (item) + (member (gmsm2 (gnrt item)) '(1 2))) + list)))) + :strt :cmbn + :orgn `(,B -> ,C))) + (cone-i (cone i)) + (efhm-cone (efhm cone-i)) + (rrdct-efhm-cone (rrdct efhm-cone)) + (lrdct-efhm-cone (lrdct efhm-cone)) + (rdct-C-cone-i (aibjc-rdct A i rho B j sigma C)) + (final-lrdct (cmps rdct-C-cone-i lrdct-efhm-cone)) + ) + + (the homotopy-equivalence (progn + (build-hmeq + :lrdct final-lrdct + :rrdct rrdct-efhm-cone + :orgn `(remove-covers-efhm ,chcm))))) + ) + + +(DEFMETHOD SEARCH-EFHM (remove-covers (orgn (eql 'remove-covers))) + (declare (type chain-complex remove-covers)) + (the homotopy-equivalence + (remove-covers-efhm remove-covers + ))) + diff --git a/src/pushout/suspension2.lisp b/src/pushout/suspension2.lisp new file mode 100644 index 0000000..d817808 --- /dev/null +++ b/src/pushout/suspension2.lisp @@ -0,0 +1,138 @@ +;;;============================================================================ +;;; +;;; Subject: Suspensions2 +;;; +;;; +;;;---------------------------------------------------------------------------- +;;; +;;; Author: Jónathan Heras Vicente +;;; 13/10/09 +;;; +;;;============================================================================ + +;;; Adapted by Julián Cuevas, Jose Divasón, Miguel Marco Buzunariz and Ana Romero. +;;; August 2019 + +(in-package #:cat) + +(provide "suspension2") + +(DEFUN suspension2-basis (basis) + (declare (type basis basis)) + (when (eq basis :locally-effective) + (return-from suspension2-basis :locally-effective)) + (flet ((rslt (degr) + (declare (fixnum degr)) + (funcall basis (1- degr)))) + (the basis #'rslt))) + + + +(defun suspension2-intr-dffr (dffr) + (declare (type morphism dffr)) + (flet ((rslt (cmbn) + (declare (type cmbn cmbn)) + (with-cmbn (degr list) cmbn + (if (> degr 0) + (let ((cmbn-bis (make-cmbn :degr (1- degr) :list list))) + (make-cmbn :degr (1- degr) + :list (mapcar #'(lambda (old) + (term (* -1 (cffc old)) + (gnrt old)) + ) + (cmbn-list (? dffr cmbn-bis)) ) + )) + (zero-cmbn (1- degr)))))) + (the intr-mrph #'rslt)) + ) + + + +(DEFMETHOD SUSPENSION2 ((chcm chain-complex)) + (the chain-complex + (with-slots (cmpr basis dffr) chcm + (build-chcm + :cmpr cmpr + :basis (suspension2-basis basis) + :bsgn nil + :intr-dffr (suspension2-intr-dffr dffr) + :strt :cmbn + :orgn `(suspension2 ,chcm))))) + + + + + +(DEFUN SUSPENSION2-INTR (mrph) + (declare (type morphism mrph)) + (flet ((rslt (cmbn) + (declare (type cmbn cmbn)) + (with-cmbn (degr list) cmbn + (make-cmbn :degr (+ degr (degr mrph)) + :list (mapcar #'(lambda (old) + (term (* -1 (cffc old)) + (gnrt old)) + ) + (cmbn-list + (? mrph (make-cmbn :degr (1- degr) + :list list))) ) + )))) + (the intr-mrph #'rslt))) + + + + +(DEFMETHOD SUSPENSION2 ((mrph morphism)) + (the morphism + (let ((orgn (orgn mrph))) + (declare (list orgn)) + (when (eq (first orgn) 'zero-mrph) + (return-from suspension2 + (zero-mrph (suspension2 (sorc mrph)) + (suspension2 (trgt mrph)) + (degr mrph)))) + (when (eq (first orgn) 'idnt-mrph) + (return-from suspension2 + (idnt-mrph (suspension2 (sorc mrph))))) + (build-mrph + :sorc (suspension2 (sorc mrph)) + :trgt (suspension2 (trgt mrph)) + :degr (degr mrph) + :intr (suspension2-intr mrph) + :strt :cmbn + :orgn `(suspension2 ,mrph))))) + + + + +(DEFMETHOD SUSPENSION2 ((rdct reduction)) + (the reduction (progn + (when (eq (first (orgn rdct)) 'trivial-rdct) + (return-from suspension2 + (trivial-rdct (suspension2 (second (orgn rdct)))))) + (build-rdct + :f (suspension2 (f rdct)) + :g (suspension2 (g rdct)) + :h (suspension2 (h rdct)) + :orgn `(suspension2 ,rdct))))) + + +(DEFMETHOD SUSPENSION2 ((hmeq homotopy-equivalence)) + (the homotopy-equivalence (progn + (when (eq (first (orgn hmeq)) 'trivial-hmeq) + (return-from suspension2 + (trivial-hmeq (suspension2 (second (orgn hmeq)))))) + (build-hmeq + :lrdct (suspension2 (lrdct hmeq)) + :rrdct (suspension2 (rrdct hmeq)) + :orgn `(suspension2 ,hmeq))))) + + +(DEFMETHOD SEARCH-EFHM (suspension2 (orgn (eql 'suspension2))) + (declare (type chain-complex suspension2)) + (suspension2 (efhm (second (orgn suspension2))))) + + + + + diff --git a/src/special-smsts.lisp b/src/special-smsts.lisp index 12a2fba..0e4fb3f 100644 --- a/src/special-smsts.lisp +++ b/src/special-smsts.lisp @@ -236,7 +236,7 @@ :bndr-strt :gnrt :orgn `(build-finite-ss ,list)))) (setf (symbol-value ind-smst) rslt) - (inspect rslt) + ;;(inspect rslt) (unless (check-smst rslt 0 (length table)) (pop *smst-list*) (pop *chcm-list*)