Edit detail for SandBoxGrassmannIsometry revision 4 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)

simplifyHat:=rule
  dot(P, Q)^2-dot(P,P)*dot(Q,Q) == hat(P,Q)^2
  -dot(P,Q)^2+dot(P,P)*dot(Q,Q) == -hat(P,Q)^2
  dot(Q,R)*dot(P,R)-dot(R,R)*dot(P,Q) == dot(hat(R,Q),hat(R,P))

(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

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

   (6)

   Type: Matrix(Expression(Integer))
2. Isometry from Trivector
   axiom

   eq44 := matrix [[dot(P, P), dot(P, Q)+a, dot(P, R)+b], _
                   [dot(P, Q)-a, dot(Q, Q), dot(Q, R)+c], _
                   [dot(P, R)-b, dot(Q, R)-c, dot(R, R)]]

   (7)

   Type: Matrix(Expression(Integer))
   axiom

   eq47a := adjoint(eq44);

   Type: Record(adjMat: Matrix(Expression(Integer)),detMat: Expression(Integer))

)set output tex off

)set output algebra on

eq47a.adjMat

   (13)
   [
                                    2    2
     [Q{\cdot}QR{\cdot}R - Q{\cdot}R  + c ,
      (- P{\cdot}Q - a)R{\cdot}R + (P{\cdot}R + b)Q{\cdot}R - cP{\cdot}R -
b c,
      (P{\cdot}Q + a)Q{\cdot}R + (- P{\cdot}R - b)Q{\cdot}Q + cP{\cdot}Q +
a c]
     ,

     [(- P{\cdot}Q + a)R{\cdot}R + (P{\cdot}R - b)Q{\cdot}R + cP{\cdot}R -
b c,
                                    2    2
      P{\cdot}PR{\cdot}R - P{\cdot}R  + b ,

         - P{\cdot}PQ{\cdot}R + (P{\cdot}Q - a)P{\cdot}R + bP{\cdot}Q
       +
         - cP{\cdot}P - a b
       ]
     ,

     [(P{\cdot}Q - a)Q{\cdot}R + (- P{\cdot}R + b)Q{\cdot}Q - cP{\cdot}Q +
a c,

         - P{\cdot}PQ{\cdot}R + (P{\cdot}Q + a)P{\cdot}R - bP{\cdot}Q
       +
         cP{\cdot}P - a b
       ,
                                    2    2
      P{\cdot}PQ{\cdot}Q - P{\cdot}Q  + a ]
     ]

)set output algebra off

)set output tex on

eq47a.detMat

(8)

Simplifications

eq45 := a*R-b*Q+c*P = v

(9)

eq45a := rule
  a*dot(R, R)-b*dot(R, Q)+c*dot(R, P) == dot(R, v)
  a*dot(Q, R)-b*dot(Q, Q)+c*dot(Q, P) == dot(Q, v)
  a*dot(P, R)-b*dot(P, Q)+c*dot(P, P) == dot(P, v)

(10)

eq47b := map(x+->eq45a simplifyHat x,eq47a.adjMat)

(11)

map(x+->x^2,eq45)

(12)

eq47d := rule
  dot(R,R)*a^2 + dot(Q,Q)*b^2 + dot(P,P)*c^2 - _
  2*c*b*dot(P,Q) + 2*a*c*dot(R,P) - 2*a*b*dot(R,Q) == v^2

(13)

eq47d(eq47a.detMat)

(14)