CINXE.COM

<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1 plus MathML 2.0 plus SVG 1.1//EN" "http://www.w3.org/2002/04/xhtml-math-svg/xhtml-math-svg-flat.dtd" > <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title> general covariance in nLab </title> <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /> <meta name="robots" content="index,follow" /> <meta name="viewport" content="width=device-width, initial-scale=1" /> <link href="/stylesheets/instiki.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/mathematics.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/syntax.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/nlab.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link rel="stylesheet" type="text/css" href="https://cdn.jsdelivr.net/gh/dreampulse/computer-modern-web-font@master/fonts.css"/> <style type="text/css"> h1#pageName, div.info, .newWikiWord a, a.existingWikiWord, .newWikiWord a:hover, [actiontype="toggle"]:hover, #TextileHelp h3 { color: #226622; } a:visited.existingWikiWord { color: #164416; } </style> <style type="text/css"><![CDATA[/*></style> <script src="/javascripts/prototype.js?1660229990" type="text/javascript"></script> <script src="/javascripts/effects.js?1660229990" type="text/javascript"></script> <script src="/javascripts/dragdrop.js?1660229990" type="text/javascript"></script> <script src="/javascripts/controls.js?1660229990" type="text/javascript"></script> <script src="/javascripts/application.js?1660229990" type="text/javascript"></script> <script src="/javascripts/page_helper.js?1660229990" type="text/javascript"></script> <script src="/javascripts/thm_numbering.js?1660229990" type="text/javascript"></script> <script type="text/x-mathjax-config"> <![CDATA[//><!]]> </script> <script type="text/javascript"> <![CDATA[//><!]]> </script> <link href="https://ncatlab.org/nlab/atom_with_headlines" rel="alternate" title="Atom with headlines" type="application/atom+xml" /> <link href="https://ncatlab.org/nlab/atom_with_content" rel="alternate" title="Atom with full content" type="application/atom+xml" /> <script type="text/javascript"> document.observe("dom:loaded", function() { generateThmNumbers(); }); </script> </head> <body> <div id="Container"> <div id="Content"> <h1 id="pageName"> <span style="float: left; margin: 0.5em 0.25em -0.25em 0"> <svg xmlns="http://www.w3.org/2000/svg" width="1.872em" height="1.8em" viewBox="0 0 190 181"> <path fill="#226622" d="M72.8 145c-1.6 17.3-15.7 10-23.6 20.2-5.6 7.3 4.8 15 11.4 15 11.5-.2 19-13.4 26.4-20.3 3.3-3 8.2-4 11.2-7.2a14 14 0 0 0 2.9-11.1c-1.4-9.6-12.4-18.6-16.9-27.2-5-9.6-10.7-27.4-24.1-27.7-17.4-.3-.4 26 4.7 30.7 2.4 2.3 5.4 4.1 7.3 6.9 1.6 2.3 2.1 5.8-1 7.2-5.9 2.6-12.4-6.3-15.5-10-8.8-10.6-15.5-23-26.2-31.8-5.2-4.3-11.8-8-18-3.7-7.3 4.9-4.2 12.9.2 18.5a81 81 0 0 0 30.7 23c3.3 1.5 12.8 5.6 10 10.7-2.5 5.2-11.7 3-15.6 1.1-8.4-3.8-24.3-21.3-34.4-13.7-3.5 2.6-2.3 7.6-1.2 11.1 2.8 9 12.2 17.2 20.9 20.5 17.3 6.7 34.3-8 50.8-12.1z"/> <path fill="#a41e32" d="M145.9 121.3c-.2-7.5 0-19.6-4.5-26-5.4-7.5-12.9-1-14.1 5.8-1.4 7.8 2.7 14.1 4.8 21.3 3.4 12 5.8 29-.8 40.1-3.6-6.7-5.2-13-7-20.4-2.1-8.2-12.8-13.2-15.1-1.9-2 9.7 9 21.2 12 30.1 1.2 4 2 8.8 6.4 10.3 6.9 2.3 13.3-4.7 17.7-8.8 12.2-11.5 36.6-20.7 43.4-36.4 6.7-15.7-13.7-14-21.3-7.2-9.1 8-11.9 20.5-23.6 25.1 7.5-23.7 31.8-37.6 38.4-61.4 2-7.3-.8-29.6-13-19.8-14.5 11.6-6.6 37.6-23.3 49.2z"/> <path fill="#193c78" d="M86.3 47.5c0-13-10.2-27.6-5.8-40.4 2.8-8.4 14.1-10.1 17-1 3.8 11.6-.3 26.3-1.8 38 11.7-.7 10.5-16 14.8-24.3 2.1-4.2 5.7-9.1 11-6.7 6 2.7 7.4 9.2 6.6 15.1-2.2 14-12.2 18.8-22.4 27-3.4 2.7-8 6.6-5.9 11.6 2 4.4 7 4.5 10.7 2.8 7.4-3.3 13.4-16.5 21.7-16 14.6.7 12 21.9.9 26.2-5 1.9-10.2 2.3-15.2 3.9-5.8 1.8-9.4 8.7-15.7 8.9-6.1.1-9-6.9-14.3-9-14.4-6-33.3-2-44.7-14.7-3.7-4.2-9.6-12-4.9-17.4 9.3-10.7 28 7.2 35.7 12 2 1.1 11 6.9 11.4 1.1.4-5.2-10-8.2-13.5-10-11.1-5.2-30-15.3-35-27.3-2.5-6 2.8-13.8 9.4-13.6 6.9.2 13.4 7 17.5 12C70.9 34 75 43.8 86.3 47.4z"/> </svg> </span> <span class="webName">nLab</span> general covariance </h1> <div class="navigation"> <span class="skipNav"><a href='#navEnd'>Skip the Navigation Links</a> | </span> <span style="display:inline-block; width: 0.3em;"></span> <a href="/nlab/show/HomePage" accesskey="H" title="Home page">Home Page</a> | <a href="/nlab/all_pages" accesskey="A" title="List of all pages">All Pages</a> | <a href="/nlab/latest_revisions" accesskey="U" title="Latest edits and page creations">Latest Revisions</a> | <a href="https://nforum.ncatlab.org/discussion/4199/#Item_27" title="Discuss this page in its dedicated thread on the nForum" style="color: black">Discuss this page</a> | <form accept-charset="utf-8" action="/nlab/search" id="navigationSearchForm" method="get"> <fieldset class="search"><input type="text" id="searchField" name="query" value="Search" style="display:inline-block; float: left;" onfocus="this.value == 'Search' ? this.value = '' : true" onblur="this.value == '' ? this.value = 'Search' : true" /></fieldset> </form> <span id='navEnd'></span> </div> <div id="revision"> <html xmlns="http://www.w3.org/1999/xhtml" xmlns:svg="http://www.w3.org/2000/svg" xml:lang="en" lang="en"> <head><meta http-equiv="Content-type" content="application/xhtml+xml;charset=utf-8" /><title>Contents</title></head> <body> <div class="rightHandSide"> <div class="toc clickDown" tabindex="0"> <h3 id="context">Context</h3> <h4 id="physics">Physics</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/physics">physics</a></strong>, <a class="existingWikiWord" href="/nlab/show/mathematical+physics">mathematical physics</a>, <a class="existingWikiWord" href="/nlab/show/philosophy+of+physics">philosophy of physics</a></p> <h2 id="surveys_textbooks_and_lecture_notes">Surveys, textbooks and lecture notes</h2> <ul> <li> <p><em><a class="existingWikiWord" href="/nlab/show/higher+category+theory+and+physics">(higher) category theory and physics</a></em></p> </li> <li> <p><em><a class="existingWikiWord" href="/nlab/show/geometry+of+physics">geometry of physics</a></em></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/books+and+reviews+in+mathematical+physics">books and reviews</a>, <a class="existingWikiWord" href="/nlab/show/physics+resources">physics resources</a></p> </li> </ul> <hr /> <p><a class="existingWikiWord" href="/nlab/show/theory+%28physics%29">theory (physics)</a>, <a class="existingWikiWord" href="/nlab/show/model+%28physics%29">model (physics)</a></p> <p><a class="existingWikiWord" href="/nlab/show/experiment">experiment</a>, <a class="existingWikiWord" href="/nlab/show/measurement">measurement</a>, <a class="existingWikiWord" href="/nlab/show/computable+physics">computable physics</a></p> <ul> <li> <p><strong><a class="existingWikiWord" href="/nlab/show/mechanics">mechanics</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/mass">mass</a>, <a class="existingWikiWord" href="/nlab/show/charge">charge</a>, <a class="existingWikiWord" href="/nlab/show/momentum">momentum</a>, <a class="existingWikiWord" href="/nlab/show/angular+momentum">angular momentum</a>, <a class="existingWikiWord" href="/nlab/show/moment+of+inertia">moment of inertia</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/dynamics+on+Lie+groups">dynamics on Lie groups</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/rigid+body+dynamics">rigid body dynamics</a></li> </ul> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/field+%28physics%29">field (physics)</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Lagrangian+mechanics">Lagrangian mechanics</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/configuration+space">configuration space</a>, <a class="existingWikiWord" href="/nlab/show/state">state</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/action+functional">action functional</a>, <a class="existingWikiWord" href="/nlab/show/Lagrangian">Lagrangian</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/covariant+phase+space">covariant phase space</a>, <a class="existingWikiWord" href="/nlab/show/Euler-Lagrange+equations">Euler-Lagrange equations</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Hamiltonian+mechanics">Hamiltonian mechanics</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/phase+space">phase space</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/symplectic+geometry">symplectic geometry</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Poisson+manifold">Poisson manifold</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/symplectic+manifold">symplectic manifold</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/symplectic+groupoid">symplectic groupoid</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/multisymplectic+geometry">multisymplectic geometry</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/n-symplectic+manifold">n-symplectic manifold</a></li> </ul> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/spacetime">spacetime</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/smooth+Lorentzian+manifold">smooth Lorentzian manifold</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/special+relativity">special relativity</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/general+relativity">general relativity</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/gravity">gravity</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/supergravity">supergravity</a>, <a class="existingWikiWord" href="/nlab/show/dilaton+gravity">dilaton gravity</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/black+hole">black hole</a></p> </li> </ul> </li> </ul> </li> </ul> </li> <li> <p><strong><a class="existingWikiWord" href="/nlab/show/classical+field+theory">Classical field theory</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/classical+physics">classical physics</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/classical+mechanics">classical mechanics</a></li> <li><a class="existingWikiWord" href="/nlab/show/waves">waves</a> and <a class="existingWikiWord" href="/nlab/show/optics">optics</a></li> <li><a class="existingWikiWord" href="/nlab/show/thermodynamics">thermodynamics</a></li> </ul> </li> </ul> </li> <li> <p><strong><a class="existingWikiWord" href="/nlab/show/quantum+mechanics">Quantum Mechanics</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/quantum+mechanics+in+terms+of+dagger-compact+categories">in terms of ∞-compact categories</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/quantum+information">quantum information</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Hamiltonian+operator">Hamiltonian operator</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/density+matrix">density matrix</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Kochen-Specker+theorem">Kochen-Specker theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Bell%27s+theorem">Bell's theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Gleason%27s+theorem">Gleason's theorem</a></p> </li> </ul> </li> <li> <p><strong><a class="existingWikiWord" href="/nlab/show/quantization">Quantization</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/geometric+quantization">geometric quantization</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/deformation+quantization">deformation quantization</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/path+integral">path integral quantization</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/semiclassical+approximation">semiclassical approximation</a></p> </li> </ul> </li> <li> <p><strong><a class="existingWikiWord" href="/nlab/show/quantum+field+theory">Quantum Field Theory</a></strong></p> <ul> <li> <p>Axiomatizations</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/AQFT">algebraic QFT</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Wightman+axioms">Wightman axioms</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Haag-Kastler+axioms">Haag-Kastler axioms</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/operator+algebra">operator algebra</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/local+net">local net</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/conformal+net">conformal net</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Reeh-Schlieder+theorem">Reeh-Schlieder theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Osterwalder-Schrader+theorem">Osterwalder-Schrader theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/PCT+theorem">PCT theorem</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Bisognano-Wichmann+theorem">Bisognano-Wichmann theorem</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/modular+theory">modular theory</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/spin-statistics+theorem">spin-statistics theorem</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/boson">boson</a>, <a class="existingWikiWord" href="/nlab/show/fermion">fermion</a></li> </ul> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/FQFT">functorial QFT</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/cobordism">cobordism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2Cn%29-category+of+cobordisms">(∞,n)-category of cobordisms</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/cobordism+hypothesis">cobordism hypothesis</a>-theorem</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/extended+topological+quantum+field+theory">extended topological quantum field theory</a></p> </li> </ul> </li> </ul> </li> <li> <p>Tools</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/perturbative+quantum+field+theory">perturbative quantum field theory</a>, <a class="existingWikiWord" href="/nlab/show/vacuum">vacuum</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/effective+quantum+field+theory">effective quantum field theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/renormalization">renormalization</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/BV-BRST+formalism">BV-BRST formalism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/geometric+%E2%88%9E-function+theory">geometric ∞-function theory</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/particle+physics">particle physics</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/phenomenology">phenomenology</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/model+%28in+particle+phyiscs%29">models</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/standard+model+of+particle+physics">standard model of particle physics</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/fields+and+quanta+-+table">fields and quanta</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/GUT">Grand Unified Theories</a>, <a class="existingWikiWord" href="/nlab/show/MSSM">MSSM</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/scattering+amplitude">scattering amplitude</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/on-shell+recursion">on-shell recursion</a>, <a class="existingWikiWord" href="/nlab/show/KLT+relations">KLT relations</a></li> </ul> </li> </ul> </li> <li> <p>Structural phenomena</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/universality+class">universality class</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/quantum+anomaly">quantum anomaly</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Green-Schwarz+mechanism">Green-Schwarz mechanism</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/instanton">instanton</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/spontaneously+broken+symmetry">spontaneously broken symmetry</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Kaluza-Klein+mechanism">Kaluza-Klein mechanism</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/integrable+systems">integrable systems</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/holonomic+quantum+fields">holonomic quantum fields</a></p> </li> </ul> </li> <li> <p>Types of quantum field thories</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/TQFT">TQFT</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/2d+TQFT">2d TQFT</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Dijkgraaf-Witten+theory">Dijkgraaf-Witten theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Chern-Simons+theory">Chern-Simons theory</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/TCFT">TCFT</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/A-model">A-model</a>, <a class="existingWikiWord" href="/nlab/show/B-model">B-model</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homological+mirror+symmetry">homological mirror symmetry</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/QFT+with+defects">QFT with defects</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/conformal+field+theory">conformal field theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%281%2C1%29-dimensional+Euclidean+field+theories+and+K-theory">(1,1)-dimensional Euclidean field theories and K-theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/%282%2C1%29-dimensional+Euclidean+field+theory">(2,1)-dimensional Euclidean field theory and elliptic cohomology</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/CFT">CFT</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/WZW+model">WZW model</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/6d+%282%2C0%29-supersymmetric+QFT">6d (2,0)-supersymmetric QFT</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/gauge+theory">gauge theory</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/field+strength">field strength</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/gauge+group">gauge group</a>, <a class="existingWikiWord" href="/nlab/show/gauge+transformation">gauge transformation</a>, <a class="existingWikiWord" href="/nlab/show/gauge+fixing">gauge fixing</a></p> </li> <li> <p>examples</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/electromagnetic+field">electromagnetic field</a>, <a class="existingWikiWord" href="/nlab/show/QED">QED</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/electric+charge">electric charge</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/magnetic+charge">magnetic charge</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Yang-Mills+field">Yang-Mills field</a>, <a class="existingWikiWord" href="/nlab/show/QCD">QCD</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Yang-Mills+theory">Yang-Mills theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/spinors+in+Yang-Mills+theory">spinors in Yang-Mills theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/topological+Yang-Mills+theory">topological Yang-Mills theory</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Kalb-Ramond+field">Kalb-Ramond field</a></li> <li><a class="existingWikiWord" href="/nlab/show/supergravity+C-field">supergravity C-field</a></li> <li><a class="existingWikiWord" href="/nlab/show/RR+field">RR field</a></li> <li><a class="existingWikiWord" href="/nlab/show/first-order+formulation+of+gravity">first-order formulation of gravity</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/general+covariance">general covariance</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/supergravity">supergravity</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/D%27Auria-Fre+formulation+of+supergravity">D'Auria-Fre formulation of supergravity</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/gravity+as+a+BF-theory">gravity as a BF-theory</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/sigma-model">sigma-model</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/particle">particle</a>, <a class="existingWikiWord" href="/nlab/show/relativistic+particle">relativistic particle</a>, <a class="existingWikiWord" href="/nlab/show/fundamental+particle">fundamental particle</a>, <a class="existingWikiWord" href="/nlab/show/spinning+particle">spinning particle</a>, <a class="existingWikiWord" href="/nlab/show/superparticle">superparticle</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/string">string</a>, <a class="existingWikiWord" href="/nlab/show/spinning+string">spinning string</a>, <a class="existingWikiWord" href="/nlab/show/superstring">superstring</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/membrane">membrane</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/AKSZ+theory">AKSZ theory</a></p> </li> </ul> </li> </ul> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/string+theory">String Theory</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/string+theory+results+applied+elsewhere">string theory results applied elsewhere</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/number+theory+and+physics">number theory and physics</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Riemann+hypothesis+and+physics">Riemann hypothesis and physics</a></li> </ul> </li> </ul> <div> <p> <a href="/nlab/edit/physicscontents">Edit this sidebar</a> </p> </div></div></div> </div> </div> <h1 id="contents">Contents</h1> <div class='maruku_toc'> <ul> <li><a href='#Idea'>Idea</a></li> <li><a href='#HistoryAndOriginalFormulation'>History and original formulation</a></li> <li><a href='#ModernFormulationInDifferentialGeometry'>Modern formulation in differential geometry</a></li> <ul> <li><a href='#in_gravity'>In gravity</a></li> <li><a href='#RelationToPrincipleOfEquivalenceInGravity'>Relation to the “principle of equivalence” in gravity</a></li> <li><a href='#in_other_topological_field_theories'>In other topological field theories</a></li> </ul> <li><a href='#InHomotopyTypeTheory'>Formalization in homotopy type theory</a></li> <ul> <li><a href='#InformalIntroduction'>Informal introduction</a></li> <li><a href='#introduction_in_terms_of_type_theory'>Introduction in terms of type theory</a></li> <li><a href='#the_ambient_theory'>The ambient theory</a></li> <li><a href='#the_diffeomorphism_group'>The diffeomorphism group</a></li> <li><a href='#the_context_of_general_covariance'>The context of general covariance</a></li> <li><a href='#generally_covariant_field_configuration_spaces'>Generally covariant field configuration spaces</a></li> <li><a href='#GravityInHoTT'>Generally covariant field of gravity</a></li> </ul> <li><a href='#References'>References</a></li> <ul> <li><a href='#ReferencesHistory'>History</a></li> <li><a href='#ReferencesFormalizations'>Formalizations of general covariance</a></li> <li><a href='#FormalizationInHomtopyTypeTheory'>Formalization in homotopy type theory</a></li> </ul> </ul> </div> <h2 id="Idea">Idea</h2> <p>In <a class="existingWikiWord" href="/nlab/show/physics">physics</a>, the term <em>general covariance</em> is meant to indicate the property of a <a class="existingWikiWord" href="/nlab/show/physical+system">physical system</a> or <a class="existingWikiWord" href="/nlab/show/model+%28in+theoretical+physics%29">model (in theoretical physics)</a> whose <a class="existingWikiWord" href="/nlab/show/configuration+space">configurations</a>, <a class="existingWikiWord" href="/nlab/show/action+functional">action functional</a> and <a class="existingWikiWord" href="/nlab/show/equations+of+motion">equations of motion</a> are all <a class="existingWikiWord" href="/nlab/show/equivariance">equivariant</a> under the <a class="existingWikiWord" href="/nlab/show/action">action</a> of the <a class="existingWikiWord" href="/nlab/show/diffeomorphism+group">diffeomorphism group</a> on the <a class="existingWikiWord" href="/nlab/show/smooth+manifold">smooth manifold</a> underlying the <a class="existingWikiWord" href="/nlab/show/spacetime">spacetime</a> or the <a class="existingWikiWord" href="/nlab/show/worldvolume">worldvolume</a> of the system. Here “covariance” is as in “<a class="existingWikiWord" href="/nlab/show/covariant+tensor">covariant tensor</a>” another term for behaviour under diffeomorphisms.</p> <p>The term <em><a class="existingWikiWord" href="/nlab/show/general+relativity">general relativity</a></em> for <a class="existingWikiWord" href="/nlab/show/Einstein">Einstein</a>-<a class="existingWikiWord" href="/nlab/show/gravity">gravity</a> originates in at least closely related ideas (see <em><a href="#HistoryAndOriginalFormulation">History and original formulation</a></em> below), and Einstein-gravity is the archtypical example of a generally covariant physical system:</p> <p>here, the <a class="existingWikiWord" href="/nlab/show/configuration+space">configuration space</a> of physical fields over a <a class="existingWikiWord" href="/nlab/show/smooth+manifold">smooth manifold</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> is not quite the space of <a class="existingWikiWord" href="/nlab/show/Riemannian+metrics">Riemannian metrics</a> on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> itself, but is the <a class="existingWikiWord" href="/nlab/show/quotient">quotient</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mi>Σ</mi><mo>,</mo><mstyle mathvariant="bold"><mi>Fields</mi></mstyle><mo stretchy="false">]</mo><mo stretchy="false">/</mo><mstyle mathvariant="bold"><mi>Diff</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">[\Sigma,\mathbf{Fields}]/\mathbf{Diff}(\Sigma)</annotation></semantics></math> of this space by the <a class="existingWikiWord" href="/nlab/show/action">action</a> of the <a class="existingWikiWord" href="/nlab/show/diffeomorphism+group">diffeomorphism group</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Diff</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{Diff}(\Sigma)</annotation></semantics></math>: two Riemannian metrics <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>g</mi> <mn>1</mn></msub></mrow><annotation encoding="application/x-tex">g_1</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>g</mi> <mn>2</mn></msub></mrow><annotation encoding="application/x-tex">g_2</annotation></semantics></math> on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> represent the same field of <a class="existingWikiWord" href="/nlab/show/gravity">gravity</a> on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> if there is a <a class="existingWikiWord" href="/nlab/show/diffeomorphism">diffeomorphism</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>Σ</mi><mover><mo>→</mo><mo>≃</mo></mover><mi>Σ</mi></mrow><annotation encoding="application/x-tex">f : \Sigma \stackrel{\simeq}{\to} \Sigma</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>g</mi> <mn>2</mn></msub><mo>=</mo><msup><mi>f</mi> <mo>*</mo></msup><msub><mi>g</mi> <mn>1</mn></msub></mrow><annotation encoding="application/x-tex">g_2 = f^* g_1</annotation></semantics></math>.</p> <p>Or rather, such a diffeomorphism is a <a class="existingWikiWord" href="/nlab/show/gauge+transformation">gauge transformation</a> between the two field configurations. The configuration space is not the naive <a class="existingWikiWord" href="/nlab/show/quotient">quotient</a> of fields by diffeomorphisms as above, but is the <a class="existingWikiWord" href="/nlab/show/homotopy+quotient">homotopy quotient</a>, or <em><a class="existingWikiWord" href="/nlab/show/action+groupoid">action groupoid</a></em>, denoted <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mi>Σ</mi><mo>,</mo><mstyle mathvariant="bold"><mi>Fields</mi></mstyle><mo stretchy="false">]</mo><mo>⫽</mo><mstyle mathvariant="bold"><mi>Diff</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">[\Sigma,\mathbf{Fields}]\sslash \mathbf{Diff}(\Sigma)</annotation></semantics></math>. In the physics literature this action groupoid is most familiar in its <a class="existingWikiWord" href="/nlab/show/infinitesimal+cohesion">infinitesimal approximation</a>, the corresponding <a class="existingWikiWord" href="/nlab/show/Lie+algebroid">Lie algebroid</a>, whose formal dual is a <a class="existingWikiWord" href="/nlab/show/BRST+complex">BRST complex</a> whose degree-1 elements are accordingly called the <em>diffeomorphism ghosts</em> (see there).</p> <p>As with all <a class="existingWikiWord" href="/nlab/show/gauge+transformations">gauge transformations</a>, they relate physical configurations which may be nominally different, but <a class="existingWikiWord" href="/nlab/show/equivalence">equivalent</a>. Therefore <em>general covariance</em> is an instance of the general <em><a class="existingWikiWord" href="/nlab/show/principle+of+equivalence">principle of equivalence</a></em> in mathematics which says that sensible statements about <a class="existingWikiWord" href="/nlab/show/objects">objects</a> must respect the <a class="existingWikiWord" href="/nlab/show/isomorphisms">isomorphisms</a> and more general <a class="existingWikiWord" href="/nlab/show/equivalences">equivalences</a> between these objects.</p> <p>A physical system which is not generally covariant in this sense is hence one where the <a class="existingWikiWord" href="/nlab/show/smooth+manifold">smooth manifold</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> as above, underlying <a class="existingWikiWord" href="/nlab/show/spacetime">spacetime</a>/<a class="existingWikiWord" href="/nlab/show/worldvolume">worldvolume</a> is not regarded as modelling an absolute physical system (such as the <a class="existingWikiWord" href="/nlab/show/observable+universe">observable universe</a> in gravity), but a <a class="existingWikiWord" href="/nlab/show/subsystem">subsystem</a> that is equipped with ambient <a class="existingWikiWord" href="/nlab/show/structure">structure</a> that <a class="existingWikiWord" href="/nlab/show/spontaneous+symmetry+breaking">breaks</a> the diffeomorphism symmetry. Notably systems like <a class="existingWikiWord" href="/nlab/show/electromagnetism">electromagnetism</a> or <a class="existingWikiWord" href="/nlab/show/Yang-Mills+theory">Yang-Mills theory</a> have traditionally been written in a non-generally covariant form describing gauge fields on a fixed gravitational background, as for instance the space inhabited by a particle accelerator. This ambient structure on the spacetime <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> breaks its general diffeomorphism invariance and hence the effective resulting theory on this background is not generally covariant (a special case of the general phenomenon of <a class="existingWikiWord" href="/nlab/show/spontaneous+symmetry+breaking">spontaneous symmetry breaking</a>).</p> <p>On the other hand, such a model consisting of background (e.g. the particle accelerator) and quantum fields propagating in it is ultimately to be understood as an approximation to a more encompassing model in which also the background is dynamical, and which is again generally covariant. Specific for electromagnetism and Yang-Mills theory this refined generally covariant model is known as <em><a class="existingWikiWord" href="/nlab/show/Einstein-Maxwell+theory">Einstein-Maxwell theory</a></em> or more generally <em><a class="existingWikiWord" href="/nlab/show/Einstein-Yang-Mills+theory">Einstein-Yang-Mills theory</a></em>.</p> <p>The idea of general covariance has a long and convoluted history and the literature witnesses plenty of disagreement about how to interpret and formalize it in technical detail (<a href="#Norton">Norton</a>). Already early arguments by <a class="existingWikiWord" href="/nlab/show/Einstein">Einstein</a> himself (e.g. the “<a class="existingWikiWord" href="/nlab/show/hole+paradox">hole paradox</a>” (<a href="#EinsteinGrossmann">Einstein-Grossmann</a>)) show that the discussion has suffered from the beginning from lack of the basic <a class="existingWikiWord" href="/nlab/show/category+theory">category theoretic</a> concept of <a class="existingWikiWord" href="/nlab/show/isomorphism">isomorphism</a> in the <a class="existingWikiWord" href="/nlab/show/category">category</a> <a class="existingWikiWord" href="/nlab/show/Diff">Diff</a> of <a class="existingWikiWord" href="/nlab/show/smooth+manifolds">smooth manifolds</a>. Below in <em><a href="#InHomotopyTypeTheory">Formalization in homotopy type theory</a></em> we indicate a formalization of general covariance that is general, fundamental, and accurately reflects the role of the term in theoretical physics.</p> <h2 id="HistoryAndOriginalFormulation">History and original formulation</h2> <blockquote> <p>The question of general covariance of physical theories in space and time can be traced back to the famous debate between <a class="existingWikiWord" href="/nlab/show/Gottfried+Wilhelm+Leibniz">Gottfried Wilhelm Leibniz</a> and <a class="existingWikiWord" href="/nlab/show/Samuel+Clarke">Samuel Clarke</a> (the latter assisted by Sir <a class="existingWikiWord" href="/nlab/show/Isaac+Newton">Isaac Newton</a>) on the <a class="existingWikiWord" href="/nlab/show/ontology">ontological</a> status of space in the years 1715–1716 (<a href="#Alexander">Alexander</a>), the central question being if space exists as a substance or as an absolute being and absolute motion is present (Clarke) or if it is constituted only in relation to co-existent things allowing for relativism in motions only (Leibniz). This kind of problems also played an important role when the general theory of relativity was being developed in the years around 1910. While <a class="existingWikiWord" href="/nlab/show/Albert+Einstein">Albert Einstein</a> first characterized generally covariant field equations as inadmissible since they did not determine the <a class="existingWikiWord" href="/nlab/show/Riemannian+metric">metric field</a> uniquely as shown in the hole argument ( <em>Lochbetrachtung</em> ) in the appendix of (<a href="#EinsteinGrossmann">Einstein-Grossmann</a>), he later accepted (<a href="#Einstein1916">Einstein 1916</a>) that all <a class="existingWikiWord" href="/nlab/show/physical+laws">physical laws</a> had to be expressed by <a class="existingWikiWord" href="/nlab/show/equations">equations</a> that are valid in all <a class="existingWikiWord" href="/nlab/show/coordinate+systems">coordinate systems</a>, i. e., which are covariant (generally covariant) under arbitrary <a class="existingWikiWord" href="/nlab/show/substitution">substitutions</a>.</p> <blockquote> <p><em>Die allgemeinen Naturgesetze sind durch Gleichungen auszudrücken, die für alle Koordinatensysteme gelten, d. h. die beliebigen Substitutionen gegenüber kovariant (allgemein kovariant) sind.</em> (<a href="#Einstein1916">Einstein 1916 p. 776</a>)</p> </blockquote> <p>The hole argument was dismissed by the reasoning that it is not the <a class="existingWikiWord" href="/nlab/show/spacetime">spacetime</a> <a class="existingWikiWord" href="/nlab/show/Riemannian+metric">metric</a> that has to be fixed uniquely by the <a class="existingWikiWord" href="/nlab/show/equations+of+motion">field equations</a>, but only the physical phenomena that occur in spacetime need to be given a unique expression with reference to any description of spacetime. All physical statements are given in terms of spacetime coincidences; <a class="existingWikiWord" href="/nlab/show/measurement">measurements</a> result in statements on meetings of material points of the measuring rods with other material points or in coincidences between watch hands and points on the clockface. The introduction of a reference system merely serves the easy description of the totality of all these coincidences (point-coincidence argument) (<a href="#Einstein1916">Einstein 1916 p. 776f</a>).</p> <p>from (<a href="#BrunettiPorrmannRuzzi">Brunetti-Pormann-Ruzzi</a>)</p> </blockquote> <h2 id="ModernFormulationInDifferentialGeometry">Modern formulation in differential geometry</h2> <p>We discuss the modern formulation of general covariance in <a class="existingWikiWord" href="/nlab/show/differential+geometry">differential geometry</a>.</p> <h3 id="in_gravity">In gravity</h3> <p>Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi><mo>∈</mo></mrow><annotation encoding="application/x-tex">\Sigma \in </annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/SmoothMfd">SmoothMfd</a> be a <a class="existingWikiWord" href="/nlab/show/smooth+manifold">smooth manifold</a>. Write <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Riem</mi><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Riem(\Sigma)</annotation></semantics></math> for the space of (<a class="existingWikiWord" href="/nlab/show/pseudo-Riemannian+metric">pseudo</a>-)<a class="existingWikiWord" href="/nlab/show/Riemannian+metrics">Riemannian metrics</a> on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math>. For <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>Σ</mi><mo>→</mo><mi>Σ</mi></mrow><annotation encoding="application/x-tex">f : \Sigma \to \Sigma</annotation></semantics></math> a <a class="existingWikiWord" href="/nlab/show/diffeomorphism">diffeomorphism</a>, there is a <a class="existingWikiWord" href="/nlab/show/function">function</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>f</mi> <mo>*</mo></msup><mo>:</mo><mi>Riem</mi><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo>→</mo><mi>Riem</mi><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f^* : Riem(\Sigma) \to Riem(\Sigma)</annotation></semantics></math> which sends a Riemannian metric to its pullback:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><msup><mi>f</mi> <mo>*</mo></msup><mi>g</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>v</mi><mo>,</mo><mi>w</mi><mo stretchy="false">)</mo><mo>≔</mo><mi>g</mi><mo stretchy="false">(</mo><msub><mi>f</mi> <mo>*</mo></msub><mi>v</mi><mo>,</mo><msub><mi>f</mi> <mo>*</mo></msub><mi>w</mi><mo stretchy="false">)</mo><mspace width="thinmathspace"></mspace><mo>,</mo></mrow><annotation encoding="application/x-tex"> (f^*g)(v,w) \coloneqq g(f_* v, f_* w) \,, </annotation></semantics></math></div> <p>where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>f</mi> <mo>*</mo></msub><mo>:</mo><mi>T</mi><mi>Σ</mi><mo>→</mo><mi>T</mi><mi>Σ</mi></mrow><annotation encoding="application/x-tex">f_* : T\Sigma \to T\Sigma</annotation></semantics></math> is the canonical map induced on the <a class="existingWikiWord" href="/nlab/show/tangent+bundle">tangent bundle</a> (see at <em><a class="existingWikiWord" href="/nlab/show/derivative">derivative</a></em>).</p> <p>Say that two metrics <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>g</mi> <mn>1</mn></msub><mo>,</mo><msub><mi>g</mi> <mn>2</mn></msub></mrow><annotation encoding="application/x-tex">g_1, g_2</annotation></semantics></math> are <a class="existingWikiWord" href="/nlab/show/gauge+transformation">gauge equivalent</a> if there is a diffeomorphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi></mrow><annotation encoding="application/x-tex">f</annotation></semantics></math> such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>g</mi> <mn>2</mn></msub><mo>=</mo><msup><mi>f</mi> <mo>*</mo></msup><msub><mi>g</mi> <mn>1</mn></msub></mrow><annotation encoding="application/x-tex">g_2 = f^* g_1</annotation></semantics></math>. This is an <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a>. Write <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Riem</mi><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo stretchy="false">/</mo><mi>Diff</mi><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Riem(\Sigma)/Diff(\Sigma)</annotation></semantics></math> for the corresponding set of <a class="existingWikiWord" href="/nlab/show/equivalence+classes">equivalence classes</a>.</p> <p>The statement of <em>general covariance</em> is that the distinct configurations of the gravitational field form the set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Riem</mi><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo stretchy="false">/</mo><mi>Diff</mi><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Riem(\Sigma)/Diff(\Sigma)</annotation></semantics></math>. In particular, if <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> is <a class="existingWikiWord" href="/nlab/show/compact+topological+space">compact</a>, then the <a class="existingWikiWord" href="/nlab/show/Einstein-Hilbert+action">Einstein-Hilbert action</a> functional which <em>a priori</em> is defined on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Riem</mi><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Riem(\Sigma)</annotation></semantics></math> descends to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Riem</mi><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo stretchy="false">/</mo><mi>Diff</mi><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Riem(\Sigma)/Diff(\Sigma)</annotation></semantics></math></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi>S</mi> <mi>EH</mi></msub><mo>:</mo><mi>Riem</mi><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo stretchy="false">/</mo><mi>Diff</mi><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo>→</mo><mi>ℝ</mi><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> S_{EH} : Riem(\Sigma)/Diff(\Sigma) \to \mathbb{R} \,. </annotation></semantics></math></div> <p>While this captures the idea of general covariance accurately, for further development of the theory of <a class="existingWikiWord" href="/nlab/show/gravity">gravity</a>, however, the set <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Riem</mi><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo stretchy="false">/</mo><mi>Diff</mi><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Riem(\Sigma)/Diff(\Sigma)</annotation></semantics></math> needs to be refined. It is really equipped with the structure of a <a class="existingWikiWord" href="/nlab/show/smooth+space">smooth space</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Riem</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo stretchy="false">/</mo><mstyle mathvariant="bold"><mi>Diff</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{Riem}(\Sigma)/\mathbf{Diff}(\Sigma)</annotation></semantics></math> (in order to perform <a class="existingWikiWord" href="/nlab/show/variational+calculus">variational calculus</a> and hence derive the <a class="existingWikiWord" href="/nlab/show/equations+of+motion">equations of motion</a> of the theory), and second it is to be refined to a <a class="existingWikiWord" href="/nlab/show/smooth+infinity-groupoid">smooth groupoid</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Riem</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo>⫽</mo><mstyle mathvariant="bold"><mi>Diff</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{Riem}(\Sigma)\sslash\mathbf{Diff}(\Sigma)</annotation></semantics></math>.</p> <p>Finally, for setups that admit to introduce <a class="existingWikiWord" href="/nlab/show/fermions">fermions</a>/<a class="existingWikiWord" href="/nlab/show/spinors">spinors</a> into the model one needs to refine Riemannian metrics to <a class="existingWikiWord" href="/nlab/show/vielbein">vielbein</a> fields/<a class="existingWikiWord" href="/nlab/show/orthogonal+structures">orthogonal structures</a>. The fully refined generally covariance smooth configuration groupoid is then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mi>Σ</mi><mo>,</mo><mstyle mathvariant="bold"><mi>orth</mi></mstyle><mo stretchy="false">]</mo><mo>⫽</mo><mstyle mathvariant="bold"><mi>Diff</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">[\Sigma, \mathbf{orth}]\sslash \mathbf{Diff}(\Sigma)</annotation></semantics></math>, discussed in more detail <a href="#GravityInHoTT">below</a>.</p> <h3 id="RelationToPrincipleOfEquivalenceInGravity">Relation to the “principle of equivalence” in gravity</h3> <p>The <em><a class="existingWikiWord" href="/nlab/show/equivalence+principle+%28physics%29">principle of equivalence</a></em> in <a class="existingWikiWord" href="/nlab/show/general+relativity">general relativity</a> is formally the statement that around every point in a (<a class="existingWikiWord" href="/nlab/show/pseudo-Riemannian+metric">pseudo</a>-)<a class="existingWikiWord" href="/nlab/show/Riemannian+manifold">Riemannian manifold</a> one can find a <a class="existingWikiWord" href="/nlab/show/coordinate+system">coordinate system</a> such that the <a class="existingWikiWord" href="/nlab/show/Levi-Civita+connection">Levi-Civita connection</a> vanishes (“<a class="existingWikiWord" href="/nlab/show/Riemann+normal+coordinates">Riemann normal coordinates</a>”), which means that to <strong>first <a class="existingWikiWord" href="/nlab/show/infinitesimal+space">infinitesimal</a> order</strong> around that point particle dynamics subject to the force of gravity is equivalent to dynamics in <a class="existingWikiWord" href="/nlab/show/Minkowski+spacetime">Minkowski spacetime</a> with vanishing field of gravity.</p> <p>By the above, this is a special case of the principle of general covariance: for every field configuration <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>g</mi></mrow><annotation encoding="application/x-tex">g</annotation></semantics></math> and every given point there is a gauge equivalent field configuration <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>f</mi> <mo>*</mo></msup><mi>g</mi></mrow><annotation encoding="application/x-tex">f^* g</annotation></semantics></math> such that the “force of gravity” (the Levi-Civita connection) vanishes at that point.</p> <p>It is via this relation that the physical “<a class="existingWikiWord" href="/nlab/show/equivalence+principle+%28physics%29">principle of equivalence</a>” relates to the mathematical <em><a class="existingWikiWord" href="/nlab/show/principle+of+equivalence">principle of equivalence</a></em>: this says that formulations need to respect the given notion of <a class="existingWikiWord" href="/nlab/show/equivalence">equivalence</a>/<a class="existingWikiWord" href="/nlab/show/gauge+transformation">gauge transformation</a>, and so</p> <p><a class="existingWikiWord" href="/nlab/show/principle+of+equivalence">principle of equivalence</a> in mathematics <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⇒</mo></mrow><annotation encoding="application/x-tex">\Rightarrow</annotation></semantics></math> principle of general covariance <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⇒</mo></mrow><annotation encoding="application/x-tex">\Rightarrow</annotation></semantics></math> principle of equivalence in physics .</p> <h3 id="in_other_topological_field_theories">In other topological field theories</h3> <h2 id="InHomotopyTypeTheory">Formalization in homotopy type theory</h2> <p>We discuss here that general covariance in field theory has a natural formalization in <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>, hence internal to any <a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-topos">(∞,1)-topos</a>. For exposition, background and further details on the discussion of <a class="existingWikiWord" href="/nlab/show/classical+field+theory">classical</a>/<a class="existingWikiWord" href="/nlab/show/quantum+field+theory">quantum field theory</a> in this fashion see (<a href="#SchreiberLectures">Schreiber, ESI lectures</a>) and (<a href="#SchreiberShulman">Schreiber-Shulman</a>).</p> <p>The same kind of construction yields important <a class="existingWikiWord" href="/nlab/show/moduli+stacks">moduli stacks</a>, for instance the <a class="existingWikiWord" href="/nlab/show/moduli+stack+of+Riemann+surfaces">moduli stack of Riemann surfaces</a>, see <a href="moduli+space+of+curves#InTermsOfTheHigherToposOfSmoothStacks">this remark</a> there.</p> <h3 id="InformalIntroduction">Informal introduction</h3> <p>Let <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> be a <a class="existingWikiWord" href="/nlab/show/smooth+manifold">smooth manifold</a> to be thought of as <a class="existingWikiWord" href="/nlab/show/spacetime">spacetime</a>.</p> <p>Then the central idea of <em>general covariance</em> is that for</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi>i</mi> <mn>1</mn></msub><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mi>U</mi><mo>↪</mo><mi>Σ</mi></mrow><annotation encoding="application/x-tex"> i_1 \;\colon\; U \hookrightarrow \Sigma </annotation></semantics></math></div> <p>and</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi>i</mi> <mn>2</mn></msub><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mi>U</mi><mo>↪</mo><mi>Σ</mi></mrow><annotation encoding="application/x-tex"> i_2 \;\colon\; U \hookrightarrow \Sigma </annotation></semantics></math></div> <p>two <a class="existingWikiWord" href="/nlab/show/subsets">subsets</a>/<a class="existingWikiWord" href="/nlab/show/submanifolds">submanifolds</a>, they should be regarded as <a class="existingWikiWord" href="/nlab/show/equivalence">equivalent</a> if there is a <a class="existingWikiWord" href="/nlab/show/diffeomorphism">diffeomorphism</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ϕ</mi><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mi>Σ</mi><mover><mo>⟶</mo><mrow></mrow></mover><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\phi \;\colon\; \Sigma \stackrel{}{\longrightarrow} \Sigma</annotation></semantics></math> which takes one to the other, hence such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>i</mi> <mn>2</mn></msub><mo>=</mo><msup><mi>ϕ</mi> <mo>*</mo></msup><msub><mi>i</mi> <mn>1</mn></msub><mo>≔</mo><mi>ϕ</mi><mo>∘</mo><msub><mi>i</mi> <mn>1</mn></msub></mrow><annotation encoding="application/x-tex">i_2 = \phi^\ast i_1 \coloneqq\phi \circ i_1 </annotation></semantics></math>.</p> <p>That this statement can be puzzling if one thinks of the case <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi><mo>=</mo><mo>*</mo></mrow><annotation encoding="application/x-tex">U = \ast</annotation></semantics></math> as being just a single point is the content of the historical “<a class="existingWikiWord" href="/nlab/show/hole+argument">hole argument</a> <a class="existingWikiWord" href="/nlab/show/paradox">paradox</a>”.</p> <p>But with just a little bit of formalization the apparent paradox is resolved, because the above evidently just says that the “<a class="existingWikiWord" href="/nlab/show/moduli+space">moduli space</a>” for “subsets of spacetime” is not the manifold <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> itself, but is rather a “<a class="existingWikiWord" href="/nlab/show/moduli+stack">moduli stack</a>” namely the <a class="existingWikiWord" href="/nlab/show/quotient+stack">quotient stack</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi><mo stretchy="false">/</mo><mo stretchy="false">/</mo><mi>Diff</mi><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\Sigma //Diff(\Sigma)</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> by the <a class="existingWikiWord" href="/nlab/show/action">action</a> of the <a class="existingWikiWord" href="/nlab/show/diffeomorphism+group">diffeomorphism group</a>.</p> <p>Indeed, the technical term “<a class="existingWikiWord" href="/nlab/show/quotient+stack">quotient stack</a>” is precisely defined by the condition that for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>U</mi></mrow><annotation encoding="application/x-tex">U</annotation></semantics></math> of the shape of a <a class="existingWikiWord" href="/nlab/show/disk">disk</a>/<a class="existingWikiWord" href="/nlab/show/coordinate+chart">coordinate chart</a>, then two maps</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>i</mi><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mi>U</mi><mo>↪</mo><mi>Σ</mi><mo>⟶</mo><mi>Σ</mi><mo>⫽</mo><mi>Diff</mi><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex"> i \;\colon\; U \hookrightarrow \Sigma \longrightarrow \Sigma \sslash Diff(\Sigma) </annotation></semantics></math></div> <p>to it are equivalent if (and only if) there is a diffeomorphism relating them, as above.</p> <p>So if in a generally covariant field theory spacetime is not actually the manifold <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math>, but rather the quotient stack <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi><mo>⫽</mo><mi>Diff</mi><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\Sigma \sslash Diff(\Sigma)</annotation></semantics></math>, then also a <a class="existingWikiWord" href="/nlab/show/field+%28physics%29">field</a> in this generally covariant field theory should be a field on that quotient stack, not on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> itself.</p> <p>For <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Fields</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{Fields}</annotation></semantics></math> a <a class="existingWikiWord" href="/nlab/show/moduli+space">moduli space</a>/<a class="existingWikiWord" href="/nlab/show/moduli+stack">moduli stack</a> of <a class="existingWikiWord" href="/nlab/show/field+%28physics%29">fields</a>, in a non-generally covariant field theory a field configuration is simply a map</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Φ</mi><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mi>Σ</mi><mo>⟶</mo><mstyle mathvariant="bold"><mi>Fields</mi></mstyle></mrow><annotation encoding="application/x-tex"> \Phi \;\colon\; \Sigma \longrightarrow \mathbf{Fields} </annotation></semantics></math></div> <p>and accordingly the <a class="existingWikiWord" href="/nlab/show/configuration+space">space of all field configurations</a> is the <a class="existingWikiWord" href="/nlab/show/mapping+space">mapping space</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mi>Σ</mi><mo>,</mo><mstyle mathvariant="bold"><mi>Fields</mi></mstyle><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">[\Sigma, \mathbf{Fields}]</annotation></semantics></math>.</p> <p>From this it is clear that for a generally covariant field theory we are instead to declare that the space of field configurations is</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mi>Σ</mi><mo>⫽</mo><mi>Diff</mi><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo>,</mo><mspace width="thickmathspace"></mspace><mstyle mathvariant="bold"><mi>Fields</mi></mstyle><mo stretchy="false">]</mo><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> [\Sigma \sslash Diff(\Sigma), \;\mathbf{Fields}] \,. </annotation></semantics></math></div> <p>And it is at this point that <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>/<a class="existingWikiWord" href="/nlab/show/%28infinity%2C1%29-topos+theory">higher topos theory</a> works a little wonder for us – namely it provides proof – and this is what is discussed below – that</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mi>Σ</mi><mo>⫽</mo><mi>Diff</mi><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo>,</mo><mspace width="thickmathspace"></mspace><mstyle mathvariant="bold"><mi>Fields</mi></mstyle><mo stretchy="false">]</mo><mo>≃</mo><mo stretchy="false">[</mo><mi>Σ</mi><mo>,</mo><mspace width="thickmathspace"></mspace><mstyle mathvariant="bold"><mi>Fields</mi></mstyle><mo stretchy="false">]</mo><mo>⫽</mo><mi>Diff</mi><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> [\Sigma \sslash Diff(\Sigma),\; \mathbf{Fields}] \simeq [\Sigma,\; \mathbf{Fields}] \sslash Diff(\Sigma) \,. </annotation></semantics></math></div> <p>In words, the right hand side is the time-honored answer: two fields <em>on</em> a spacetime manifold <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math>, which are such that one goes over into the other when pulled back along a diffeomorphism, are <a class="existingWikiWord" href="/nlab/show/gauge+equivalence">gauge equivalent</a>. This is the statement of general covariance, derived here, formally, from just the condition that any two shapes <em>in</em> spacetime are to be equivalent if related by a diffeomorphism.</p> <p>Here to read the above equivalence as a theorem, we have to read the left hand side, as it should, be “in the context of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Diff</mi><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Diff(\Sigma)</annotation></semantics></math>-actions”. Such <a class="existingWikiWord" href="/nlab/show/context">context</a>-dependence is precisely what <em><a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent</a></em> <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a> takes care of, and this is what the following technical statement deals with.</p> <h3 id="introduction_in_terms_of_type_theory">Introduction in terms of type theory</h3> <p>A basic idea of traditional <a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent type theory</a> is of course that <a class="existingWikiWord" href="/nlab/show/types">types</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi></mrow><annotation encoding="application/x-tex">A</annotation></semantics></math> may appear <em>in <a class="existingWikiWord" href="/nlab/show/context">context</a></em> of other types <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi></mrow><annotation encoding="application/x-tex">\Gamma</annotation></semantics></math>. The traditional interpretation of such a dependent type</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>:</mo><mi>Γ</mi><mo>⊢</mo><mi>A</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo><mo>:</mo><mi>Type</mi></mrow><annotation encoding="application/x-tex"> x : \Gamma \vdash A(x) : Type </annotation></semantics></math></div> <p>is that of a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi></mrow><annotation encoding="application/x-tex">\Gamma</annotation></semantics></math>-parameterized family or <em><a class="existingWikiWord" href="/nlab/show/bundle">bundle</a></em> of types, whose <a class="existingWikiWord" href="/nlab/show/fiber">fiber</a> over <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>x</mi><mo>∈</mo><mi>Γ</mi></mrow><annotation encoding="application/x-tex">x \in \Gamma</annotation></semantics></math> is <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>A</mi><mo stretchy="false">(</mo><mi>x</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">A(x)</annotation></semantics></math>.</p> <p>But in <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>, types are <a class="existingWikiWord" href="/nlab/show/homotopy+types">homotopy types</a> and, hence so are the contexts. A <a class="existingWikiWord" href="/nlab/show/type+in+context">type in context</a> is now in general something more refined than just a family of types. It is really a family of types equipped with <em><a class="existingWikiWord" href="/nlab/show/equivariance">equivariance</a></em> structure with respect to the <a class="existingWikiWord" href="/nlab/show/homotopy+groups">homotopy groups</a> of the context type.</p> <p>Hence in homotopy theory <a class="existingWikiWord" href="/nlab/show/types+in+context">types in context</a> generically satisfy an <a class="existingWikiWord" href="/nlab/show/equivariance">equivariance</a>-principle.</p> <p>Specifically, if the context type is <a class="existingWikiWord" href="/nlab/show/n-connected+object+in+an+%28infinity%2C1%29-topos">connected</a> and <a class="existingWikiWord" href="/nlab/show/pointed+object">pointed</a>, then it is equivalent to the <a class="existingWikiWord" href="/nlab/show/delooping">delooping</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Γ</mi><mo>≃</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>G</mi></mrow><annotation encoding="application/x-tex">\Gamma \simeq \mathbf{B}G</annotation></semantics></math> of an <a class="existingWikiWord" href="/nlab/show/%E2%88%9E-group">∞-group</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi></mrow><annotation encoding="application/x-tex">G</annotation></semantics></math>. One finds – this is discussed at <em><a class="existingWikiWord" href="/nlab/show/%E2%88%9E-action">∞-action</a></em> – that the <a class="existingWikiWord" href="/nlab/show/context">context</a> defined by the type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>G</mi></mrow><annotation encoding="application/x-tex">\mathbf{B}G</annotation></semantics></math> is that of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi></mrow><annotation encoding="application/x-tex">G</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/equivariance">equivariance</a>: every type in the context is a type in the original context, but now equipped with a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi></mrow><annotation encoding="application/x-tex">G</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/%E2%88%9E-action">∞-action</a>. In a precise sense, the homotopy type theory of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi></mrow><annotation encoding="application/x-tex">G</annotation></semantics></math>-<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>∞</mn></mrow><annotation encoding="application/x-tex">\infty</annotation></semantics></math>-actions is equivalent to plain homotopy type theory <em>in <a class="existingWikiWord" href="/nlab/show/context">context</a></em> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>G</mi></mrow><annotation encoding="application/x-tex">\mathbf{B}G</annotation></semantics></math>.</p> <p>In the following we discuss this for the case that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi></mrow><annotation encoding="application/x-tex">G</annotation></semantics></math> is an <a class="existingWikiWord" href="/nlab/show/automorphism+%E2%88%9E-group">automorphism ∞-group</a> of a type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> which is regarded as representing <a class="existingWikiWord" href="/nlab/show/spacetime">spacetime</a> or a <a class="existingWikiWord" href="/nlab/show/worldvolume">worldvolume</a>. We show that in this context the rules of homotopy type theory automatically induce the principle of general covariance and naturally produce configurations spaces of generally covariant field theories: for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Fields</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{Fields}</annotation></semantics></math> a moduli object for the given fields, so that a field configuration is a function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ϕ</mi><mo>:</mo><mi>Σ</mi><mo>→</mo><mstyle mathvariant="bold"><mi>Fields</mi></mstyle></mrow><annotation encoding="application/x-tex">\phi : \Sigma \to \mathbf{Fields}</annotation></semantics></math>, the configuration space of <em>covariant</em> fields is the <a class="existingWikiWord" href="/nlab/show/function+type">function type</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>Σ</mi><mo>→</mo><mstyle mathvariant="bold"><mi>Fields</mi></mstyle><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(\Sigma \to \mathbf{Fields})</annotation></semantics></math> but formed in the “general covariance context” <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{B}\mathbf{Aut}(\Sigma)</annotation></semantics></math>. When <a class="existingWikiWord" href="/nlab/show/categorical+semantics">interpreted</a> in <a class="existingWikiWord" href="/nlab/show/smooth+infinity-groupoid">smooth models</a>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Conf</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{Conf}</annotation></semantics></math> is the smooth groupoid of field configurations and diffeomorphism gauge transformations acting on them, the <a class="existingWikiWord" href="/nlab/show/Lie+integration">Lie integrations</a> of the <a class="existingWikiWord" href="/nlab/show/BRST+complex">BRST complex</a> whose degree-1 elements are the <em>diffeomorphism ghosts</em>.</p> <p>More precisely, we show the following.</p> <div class="num_defn"> <h6 id="definition">Definition</h6> <p>Consider in homotopy type theory two types <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><mi>Σ</mi><mo>,</mo><mstyle mathvariant="bold"><mi>Fields</mi></mstyle><mo>:</mo><mi>Type</mi></mrow><annotation encoding="application/x-tex">\vdash \Sigma, \mathbf{Fields} : Type</annotation></semantics></math>, to be called <em>spacetime</em> and <em>field moduli</em>. Let</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo>:</mo><mi>Type</mi></mrow><annotation encoding="application/x-tex"> \vdash \mathbf{B}\mathbf{Aut}(\Sigma) : Type </annotation></semantics></math></div> <p>be the image of the name of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math>, with essentially unique term</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><mi>Σ</mi><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> \vdash \Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \,. </annotation></semantics></math></div> <p>Perform the canonical context extension of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> and trivial context extension of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Fields</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{Fields}</annotation></semantics></math> to get types in context</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Σ</mi><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo>⊢</mo><mi>Σ</mi><mo>:</mo><mi>Type</mi></mrow><annotation encoding="application/x-tex"> \Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash \Sigma : Type </annotation></semantics></math></div> <p>and</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Σ</mi><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo>⊢</mo><mstyle mathvariant="bold"><mi>Fields</mi></mstyle><mo>:</mo><mi>Type</mi><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> \Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash \mathbf{Fields} : Type \,. </annotation></semantics></math></div> <p>Form then the type of field moduli</p> <p>“<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Conf</mi></mstyle><mo>≔</mo><mo stretchy="false">(</mo><mi>Σ</mi><mo>→</mo><mstyle mathvariant="bold"><mi>Fields</mi></mstyle><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{Conf} \coloneqq (\Sigma \to \mathbf{Fields})</annotation></semantics></math>”</p> <p><em>in this context</em>:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Conf</mi></mstyle><mo>≔</mo><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mi>Σ</mi><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo>⊢</mo><mo stretchy="false">(</mo><mi>Σ</mi><mo>→</mo><mstyle mathvariant="bold"><mi>Fields</mi></mstyle><mo stretchy="false">)</mo><mo>:</mo><mi>Type</mi><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> \mathbf{Conf} \coloneqq \;\;\;\;\; \Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash (\Sigma \to \mathbf{Fields}) : Type \,. </annotation></semantics></math></div></div> <div class="num_prop"> <h6 id="proposition">Proposition</h6> <p>The <a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Conf</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{Conf}</annotation></semantics></math> in the model <a class="existingWikiWord" href="/nlab/show/Smooth%E2%88%9EGrpd">Smooth∞Grpd</a> of the homotopy type theory, and for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi><mo>∈</mo></mrow><annotation encoding="application/x-tex">\Sigma \in</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/SmoothMfd">SmoothMfd</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>↪</mo><mi>Smooth</mi><mn>∞</mn><mi>Grpd</mi></mrow><annotation encoding="application/x-tex">\hookrightarrow Smooth \infty Grpd</annotation></semantics></math>, is given by the <a class="existingWikiWord" href="/nlab/show/diffeological+space">diffeological groupoid</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Conf</mi></mstyle><mo>=</mo><mo stretchy="false">[</mo><mi>Σ</mi><mo>,</mo><mstyle mathvariant="bold"><mi>Fields</mi></mstyle><mo stretchy="false">]</mo><mo>⫽</mo><mstyle mathvariant="bold"><mi>Diff</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex"> \mathbf{Conf} = [\Sigma, \mathbf{Fields}]\sslash \mathbf{Diff}(\Sigma) </annotation></semantics></math></div> <p>whose objects are field configurations on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> and whose morphisms are diffeomorphism gauge transformations between them. In particular the corresponding <a class="existingWikiWord" href="/nlab/show/Lie+algebroid">Lie algebroid</a> is dual to the <a class="existingWikiWord" href="/nlab/show/BRST+complex">BRST complex</a> of fields with diffeomorphism ghosts in degree 1.</p> </div> <h3 id="the_ambient_theory">The ambient theory</h3> <p>Write <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>H</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{H}</annotation></semantics></math> for the ambient <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>, or rather an <a class="existingWikiWord" href="/nlab/show/categorical+semantics">interpretation</a> given by an <a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-topos">(∞,1)-topos</a>. For standard applications in <a class="existingWikiWord" href="/nlab/show/physics">physics</a> we have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>H</mi></mstyle><mo>=</mo></mrow><annotation encoding="application/x-tex">\mathbf{H} = </annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/Smooth%E2%88%9EGrpd">Smooth∞Grpd</a> or <a class="existingWikiWord" href="/nlab/show/SmoothSuper%E2%88%9EGrpd">SmoothSuper∞Grpd</a> or similar, but none of the following general discussion depends on a concrete choice for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>H</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{H}</annotation></semantics></math>.</p> <p>Pick once and for all an <a class="existingWikiWord" href="/nlab/show/object">object</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Σ</mi><mo>∈</mo><mstyle mathvariant="bold"><mi>H</mi></mstyle></mrow><annotation encoding="application/x-tex"> \Sigma \in \mathbf{H} </annotation></semantics></math></div> <p>supposed to represent the <a class="existingWikiWord" href="/nlab/show/space">space</a> underlying <a class="existingWikiWord" href="/nlab/show/spacetime">spacetime</a> or the <a class="existingWikiWord" href="/nlab/show/worldvolume">worldvolume</a> of a <a class="existingWikiWord" href="/nlab/show/model+%28in+theoretical+physics%29">model (in theoretical physics)</a>,</p> <h3 id="the_diffeomorphism_group">The diffeomorphism group</h3> <p>Write</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo>∈</mo><mi>Grp</mi><mo stretchy="false">(</mo><mstyle mathvariant="bold"><mi>H</mi></mstyle><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex"> \mathbf{Aut}(\Sigma) \in Grp(\mathbf{H}) </annotation></semantics></math></div> <p>for the <a class="existingWikiWord" href="/nlab/show/automorphism+%E2%88%9E-group">automorphism ∞-group</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math>. As discussed there, this is the <a class="existingWikiWord" href="/nlab/show/loop+space+object">loop space object</a> of the <a class="existingWikiWord" href="/nlab/show/homotopy+image">homotopy image</a>-factorization of</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>*</mo><mover><mo>→</mo><mrow><mo>⊢</mo><mi>Σ</mi></mrow></mover><mi>Type</mi><mspace width="thinmathspace"></mspace><mo>,</mo></mrow><annotation encoding="application/x-tex"> * \stackrel{\vdash \Sigma}{\to} Type \,, </annotation></semantics></math></div> <p>hence the factorization by an <a class="existingWikiWord" href="/nlab/show/effective+epimorphism+in+an+%28infinity%2C1%29-category">effective epimorphism</a> followed by a <a class="existingWikiWord" href="/nlab/show/monomorphism+in+an+%28infinity%2C1%29-category">monomorphism</a>:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>*</mo><mover><mo>→</mo><mrow></mrow></mover><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mover><mo>↪</mo><mrow></mrow></mover><mi>Type</mi><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> * \stackrel{}{\to} \mathbf{B}\mathbf{Aut}(\Sigma) \stackrel{}{\hookrightarrow} Type \,. </annotation></semantics></math></div> <p>In the standard <a class="existingWikiWord" href="/nlab/show/categorical+semantics">interpretation</a> of the homotopy type theory in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>H</mi></mstyle><mo>=</mo></mrow><annotation encoding="application/x-tex">\mathbf{H} = </annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/Smooth%E2%88%9EGrpd">Smooth∞Grpd</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> could be an ordinary <a class="existingWikiWord" href="/nlab/show/smooth+manifold">smooth manifold</a> or <a class="existingWikiWord" href="/nlab/show/orbifold">orbifold</a>, in particular, and then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo>=</mo><mstyle mathvariant="bold"><mo lspace="0em" rspace="thinmathspace">Diff</mo></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{Aut}(\Sigma) = \mathbf{\Diff}(\Sigma)</annotation></semantics></math> is the <a class="existingWikiWord" href="/nlab/show/diffeomorphism+group">diffeomorphism group</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math>, regarded as a <a class="existingWikiWord" href="/nlab/show/diffeological+space">diffeological</a> <a class="existingWikiWord" href="/nlab/show/group+object">group object</a>. In view of this archetypical example we will in the following often say <em><a class="existingWikiWord" href="/nlab/show/diffeomorphism">diffeomorphism</a></em> for short instead of <em>auto-equivalence in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>H</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{H}</annotation></semantics></math></em> and similarly refer to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{Aut}(\Sigma)</annotation></semantics></math> loosely as the <em>diffeomorphism group</em> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math>. But even in the specifical model <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>H</mi></mstyle><mo>=</mo></mrow><annotation encoding="application/x-tex">\mathbf{H} = </annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/Smooth%E2%88%9EGrpd">Smooth∞Grpd</a>/<a class="existingWikiWord" href="/nlab/show/SmoothSuper%E2%88%9EGrpd">SmoothSuper∞Grpd</a>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> can be much more general than a <a class="existingWikiWord" href="/nlab/show/smooth+manifold">smooth manifold</a> or <a class="existingWikiWord" href="/nlab/show/supermanifold">supermanifold</a> or <a class="existingWikiWord" href="/nlab/show/orbifold">orbifold</a>.</p> <h3 id="the_context_of_general_covariance">The context of general covariance</h3> <p>Write then <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo>∈</mo><mstyle mathvariant="bold"><mi>H</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{B} \mathbf{Aut}(\Sigma) \in \mathbf{H}</annotation></semantics></math> for the <a class="existingWikiWord" href="/nlab/show/delooping">delooping</a> of the diffeomorphism group. The essentially unique <a class="existingWikiWord" href="/nlab/show/term">term</a> of this type is to be thought of as being <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> itself, and so we write it as</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><mi>Σ</mi><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> \vdash \Sigma : \mathbf{B} \mathbf{Aut}(\Sigma) \,. </annotation></semantics></math></div> <p>By the discussion at <em><a class="existingWikiWord" href="/nlab/show/%E2%88%9E-action">∞-action</a></em>, a <a class="existingWikiWord" href="/nlab/show/type+in+context">type in context</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{B}\mathbf{Aut}(\Sigma)</annotation></semantics></math></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Σ</mi><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo>⊢</mo><mi>V</mi><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex"> \Sigma : \mathbf{B} \mathbf{Aut}(\Sigma) \vdash V(\Sigma) </annotation></semantics></math></div> <p>is a type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><mi>V</mi><mo>:</mo><mi>Type</mi></mrow><annotation encoding="application/x-tex">\vdash V : Type</annotation></semantics></math> in the absolute context equipped with an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{Aut}(\Sigma)</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/%E2%88%9E-action">∞-action</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ρ</mi><mo>:</mo><mi>V</mi><mo>×</mo><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo>→</mo><mi>V</mi></mrow><annotation encoding="application/x-tex">\rho : V \times \mathbf{Aut}(\Sigma) \to V</annotation></semantics></math> on it. The <a class="existingWikiWord" href="/nlab/show/dependent+sum">dependent sum</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>Σ</mi><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow></munder><mi>V</mi><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo>:</mo><mi>Type</mi><mspace width="thinmathspace"></mspace><mo>,</mo></mrow><annotation encoding="application/x-tex"> \vdash \sum_{\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma)} V(\Sigma) : Type \,, </annotation></semantics></math></div> <p>which we also write</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>V</mi><mo>⫽</mo><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo>≔</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>Σ</mi><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow></munder><mi>V</mi><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mspace width="thinmathspace"></mspace><mo>,</mo></mrow><annotation encoding="application/x-tex"> V \sslash \mathbf{Aut}(\Sigma) \coloneqq \sum_{\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma)} V(\Sigma) \,, </annotation></semantics></math></div> <p>is the total space of the universal <a class="existingWikiWord" href="/nlab/show/associated+%E2%88%9E-bundle">associated</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>V</mi></mrow><annotation encoding="application/x-tex">V</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/fiber+%E2%88%9E-bundle">fiber ∞-bundle</a>:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>V</mi></mtd> <mtd><mo>→</mo></mtd> <mtd><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow></munder><mi>V</mi><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd><msup><mo stretchy="false">↓</mo> <mover><mi>ρ</mi><mo>¯</mo></mover></msup></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mtd></mtr></mtable></mrow><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> \array{ V &\to& \sum_{\mathbf{B}\mathbf{Aut}(\Sigma)} V(\Sigma) \\ && \downarrow^{\overline{\rho}} \\ && \mathbf{B}\mathbf{Aut}(\Sigma) } \,. </annotation></semantics></math></div> <p>Hence the <a class="existingWikiWord" href="/nlab/show/categorical+semantics">interpretation</a> of the context <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma)</annotation></semantics></math> is the <a class="existingWikiWord" href="/nlab/show/slice+%28%E2%88%9E%2C1%29-topos">slice (∞,1)-topos</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mstyle mathvariant="bold"><mi>H</mi></mstyle> <mrow><mo stretchy="false">/</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow></msub></mrow><annotation encoding="application/x-tex">\mathbf{H}_{/\mathbf{B}\mathbf{Aut}(\Sigma)}</annotation></semantics></math> and equivalently is the <a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-topos">(∞,1)-topos</a> of objects in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>H</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{H}</annotation></semantics></math> equipped with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi></mrow><annotation encoding="application/x-tex">G</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/%E2%88%9E-actions">∞-actions</a> and of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi></mrow><annotation encoding="application/x-tex">G</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/equivariance">equivariant</a> <a class="existingWikiWord" href="/nlab/show/morphisms">morphisms</a> between them:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mstyle mathvariant="bold"><mi>H</mi></mstyle> <mrow><mo stretchy="false">/</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow></msub><mo>≃</mo><msub><mi>Act</mi> <mstyle mathvariant="bold"><mi>H</mi></mstyle></msub><mo stretchy="false">(</mo><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> \mathbf{H}_{/\mathbf{B}\mathbf{Aut}(\Sigma)} \simeq Act_{\mathbf{H}}(\mathbf{Aut}(\Sigma)) \,. </annotation></semantics></math></div> <p>Hence a <a class="existingWikiWord" href="/nlab/show/type+in+context">type in context</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma)</annotation></semantics></math> is a “generally covariant type” with respect to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> in the sense that it transforms <a class="existingWikiWord" href="/nlab/show/covariant+functor">covariantly</a> by equivalences under diffeomorphisms of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math>. In summary then</p> <p><strong>Fact.</strong> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma)</annotation></semantics></math> <em>is the <strong><a class="existingWikiWord" href="/nlab/show/context">context</a> of general covariance</strong> with respect to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math>.</em></p> <p>In the precise formal sense.</p> <p>In particular, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> itself is canonically equipped with the defining action of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{Aut}(\Sigma)</annotation></semantics></math> on it, which <a class="existingWikiWord" href="/nlab/show/syntax">syntactically</a> we may write</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Σ</mi><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo>⊢</mo><mi>Σ</mi><mo>:</mo><mi>Type</mi></mrow><annotation encoding="application/x-tex"> \Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash \Sigma : Type </annotation></semantics></math></div> <p>and which <a class="existingWikiWord" href="/nlab/show/categorical+semantics">semantically</a> is exhibited by the universal <a class="existingWikiWord" href="/nlab/show/associated+%E2%88%9E-bundle">associated</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/fiber+%E2%88%9E-bundle">fiber ∞-bundle</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>Σ</mi></mtd> <mtd><mo>→</mo></mtd> <mtd><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>Σ</mi><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow></munder><mi>Σ</mi></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd><msup><mo stretchy="false">↓</mo> <mover><mrow><msub><mi>ρ</mi> <mi>Σ</mi></msub></mrow><mo>¯</mo></mover></msup></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mtd></mtr></mtable></mrow><mspace width="thinmathspace"></mspace><mo>,</mo></mrow><annotation encoding="application/x-tex"> \array{ \Sigma &\to& \sum_{\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma)} \Sigma \\ && \downarrow^{\overline{\rho_{\Sigma}}} \\ && \mathbf{B} \mathbf{Aut}(\Sigma) } \,, </annotation></semantics></math></div> <p>given by the <a class="existingWikiWord" href="/nlab/show/pullback">pullback</a> of the <a class="existingWikiWord" href="/nlab/show/universe">universe</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mover><mi>Type</mi><mo>˜</mo></mover><mo>→</mo><mi>Type</mi></mrow><annotation encoding="application/x-tex">\widetilde Type \to Type</annotation></semantics></math> along the defining <a class="existingWikiWord" href="/nlab/show/monomorphism+in+an+%28infinity%2C1%29-category">inclusion</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo>↪</mo><mi>Type</mi></mrow><annotation encoding="application/x-tex">\mathbf{B}\mathbf{Aut} \hookrightarrow Type</annotation></semantics></math>.</p> <p>Here the total space</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Σ</mi><mo>⫽</mo><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo>≔</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>Σ</mi><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow></munder><mi>Σ</mi></mrow><annotation encoding="application/x-tex"> \Sigma \sslash \mathbf{Aut}(\Sigma) \coloneqq \sum_{\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) } \Sigma </annotation></semantics></math></div> <p>is the <a class="existingWikiWord" href="/nlab/show/homotopy+quotient">homotopy quotient</a> or <a class="existingWikiWord" href="/nlab/show/action+groupoid">action groupoid</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{Aut}(\Sigma)</annotation></semantics></math>. This is the type characterized by the fact that a <a class="existingWikiWord" href="/nlab/show/function">function</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mo>:</mo><mi>U</mi><mo>→</mo><mi>Σ</mi><mo>⫽</mo><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f : U \to \Sigma \sslash \mathbf{Aut}(\Sigma)</annotation></semantics></math> is a function to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> which is regarded as (<a class="existingWikiWord" href="/nlab/show/gauge+equivalence">gauge</a>) <a class="existingWikiWord" href="/nlab/show/equivalence">equivalent</a> to another function to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> if both differ by postcomposition with a diffeomorphism of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math>.</p> <h3 id="generally_covariant_field_configuration_spaces">Generally covariant field configuration spaces</h3> <p>Let now</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Fields</mi></mstyle><mo>∈</mo><mstyle mathvariant="bold"><mi>H</mi></mstyle></mrow><annotation encoding="application/x-tex"> \mathbf{Fields} \in \mathbf{H} </annotation></semantics></math></div> <p>be an object that represents the <a class="existingWikiWord" href="/nlab/show/moduli+%E2%88%9E-stack">moduli ∞-stack</a> of field configurations on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> for some <a class="existingWikiWord" href="/nlab/show/model+%28in+theoretical+physics%29">model (in theoretical physics)</a> to be described. For instance for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi><mo>∈</mo><mi>Grp</mi><mo stretchy="false">(</mo><mstyle mathvariant="bold"><mi>H</mi></mstyle><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">G \in Grp(\mathbf{H})</annotation></semantics></math> an <a class="existingWikiWord" href="/nlab/show/%E2%88%9E-group">∞-group</a> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>H</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{H}</annotation></semantics></math> a <a class="existingWikiWord" href="/nlab/show/cohesive+homotopy+type+theory">cohesive homotopy type theory</a>, we could have <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Fields</mi></mstyle><mo>=</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><msub><mi>G</mi> <mi>conn</mi></msub></mrow><annotation encoding="application/x-tex">\mathbf{Fields} = \mathbf{B}G_{conn}</annotation></semantics></math> the moduli for a choice of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi></mrow><annotation encoding="application/x-tex">G</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/connection+on+an+%E2%88%9E-bundle">principal ∞-connection</a>, being the moduli for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi></mrow><annotation encoding="application/x-tex">G</annotation></semantics></math>-(<a class="existingWikiWord" href="/nlab/show/higher+gauge+theory">higher</a>)<a class="existingWikiWord" href="/nlab/show/gauge+fields">gauge fields</a>. For general <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Fields</mi></mstyle><mo>=</mo><mi>X</mi><mo>∈</mo><mstyle mathvariant="bold"><mi>H</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{Fields} = X \in \mathbf{H}</annotation></semantics></math> we may always regard <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math> as the <a class="existingWikiWord" href="/nlab/show/target+space">target space</a> of a <a class="existingWikiWord" href="/nlab/show/sigma-model">sigma-model</a>.</p> <p>Then the <a class="existingWikiWord" href="/nlab/show/internal+hom">internal hom</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Fields</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo>≔</mo><mo stretchy="false">[</mo><mi>Σ</mi><mo>,</mo><mstyle mathvariant="bold"><mi>Fields</mi></mstyle><mo stretchy="false">]</mo><mo>∈</mo><mstyle mathvariant="bold"><mi>H</mi></mstyle></mrow><annotation encoding="application/x-tex"> \mathbf{Fields}(\Sigma) \coloneqq [\Sigma, \mathbf{Fields}] \in \mathbf{H} </annotation></semantics></math></div> <p>hence the <a class="existingWikiWord" href="/nlab/show/function+type">function type</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><mi>Σ</mi><mo>→</mo><mstyle mathvariant="bold"><mi>Fields</mi></mstyle><mo>:</mo><mi>Type</mi></mrow><annotation encoding="application/x-tex"> \vdash \Sigma \to \mathbf{Fields} : Type </annotation></semantics></math></div> <p>is the <em>naive</em> <a class="existingWikiWord" href="/nlab/show/configuration+space">configuration space</a> of the model. This is not generally covariant, precisely so by the above definition: it is not in the generally covariant context <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mstyle mathvariant="bold"><mi>H</mi></mstyle> <mrow><mo stretchy="false">/</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow></msub></mrow><annotation encoding="application/x-tex">\mathbf{H}_{/\mathbf{B} \mathbf{Aut}(\Sigma)}</annotation></semantics></math>.</p> <p>But by the <a class="existingWikiWord" href="/nlab/show/inverse+image">inverse image</a> of the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{B}\mathbf{Aut}(\Sigma)</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/dependent+product">dependent product</a> <a class="existingWikiWord" href="/nlab/show/%C3%A9tale+geometric+morphism">étale geometric morphism</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mstyle mathvariant="bold"><mi>H</mi></mstyle> <mrow><mo stretchy="false">/</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>G</mi></mrow></msub><mover><mover><munder><mo>→</mo><mrow><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow></munder></mrow></munder><mover><mo>←</mo><mrow></mrow></mover></mover><mover><mo>→</mo><mrow><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow></munder></mrow></mover></mover><mstyle mathvariant="bold"><mi>H</mi></mstyle></mrow><annotation encoding="application/x-tex"> \mathbf{H}_{/\mathbf{B}G} \stackrel{\overset{\sum_{\mathbf{B}\mathbf{Aut}(\Sigma)}}{\to}}{ \stackrel{\overset{}{\leftarrow}}{\underset{\prod_{\mathbf{B}\mathbf{Aut}(\Sigma)}}{\to}}} \mathbf{H} </annotation></semantics></math></div> <p>which is <a class="existingWikiWord" href="/nlab/show/context+enlargement">context enlargement</a> by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{B}\mathbf{Aut}(\Sigma)</annotation></semantics></math>, the moduli type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Fields</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{Fields}</annotation></semantics></math> is freely moved to the general covariant context, where it is regarded as equipped with the <a href="infinity-action#TrivialAction">trivial ∞-action</a>. Accordingly we will write just <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Fields</mi></mstyle><mo>∈</mo><msub><mstyle mathvariant="bold"><mi>H</mi></mstyle> <mrow><mo stretchy="false">/</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow></msub></mrow><annotation encoding="application/x-tex">\mathbf{Fields} \in \mathbf{H}_{/\mathbf{B}\mathbf{Aut}(\Sigma)}</annotation></semantics></math> with that trivial action understood, which is justified by the precise syntactic expression for it:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Σ</mi><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo>⊢</mo><mstyle mathvariant="bold"><mi>Fields</mi></mstyle><mo>:</mo><mi>Type</mi></mrow><annotation encoding="application/x-tex"> \Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash \mathbf{Fields} : Type </annotation></semantics></math></div> <p>We may then form the <em>configuration space of fields in the generally covariant context</em> . As before, a field <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ϕ</mi></mrow><annotation encoding="application/x-tex">\phi</annotation></semantics></math> should be a function on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> with values in the moduli type of field configurations, but now we interpret this statement in the generally covariant context. Syntactically this simply means that a field is now a term in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{B}\mathbf{Aut}(\Sigma)</annotation></semantics></math>-context</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Σ</mi><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo>⊢</mo><mi>ϕ</mi><mo>:</mo><mi>Σ</mi><mo>→</mo><mstyle mathvariant="bold"><mi>Fields</mi></mstyle></mrow><annotation encoding="application/x-tex"> \Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash \phi : \Sigma \to \mathbf{Fields} </annotation></semantics></math></div> <p>and that accordingly the configuration space of fields is</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>Σ</mi><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo>⊢</mo><mi>Σ</mi><mo>→</mo><mstyle mathvariant="bold"><mi>Fields</mi></mstyle><mo>:</mo><mi>Type</mi><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> \Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash \Sigma \to \mathbf{Fields} : Type \,. </annotation></semantics></math></div> <p>The <a class="existingWikiWord" href="/nlab/show/categorical+semantics">semantics</a> of this is the <a class="existingWikiWord" href="/nlab/show/internal+hom">internal hom</a> in the <a class="existingWikiWord" href="/nlab/show/slice+%28%E2%88%9E%2C1%29-topos">slice (∞,1)-topos</a>, the <em><a href="infinity-action#CartesianClosedMonoidalStructure">Internal hom of ∞-actions</a></em></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Conf</mi></mstyle><mo>≔</mo><mo stretchy="false">[</mo><mi>Σ</mi><mo>⫽</mo><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo>,</mo><mstyle mathvariant="bold"><mi>Fields</mi></mstyle><mo stretchy="false">]</mo><mo>∈</mo><msub><mstyle mathvariant="bold"><mi>H</mi></mstyle> <mrow><mo stretchy="false">/</mo><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow></msub><mspace width="thinmathspace"></mspace><mo>,</mo></mrow><annotation encoding="application/x-tex"> \mathbf{Conf} \coloneqq [\Sigma \sslash \mathbf{Aut}(\Sigma), \mathbf{Fields}] \in \mathbf{H}_{/\mathbf{Aut}(\Sigma)} \,, </annotation></semantics></math></div> <p>The central observation now is that discussed at <em><a href="infinity-action#GeneralCovariance">∞-action – Examples – General covariance</a></em>:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Conf</mi></mstyle><mo>≃</mo><mo stretchy="false">[</mo><mi>Σ</mi><mo>,</mo><mstyle mathvariant="bold"><mi>Fields</mi></mstyle><mo stretchy="false">]</mo><mo>⫽</mo><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex"> \mathbf{Conf} \simeq [\Sigma,\mathbf{Fields}] \sslash \mathbf{Aut}(\Sigma) </annotation></semantics></math></div> <p>is the <a class="existingWikiWord" href="/nlab/show/homotopy+quotient">homotopy quotient</a> of the naive fields <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∈</mo><mstyle mathvariant="bold"><mi>Fields</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\in \mathbf{Fields}(\Sigma)</annotation></semantics></math> by the action of the <a class="existingWikiWord" href="/nlab/show/diffeomorphism+group">diffeomorphism group</a>, exhibiting a <a class="existingWikiWord" href="/nlab/show/gauge+equivalence">gauge equivalence</a> between any two field configurations that differ after pullback along a diffeomorphism.</p> <p>This is precisely as it should be for configuration space of generally covariant theories. We have found:</p> <p><strong>Fact</strong>. In terms of homotopy type theory, configuration spaces of a generally covariant theory over <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> are precisely the ordinary configuration spaces of fields, but formed in the context <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{B}\mathbf{Aut}(\Sigma)</annotation></semantics></math>:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Conf</mi></mstyle><msub><mo>=</mo> <mi>def</mi></msub><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mi>Σ</mi><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>Σ</mi><mo stretchy="false">)</mo><mo>⊢</mo><mo stretchy="false">(</mo><mi>Σ</mi><mo>→</mo><mstyle mathvariant="bold"><mi>Field</mi></mstyle><mo stretchy="false">)</mo><mo>:</mo><mi>Type</mi><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> \mathbf{Conf} =_{def} \;\;\;\;\;\; \Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash (\Sigma \to \mathbf{Field}) : Type \,. </annotation></semantics></math></div> <h3 id="GravityInHoTT">Generally covariant field of gravity</h3> <p>We now spell out the example of ordinary <a class="existingWikiWord" href="/nlab/show/Einstein">Einstein</a>-<a class="existingWikiWord" href="/nlab/show/gravity">gravity</a> in this language. Plenty of further examples work analogously.</p> <p>For pure <a class="existingWikiWord" href="/nlab/show/gravity">gravity</a>, we choose <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>H</mi></mstyle><mo>=</mo></mrow><annotation encoding="application/x-tex">\mathbf{H} = </annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/Smooth%E2%88%9EGrpd">Smooth∞Grpd</a> or <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>=</mo></mrow><annotation encoding="application/x-tex">=</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/SynthDiff%E2%88%9EGrpd">SynthDiff∞Grpd</a>.</p> <p>If we denote by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>D</mi> <mi>n</mi></msup><mo>∈</mo></mrow><annotation encoding="application/x-tex">D^n \in </annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/SynthDiff%E2%88%9EGrpd">SynthDiff∞Grpd</a> the first order <a class="existingWikiWord" href="/nlab/show/infinitesimal+object">infinitesimal neighbourhood</a> of the origin in the <a class="existingWikiWord" href="/nlab/show/Cartesian+space">Cartesian space</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>ℝ</mi> <mi>n</mi></msup></mrow><annotation encoding="application/x-tex">\mathbb{R}^n</annotation></semantics></math>, then</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>=</mo><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><msup><mi>D</mi> <mi>n</mi></msup><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex"> GL(n) = \mathbf{Aut}(D^n) </annotation></semantics></math></div> <p>is the <a class="existingWikiWord" href="/nlab/show/automorphism+%E2%88%9E-group">automorphism ∞-group</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>D</mi> <mi>n</mi></msup></mrow><annotation encoding="application/x-tex">D^n</annotation></semantics></math>. Accordingly we write the unique term of the <a class="existingWikiWord" href="/nlab/show/delooping">delooping</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{B}GL(n)</annotation></semantics></math> as</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><msup><mi>D</mi> <mi>n</mi></msup><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> \vdash D^n : \mathbf{B}GL(n) \,. </annotation></semantics></math></div> <p>The fields of Einstein gravity are <a class="existingWikiWord" href="/nlab/show/orthogonal+structures">orthogonal structures</a> (<a class="existingWikiWord" href="/nlab/show/Riemannian+metrics">Riemannian metrics</a>) on a <a class="existingWikiWord" href="/nlab/show/smooth+manifold">smooth manifold</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi><mo>∈</mo></mrow><annotation encoding="application/x-tex">\Sigma \in </annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/SmoothMfd">SmoothMfd</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>↪</mo><mstyle mathvariant="bold"><mi>H</mi></mstyle></mrow><annotation encoding="application/x-tex">\hookrightarrow \mathbf{H}</annotation></semantics></math> of <a class="existingWikiWord" href="/nlab/show/dimension">dimension</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi></mrow><annotation encoding="application/x-tex">n</annotation></semantics></math>. As discussed at <em><a class="existingWikiWord" href="/nlab/show/orthogonal+structure">orthogonal structure</a></em> and <em><a class="existingWikiWord" href="/nlab/show/vielbein">vielbein</a></em>, we are to regard <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> in the <a class="existingWikiWord" href="/nlab/show/context">context</a> of the <a class="existingWikiWord" href="/nlab/show/delooping">delooping</a> of the <a class="existingWikiWord" href="/nlab/show/general+linear+group">general linear group</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>∈</mo><mi>Grp</mi><mo stretchy="false">(</mo><mstyle mathvariant="bold"><mi>H</mi></mstyle><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">GL(n) \in Grp(\mathbf{H})</annotation></semantics></math> via its <a class="existingWikiWord" href="/nlab/show/tangent+bundle">tangent bundle</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi><mi>Σ</mi><mo>→</mo><mi>Σ</mi></mrow><annotation encoding="application/x-tex">T \Sigma \to \Sigma</annotation></semantics></math>, by which we always mean here the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">GL(n)</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/principal+bundle">principal bundle</a> to which the tangent bundle is <a class="existingWikiWord" href="/nlab/show/associated+bundle">associated</a>.</p> <p>By the discussion at <em><a class="existingWikiWord" href="/nlab/show/principal+%E2%88%9E-bundle">principal ∞-bundle</a></em> this is modulated by a morphism</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>Σ</mi><mover><mo>→</mo><mrow><mo>⊢</mo><mi>T</mi><mi>Σ</mi></mrow></mover><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>∈</mo><msub><mstyle mathvariant="bold"><mi>H</mi></mstyle> <mrow><mo stretchy="false">/</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow></msub></mrow><annotation encoding="application/x-tex"> (\Sigma \stackrel{\vdash T \Sigma}{\to} \mathbf{B} GL(n)) \in \mathbf{H}_{/\mathbf{B} GL(n)} </annotation></semantics></math></div> <p>to the <a class="existingWikiWord" href="/nlab/show/delooping">delooping</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{B}GL(n)</annotation></semantics></math> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">GL(n)</annotation></semantics></math> (the <a class="existingWikiWord" href="/nlab/show/moduli+stack">moduli stack</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">GL(n)</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/principal+bundles">principal bundles</a>) in that we have a <a class="existingWikiWord" href="/nlab/show/fiber+sequence">fiber sequence</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>T</mi><mi>Σ</mi></mtd> <mtd><mo>→</mo></mtd> <mtd><mi>Σ</mi></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd><msup><mo stretchy="false">↓</mo> <mpadded width="0"><mrow><mo>⊢</mo><mi>T</mi><mi>Σ</mi></mrow></mpadded></msup></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex"> \array{ T \Sigma &\to& \Sigma \\ && \downarrow^{\mathrlap{\vdash T \Sigma}} \\ && \mathbf{B}GL(n) } </annotation></semantics></math></div> <p>in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>H</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{H}</annotation></semantics></math>. (A detailed exposition of this and the following, with further pointers, is in (<a href="#SchreiberLectures">Schreiber, ESI lectures</a>).)</p> <p>Therefore the <a class="existingWikiWord" href="/nlab/show/syntax">syntax</a> of the tangent bundle as a <a class="existingWikiWord" href="/nlab/show/dependent+type">dependent type</a> is</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msup><mi>D</mi> <mi>n</mi></msup><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>⊢</mo><mi>T</mi><mi>Σ</mi><mo stretchy="false">(</mo><msup><mi>D</mi> <mi>n</mi></msup><mo stretchy="false">)</mo><mo>:</mo><mi>Type</mi></mrow><annotation encoding="application/x-tex"> D^n : \mathbf{B}GL(n) \vdash T \Sigma(D^n) : Type </annotation></semantics></math></div> <p>and since <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>D</mi> <mi>n</mi></msup></mrow><annotation encoding="application/x-tex">D^n</annotation></semantics></math> is essentially unique we will notationally suppress it in the <a class="existingWikiWord" href="/nlab/show/succedent">succedent</a> on the right and just write</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msup><mi>D</mi> <mi>n</mi></msup><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>⊢</mo><mi>T</mi><mi>Σ</mi><mo>:</mo><mi>Type</mi><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> D^n : \mathbf{B}GL(n) \vdash T \Sigma : Type \,. </annotation></semantics></math></div> <p>Let then</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>O</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mover><mo>→</mo><mstyle mathvariant="bold"><mi>orth</mi></mstyle></mover><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>∈</mo><msub><mstyle mathvariant="bold"><mi>H</mi></mstyle> <mrow><mo stretchy="false">/</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow></msub></mrow><annotation encoding="application/x-tex"> (\mathbf{B} O(n) \stackrel{\mathbf{orth}}{\to} \mathbf{B} GL(n)) \in \mathbf{H}_{/\mathbf{B}GL(n)} </annotation></semantics></math></div> <p>be the <a class="existingWikiWord" href="/nlab/show/delooping">delooping</a> of the inclusion <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>O</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>→</mo><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">O(n) \to GL(n)</annotation></semantics></math> of the <a class="existingWikiWord" href="/nlab/show/maximal+compact+subgroup">maximal compact subgroup</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">GL(n)</annotation></semantics></math>, the <a class="existingWikiWord" href="/nlab/show/orthogonal+group">orthogonal group</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>O</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">O(n)</annotation></semantics></math>, regarded as an <a class="existingWikiWord" href="/nlab/show/object">object</a> in the <a class="existingWikiWord" href="/nlab/show/slice-%28%E2%88%9E%2C1%29-topos">slice-(∞,1)-topos</a> over <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{B}GL(n)</annotation></semantics></math>. Since this sits in the <a class="existingWikiWord" href="/nlab/show/homotopy+fiber+sequence">homotopy fiber sequence</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo stretchy="false">/</mo><mi>O</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mtd> <mtd><mo>→</mo></mtd> <mtd><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>O</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd><msup><mo stretchy="false">↓</mo> <mpadded width="0"><mi>orth</mi></mpadded></msup></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex"> \array{ GL(n)/O(n) &\to& \mathbf{B}O(n) \\ && \downarrow^{\mathrlap{orth}} \\ && \mathbf{B}GL(n) } </annotation></semantics></math></div> <p>with the <a class="existingWikiWord" href="/nlab/show/coset">coset</a> <a class="existingWikiWord" href="/nlab/show/smooth+space">smooth space</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo stretchy="false">/</mo><mi>O</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">GL(n)/O(n)</annotation></semantics></math>, the <a class="existingWikiWord" href="/nlab/show/syntax">syntax</a> of this object is the <a class="existingWikiWord" href="/nlab/show/dependent+type">dependent type</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msup><mi>D</mi> <mi>n</mi></msup><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>⊢</mo><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo stretchy="false">/</mo><mi>O</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>Type</mi><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> D^n : \mathbf{B}GL(n) \vdash GL(n)/O(n) : Type \,. </annotation></semantics></math></div> <p>In view of the <a class="existingWikiWord" href="/nlab/show/equivalence+of+%28%E2%88%9E%2C1%29-categories">equivalence of (∞,1)-categories</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mstyle mathvariant="bold"><mi>H</mi></mstyle> <mrow><mo stretchy="false">/</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow></msub><mo>≃</mo><msub><mi>Act</mi> <mstyle mathvariant="bold"><mi>H</mi></mstyle></msub><mo stretchy="false">(</mo><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex"> \mathbf{H}_{/\mathbf{B}GL(n)} \simeq Act_{\mathbf{H}}(GL(n)) </annotation></semantics></math></div> <p>this expresses the canonical <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">GL(n)</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/%E2%88%9E-action">action</a> on the coset <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo stretchy="false">/</mo><mi>O</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">GL(n)/O(n)</annotation></semantics></math> (by mutliplication from the “other side”).</p> <p>The <a class="existingWikiWord" href="/nlab/show/syntax">syntax</a> of the <a class="existingWikiWord" href="/nlab/show/moduli+stack">moduli stack</a> of <a class="existingWikiWord" href="/nlab/show/vielbein">vielbein</a> fields / <a class="existingWikiWord" href="/nlab/show/Riemannian+metrics">Riemannian metrics</a> on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> is</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo>⊢</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><msup><mi>D</mi> <mi>n</mi></msup><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow></munder><mi>T</mi><mi>Σ</mi><mo>→</mo><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo stretchy="false">/</mo><mi>O</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>Type</mi><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> \vdash \prod_{D^n : \mathbf{B}GL(n)} T \Sigma \to GL(n)/O(n) : Type \,. </annotation></semantics></math></div> <p>This almost verbatim expresses the familiar statement:</p> <blockquote> <p>A <a class="existingWikiWord" href="/nlab/show/vielbein">vielbein</a> on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math> is a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">GL(n)</annotation></semantics></math>-equivariant map from <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi><mi>Σ</mi></mrow><annotation encoding="application/x-tex">T \Sigma</annotation></semantics></math> to the coset <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo stretchy="false">/</mo><mi>O</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">GL(n)/O(n)</annotation></semantics></math>.</p> </blockquote> <p>The <a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a> of such a <a class="existingWikiWord" href="/nlab/show/vielbein">vielbein</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>e</mi></mrow><annotation encoding="application/x-tex">e</annotation></semantics></math> is as a diagram</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>Σ</mi></mtd> <mtd></mtd> <mtd><mover><mo>→</mo><mrow></mrow></mover></mtd> <mtd></mtd> <mtd><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>O</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd></mtd> <mtd><mo>↘</mo></mtd> <mtd><msub><mo>⇙</mo> <mi>e</mi></msub></mtd> <mtd><msub><mo>↙</mo> <mpadded width="0"><mi>orth</mi></mpadded></msub></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mtd></mtr></mtable></mrow><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> \array{ \Sigma && \stackrel{}{\to}&& \mathbf{B}O(n) \\ & \searrow &\swArrow_{e}& \swarrow_{\mathrlap{orth}} \\ && \mathbf{B}GL(n) } \,. </annotation></semantics></math></div> <p>This in turn almost verbatim expresses the familar equivalent statement</p> <blockquote> <p>A vielbein is a <a class="existingWikiWord" href="/nlab/show/reduction+of+the+structure+group">reduction of the structure group</a> of the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">GL(n)</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/principal+bundle">principal bundle</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi><mi>Σ</mi></mrow><annotation encoding="application/x-tex">T \Sigma</annotation></semantics></math> along <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>O</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>→</mo><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">O(n) \to GL(n)</annotation></semantics></math>.</p> </blockquote> <p>This is still the naive space of fields, not yet generally covariant. So we next pass to the general covariant <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>T</mi><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{B}\mathbf{Aut}(T\Sigma)</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/context">context</a> and form the correct generally covariant space of fields, being the <a class="existingWikiWord" href="/nlab/show/type+in+context">type in context</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>T</mi><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{B} \mathbf{Aut}(T \Sigma)</annotation></semantics></math> given by</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Conf</mi></mstyle><mo>≔</mo><mo>⊢</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><msup><mi>D</mi> <mi>n</mi></msup><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow></munder><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>T</mi><mi>Σ</mi><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>T</mi><mi>Σ</mi><mo stretchy="false">)</mo></mrow></munder><mi>T</mi><mi>Σ</mi><mo>→</mo><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo stretchy="false">/</mo><mi>O</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>Type</mi><mspace width="thinmathspace"></mspace><mo>,</mo></mrow><annotation encoding="application/x-tex"> \mathbf{Conf} \coloneqq \vdash \prod_{D^n : \mathbf{B}GL(n)} \sum_{T\Sigma : \mathbf{B}\mathbf{Aut}(T\Sigma)} T \Sigma \to GL(n)/O(n) : Type \,, </annotation></semantics></math></div> <p>which is the integrated <a class="existingWikiWord" href="/nlab/show/BRST+complex">BRST complex</a> of Einstein gravity field configurations modulo diffeomorphism ghosts: the <a class="existingWikiWord" href="/nlab/show/smooth+infinity-groupoid">smooth groupoid</a> whose</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/objects">objects</a> are <a class="existingWikiWord" href="/nlab/show/vielbein">vielbein</a> fields <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>e</mi></mrow><annotation encoding="application/x-tex">e</annotation></semantics></math> on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi></mrow><annotation encoding="application/x-tex">X</annotation></semantics></math>;</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/morphisms">morphisms</a> are</p> <ol> <li> <p>orthogonal frame transformations of the fibers of the tangent bundle;</p> </li> <li> <p>general diffeomorphisms of the base <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Σ</mi></mrow><annotation encoding="application/x-tex">\Sigma</annotation></semantics></math>.</p> </li> </ol> </li> </ul> <p>We unwind this a bit more.</p> <p>A slight subtlety in interpreting the above expression is that in</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msup><mi>D</mi> <mi>n</mi></msup><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>⊢</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>Aut</mi><mo stretchy="false">(</mo><mi>T</mi><mi>Σ</mi><mo stretchy="false">)</mo><mo>:</mo><mi>Type</mi></mrow><annotation encoding="application/x-tex"> D^n : \mathbf{B}GL(n) \vdash \mathbf{B}Aut(T \Sigma) : Type </annotation></semantics></math></div> <p>the <a class="existingWikiWord" href="/nlab/show/automorphism+%E2%88%9E-group">automorphism ∞-group</a> of the tangent bundle it to be formed in the <a class="existingWikiWord" href="/nlab/show/context">context</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{B}GL(n)</annotation></semantics></math>. By the discussion at <em><a class="existingWikiWord" href="/nlab/show/automorphism+%E2%88%9E-group">automorphism ∞-group</a></em> the <a class="existingWikiWord" href="/nlab/show/delooping">delooping</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>Aut</mi><mo stretchy="false">(</mo><mi>T</mi><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{B}Aut(T \Sigma)</annotation></semantics></math> is the <a class="existingWikiWord" href="/nlab/show/%E2%88%9E-image">∞-image</a> of the name</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mo>*</mo><mover><mo>→</mo><mrow></mrow></mover><mi>Type</mi><mo stretchy="false">)</mo><mo>∈</mo><msub><mstyle mathvariant="bold"><mi>H</mi></mstyle> <mrow><mo stretchy="false">/</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow></msub></mrow><annotation encoding="application/x-tex"> (* \stackrel{}{\to} Type) \in \mathbf{H}_{/\mathbf{B}GL(n)} </annotation></semantics></math></div> <p>of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>Σ</mi><mo>→</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(\Sigma \to \mathbf{B}GL(n))</annotation></semantics></math> in the slice. By the discussion at <a href="over-%28infinity%2C1%29-topos#ObjectClassifier">slice-(∞,1)-topos – Object classifier</a> the <a class="existingWikiWord" href="/nlab/show/object+classifier">object classifier</a> in the slice is the <a class="existingWikiWord" href="/nlab/show/projection">projection</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>Type</mi><mo>×</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>→</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(Type \times \mathbf{B}GL(n) \to \mathbf{B}GL(n))</annotation></semantics></math>.</p> <p>So the name and its pullback are given by a diagram of the form</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>Σ</mi></mtd> <mtd></mtd> <mtd><mo>→</mo></mtd> <mtd></mtd> <mtd><mover><mi>Type</mi><mo>^</mo></mover><mo>×</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd><msup><mrow></mrow> <mpadded width="0" lspace="-100%width"><mrow></mrow></mpadded></msup><mo stretchy="false">↓</mo></mtd> <mtd></mtd> <mtd><mo>⇙</mo></mtd> <mtd></mtd> <mtd><mo stretchy="false">↓</mo></mtd></mtr> <mtr><mtd><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mtd> <mtd></mtd> <mtd><mover><mo>→</mo><mrow><mo stretchy="false">(</mo><mo>⊢</mo><mi>Σ</mi><mo>,</mo><mi>id</mi><mo stretchy="false">)</mo></mrow></mover></mtd> <mtd></mtd> <mtd><mi>Type</mi><mo>×</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd></mtd> <mtd><msub><mrow></mrow> <mpadded width="0" lspace="-100%width"><mi>id</mi></mpadded></msub><mo>↘</mo></mtd> <mtd><mo>⇙</mo></mtd> <mtd><mo>↙</mo></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex"> \array{ \Sigma &&\to&& \widehat{Type} \times \mathbf{B}GL(n) \\ {}^{\mathllap{}}\downarrow &&\swArrow&& \downarrow \\ \mathbf{B}GL(n) &&\stackrel{(\vdash \Sigma, id)}{\to}&& Type \times \mathbf{B}GL(n) \\ & {}_{\mathllap{id}}\searrow &\swArrow& \swarrow \\ && \mathbf{B}GL(n) } </annotation></semantics></math></div> <p>in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>H</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{H}</annotation></semantics></math>. Here the <a class="existingWikiWord" href="/nlab/show/%E2%88%9E-image">∞-image</a> is directly read off to be the factorization in the third column of</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>T</mi><mi>Σ</mi></mtd> <mtd><mo>→</mo></mtd> <mtd><mi>Σ</mi></mtd> <mtd><mo>→</mo></mtd> <mtd><mo stretchy="false">(</mo><mi>T</mi><mi>Σ</mi><mo>⫽</mo><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>T</mi><mi>Σ</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>×</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mtd> <mtd><mo>→</mo></mtd> <mtd><mover><mi>Type</mi><mo>^</mo></mover><mo>×</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd><mo stretchy="false">↓</mo></mtd> <mtd></mtd> <mtd><msup><mrow></mrow> <mpadded width="0" lspace="-100%width"><mrow></mrow></mpadded></msup><mo stretchy="false">↓</mo></mtd> <mtd></mtd> <mtd><mo stretchy="false">↓</mo></mtd> <mtd></mtd> <mtd><mo stretchy="false">↓</mo></mtd></mtr> <mtr><mtd><mo>*</mo></mtd> <mtd><mo>→</mo></mtd> <mtd><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mtd> <mtd><mover><mo>→</mo><mrow></mrow></mover></mtd> <mtd><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>T</mi><mi>Σ</mi><mo stretchy="false">)</mo><mo>×</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mtd> <mtd><mo>→</mo></mtd> <mtd><mi>Type</mi><mo>×</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><msub><mrow></mrow> <mpadded width="0" lspace="-100%width"><mi>id</mi></mpadded></msub><mo>↘</mo></mtd> <mtd><mo>⇙</mo></mtd> <mtd><mo>↙</mo></mtd></mtr> <mtr><mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd></mtd> <mtd><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mtd></mtr></mtable></mrow><mspace width="thinmathspace"></mspace><mo>,</mo></mrow><annotation encoding="application/x-tex"> \array{ T \Sigma &\to& \Sigma &\to& (T \Sigma \sslash \mathbf{Aut}(T\Sigma)) \times \mathbf{B}GL(n) &\to& \widehat{Type} \times \mathbf{B}GL(n) \\ \downarrow && {}^{\mathllap{}}\downarrow && \downarrow && \downarrow \\ * &\to& \mathbf{B}GL(n) &\stackrel{}{\to}& \mathbf{B}\mathbf{Aut}(T \Sigma) \times \mathbf{B}GL(n) &\to& Type \times \mathbf{B}GL(n) \\ && & {}_{\mathllap{id}}\searrow &\swArrow& \swarrow \\ && && \mathbf{B}GL(n) } \,, </annotation></semantics></math></div> <p>where each square and hence each rectangle is an <a class="existingWikiWord" href="/nlab/show/%28%E2%88%9E%2C1%29-pullback">(∞,1)-pullback</a> in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>H</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{H}</annotation></semantics></math>. This shows that the automorphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>∞</mn></mrow><annotation encoding="application/x-tex">\infty</annotation></semantics></math>-group of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi><mi>Σ</mi></mrow><annotation encoding="application/x-tex">T \Sigma</annotation></semantics></math> in the context of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{B}GL(n)</annotation></semantics></math> is just the absolute automorphism <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mn>∞</mn></mrow><annotation encoding="application/x-tex">\infty</annotation></semantics></math>-group freely <a class="existingWikiWord" href="/nlab/show/context+extension">context extended</a>. The <a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a> of the <a class="existingWikiWord" href="/nlab/show/dependent+type">dependent type</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msup><mi>D</mi> <mi>n</mi></msup><mo lspace="verythinmathspace">:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>,</mo><mi>T</mi><mi>Σ</mi><mo lspace="verythinmathspace">:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>T</mi><mi>Σ</mi><mo stretchy="false">)</mo><mo>⊢</mo><mi>T</mi><mi>Σ</mi><mo lspace="verythinmathspace">:</mo><mi>Type</mi></mrow><annotation encoding="application/x-tex"> D^n \colon \mathbf{B}GL(n), T \Sigma \colon \mathbf{B}\mathbf{Aut}(T \Sigma) \vdash T \Sigma \colon Type </annotation></semantics></math></div> <p>is the third column from the left in the above diagram. This means that the dependent sum in</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Conf</mi></mstyle><mo>≔</mo><mo>⊢</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∏</mo> <mrow><msup><mi>D</mi> <mi>n</mi></msup><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow></munder><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mrow><mi>T</mi><mi>Σ</mi><mo>:</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>T</mi><mi>Σ</mi><mo stretchy="false">)</mo></mrow></munder><mi>T</mi><mi>Σ</mi><mo>→</mo><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo stretchy="false">/</mo><mi>O</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo><mo>:</mo><mi>Type</mi><mspace width="thinmathspace"></mspace><mo>,</mo></mrow><annotation encoding="application/x-tex"> \mathbf{Conf} \coloneqq \vdash \prod_{D^n : \mathbf{B}GL(n)} \sum_{T\Sigma : \mathbf{B}\mathbf{Aut}(T\Sigma)} T \Sigma \to GL(n)/O(n) : Type \,, </annotation></semantics></math></div> <p>forms the internal hom in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mstyle mathvariant="bold"><mi>H</mi></mstyle> <mrow><mo stretchy="false">/</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow></msub></mrow><annotation encoding="application/x-tex">\mathbf{H}_{/\mathbf{B}GL(n)}</annotation></semantics></math> between the homotopy fiber of that third column formed in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mstyle mathvariant="bold"><mi>H</mi></mstyle> <mrow><mo stretchy="false">/</mo><mstyle mathvariant="bold"><mi>B</mi></mstyle><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow></msub></mrow><annotation encoding="application/x-tex">\mathbf{H}_{/\mathbf{B}GL(n)}</annotation></semantics></math>, which is the second column (and therefore now does rememeber the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>GL</mi><mo stretchy="false">(</mo><mi>n</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">GL(n)</annotation></semantics></math>-action on <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi><mi>Σ</mi></mrow><annotation encoding="application/x-tex">T \Sigma</annotation></semantics></math>) with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>orth</mi></mstyle></mrow><annotation encoding="application/x-tex">\mathbf{orth}</annotation></semantics></math>, rememeberting that the result has an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mstyle mathvariant="bold"><mi>Aut</mi></mstyle><mo stretchy="false">(</mo><mi>T</mi><mi>Σ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathbf{Aut}(T\Sigma)</annotation></semantics></math>-action by precomposition.</p> <h2 id="References">References</h2> <h3 id="ReferencesHistory">History</h3> <p>The pre-history of the idea of general covariance is reviewed in</p> <ul id="Alexander"> <li>H. G. Alexander (ed.), <em>The Leibniz-Clarke Correspondence: Together With Extracts from Newton’s Principia and Opticks</em>, Manchester University Press (1998)</li> </ul> <p>The original articles by Einstein on the idea of general covariance include his <em>Entwurf</em> (sketch)</p> <ul id="EinsteinGrossmann"> <li><a class="existingWikiWord" href="/nlab/show/Albert+Einstein">Albert Einstein</a>, M. Grossmann, <em>Entwurf einer verallgemeinerten Relativitätstheorie und einer Theorie der Gravitation</em> Zeitschrift für Math. Phys. 62, 225–259 (1914)</li> </ul> <p>of the theory of <a class="existingWikiWord" href="/nlab/show/gravity">gravity</a> (where the notion of general covariance is still rejected) and then the full development of <a class="existingWikiWord" href="/nlab/show/general+relativity">general relativity</a></p> <ul id="Einstein1916"> <li><a class="existingWikiWord" href="/nlab/show/Albert+Einstein">Albert Einstein</a>, <em>Die Grundlage der allgemeinen Relativitätstheorie. Ann. Phys. (Leipzig) 49, 769–822 (1916)</em></li> </ul> <p>where it is fully embraced.</p> <p>An attempt at a fairly comprehensive review of the history of the idea of general covariance and its reception up to modern days is in</p> <ul id="Norton"> <li>J. D. Norton, <em>General covariance and the foundations of general relativity: eight decades of dispute</em>, Rep. Prog. Phys <strong>56</strong> (1993), (<a href="http://www.pitt.edu/~jdnorton/papers/decades.pdf">original pdf</a>, <a href="http://www.pitt.edu/~jdnorton/papers/decades_re-set.pdf">reprint pdf</a>)</li> </ul> <h3 id="ReferencesFormalizations">Formalizations of general covariance</h3> <p>A formalization in the context of <a class="existingWikiWord" href="/nlab/show/AQFT">AQFT</a> is proposed and discussed in</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Klaus+Fredenhagen">Klaus Fredenhagen</a>, <a class="existingWikiWord" href="/nlab/show/Rudolf+Haag">Rudolf Haag</a>, <em>Generally covariant quantum field theory and scaling limits</em>, Comm. Math. Phys. Volume 108, Number 1 (1987), 91-115. (<a href="http://projecteuclid.org/euclid.cmp/1104116359">EUCLID</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Romeo+Brunetti">Romeo Brunetti</a>, <a class="existingWikiWord" href="/nlab/show/Klaus+Fredenhagen">Klaus Fredenhagen</a>, <a class="existingWikiWord" href="/nlab/show/Rainer+Verch">Rainer Verch</a>, <em>The generally covariant locality principle – A new paradigm for local quantum physics</em>, Commun.Math.Phys.237:31-68,2003 (<a href="http://arxiv.org/abs/math-ph/0112041">math-ph/0112041</a>)</p> </li> </ul> <p>A review is in</p> <ul id="BrunettiPorrmannRuzzi"> <li><a class="existingWikiWord" href="/nlab/show/Romeo+Brunetti">Romeo Brunetti</a>, Martin Porrmann, Giuseppe Ruzzi, <em>General Covariance in Algebraic Quantum Field Theory</em> (<a href="http://arxiv.org/abs/math-ph/0512059">arXiv:math-ph/0512059</a>)</li> </ul> <p>For more see the references at <em><a class="existingWikiWord" href="/nlab/show/AQFT+on+curved+spacetimes">AQFT on curved spacetimes</a></em>.</p> <p>Via <a class="existingWikiWord" href="/nlab/show/quotient+stacks">quotient stacks</a> in <a class="existingWikiWord" href="/nlab/show/BV-formalism">BV-formalism</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Filip+Dul">Filip Dul</a>: <em>General Covariance from the Viewpoint of Stacks</em>, Lett Math Phys 113 (2023) 30 [<a href="https://arxiv.org/abs/2112.15473">arXiv:2112.15473</a>, <a href="https://doi.org/10.1007/s11005-023-01653-3">doi:10.1007/s11005-023-01653-3</a>]</li> </ul> <h3 id="FormalizationInHomtopyTypeTheory">Formalization in homotopy type theory</h3> <p>Background and context for the above formalization of <a class="existingWikiWord" href="/nlab/show/classical+field+theory">classical</a>/<a class="existingWikiWord" href="/nlab/show/quantum+field+theory">quantum field theory</a> in <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a> see</p> <ul id="SchreiberLectures"> <li><a class="existingWikiWord" href="/nlab/show/Urs+Schreiber">Urs Schreiber</a>, <em><a class="existingWikiWord" href="/nlab/show/twisted+smooth+cohomology+in+string+theory">twisted smooth cohomology in string theory</a></em>, Lectures at <em><a href="http://maths-old.anu.edu.au/esi/2012/">ESI program on K-theory and quantum fields</a></em> (2012)</li> </ul> <ul id="SchreiberShulman"> <li><a class="existingWikiWord" href="/nlab/show/Urs+Schreiber">Urs Schreiber</a>, <a class="existingWikiWord" href="/nlab/show/Mike+Shulman">Mike Shulman</a>, <em><a class="existingWikiWord" href="/schreiber/show/Quantum+gauge+field+theory+in+Cohesive+homotopy+type+theory">Quantum gauge field theory in Cohesive homotopy type theory</a></em> (2012)</li> </ul> <p>See also <em><a class="existingWikiWord" href="/nlab/show/higher+category+theory+and+physics">higher category theory and physics</a></em>.</p> </body></html> </div> <div class="revisedby"> <p> Last revised on February 18, 2025 at 10:31:30. See the <a href="/nlab/history/general+covariance" style="color: #005c19">history</a> of this page for a list of all contributions to it. </p> </div> <div class="navigation navfoot"> <a href="/nlab/edit/general+covariance" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/4199/#Item_27">Discuss</a><span class="backintime"><a href="/nlab/revision/general+covariance/29" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/general+covariance" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/general+covariance" accesskey="S" class="navlink" id="history" rel="nofollow">History (29 revisions)</a> <a href="/nlab/show/general+covariance/cite" style="color: black">Cite</a> <a href="/nlab/print/general+covariance" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/general+covariance" id="view_source" rel="nofollow">Source</a> </div> </div>  </div>  </body> </html>