{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "9ef0376e",
   "metadata": {},
   "source": [
    "# Highest-Power Coefficient in the EMR Curvature Formula\n",
    "\n",
    "This notebook reproduces the finite-dimensional computation behind\n",
    "Theorem 3.4 of *Diffeomorphism Groups of Circle Bundles over Integral\n",
    "Symplectic Manifolds*.  The program alternates over all permutations\n",
    "and contracts copies of the standard complex structure.\n",
    "\n",
    "The complete research code is available in\n",
    "[EMR-Paper-Computation](https://github.com/egisatoshi/EMR-Paper-Computation).\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d3711f1e",
   "metadata": {},
   "source": [
    "## Standard complex structure\n",
    "\n",
    "On a real vector space of dimension $2k$, let\n",
    "\n",
    "$$\n",
    "J=\\begin{pmatrix}0&I_k\\\\-I_k&0\\end{pmatrix}.\n",
    "$$\n",
    "\n",
    "The notebook uses $k=2$ for a quick interactive calculation.  The\n",
    "final section records the larger computations with exactly the same\n",
    "definitions.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "bcf9489d",
   "metadata": {},
   "outputs": [],
   "source": [
    "def k := 2\n",
    "\n",
    "def J :=\n",
    "  generateTensor\n",
    "    (\\match as list integer with\n",
    "       | [$i, #(i + k)] -> 1\n",
    "       | [$i, #(i - k)] -> -1\n",
    "       | _ -> 0)\n",
    "    [2 * k, 2 * k]\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "ea7fc60c",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "$\\begin{pmatrix} 0 & 0 & 1 & 0 \\\\ 0 & 0 & 0 & 1 \\\\ -1 & 0 & 0 & 0 \\\\ 0 & -1 & 0 & 0 \\\\ \\end{pmatrix}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "J\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "45787b87",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "$\\begin{pmatrix} -1 & 0 & 0 & 0 \\\\ 0 & -1 & 0 & 0 \\\\ 0 & 0 & -1 & 0 \\\\ 0 & 0 & 0 & -1 \\\\ \\end{pmatrix}$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "withSymbols [a, b, c] J_a~c . J_c~b\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "277c0f2d",
   "metadata": {},
   "source": [
    "## Alternating product\n",
    "\n",
    "Let $S_k$ be the signed sum of products\n",
    "\n",
    "$$\n",
    "S_k=\\sum_{\\sigma\\in S_{2k}}\\operatorname{sgn}(\\sigma)\n",
    "    \\prod_{i=1}^{k}J_{\\sigma(2i-1),\\sigma(2i)}.\n",
    "$$\n",
    "\n",
    "`evenAndOddPermutations` supplies the two signs separately.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "75798bdb",
   "metadata": {},
   "outputs": [],
   "source": [
    "def S :=\n",
    "  let (es, os) := evenAndOddPermutations (2 * k) in\n",
    "    sum (map (\\σ -> product (map (\\i -> J_(σ (2 * i - 1))_(σ (2 * i))) (between 1 k))) es) -\n",
    "    sum (map (\\σ -> product (map (\\i -> J_(σ (2 * i - 1))_(σ (2 * i))) (between 1 k))) os)\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "232adb98",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "$-8$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "S\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "40b251a9",
   "metadata": {},
   "source": [
    "## Curvature coefficient\n",
    "\n",
    "The highest power of the bundle parameter $p$ is built from\n",
    "\n",
    "$$\n",
    "T_{abc}{}^d=-J_{bc}J_a{}^d+J_{ac}J_b{}^d\n",
    "             +2J_{ab}J_c{}^d.\n",
    "$$\n",
    "\n",
    "The indices $a_0,\\ldots,a_{k-1}$ form a cyclic chain.  Tensor product\n",
    "followed by `.` contracts that chain, while the outer fold adds the\n",
    "even and odd permutation contributions.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "12a467b0",
   "metadata": {},
   "outputs": [],
   "source": [
    "def T_a_b_c~d :=\n",
    "  -1 * J_b_c . J_a~d +\n",
    "  J_a_c . J_b~d +\n",
    "  2 * J_a_b . J_c~d\n",
    "\n",
    "def S' :=\n",
    "  withSymbols [a]\n",
    "    let (es, os) := evenAndOddPermutations (2 * k) in\n",
    "      (\\xs -> foldl (+) (head xs) (tail xs))\n",
    "        (map\n",
    "          (\\σ ->\n",
    "            (\\xs -> foldl (.) (head xs) (tail xs))\n",
    "              (map (\\i -> T_(σ (2 * i - 1))_(σ (2 * i))_(a_(modulo i k))~(a_(i - 1))) (between 1 k)))\n",
    "          es) -\n",
    "      (\\xs -> foldl (+) (head xs) (tail xs))\n",
    "        (map\n",
    "          (\\σ ->\n",
    "            (\\xs -> foldl (.) (head xs) (tail xs))\n",
    "              (map (\\i -> T_(σ (2 * i - 1))_(σ (2 * i))_(a_(modulo i k))~(a_(i - 1))) (between 1 k)))\n",
    "          os)\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "9649a4a6",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "$192$"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "S'\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ed1338ff",
   "metadata": {},
   "source": [
    "## Higher dimensions\n",
    "\n",
    "The same program gives\n",
    "\n",
    "$$\n",
    "\\begin{array}{c|rr}\n",
    "k&S_k&S'_k\\\\ \\hline\n",
    "2&-8&192\\\\\n",
    "3&-48&0\\\\\n",
    "4&384&61440\n",
    "\\end{array}\n",
    "$$\n",
    "\n",
    "On Egison 5.1.0 the full $k=4$ run takes about 25 minutes.  Keeping\n",
    "the interactive notebook at $k=2$ makes every cell quick to rerun;\n",
    "changing the first definition to `def k := 4` performs the complete\n",
    "Theorem 3.4 computation without any other code changes.\n"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Egison",
   "language": "egison",
   "name": "egison"
  },
  "language_info": {
   "codemirror_mode": "egison",
   "file_extension": ".egi",
   "mimetype": "text/x-egison",
   "name": "egison"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}