gheber / kenzo

A repackaged version of the Kenzo program by Francis Sergeraert and collaborators.
https://sur-l-analysis-sit.us/
Other
50 stars 8 forks source link

k-pi-n.lisp #99

Closed gheber closed 8 years ago

gheber commented 8 years ago

; in: DEFUN K-Z-1 ; (THE CAT::AB-SIMPLICIAL-GROUP ; (CAT::BUILD-AB-SMGR :CMPR #'CAT::K-Z-1-CMPR :BASIS :LOCALLY-EFFECTIVE ; :BSPN CAT::+EMPTY-LIST+ :FACE #'CAT::K-Z-1-FACE ; :SINTR-GRML #'CAT::K-Z-1-GRML :SINTR-GRIN ...)) ; ; note: type assertion too complex to check: ; (VALUES AB-SIMPLICIAL-GROUP &REST T).

; in: DEFUN K-Z ; (THE CAT::AB-SIMPLICIAL-GROUP ; (IF (= CAT::N 1) ; (CAT::K-Z-1) ; (CAT::CLASSIFYING-SPACE (CAT::K-Z (1- CAT::N))))) ; ; note: type assertion too complex to check: ; (VALUES AB-SIMPLICIAL-GROUP &REST T).

; in: DEFUN CIRCLE ; (THE CAT::CHAIN-COMPLEX ; (CAT::BUILD-CHCM :CMPR #'CAT::CIRCLE-CMPR :BASIS #'CAT::CIRCLE-BASIS ; :BSGN '* :INTR-DFFR #'CAT::ZERO-INTR-DFFR :STRT :CMBN ; :ORGN ...)) ; ; note: type assertion too complex to check: ; (VALUES CHAIN-COMPLEX &REST T).

; in: DEFUN KZ1-RDCT-F-INTR ; (THE CAT::CMBN ; (CAT::WITH-CMBN (CAT::DEGR LIST) CAT::CMBN ; (CASE CAT::DEGR ; (0 ; (IF LIST ; # ; #)) ; (1 ; (LET # ; #)) ; (OTHERWISE (CAT::ZERO-CMBN CAT::DEGR))))) ; ; note: type assertion too complex to check: ; (VALUES CMBN &REST T).

; in: DEFUN KZ1-RDCT-F ; (THE CAT::MORPHISM ; (CAT::BUILD-MRPH :SORC (CAT::K-Z-1) :TRGT (CAT::CIRCLE) :DEGR 0 :INTR ; #'CAT::KZ1-RDCT-F-INTR :STRT :CMBN :ORGN ...)) ; ; note: type assertion too complex to check: ; (VALUES MORPHISM &REST T).

; in: DEFUN KZ1-RDCT-G-INTR ; (THE CAT::CMBN ; (CAT::WITH-CMBN (CAT::DEGR LIST) CAT::CMBN ; (IF LIST ; (ECASE CAT::DEGR (0 #) (1 #)) ; (CAT::ZERO-CMBN CAT::DEGR)))) ; ; note: type assertion too complex to check: ; (VALUES CMBN &REST T).

; in: DEFUN KZ1-RDCT-G ; (THE CAT::MORPHISM ; (CAT::BUILD-MRPH :SORC (CAT::CIRCLE) :TRGT (CAT::K-Z-1) :DEGR 0 :INTR ; #'CAT::KZ1-RDCT-G-INTR :STRT :CMBN :ORGN ...)) ; ; note: type assertion too complex to check: ; (VALUES MORPHISM &REST T).

; in: DEFUN KZ1-RDCT-H ; (THE CAT::MORPHISM ; (CAT::BUILD-MRPH :SORC (CAT::K-Z-1) :TRGT (CAT::K-Z-1) :DEGR 1 :INTR ; #'CAT::KZ1-RDCT-H-INTR :STRT :GNRT :ORGN ...)) ; ; note: type assertion too complex to check: ; (VALUES MORPHISM &REST T).

; in: DEFUN KZ1-RDCT ; (THE CAT::REDUCTION ; (CAT::BUILD-RDCT :F (CAT::KZ1-RDCT-F) :G (CAT::KZ1-RDCT-G) :H ; (CAT::KZ1-RDCT-H) :ORGN '(CAT::KZ1-RDCT))) ; ; note: type assertion too complex to check: ; (VALUES REDUCTION &REST T).

; in: DEFUN KZ1-EFHM ; (THE CAT::HOMOTOPY-EQUIVALENCE ; (CAT::BUILD-HMEQ :LRDCT (CAT::TRIVIAL-RDCT (CAT::K-Z-1)) :RRDCT ; (CAT::KZ1-RDCT) :ORGN '(CAT::KZ1-EFHM))) ; ; note: type assertion too complex to check: ; (VALUES HOMOTOPY-EQUIVALENCE &REST T).

; in: DEFUN K-Z2-1-GRML ; (THE CAT::SIMPLICIAL-MRPH ; (CAT::BUILD-SMMR :SORC ; (CAT::CRTS-PRDC (CAT::R-PROJ-SPACE) ; (CAT::R-PROJ-SPACE)) ; :TRGT (CAT::R-PROJ-SPACE) :DEGR 0 :SINTR ; #'CAT::K-Z2-1-GRML-INTR :ORGN '(CAT::K-Z2-1-GRML))) ; ; note: type assertion too complex to check: ; (VALUES SIMPLICIAL-MRPH &REST T).

; in: DEFUN K-Z2-1-GRIN ; (THE CAT::SIMPLICIAL-MRPH ; (CAT::BUILD-SMMR :SORC (CAT::R-PROJ-SPACE) :TRGT (CAT::R-PROJ-SPACE) ; :DEGR 0 :SINTR #'CAT::K-Z2-1-GRIN-INTR :INTR #'IDENTITY ; :STRT ...)) ; ; note: type assertion too complex to check: ; (VALUES SIMPLICIAL-MRPH &REST T).

; in: DEFUN K-Z2 ; (THE CAT::AB-SIMPLICIAL-GROUP ; (IF (= CAT::N 1) ; (CAT::K-Z2-1) ; (CAT::CLASSIFYING-SPACE (CAT::K-Z2 (1- CAT::N))))) ; ; note: type assertion too complex to check: ; (VALUES AB-SIMPLICIAL-GROUP &REST T).

; in: DEFUN HOPF-FIBRATION ; (THE CAT::SIMPLICIAL-MRPH ; (CAT::BUILD-SMMR :SORC (CAT::SPHERE 2) :TRGT (CAT::K-Z-1) :DEGR -1 ; :SINTR (CAT::HOPF-FIBRATION-SINTR CAT::N) :ORGN ; `(CAT::HOPF-FIBRATION ,CAT::N))) ; ; note: type assertion too complex to check: ; (VALUES SIMPLICIAL-MRPH &REST T).

; in: DEFUN Z-COCYCLE-GBAR ; (THE CAT::ABSM ; (COND ((= CAT::N 1) (CAT::Z-BAR-ABSM (NREVERSE #))) ; ((= CAT::N CAT::DMNS) ; (LET (#) ; (DECLARE #) ; (IF # ; # ; #))) ; (T ; (LET (# #) ; (DECLARE #) ; (DOLIST # # #) ; (SETF #) ; (MAPC #'# CAT::COCYCLE2) ; (LET # ; # ; #))))) ; ; note: type assertion too complex to check: ; (VALUES ABSM &REST T).

; in: DEFUN Z-COCYCLE-GBAR-HEAD ; (THE CAT::ABSM ; (COND ; ((= CAT::N 1) ; (ERROR ; "In Z-COCYCLE-GBAR-HEAD, this point should not have been reached.")) ; ((= CAT::N CAT::DMNS) ; (LET (#) ; (DECLARE #) ; (IF # ; # ; #))) ; (T ; (LET (# #) ; (DECLARE #) ; (DOLIST # # #) ; (SETF #) ; (MAPC #'# CAT::COCYCLE2) ; (CAT::Z-COCYCLE-GBAR # # CAT::COCYCLE2))))) ; ; note: type assertion too complex to check: ; (VALUES ABSM &REST T).

; in: DEFUN Z2-COCYCLE-GBAR ; (THE CAT::ABSM ; (PROGN ; (MAPC #'(LAMBDA (CONS) (DECLARE #) (SETF #)) CAT::COCYCLE) ; (COND ((= CAT::N 1) (CAT::Z2-BAR-ABSM #)) ; ((= CAT::N CAT::DMNS) ; (LET # ; # ; #)) ; (T ; (LET # ; # ; # ; # ; # ; #))))) ; ; note: type assertion too complex to check: ; (VALUES ABSM &REST T).

; in: DEFUN Z2-COCYCLE-GBAR-HEAD ; (THE CAT::ABSM ; (PROGN ; (MAPC #'(LAMBDA (CONS) (SETF #)) CAT::COCYCLE) ; (COND ; ((= CAT::N 1) ; (ERROR ; "In Z2-COCYCLE-GBAR-HEAD, this point should not have been reached.")) ; ((= CAT::N CAT::DMNS) ; (LET # ; # ; #)) ; (T ; (LET # ; # ; # ; # ; # ; #))))) ; ; note: type assertion too complex to check: ; (VALUES ABSM &REST T).

; in: DEFUN K-Z-FUNDAMENTAL-CLASS ; (THE CAT::MORPHISM ; (CAT::BUILD-MRPH :SORC (CAT::K-Z CAT::N) :TRGT (CAT::Z-CHCM) :DEGR ; (- CAT::N) :INTR ; #'(LAMBDA (CAT::DMNS CAT::GMSM) ; (DECLARE (FIXNUM CAT::DMNS) ; (TYPE CAT::GMSM CAT::GMSM)) ; (IF (= CAT::DMNS CAT::N) ; (DO # # #) ; (CAT::ZERO-CMBN #))) ; :STRT :GNRT :ORGN ...)) ; ; note: type assertion too complex to check: ; (VALUES MORPHISM &REST T).

; in: DEFUN K-Z2-FUNDAMENTAL-CLASS ; (THE CAT::MORPHISM ; (CAT::BUILD-MRPH :SORC (CAT::K-Z2 CAT::N) :TRGT (CAT::Z-CHCM) :DEGR ; (- CAT::N) :INTR ; #'(LAMBDA (CAT::DMNS CAT::GMSM) ; (DECLARE (FIXNUM CAT::DMNS) ; (IGNORE CAT::GMSM)) ; (IF (= CAT::DMNS CAT::N) ; (CAT::TERM-CMBN 0 1 :Z-GNRT) ; (CAT::ZERO-CMBN #))) ; :STRT :GNRT :ORGN ...)) ; ; note: type assertion too complex to check: ; (VALUES MORPHISM &REST T).