help links subscribe changes refresh edit

	SandBox
DependentTypeTest1 ←	↑	→ DerivFunc

DependentTypeTest2

Edit detail for DependentTypeTest2 revision 1 of 1

	1
Editor: pagani Time: 2022/09/03 15:11:28 GMT+0
Note:

changed:
-
\begin{spad}
--)lisp (defvar |$inclAssertions| nil)

-- in principle d:V[k]->V[k+1], then what is d d = 0?
-- each vector space V[k] has its own zero! But we will
-- only use one zero form for all. ZeroChain()?


)abbrev category CCHNCAT CoChainCategory
CoChainCategory() : Category == SetCategory with
        degree : % -> Polynomial Integer 
        mainType : % -> String -- trick: get the type
 
)abbrev category ZCHNCAT ZeroChainCategory
ZeroChainCategory() : Category == SetCategory with
        null : %
 
)abbrev domain ZCHN ZeroChain
ZeroChain : Exports == Implementation where
  BOP ==> BasicOperator 
  PINT ==> Polynomial Integer
  Exports == Join(CoChainCategory,ZeroChainCategory) with
    degree : % -> PINT 
    d : % -> %
    --null   : %
  Implementation == BOP add 
    Rep := BOP  
    null == operator("0"::Symbol) 
    degree x == 0::PINT
    d x == null()
    mainType x == "ZeroChain"
    

)abbrev domain COCHN CoChain
CoChain(p) : Exports == Implementation where 
  p:Polynomial Integer
  BOP ==> BasicOperator 
  CTOF ==> CoercibleTo OutputForm
  CVTS ==> ConvertibleTo String
  PINT ==> Polynomial Integer
  Exports == Join(CTOF, CVTS, CoChainCategory) with
    coerce : Symbol -> %
    degree : % -> PINT    
  Implementation == BOP add 
    Rep := BOP  
    coerce(s:Symbol):% == operator s
    degree x == p
    mainType x == "CoChain"
  

)abbrev domain WEDGE WedgeProduct
WedgeProduct(a,b) : Exports == Implementation where 
  CCCAT ==> CoChainCategory
  OF ==> OutputForm
  a:CCCAT
  b:CCCAT 
  CTOF ==> CoercibleTo OutputForm
  CVTS ==> ConvertibleTo String
  PINT ==> Polynomial Integer
  Exports == Join(CTOF, CVTS, CoChainCategory) with
    if a has ZeroChainCategory or b has ZeroChainCategory then
      _* : (a,b) -> ZeroChain
    else
      _* : (a,b) -> %
      degree : % -> PINT    
  Implementation == add 
    if a has ZeroChainCategory or b has ZeroChainCategory then
      Rep := ZeroChain
      (x:a * y:b):ZeroChain == null()$ZeroChain 
    else
      Rep := Record(left:a,right:b)   
      x * y == [x,y]@Rep
      degree x == degree(x.left)$a + degree(x.right)$b
      mainType x == "WedgeProduct"
      coerce(x:%):OutputForm == tensor(x.left::OF,x.right::OF)
    ------ temp using tensor, lack of wedge symbol 

)abbrev domain EXTDF ExteriorDerivative
ExteriorDerivative(a) : Exports == Implementation where 
  CCCAT ==> CoChainCategory
  OF ==> OutputForm
  a:CCCAT
  CTOF ==> CoercibleTo OutputForm
  CVTS ==> ConvertibleTo String
  PINT ==> Polynomial Integer
  Exports == Join(CTOF, CVTS, CoChainCategory) with
    d : % -> ZeroChain
    d : a -> %
    degree : % -> PINT    
  Implementation == add
    if a has ZeroChainCategory then
      Rep := ZeroChain
    else
      Rep := Record(arg:a) 
      d(x:%):ZeroChain == null()$ZeroChain
      d(x:a):% == [x]@Rep
      degree x == 1 + degree(x.arg)$a 
      mainType x == "ExteriorDerivative"
      coerce(x:%):OutputForm ==
        dsym:=outputForm("d"::Symbol)$OF
        mainType(x.arg)$a = "CoChain" => hconcat(dsym,x.arg::OF) 
        hconcat(dsym,paren(x.arg::OF))
 
)abbrev domain HODGE HodgeStar
HodgeStar(a) : Exports == Implementation where 
  CCCAT ==> CoChainCategory
  OF ==> OutputForm
  a:CCCAT
  CTOF ==> CoercibleTo OutputForm
  CVTS ==> ConvertibleTo String
  PINT ==> Polynomial Integer
  Exports == Join(CTOF, CVTS, CoChainCategory) with
    hodge : a -> %
    degree : % -> PINT    
  Implementation == add 
    Rep := Record(arg:a) 
    n:PINT:="spacedim"::Symbol::PINT
    degree x == n - degree(x.arg)$a 
    hodge x == [x]@Rep
    mainType x == "HodgeStar"
    coerce(x:%):OutputForm ==
      dsym:=outputForm("*"::Symbol)$OF
      mT:String:=mainType(x.arg)$a
      mT ~= "WedgeProduct" => hconcat(dsym,x.arg::OF) 
      hconcat(dsym,paren(x.arg::OF))

