Edit detail for SandBoxGrassmannIsometry revision 3 of 7

Grassmann Algebra Operators

Symmetric inner product

idot:=display(operator('dot,2), (x:List OutputForm):OutputForm +->
hconcat([x.1,_{_\cdot_} ,x.2]));

dot(A:EXPR INT,B:EXPR INT):EXPR INT == (smaller?(A,B)=>idot(A,B);idot(B,A))

   Function declaration dot : (Expression(Integer),Expression(Integer))
       -> Expression(Integer) has been added to workspace.

dot(P, Q)=dot(Q,P)

Compiling function dot with type (Expression(Integer),Expression(
      Integer)) -> Expression(Integer)

(1)

Exterior product

ihat:=display(operator('hat,2), (x:List OutputForm):OutputForm +->
hconcat([x.1,_{_\wedge_} ,x.2]));

hat(A:EXPR INT,B:EXPR INT):EXPR INT == (smaller?(A,B)=>ihat(A,B);-ihat(B,A))

   Function declaration hat : (Expression(Integer),Expression(Integer))
       -> Expression(Integer) has been added to workspace.

hat(P, Q)=-hat(Q,P)

Compiling function hat with type (Expression(Integer),Expression(
      Integer)) -> Expression(Integer)

(2)

1+1

(3)

1. Proof of the main theorem 15 (isometry from bivector)
   axiom

   eq33 := matrix [[-dot(P,P), -dot(P,Q)+c],[dot(Q,P)+c, dot(Q,Q)]]

   (4)

   Type: Matrix(Expression(Integer))
   axiom

   eq35 := inverse(eq33)

   (5)

   Type: Union(Matrix(Expression(Integer)),...)
   axiom

   simplifyHatSquare:=ruleset([rule dot(P, Q)^2-dot(P, P)*dot(Q, Q) == hat(P, Q)^2,rule
   -dot(P, Q)^2+dot(P, P)*dot(Q, Q) == -hat(P, Q)^2])

   (6)

   Type: Ruleset(Integer,Integer,Expression(Integer))
   axiom

   map(x+->simplifyHatSquare(x),eq35)

   (7)

   Type: Matrix(Expression(Integer))