Machine-Native ReasoningReading edition

PRIQ: additional mathematical material

Reading tools
Reading library

Saved reading

Read side by side

Loading chapter…
Resources & source
PDF and editable source · Chapter source · About this edition

Let \(q:X_{\mathrm f}\to X_{\mathrm f}/\operatorname{Ker}C\) be the canonical quotient map. Since \(C\) is surjective, there is a unique vector-space isomorphism \[\widetilde C:X_{\mathrm f}/\operatorname{Ker}C\to X_{\mathrm c},\qquad C=\widetilde Cq.\] The multilinear map \(CA_m^{\mathrm f}:X_{\mathrm f}^m\to X_{\mathrm c}\) descends if and only if its value is unchanged when one input is altered by an element of \(\operatorname{Ker}C\). The induced quotient tensor has the coarse space as its target: \[\overline A_m:(X_{\mathrm f}/\operatorname{Ker}C)^m\longrightarrow X_{\mathrm c},\qquad \overline A_m([x_1],\ldots,[x_m])=CA_m^{\mathrm f}(x_1,\ldots,x_m).\] It follows that \[A_m^{\mathrm c}=\overline A_m(\widetilde C^{-1},\ldots,\widetilde C^{-1}).\] There is no additional output factor \(\widetilde C\) in this convention, since \(\overline A_m\) already takes values in \(X_{\mathrm c}\). Equivalently, define the quotient-valued tensor \[\overline B_m([x_1],\ldots,[x_m])=qA_m^{\mathrm f}(x_1,\ldots,x_m).\] The slot-kernel criterion makes this independent of the representatives. Now \(\overline A_m=\widetilde C\overline B_m\), and the alternative correctly typed formula is \[A_m^{\mathrm c}=\widetilde C\overline B_m(\widetilde C^{-1},\ldots,\widetilde C^{-1}).\] This formulation makes Theorem PRIQ.3.1 independent of coordinates and of the chosen right inverse.