\end{spad}

\begin{axiom}
f:=f::CoChain(p)
g:=g::CoChain(q)
h:=f*g
degree h
k:=h*f
degree k
-- car dom (d f) --> ExteriorDerivative Type: SExpression
-- symbol car dom (d f) = 'ExteriorDerivative::Symbol => ok
degree d f  --> p+1
hodge d h --> *d(f # g)
r:=degree hodge h
eval(r,[p=7,q=3,'spacedim=15]) --> notice the quote!
-->degree % --> spacedim - q - p - 1

null()$ZeroChain

z:=d d f
z*f
f*z


CoChain(p) has ZeroChainCategory
ZeroChain has ZeroChainCategory



\end{axiom}

fricas

(1) -> <spad>
--)lisp (defvar |$inclAssertions| nil)

-- in principle d:V[k]->V[k+1], then what is d d = 0?
-- each vector space V[k] has its own zero! But we will
-- only use one zero form for all. ZeroChain()?

fricas

)abbrev category CCHNCAT CoChainCategory
CoChainCategory() : Category == SetCategory with
        degree : % -> Polynomial Integer 
        mainType : % -> String -- trick: get the type

fricas

)abbrev category ZCHNCAT ZeroChainCategory
ZeroChainCategory() : Category == SetCategory with
        null : %

fricas

)abbrev domain ZCHN ZeroChain
ZeroChain : Exports == Implementation where
  BOP ==> BasicOperator 
  PINT ==> Polynomial Integer
  Exports == Join(CoChainCategory,ZeroChainCategory) with
    degree : % -> PINT 
    d : % -> %
    --null   : %
  Implementation == BOP add 
    Rep := BOP  
    null == operator("0"::Symbol) 
    degree x == 0::PINT
    d x == null()
    mainType x == "ZeroChain"

fricas

)abbrev domain COCHN CoChain
CoChain(p) : Exports == Implementation where 
  p:Polynomial Integer
  BOP ==> BasicOperator 
  CTOF ==> CoercibleTo OutputForm
  CVTS ==> ConvertibleTo String
  PINT ==> Polynomial Integer
  Exports == Join(CTOF, CVTS, CoChainCategory) with
    coerce : Symbol -> %
    degree : % -> PINT    
  Implementation == BOP add 
    Rep := BOP  
    coerce(s:Symbol):% == operator s
    degree x == p
    mainType x == "CoChain"

fricas

)abbrev domain WEDGE WedgeProduct
WedgeProduct(a,b) : Exports == Implementation where 
  CCCAT ==> CoChainCategory
  OF ==> OutputForm
  a:CCCAT
  b:CCCAT 
  CTOF ==> CoercibleTo OutputForm
  CVTS ==> ConvertibleTo String
  PINT ==> Polynomial Integer
  Exports == Join(CTOF, CVTS, CoChainCategory) with
    if a has ZeroChainCategory or b has ZeroChainCategory then
      _* : (a,b) -> ZeroChain
    else
      _* : (a,b) -> %
      degree : % -> PINT    
  Implementation == add 
    if a has ZeroChainCategory or b has ZeroChainCategory then
      Rep := ZeroChain
      (x:a * y:b):ZeroChain == null()$ZeroChain 
    else
      Rep := Record(left:a,right:b)   
      x * y == [x,y]@Rep
      degree x == degree(x.left)$a + degree(x.right)$b
      mainType x == "WedgeProduct"
      coerce(x:%):OutputForm == tensor(x.left::OF,x.right::OF)
    ------ temp using tensor, lack of wedge symbol

