added pushouts
This commit is contained in:
jodivaso
parent
597d021f7b
commit
0f614d77ea
30
kenzo.asd
30
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")))
|
||||
|
||||
|
||||
))))
|
||||
|
||||
95
src/pushout/AiBjC-rdct.lisp
Normal file
95
src/pushout/AiBjC-rdct.lisp
Normal file
@ -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))))
|
||||
642
src/pushout/Examples.lisp
Normal file
642
src/pushout/Examples.lisp
Normal file
@ -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)
|
||||
|
||||
377
src/pushout/Pushout.lisp
Normal file
377
src/pushout/Pushout.lisp
Normal file
@ -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 "<PUSHOUT-GSM ~A ~A>"
|
||||
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)
|
||||
))
|
||||
|
||||
|
||||
|
||||
|
||||
210
src/pushout/cones2.lisp
Normal file
210
src/pushout/cones2.lisp
Normal file
@ -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)))
|
||||
|
||||
210
src/pushout/direct-sum.lisp
Normal file
210
src/pushout/direct-sum.lisp
Normal file
@ -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 "<DIRECT-SUM-GSM ~A ~A>"
|
||||
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)))))
|
||||
|
||||
|
||||
150
src/pushout/remove-covers.lisp
Normal file
150
src/pushout/remove-covers.lisp
Normal file
@ -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
|
||||
)))
|
||||
|
||||
138
src/pushout/suspension2.lisp
Normal file
138
src/pushout/suspension2.lisp
Normal file
@ -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)))))
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
@ -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*)
|
||||
|
||||
Loading…
Reference in New Issue
Block a user