fricas

)abbrev domain EXTDF ExteriorDerivative
ExteriorDerivative(a) : Exports == Implementation where 
  CCCAT ==> CoChainCategory
  OF ==> OutputForm
  a:CCCAT
  CTOF ==> CoercibleTo OutputForm
  CVTS ==> ConvertibleTo String
  PINT ==> Polynomial Integer
  Exports == Join(CTOF, CVTS, CoChainCategory) with
    d : % -> ZeroChain
    d : a -> %
    degree : % -> PINT    
  Implementation == add
    if a has ZeroChainCategory then
      Rep := ZeroChain
    else
      Rep := Record(arg:a) 
      d(x:%):ZeroChain == null()$ZeroChain
      d(x:a):% == [x]@Rep
      degree x == 1 + degree(x.arg)$a 
      mainType x == "ExteriorDerivative"
      coerce(x:%):OutputForm ==
        dsym:=outputForm("d"::Symbol)$OF
        mainType(x.arg)$a = "CoChain" => hconcat(dsym,x.arg::OF) 
        hconcat(dsym,paren(x.arg::OF))

fricas

)abbrev domain HODGE HodgeStar
HodgeStar(a) : Exports == Implementation where 
  CCCAT ==> CoChainCategory
  OF ==> OutputForm
  a:CCCAT
  CTOF ==> CoercibleTo OutputForm
  CVTS ==> ConvertibleTo String
  PINT ==> Polynomial Integer
  Exports == Join(CTOF, CVTS, CoChainCategory) with
    hodge : a -> %
    degree : % -> PINT    
  Implementation == add 
    Rep := Record(arg:a) 
    n:PINT:="spacedim"::Symbol::PINT
    degree x == n - degree(x.arg)$a 
    hodge x == [x]@Rep
    mainType x == "HodgeStar"
    coerce(x:%):OutputForm ==
      dsym:=outputForm("*"::Symbol)$OF
      mT:String:=mainType(x.arg)$a
      mT ~= "WedgeProduct" => hconcat(dsym,x.arg::OF) 
      hconcat(dsym,paren(x.arg::OF))</spad>

fricas

Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/5250937285633644280-25px001.spad
      using old system compiler.
   CCHNCAT abbreviates category CoChainCategory 
------------------------------------------------------------------------
   initializing NRLIB CCHNCAT for CoChainCategory 
   compiling into NRLIB CCHNCAT 

;;;     ***       |CoChainCategory| REDEFINED
Time: 0 SEC.

   finalizing NRLIB CCHNCAT 
   Processing CoChainCategory for Browser database:
--->-->CoChainCategory(constructor): Not documented!!!!
--->-->CoChainCategory((degree ((Polynomial (Integer)) %))): Not documented!!!!
--->-->CoChainCategory((mainType ((String) %))): Not documented!!!!
--->-->CoChainCategory(): Missing Description
; compiling file "/var/aw/var/LatexWiki/CCHNCAT.NRLIB/CCHNCAT.lsp" (written 02 NOV 2024 02:52:10 AM):

; wrote /var/aw/var/LatexWiki/CCHNCAT.NRLIB/CCHNCAT.fasl
; compilation finished in 0:00:00.000
------------------------------------------------------------------------
   CoChainCategory is now explicitly exposed in frame initial 
   CoChainCategory will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/CCHNCAT.NRLIB/CCHNCAT

   ZCHNCAT abbreviates category ZeroChainCategory 
------------------------------------------------------------------------
   initializing NRLIB ZCHNCAT for ZeroChainCategory 
   compiling into NRLIB ZCHNCAT 

;;;     ***       |ZeroChainCategory| REDEFINED
Time: 0 SEC.

   finalizing NRLIB ZCHNCAT 
   Processing ZeroChainCategory for Browser database:
--->-->ZeroChainCategory(constructor): Not documented!!!!
--->-->ZeroChainCategory((null (%) constant)): Not documented!!!!
--->-->ZeroChainCategory(): Missing Description
; compiling file "/var/aw/var/LatexWiki/ZCHNCAT.NRLIB/ZCHNCAT.lsp" (written 02 NOV 2024 02:52:10 AM):

; wrote /var/aw/var/LatexWiki/ZCHNCAT.NRLIB/ZCHNCAT.fasl
; compilation finished in 0:00:00.004
------------------------------------------------------------------------
   ZeroChainCategory is now explicitly exposed in frame initial 
   ZeroChainCategory will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/ZCHNCAT.NRLIB/ZCHNCAT

   ZCHN abbreviates domain ZeroChain 
------------------------------------------------------------------------
   initializing NRLIB ZCHN for ZeroChain 
   compiling into NRLIB ZCHN 
   compiling exported null : () -> %
Time: 0 SEC.

   compiling exported degree : % -> Polynomial Integer
Time: 0.02 SEC.

   compiling exported d : % -> %
Time: 0 SEC.

   compiling exported mainType : % -> String
      ZCHN;mainType;%S;4 is replaced by ZeroChain 
Time: 0 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |ZeroChain| REDEFINED

;;;     ***       |ZeroChain| REDEFINED
Time: 0 SEC.

   Cumulative Statistics for Constructor ZeroChain
      Time: 0.02 seconds

--------------non extending category----------------------
.. ZeroChain of cat 
(|Join| (|CoChainCategory|) (|ZeroChainCategory|)
        (CATEGORY |domain| (SIGNATURE |degree| ((|Polynomial| (|Integer|)) %))
         (SIGNATURE |d| (% %))))   has no 
(|OrderedSet|)    finalizing NRLIB ZCHN 
   Processing ZeroChain for Browser database:
--->-->ZeroChain(constructor): Not documented!!!!
--->-->ZeroChain((degree ((Polynomial (Integer)) %))): Not documented!!!!
--->-->ZeroChain((d (% %))): Not documented!!!!
--->-->ZeroChain(): Missing Description
; compiling file "/var/aw/var/LatexWiki/ZCHN.NRLIB/ZCHN.lsp" (written 02 NOV 2024 02:52:10 AM):

; wrote /var/aw/var/LatexWiki/ZCHN.NRLIB/ZCHN.fasl
; compilation finished in 0:00:00.008
------------------------------------------------------------------------
   ZeroChain is now explicitly exposed in frame initial 
   ZeroChain will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/ZCHN.NRLIB/ZCHN

   COCHN abbreviates domain CoChain 
------------------------------------------------------------------------
   initializing NRLIB COCHN for CoChain 
   compiling into NRLIB COCHN 
   compiling exported coerce : Symbol -> %
Time: 0 SEC.

   compiling exported degree : % -> Polynomial Integer
Time: 0 SEC.

   compiling exported mainType : % -> String
      COCHN;mainType;%S;3 is replaced by CoChain 
Time: 0 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |CoChain| REDEFINED

;;;     ***       |CoChain| REDEFINED
Time: 0 SEC.

   Cumulative Statistics for Constructor CoChain
      Time: 0 seconds

--------------non extending category----------------------
.. CoChain(#1) of cat 
(|Join| (|CoercibleTo| (|OutputForm|)) (|ConvertibleTo| (|String|))
        (|CoChainCategory|)
        (CATEGORY |domain| (SIGNATURE |coerce| (% (|Symbol|)))
         (SIGNATURE |degree| ((|Polynomial| (|Integer|)) %))))   has no 
(|OrderedSet|)    finalizing NRLIB COCHN 
   Processing CoChain for Browser database:
--->-->CoChain(constructor): Not documented!!!!
--->-->CoChain((coerce (% (Symbol)))): Not documented!!!!
--->-->CoChain((degree ((Polynomial (Integer)) %))): Not documented!!!!
--->-->CoChain(): Missing Description
; compiling file "/var/aw/var/LatexWiki/COCHN.NRLIB/COCHN.lsp" (written 02 NOV 2024 02:52:10 AM):

; wrote /var/aw/var/LatexWiki/COCHN.NRLIB/COCHN.fasl
; compilation finished in 0:00:00.004
------------------------------------------------------------------------
   CoChain is now explicitly exposed in frame initial 
   CoChain will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/COCHN.NRLIB/COCHN

   WEDGE abbreviates domain WedgeProduct 
------------------------------------------------------------------------
   initializing NRLIB WEDGE for WedgeProduct 
   compiling into NRLIB WEDGE 
****** Domain: a already in scope
augmenting a: (ZeroChainCategory)
Local variable Rep type redefined: (Join (CoChainCategory) (ZeroChainCategory) (CATEGORY domain (SIGNATURE degree ((Polynomial (Integer)) %)) (SIGNATURE d (% %)))) to (Join (OrderedSet) (CATEGORY domain (SIGNATURE name ((Symbol) %)) (SIGNATURE properties ((AssociationList (Symbol) (None)) %)) (SIGNATURE copy (% %)) (SIGNATURE operator (% (Symbol))) (SIGNATURE operator (% (Symbol) (NonNegativeInteger))) (SIGNATURE arity ((Union (NonNegativeInteger) failed) %)) (SIGNATURE nullary? ((Boolean) %)) (SIGNATURE unary? ((Boolean) %)) (SIGNATURE nary? ((Boolean) %)) (SIGNATURE weight ((NonNegativeInteger) %)) (SIGNATURE weight (% % (NonNegativeInteger))) (SIGNATURE equality (% % (Mapping (Boolean) % %))) (SIGNATURE comparison (% % (Mapping (Boolean) % %))) (SIGNATURE display ((Union (Mapping (OutputForm) (List (OutputForm))) failed) %)) (SIGNATURE display (% % (Mapping (OutputForm) (List (OutputForm))))) (SIGNATURE display (% % (Mapping (OutputForm) (OutputForm)))) (SIGNATURE input (% % (Mapping (InputForm) (List (InputForm))))) (SIGNATURE input ((Union (Mapping (InputForm) (List (InputForm))) failed) %)) (SIGNATURE is? ((Boolean) % (Symbol))) (SIGNATURE has? ((Boolean) % (Symbol))) (SIGNATURE assert (% % (Symbol))) (SIGNATURE deleteProperty! (% % (Symbol))) (SIGNATURE property ((Union (None) failed) % (Symbol))) (SIGNATURE setProperty (% % (Symbol) (None))) (SIGNATURE setProperties (% % (AssociationList (Symbol) (None))))))
   compiling exported * : (a,b) -> ZeroChain
Time: 0 SEC.

****** Domain: b already in scope
augmenting b: (ZeroChainCategory)
   compiling exported * : (a,b) -> ZeroChain
Time: 0 SEC.

Local variable Rep type redefined: (Join (SetCategory) (CATEGORY domain (SIGNATURE construct ((Record (: left a) (: right b)) a b)) (SIGNATURE ~= ((Boolean) (Record (: left a) (: right b)) (Record (: left a) (: right b)))) (SIGNATURE coerce ((OutputForm) (Record (: left a) (: right b)))) (SIGNATURE elt (a (Record (: left a) (: right b)) left)) (SIGNATURE elt (b (Record (: left a) (: right b)) right)) (SIGNATURE setelt! (a (Record (: left a) (: right b)) left a)) (SIGNATURE setelt! (b (Record (: left a) (: right b)) right b)) (SIGNATURE copy ((Record (: left a) (: right b)) (Record (: left a) (: right b)))))) to (Join (CoChainCategory) (ZeroChainCategory) (CATEGORY domain (SIGNATURE degree ((Polynomial (Integer)) %)) (SIGNATURE d (% %))))
   compiling exported * : (a,b) -> %
      WEDGE;*;ab%;3 is replaced by CONS 
Time: 0 SEC.

   compiling exported degree : % -> Polynomial Integer
Time: 0 SEC.

   compiling exported mainType : % -> String
      WEDGE;mainType;%S;5 is replaced by WedgeProduct 
Time: 0 SEC.

   compiling exported coerce : % -> OutputForm
Time: 0 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |WedgeProduct| REDEFINED

;;;     ***       |WedgeProduct| REDEFINED
Time: 0 SEC.

   Warnings: 
      [1] *: signature of lhs not unique:  ab chosen
      [2] degree:  left has no value
      [3] degree:  right has no value

   Cumulative Statistics for Constructor WedgeProduct
      Time: 0 seconds

   finalizing NRLIB WEDGE 
   Processing WedgeProduct for Browser database:
--->-->WedgeProduct(constructor): Not documented!!!!
--->-->WedgeProduct((* ((ZeroChain) a b))): Not documented!!!!
--->-->WedgeProduct((* (% a b))): Not documented!!!!
--->-->WedgeProduct((degree ((Polynomial (Integer)) %))): Not documented!!!!
--->-->WedgeProduct(): Missing Description
; compiling file "/var/aw/var/LatexWiki/WEDGE.NRLIB/WEDGE.lsp" (written 02 NOV 2024 02:52:10 AM):

; wrote /var/aw/var/LatexWiki/WEDGE.NRLIB/WEDGE.fasl
; compilation finished in 0:00:00.008
------------------------------------------------------------------------
   WedgeProduct is now explicitly exposed in frame initial 
   WedgeProduct will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/WEDGE.NRLIB/WEDGE

   EXTDF abbreviates domain ExteriorDerivative 
------------------------------------------------------------------------
   initializing NRLIB EXTDF for ExteriorDerivative 
   compiling into NRLIB EXTDF 
****** Domain: a already in scope
augmenting a: (ZeroChainCategory)
Local variable Rep type redefined: (Join (CoChainCategory) (ZeroChainCategory) (CATEGORY domain (SIGNATURE degree ((Polynomial (Integer)) %)) (SIGNATURE d (% %)))) to (Join (SetCategory) (CATEGORY domain (SIGNATURE construct ((Record (: left a) (: right b)) a b)) (SIGNATURE ~= ((Boolean) (Record (: left a) (: right b)) (Record (: left a) (: right b)))) (SIGNATURE coerce ((OutputForm) (Record (: left a) (: right b)))) (SIGNATURE elt (a (Record (: left a) (: right b)) left)) (SIGNATURE elt (b (Record (: left a) (: right b)) right)) (SIGNATURE setelt! (a (Record (: left a) (: right b)) left a)) (SIGNATURE setelt! (b (Record (: left a) (: right b)) right b)) (SIGNATURE copy ((Record (: left a) (: right b)) (Record (: left a) (: right b))))))
Local variable Rep type redefined: (Join (SetCategory) (CATEGORY domain (SIGNATURE construct ((Record (: arg a)) a)) (SIGNATURE ~= ((Boolean) (Record (: arg a)) (Record (: arg a)))) (SIGNATURE coerce ((OutputForm) (Record (: arg a)))) (SIGNATURE elt (a (Record (: arg a)) arg)) (SIGNATURE setelt! (a (Record (: arg a)) arg a)) (SIGNATURE copy ((Record (: arg a)) (Record (: arg a)))))) to (Join (CoChainCategory) (ZeroChainCategory) (CATEGORY domain (SIGNATURE degree ((Polynomial (Integer)) %)) (SIGNATURE d (% %))))
   compiling exported d : % -> ZeroChain
Time: 0 SEC.

   compiling exported d : a -> %
      EXTDF;d;a%;2 is replaced by LIST 
Time: 0 SEC.

   compiling exported degree : % -> Polynomial Integer
Time: 0 SEC.

   compiling exported mainType : % -> String
      EXTDF;mainType;%S;4 is replaced by ExteriorDerivative 
Time: 0 SEC.

   compiling exported coerce : % -> OutputForm
Time: 0 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |ExteriorDerivative| REDEFINED

;;;     ***       |ExteriorDerivative| REDEFINED
Time: 0 SEC.

   Warnings: 
      [1] degree:  arg has no value
      [2] coerce:  arg has no value

   Cumulative Statistics for Constructor ExteriorDerivative
      Time: 0.01 seconds

   finalizing NRLIB EXTDF 
   Processing ExteriorDerivative for Browser database:
--->-->ExteriorDerivative(constructor): Not documented!!!!
--->-->ExteriorDerivative((d ((ZeroChain) %))): Not documented!!!!
--->-->ExteriorDerivative((d (% a))): Not documented!!!!
--->-->ExteriorDerivative((degree ((Polynomial (Integer)) %))): Not documented!!!!
--->-->ExteriorDerivative(): Missing Description
; compiling file "/var/aw/var/LatexWiki/EXTDF.NRLIB/EXTDF.lsp" (written 02 NOV 2024 02:52:10 AM):

; wrote /var/aw/var/LatexWiki/EXTDF.NRLIB/EXTDF.fasl
; compilation finished in 0:00:00.008
------------------------------------------------------------------------
   ExteriorDerivative is now explicitly exposed in frame initial 
   ExteriorDerivative will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/EXTDF.NRLIB/EXTDF

   HODGE abbreviates domain HodgeStar 
------------------------------------------------------------------------
   initializing NRLIB HODGE for HodgeStar 
   compiling into NRLIB HODGE 
   compiling exported degree : % -> Polynomial Integer
Time: 0 SEC.

   compiling exported hodge : a -> %
      HODGE;hodge;a%;2 is replaced by LIST 
Time: 0 SEC.

   compiling exported mainType : % -> String
      HODGE;mainType;%S;3 is replaced by HodgeStar 
Time: 0 SEC.

   compiling exported coerce : % -> OutputForm
Time: 0 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |HodgeStar| REDEFINED

;;;     ***       |HodgeStar| REDEFINED
Time: 0 SEC.

   Warnings: 
      [1] degree:  arg has no value
      [2] coerce:  arg has no value

   Cumulative Statistics for Constructor HodgeStar
      Time: 0.02 seconds

   finalizing NRLIB HODGE 
   Processing HodgeStar for Browser database:
--->-->HodgeStar(constructor): Not documented!!!!
--->-->HodgeStar((hodge (% a))): Not documented!!!!
--->-->HodgeStar((degree ((Polynomial (Integer)) %))): Not documented!!!!
--->-->HodgeStar(): Missing Description
; compiling file "/var/aw/var/LatexWiki/HODGE.NRLIB/HODGE.lsp" (written 02 NOV 2024 02:52:10 AM):

; wrote /var/aw/var/LatexWiki/HODGE.NRLIB/HODGE.fasl
; compilation finished in 0:00:00.008
------------------------------------------------------------------------
   HodgeStar is now explicitly exposed in frame initial 
   HodgeStar will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/HODGE.NRLIB/HODGE

fricas

f:=f::CoChain(p)

$\label{eq1}f$

(1)

Type: CoChain?(p)

fricas

g:=g::CoChain(q)

$\label{eq2}g$

(2)

Type: CoChain?(q)

fricas

h:=f*g

$\label{eq3}f \otimes g$

(3)

Type: WedgeProduct?(CoChain?(p),CoChain?(q))

fricas

degree h

$\label{eq4}q + p$

(4)

Type: Polynomial(Integer)

fricas

k:=h*f

$\label{eq5}{f \otimes g}\otimes f$

(5)

Type: WedgeProduct?(WedgeProduct?(CoChain?(p),CoChain?(q)),CoChain?(p))

fricas

degree k

$\label{eq6}q +{2 \ p}$

(6)

Type: Polynomial(Integer)

fricas

-- car dom (d f) --> ExteriorDerivative

Type: SExpression?

fricas

-- symbol car dom (d f) = 'ExteriorDerivative::Symbol => ok
degree d f  --> p+1

$\label{eq7}p + 1$

(7)

Type: Polynomial(Integer)

fricas

hodge d h --> *d(f # g)

$\label{eq8}<em>{d{\left(f \otimes g \right)}}$

(8)

Type: HodgeStar?(ExteriorDerivative?(WedgeProduct?(CoChain?(p),CoChain?(q))))

fricas

r:=degree hodge h

$\label{eq9}spacedim - q - p$

(9)

Type: Polynomial(Integer)

fricas

eval(r,[p=7,q=3,'spacedim=15]) --> notice the quote!

$\label{eq10}5$

(10)

Type: Polynomial(Integer)

fricas

-->degree % --> spacedim - q - p - 1

null()$ZeroChain

$\label{eq11}0$

(11)

Type: ZeroChain?

fricas

z:=d d f

$\label{eq12}0$

(12)

Type: ZeroChain?

fricas

z*f

$\label{eq13}0$

(13)

Type: ZeroChain?

fricas

f*z

$\label{eq14}0$

(14)

Type: ZeroChain?

fricas

CoChain(p) has ZeroChainCategory

$\label{eq15} \mbox{\rm false}$

(15)

Type: Boolean

fricas

ZeroChain has ZeroChainCategory

$\label{eq16} \mbox{\rm true}$

(16)

Type: Boolean