\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{geometry of physics -- differential forms}

\begin{quote}%
This entry contains one chapter of the material at \emph{[[geometry of physics]]}.

previous chapter: \emph{[[geometry of physics -- smooth sets|smooth sets]]}

next chapter: \emph{[[geometry of physics -- integration|integration]]}


\end{quote}
\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{physics}{}\paragraph*{{Physics}}\label{physics}

[[!include physicscontents]]

\hypertarget{differential_geometry}{}\paragraph*{{Differential geometry}}\label{differential_geometry}

[[!include synthetic differential geometry - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{Differentiation}{\textbf{Differentiation}}\dotfill \pageref*{Differentiation} \linebreak
\noindent\hyperlink{DifferentialFormsLayerMod}{Model Layer}\dotfill \pageref*{DifferentialFormsLayerMod} \linebreak
\noindent\hyperlink{DifferentialFormsOnAbstractCoordinateSystem}{Differential forms on abstract coordinate systems}\dotfill \pageref*{DifferentialFormsOnAbstractCoordinateSystem} \linebreak
\noindent\hyperlink{SmoothUniversalModuliSpaceOfDifferentialForms}{Differential forms on smooth spaces}\dotfill \pageref*{SmoothUniversalModuliSpaceOfDifferentialForms} \linebreak
\noindent\hyperlink{DifferentialFormsLayerSem}{Semantic Layer}\dotfill \pageref*{DifferentialFormsLayerSem} \linebreak
\noindent\hyperlink{ConcreteObjects}{Concrete smooth spaces}\dotfill \pageref*{ConcreteObjects} \linebreak
\noindent\hyperlink{SmoothModuliSpaceOfDifferentialForms}{Smooth moduli space of differential forms on a smooth space}\dotfill \pageref*{SmoothModuliSpaceOfDifferentialForms} \linebreak
\noindent\hyperlink{DifferentialFormsLayerSyn}{Syntactic Layer}\dotfill \pageref*{DifferentialFormsLayerSyn} \linebreak
\noindent\hyperlink{images}{Images}\dotfill \pageref*{images} \linebreak


\hypertarget{Differentiation}{}\subsection*{{\textbf{Differentiation}}}\label{Differentiation}

We introduce the standard concept of \emph{[[nLab:differential forms]]} in \emph{\hyperlink{DifferentialFormsLayerMod}{Model Layer}}, adding to the traditional discussion a precise version of the statement that differential forms are equivalently ``incremental smooth $n$-dimensional measures'', which accurately captures the role that they play in [[physics]], notably in [[local action functionals]].

We define differential forms on general smooth spaces seamlessly in terms of the smooth [[moduli space]] $\Omega^\in \in Smooth0Type$ of differential forms. This has the special property that it is, for $n \geq 1$, a \emph{non-[[concrete object|concrete]]} smooth space. In \emph{\hyperlink{DifferentialFormsLayerSem}{Semantic Layer}} below we take this as occasion to discuss the notion of [[concrete objects]] in a [[local topos]], such as the topos of smooth spaces. We show how the \emph{concretification} of the smooth mapping space $[X,\Omega^n]$ for any smooth space $X$ is the \emph{smooth (moduli) space of differential forms on $X$}. Below in \emph{\hyperlink{ActionFunctionalsForChernSimonsTypeGaugeTheories}{Action functionals for Chern-Simons type gauge theories}} the theory of \emph{concretification} in a local topos is a central ingredient in the \emph{canonical existence} of certain [[nLab:action functionals]].

The process of concretification involves the general abstract notion of \emph{[[image|images]]}. The type-theory of this notion we discuss in \hyperlink{DifferentialFormsLayerSyn}{Syntactic Layer} here.

\hypertarget{DifferentialFormsLayerMod}{}\subsubsection*{{Model Layer}}\label{DifferentialFormsLayerMod}

We have seen above in \emph{\href{TheContinuumRealWorldLine}{The continuum real (world-)line}} that that [[real line]] $\mathbb{R}$ is the basic [[kinematics|kinematical structure]] in the [[differential geometry]] of [[physics]]. Notably the smooth [[path spaces]] $[\mathbb{R}, X]$ from example \ref{SmoothPathSpace} are to be thought of as the smooth spaces of \emph{trajectories} (for instance of some [[particle]]) in a [[smooth space]] $X$, hence of smooth maps $\mathbb{R} \to X$.

But moreover, \emph{[[dynamics]]} in [[physics]] is encoded by \emph{[[linear functionals|functionals]] on such trajectories}: by ``[[action functionals]]''. In the simplest case these are for instance homomorphisms of smooth spaces

\begin{displaymath}
S \colon \left[I, X\right] \to \mathbb{R}
  \,,
\end{displaymath}
where $I \hookrightarrow \mathbb{R}$ is the standard unit [[interval]].

Such [[action functionals]] we discuss in their own right in \emph{\hyperlink{VariationalCalculus}{Variational calculus}} below. Here we first examine in detail a fundamental property they all have: they are supposed to be \emph{[[local action functional|local]]}.

Foremost this means that the value associated to a trajectory is \emph{built up incrementally} from small contributions associated to small sub-trajectories: if a trajectory $\gamma$ is decomposed as a trajectory $\gamma_1$ followed by a trajectory $\gamma_2$, then the action functional is additive

\begin{displaymath}
S(\gamma) = S(\gamma_1) + S(\gamma_2)
  \,.
\end{displaymath}
As one takes this property to the limit of iterative subdivision, one finds that action functionals are entirely determined by their value on \emph{[[infinitesimal space|infinitesimal]] displacements} along the worldline. If $\gamma \colon \mathbb{R} \to X$ denotes a path and ``$\dot \gamma(x)$'' denotes the corresponding ``infinitesimal path'' at worldline parameter $x$, then the value of the action functional on such an infinitesimal path is traditionally written as

\begin{displaymath}
\mathbf{d}S(\dot \gamma)_x  \in \mathbb{R}
  \,,
\end{displaymath}
to be read as ``the small change $\mathbf{d}S$ of $S$ along the infinitesimal path $\dot \gamma_x$''.

This function $\mathbf{d}S$ that assigns numbers to infinitesimal paths is called a \emph{[[differential form]]}. Etymologically this originates in the use of ``form'' as in \emph{[[bilinear form]]}: something that is evaluated. Here it is evaluated on \emph{infinitesimal differences}, referred to as \emph{differentials}.

We define smooth differential forms on [[Cartesian spaces]] in

\begin{itemize}%
\item \emph{\hyperlink{DifferentialFormsOnAbstractCoordinateSystem}{Differential forms on abstract coordinate sysetms}}

\end{itemize}
Then we discuss how this induces a notion of smooth differential forms on general [[smooth spaces]] in

\begin{itemize}%
\item \emph{\hyperlink{SmoothUniversalModuliSpaceOfDifferentialForms}{Smooth universal moduli space of differential forms}}.

\end{itemize}
Further below we provide a precise version of the statement that ``Differential 1-forms are differential measures along paths.'' in

\begin{itemize}%
\item \emph{\hyperlink{1FormsAsSmoothFunctors}{Differential 1-forms are smooth incremental path measures}}.

\end{itemize}
\hypertarget{DifferentialFormsOnAbstractCoordinateSystem}{}\paragraph*{{Differential forms on abstract coordinate systems}}\label{DifferentialFormsOnAbstractCoordinateSystem}

We introduce the basic concept of a smooth [[differential form]] on a [[Cartesian space]] $\mathbb{R}^n$. Below in \emph{\hyperlink{SmoothUniversalModuliSpaceOfDifferentialForms}{Differential forms on smooth spaces}} we use this to define differential forms on any [[smooth space]].

\begin{defn}
\label{Differential1FormsOnCartesianSpaces}\hypertarget{Differential1FormsOnCartesianSpaces}{}
For $n \in \mathbb{N}$ a \textbf{[[smooth differential 1-form]]} $\omega$ on a [[Cartesian space]] $\mathbb{R}^n$ is an $n$-[[tuple]]

\begin{displaymath}
\left(\omega_i \in CartSp\left(\mathbb{R}^n,\mathbb{R}\right)\right)_{i = 1}^n
\end{displaymath}
of [[smooth functions]], which we think of equivalently as the [[coefficients]] of a [[formal linear combination]]

\begin{displaymath}
\omega = \sum_{i = 1}^n f_i \mathbf{d}x^i
\end{displaymath}
on a [[set]] $\{\mathbf{d}x^1, \mathbf{d}x^2, \cdots, \mathbf{d}x^n\}$ of [[cardinality]] $n$.

Write

\begin{displaymath}
\Omega^1(\mathbb{R}^k) \simeq CartSp(\mathbb{R}^k, \mathbb{R})^{\times k}\in Set
\end{displaymath}
for the set of smooth [[differential 1-forms]] on $\mathbb{R}^k$.

\end{defn}
\begin{remark}
\label{}\hypertarget{}{}
We think of $\mathbf{d} x^i$ as a measure for [[infinitesimal space|infinitesimal]] displacements along the $x^i$-[[coordinate]] of a [[Cartesian space]]. This idea is made precise below in \emph{\hyperlink{1FormsAsSmoothFunctors}{Differential 1-forms are smooth increnemental path measures}}.

\end{remark}
If we have a measure of infintesimal displacement on some $\mathbb{R}^n$ and a smooth function $f \colon \mathbb{R}^{\tilde n} \to \mathbb{R}^n$, then this induces a measure for infinitesimal displacement on $\mathbb{R}^{\tilde n}$ by sending whatever happens there first with $f$ to $\mathbb{R}^n$ and then applying the given measure there. This is captured by the following definition.

\begin{defn}
\label{PullbackOfDifferential1FormsOnCartesianSpaces}\hypertarget{PullbackOfDifferential1FormsOnCartesianSpaces}{}
For $\phi \colon \mathbb{R}^{\tilde k} \to \mathbb{R}^k$ a [[smooth function]], the \textbf{[[pullback of differential forms|pullback of differential 1-forms]]} along $\phi$ is the [[function]]

\begin{displaymath}
\phi^* \colon \Omega^1(\mathbb{R}^{k}) \to \Omega^1(\mathbb{R}^{\tilde k})
\end{displaymath}
between sets of differential 1-forms, def. \ref{Differential1FormsOnCartesianSpaces}, which is defined on [[basis]]-elements by

\begin{displaymath}
\phi^* \mathbf{d} x^i \coloneqq \sum_{j = 1}^{\tilde k} \frac{\partial \phi^i}{\partial \tilde x^j} \mathbf{d}\tilde x^j
\end{displaymath}
and then extended linearly by

\begin{displaymath}
\begin{aligned}
    \phi^* \omega & = \phi^* \left( \sum_{i} \omega_i \mathbf{d}x^i \right)
    \\
    & \coloneqq
     \sum_{i = 1}^k \left(\phi^* \omega\right)_i \sum_{j = 1}^{\tilde k} \frac{\partial \phi^i }{\partial \tilde x^j}  \mathbf{d} \tilde x^j 
    \\
    & = 
     \sum_{i = 1}^k  \sum_{j = 1}^{\tilde k} (\omega_i \circ \phi) \cdot \frac{\partial \phi^i }{\partial \tilde x^j}  \mathbf{d} \tilde x^j 
  \end{aligned}
  \,.
\end{displaymath}
\end{defn}
\begin{remark}
\label{}\hypertarget{}{}
The term ``pullback'' in \emph{[[pullback of differential forms]]} is not really related, certainly not historically, to the term \emph{[[pullback]]} in [[category theory]]. One can relate the pullback of differential forms to categorical pullbacks, but this is not really essential here. The most immediate property that both concepts share is that they take a [[morphism]] going in one direction to a map between structures over domain and codomain of that morphism which goes in the other direction, and in this sense one is ``pulling back structure along a morphism'' in both cases.

\end{remark}
Even if in the above definition we speak only about the [[set]] $\Omega^1(\mathbb{R}^k)$ of differential 1-forms, this set naturally carries further [[structure]].

\begin{defn}
\label{ModuleStructureOn1FormsOnRk}\hypertarget{ModuleStructureOn1FormsOnRk}{}
\begin{enumerate}%
\item The set $\Omega^1(\mathbb{R}^k)$ is naturally an [[abelian group]] with addition given by componentwise addition

\begin{displaymath}
\begin{aligned}
      \omega + \lambda & =
    \sum_{i = 1}^k \omega_i \mathbf{d}x^i + \sum_{j = 1}^k \lambda_j \mathbf{d}x^j
      \\
      & = \sum_{i = 1}^k(\omega_i + \lambda_i) \mathbf{d}x^i
   \end{aligned}
   \,,
\end{displaymath}

\item The abelian group $\Omega^1(\mathbb{R}^k)$ is naturally equipped with the structure of a [[module]] over the [[ring]] $C^\infty(\mathbb{R}^k,\mathbb{R}) = CartSp(\mathbb{R}^k, \mathbb{R})$ of [[smooth functions]], where the [[action]] $C^\infty(\mathbb{R}^k,\mathbb{R}) \times\Omega^1(\mathbb{R}^k) \to \Omega^1(\mathbb{R}^k)$ is given by componentwise multiplication

\begin{displaymath}
f \cdot \omega = \sum_{i = 1}^k( f \cdot \omega_i) \mathbf{d}x^i
  \,.
\end{displaymath}


\end{enumerate}
\end{defn}
\begin{defn}
\label{}\hypertarget{}{}
More abstractly, this just says that $\Omega^1(\mathbb{R}^k)$ is the [[free module]] over $C^\infty(\mathbb{R}^k)$ on the set $\{\mathbf{d}x^i\}_{i = 1}^k$.

\end{defn}
The following definition captures the idea that if $\mathbf{d} x^i$ is a measure for displacement along the $x^i$-[[coordinate]], and $\mathbf{d}x^j$ a measure for displacement along the $x^j$ coordinate, then there should be a way te get a measure, to be called $\mathbf{d}x^i \wedge \mathbf{d} x^j$, for infinitesimal \emph{surfaces} (squares) in the $x^i$-$x^j$-plane. And this should keep track of the [[orientation]] of these squares, whith

\begin{displaymath}
\mathbf{d}x^j \wedge \mathbf{d}x^i = - \mathbf{d}x^i \wedge \mathbf{d} x^j
\end{displaymath}
being the same infinitesimal measure with orientation reversed.

\begin{defn}
\label{DifferentialnForms}\hypertarget{DifferentialnForms}{}
For $k,n \in \mathbb{N}$, the \textbf{smooth [[differential forms]]} on $\mathbb{R}^k$ is the [[exterior algebra]]

\begin{displaymath}
\Omega^\bullet(\mathbb{R}^k) 
   \coloneqq
  \wedge^\bullet_{C^\infty(\mathbb{R}^k)} \Omega^1(\mathbb{R}^k)
\end{displaymath}
over the [[ring]] $C^\infty(\mathbb{R}^k)$ of [[smooth functions]] of the [[module]] $\Omega^1(\mathbb{R}^k)$ of smooth 1-forms, prop. \ref{ModuleStructureOn1FormsOnRk}.

We write $\Omega^n(\mathbb{R}^k)$ for the sub-module of degree $n$ and call its elements the \textbf{smooth [[differential n-forms]]}.

\end{defn}
\begin{remark}
\label{}\hypertarget{}{}
Explicitly this means that a [[differential n-form]] $\omega \in \Omega^n(\mathbb{R}^k)$ on $\mathbb{R}^k$ is a [[formal linear combination]] over $C^\infty(\mathbb{R}^k)$ of [[basis]] elements of the form $\mathbf{d} x^{i_1} \wedge \cdots \wedge \mathbf{d}x^{i_n}$ for $i_1 \lt i_2 \lt \cdots \lt i_n$:

\begin{displaymath}
\omega = \sum_{1 \leq i_1 \lt i_2 \lt \cdots \lt i_n \lt k} \omega_{i_1, \cdots, i_n} \mathbf{d}x^{i_1} \wedge \cdots \wedge \mathbf{d}x^{i_n}
  \,.
\end{displaymath}
\end{remark}
\begin{defn}
\label{PullbackOfDifferentialForms}\hypertarget{PullbackOfDifferentialForms}{}
The [[pullback of differential forms|pullback of differential 1-forms]] of def. \ref{Differential1FormsOnCartesianSpaces} extends as an $C^\infty(\mathbb{R}^k)$-[[associative algebra|algebra]] [[homomorphism]] to $\Omega^n(-)$, given for a smooth function $f \colon \mathbb{R}^{\tilde k} \to \mathbb{R}^k$ on basis elements by

\begin{displaymath}
f^* \left(  \mathbf{d}x^{i_1} \wedge \cdots \wedge \mathbf{d}x^{i_n} \right)
  = 
  \left(f^* \mathbf{d}x^{i_1} \wedge \cdots \wedge f^* \mathbf{d}x^{i_n} \right)
  \,.
\end{displaymath}
\end{defn}
\hypertarget{SmoothUniversalModuliSpaceOfDifferentialForms}{}\paragraph*{{Differential forms on smooth spaces}}\label{SmoothUniversalModuliSpaceOfDifferentialForms}

Above we have defined differential $n$-form on abstract coordinate systems. Here we extend this definition to one of differential $n$-forms on arbitrary [[smooth spaces]]. We start by observing that the space of \emph{all} differential $n$-forms on cordinate systems themselves naturally is a smooth space.

\begin{prop}
\label{}\hypertarget{}{}
The assignment of differential $n$-forms

\begin{displaymath}
\Omega^n(-) \colon \mathbb{R}^k \mapsto \Omega^n(\mathbb{R}^k)
\end{displaymath}
of def. \ref{DifferentialnForms} together with the [[pullback of differential forms]]-functions of def. \ref{PullbackOfDifferentialForms}

\begin{displaymath}
\itexarray{
    \mathbb{R}^{k_1} &\mapsto & \Omega^1(\mathbb{R}^{k_1})
    \\
    \uparrow^{\mathrlap{f}} && \downarrow^{\mathrlap{f^*}}
    \\
    \mathbb{R}^{k_2} &\mapsto& \Omega^1(\mathbb{R}^{k_2})
  }
\end{displaymath}
defines a [[smooth space]] in the sense of def. \ref{SmoothSpace}:

\begin{displaymath}
\Omega^n(-) \in Smooth0Type
  \,.
\end{displaymath}
\end{prop}
\begin{defn}
\label{SmoothModuliSpaceOfnForms}\hypertarget{SmoothModuliSpaceOfnForms}{}
We call this

\begin{displaymath}
\Omega^n \colon Smooth0Type
\end{displaymath}
the \textbf{universal smooth [[moduli space]]} of differential $n$-forms.

\end{defn}
The reason for this terminology is that homomorphisms of smooth spaces into $\Omega^1$ \emph{modulate} differential $n$-forms on their [[domain]], by prop. \ref{YonedaForSmoothSpaces} (and hence by the [[Yoneda lemma]]):

\begin{example}
\label{}\hypertarget{}{}
For the [[Cartesian space]] $\mathbb{R}^k$ regarded as a smooth space by example \ref{CartesianSpaceAsSmoothSpace}, there is a [[natural bijection]]

\begin{displaymath}
\Omega^n(\mathbb{R}^k) \simeq Hom(\mathbb{R}^k, \Omega^1)
\end{displaymath}
between the set of smooth $n$-forms on $\mathbb{R}^n$ according to def. \ref{Differential1FormsOnCartesianSpaces} and the set of homomorphism of smooth spaces, $\mathbb{R}^k \to \Omega^1$, according to def. \ref{HomomorphismOfSmoothSpaces}.

\end{example}
In view of this we have the following elegant definition of smooth $n$-forms on an arbitrary smooth space.

\begin{defn}
\label{DifferentialnFormOnSmoothSpace}\hypertarget{DifferentialnFormOnSmoothSpace}{}
For $X \in Smooth0Type$ a [[smooth space]], def. \ref{SmoothSpace}, a \textbf{[[differential n-form]]} on $X$ is a [[homomorphism]] of [[smooth spaces]] of the form

\begin{displaymath}
\omega \colon X \to \Omega^n(-)
  \,.
\end{displaymath}
Accordingly we write

\begin{displaymath}
\Omega^n(X) \coloneqq Smooth0Type(X,\Omega^n)
\end{displaymath}
for the set of smooth $n$-forms on $X$.

\end{defn}
We may unwind this definition to a very explicit description of differential forms on smooth spaces. This we do in a moment in remark \ref{DifferentialFormOnSmoothSpaceAsSystemOfDiffFormsOnCoordinates}.

Notice that differential 0-forms are equivalently smooth $\mathbb{R}$-valued functions.

\begin{prop}
\label{SpaceOf0FormsIsRealLine}\hypertarget{SpaceOf0FormsIsRealLine}{}
$\Omega^0 \simeq \mathbb{R}$

\end{prop}
\begin{defn}
\label{PullbackOfDifferentialFormsOnSmoothSpaces}\hypertarget{PullbackOfDifferentialFormsOnSmoothSpaces}{}
For $f \colon X \to Y$ a [[homomorphism]] of [[smooth spaces]], def. \ref{HomomorphismOfSmoothSpaces}, the \textbf{[[pullback of differential forms]]} along $f$ is the [[function]]

\begin{displaymath}
f^* \colon \Omega^n(Y) \to \Omega^n(X)
\end{displaymath}
given by the [[hom-functor]] into the smooth space $\Omega^n$ of def. \ref{SmoothModuliSpaceOfnForms}:

\begin{displaymath}
f^* \coloneqq Hom(-, \Omega^n)
 \,.
\end{displaymath}
This means that it sends an $n$-form $\omega \in \Omega^n(Y)$ which is modulated by a homomorphism $Y \to \Omega^n$ to the $n$-form $f^* \omega \in \Omega^n(X)$ which is modulated by the [[composition|composite]] $X \stackrel{f}{\to} Y \to \Omega^n$.

\end{defn}
\begin{defn}
\label{}\hypertarget{}{}
For $X = \mathbb{R}^{\tilde k}$ and $Y = \mathbb{R}^{k}$ definition \ref{PullbackOfDifferentialFormsOnSmoothSpaces} reproduces def. \ref{PullbackOfDifferentialForms}.

\end{defn}
\begin{proof}
Again by the [[Yoneda lemma]].

\end{proof}
\begin{remark}
\label{DifferentialFormOnSmoothSpaceAsSystemOfDiffFormsOnCoordinates}\hypertarget{DifferentialFormOnSmoothSpaceAsSystemOfDiffFormsOnCoordinates}{}
Using def. \ref{PullbackOfDifferentialFormsOnSmoothSpaces}

Unwinding def. \ref{DifferentialnFormOnSmoothSpace} yields the following explicit description:

a differential $n$-form $\omega \in \Omega^n(X)$ on a smooth space $X$ is

\begin{enumerate}%
\item for each way $\phi \colon \mathbb{R}^k \to X$ of laying out a coordinate system $\mathbb{R}^k$ in $X$ a differential $n$-form

\begin{displaymath}
\phi^* \omega \in \Omega^n(\mathbb{R}^k)
\end{displaymath}
on the abstract coordinate system, as given by def. \ref{DifferentialnForms};


\item for each abstract [[coordinate transformation]] $f \colon \mathbb{R}^{k_2} \to \mathbb{R}^{k_1}$ a corresponding compatibility condition between local differential forms $\phi_1 \colon \mathbb{R}^{k_1} \to X$ and $\phi_2 \colon \mathbb{R}^{k_2} \to X$ of the form

\begin{displaymath}
f^* \phi_1^* \omega = \phi_2^* \omega
  \,.
\end{displaymath}


\end{enumerate}
Hence a differential form on a smooth space is simply a collection of differential forms on all its coordinate systems such that these glue along all possible coordinate transformations.

\end{remark}
The following adds further explanation to the role of $\Omega^n \in Smooth0Tye$ as a \emph{[[moduli space]]}. Notice that since $\Omega^n$ is itself a [[smooth space]], we may speak about differential $n$-forms on $\Omega^n$ itsefl.

\begin{defn}
\label{UniversalDifferentialnForm}\hypertarget{UniversalDifferentialnForm}{}
The \textbf{universal differential $n$-forms} is the differential $n$-form

\begin{displaymath}
\omega^n_{univ} \in \Omega^n(\Omega^n)
\end{displaymath}
which is modulated by the [[identity]] [[homomorphism]] $id \colon \Omega^n \to \Omega^n$.

\end{defn}
With this definition we have:

\begin{prop}
\label{}\hypertarget{}{}
For $X \in Smooth0Type$ any [[smooth space]], every differential $n$-form on $X$, $\omega \in \Omega^n(X)$ is the pullback of differential forms, def. \ref{PullbackOfDifferentialFormsOnSmoothSpaces}, of the universal differential $n$-form, def. \ref{UniversalDifferentialnForm}, along a homomorphism $f$ from $X$ into the moduli space $\Omega^n$ of differential $n$-forms:

\begin{displaymath}
\omega = f^* \omega^n_{univ}
  \,.
\end{displaymath}
\end{prop}
\begin{remark}
\label{}\hypertarget{}{}
This statement is of course in a way a big tautology. Nevertheless it is a very useful tautology to make explicit. The whole concept of differential forms on smooth spaces here may be thought of as simply a variation of the theme of the [[Yoneda lemma]].

\end{remark}
\hypertarget{}{}\paragraph*{{\{\}}}\label{}

This ends the Model-layer discussion of differential forms. We now pass to a more advanced discussion of this topic in the \hyperlink{DifferentialFormsLayerSem}{Semantics layer below}. The reader wishing to stick to more elementary discussion for the time being should skip ahead to the Model-layer discussion of \hyperlink{Differentiation}{differentiation below}.

\hypertarget{DifferentialFormsLayerSem}{}\subsubsection*{{Semantic Layer}}\label{DifferentialFormsLayerSem}

\hypertarget{ConcreteObjects}{}\paragraph*{{Concrete smooth spaces}}\label{ConcreteObjects}

The smooth universal moduli space of differential forms $\Omega^n(-)$ from def. \ref{SmoothModuliSpaceOfnForms} is noteworthy in that it has a property not shared by many smooth spaces that one might think of more naively: while evidently being ``large'' (the space of all differential forms!) it has ``very few points'' and ``very few $k$-dimensional subspaces'' for low $k$. In fact

\begin{prop}
\label{}\hypertarget{}{}
For $k \lt n$ the smooth space $\Omega^n$ admits only a unique probe by $\mathbb{R}^k$:

\begin{displaymath}
Hom(\mathbb{R}^k, \Omega^n(-))
  \simeq
  \Omega^n(\mathbb{R}^k)
  = 
  \{0\}
  \,.
\end{displaymath}
\end{prop}
\begin{proof}
By the [[Yoneda lemma]] a smooth morphism $\mathbb{R}^k \to \Omega^n$ is a [[differential n-form]] $\omega \in \Omega^n(\mathbb{R}^k)$. But for $n \gt k$ there is only the 0 element.

\end{proof}
So while $\Omega^n()$ is a large smooth space, it is ``not supported on probes'' in low dimensions in as much as one might expect, from more naive notions of smooth spaces.

We now formalize this. The formal notion of an smooth space which \emph{is} supported on its probes is that of a \emph{[[concrete object]]}. There is a univeral map that sends any smooth space to its \emph{concretification}. The universal moduli spaces of differential forms turn out to be \emph{non-concrete} in that their concetrification is the point.

\begin{defn}
\label{ConcreteObjectsAndConcretification}\hypertarget{ConcreteObjectsAndConcretification}{}
Let $\mathbf{H}$ be a [[local topos]]. Write $\sharp \colon \mathbf{H} \to \mathbf{H}$ for the corresponding sharp modality, def. \ref{SharpModalityOfLocalTopos}. Then.

\begin{enumerate}%
\item An object $X \in \mathbf{H}$ is called a \textbf{[[concrete object]]} if

\begin{displaymath}
DeCoh_X \colon X \to \sharp X
\end{displaymath}
is a [[monomorphism]].


\item For $X \in \mathbf{H}$ any object, its \textbf{concretification} $Conc(X) \in \mathbf{H}$ is the [[image]] factorization of $DeCoh_X$, hence the factorization into an [[epimorphism]] followed by a [[monomorphism]]

\begin{displaymath}
DeCoh_X : X \to Conc(X) \hookrightarrow \sharp X
  \,.
\end{displaymath}


\end{enumerate}
\end{defn}
\begin{remark}
\label{}\hypertarget{}{}
Hence the concretification $Conc(X)$ of an object $X$ is itself a [[concrete object]] and it is [[universal property|universal]] with this property. (\ldots{})

\end{remark}
\begin{prop}
\label{DecohesOverASiteWithTerminalObject}\hypertarget{DecohesOverASiteWithTerminalObject}{}
Let $C$ be a [[site]] of definition for the [[local topos]] $\mathbf{H}$, with [[terminal object]] $*$. Then for $X \colon C^{op} \to Set$ a sheaf, $DeCoh_X$ is given over $U \in C$ by

\begin{displaymath}
X(U)
  \underoverset{Yoneda}{\simeq}{\to}
  \mathbf{H}(U, X)
  \stackrel{\Gamma_{U,X}}{\to}
  Set(\Gamma(U),\Gamma(X))
  \,.
\end{displaymath}
\end{prop}
\begin{prop}
\label{}\hypertarget{}{}
For $n \geq 1$ we have

\begin{displaymath}
Conc(\Omega^n) \simeq *
  \,.
\end{displaymath}
\end{prop}
In this sense the smooth moduli space of differential $n$-forms is \emph{maximally non-concrete}.

\hypertarget{SmoothModuliSpaceOfDifferentialForms}{}\paragraph*{{Smooth moduli space of differential forms on a smooth space}}\label{SmoothModuliSpaceOfDifferentialForms}

We discuss the smooth space of differential forms \emph{on a fixed smooth space} $X$.

\begin{remark}
\label{}\hypertarget{}{}
For $X$ a [[smooth space]], the smooth mapping space $[X, \Omega^n] \in Smooth0Type$ is the smooth space whose $\mathbb{R}^k$-plots are differential $n$-forms on the [[product]] $X \times \mathbb{R}^k$

\begin{displaymath}
[X, \Omega^n] \colon \mathbb{R}^k \mapsto \Omega^n(X \times \mathbb{R}^k)
  \,.
\end{displaymath}
This is not \emph{quite} what one usually wants to regard as an $\mathbb{R}^k$-parameterized of differential forms on $X$. That is instead usually meant to be a differential form $\omega$ on $X \times \mathbb{R}^k$ which has ``no leg along $\mathbb{R}^k$''. Another way to say this is that the family of forms on $X$ that is represented by some $\omega$ on $X \times \mathbb{R}^k$ is that which over a point $v \colon * \to \mathbb{RR}^k$ has the value $(id_X,v)^* \omega$. Under this [[pullback of differential forms]] any components of $\omega$ with ``legs along $\mathbb{R}^k$'' are identified with the 0 differential form

\end{remark}
This is captured by the following definition.

\begin{defn}
\label{SmoothSpaceOfFormsOnSmoothSpace}\hypertarget{SmoothSpaceOfFormsOnSmoothSpace}{}
For $X \in Smooth0Type$ and $n \in \mathbb{N}$, the \textbf{smooth space of differential $n$-forms} $\mathbf{\Omega}^n(X)$ on $X$ is the concretification, def. \ref{ConcreteObjectsAndConcretification}, of the smooth mapping space $[X, \Omega^n]$, def. \ref{SmoothFunctionSpace}, into the smooth moduli space of differential $n$-forms, def. \ref{SmoothModuliSpaceOfnForms}:

\begin{displaymath}
\mathbf{\Omega}^n(X) \coloneqq Conc([X, \Omega^n])
  \,.
\end{displaymath}
\end{defn}
\begin{prop}
\label{}\hypertarget{}{}
The $\mathbb{R}^k$-plots of $\mathbf{\Omega}^n(\mathbb{R}^k)$ are indeed smooth differential $n$-forms on $X \times \mathbb{R}^k$ which are such that their evaluation on vector fields tangent to $\mathbb{R}^k$ vanish.

\end{prop}
\begin{proof}
By def. \ref{Decohese}, def. \ref{ConcreteObjectsAndConcretification} and prop. \ref{DecohesOverASiteWithTerminalObject} the set of plots of $\mathbf{\Omega}^n(X)$ over $\mathbb{R}^k$ is the [[image]] of the [[function]]

\begin{displaymath}
\Omega^n(X \times \mathbb{R}^k)
  \simeq
   Hom_{Smooth0Type}(\mathbb{R}^k, [X,\Omega^n])
   \stackrel{\Gamma_{ \mathbb{R}^k, [X,\Omega^n] }}{\to}
   Hom_{Set}(\Gamma(\mathbb{R}^k), \Gamma [X, \Omega^n])
   \simeq
   Hom_{Set}(\mathbb{R}^k_s, \Omega^n(X))
  \,,
\end{displaymath}
where on the right $\mathbb{R}^k_s$ denotes, just for emphasis, the underlying set of $\mathbb{R}^k$. This function manifestly sends a smooth differential form $\omega \in \Omega^n(X \times \mathbb{R}^k)$ to the function from points $v$ of $\mathbb{R}^k$ to differential forms on $X$ given by

\begin{displaymath}
\omega \mapsto \left(v \mapsto  (id_X, v)^* \omega \right)
  \,.
\end{displaymath}
Under this function all components of differential forms with a ``leg along'' $\mathbb{R}^k$ are sent to the 0-form. Hence the image of this function is the collection of smooth forms on $X \times \mathbb{R}^k$ with ``no leg along $\mathbb{R}^k$''.

\end{proof}
\begin{remark}
\label{}\hypertarget{}{}
For $n = 0$ we have (for any $X\in Smooth0Type$)

\begin{displaymath}
\begin{aligned}
    \mathbf{\Omega}^0(X) 
      & \coloneqq Conc [X, \Omega^0]
    \\
    & \simeq Conc [X, \mathbb{R}]
    \\
    & \simeq [X, \mathbb{R}]
  \end{aligned}
  \,,
\end{displaymath}
by prop. \ref{SpaceOf0FormsIsRealLine}.

\end{remark}
\hypertarget{DifferentialFormsLayerSyn}{}\subsubsection*{{Syntactic Layer}}\label{DifferentialFormsLayerSyn}

\hypertarget{images}{}\paragraph*{{Images}}\label{images}

\begin{prop}
\label{}\hypertarget{}{}
Let a morphism $f \colon X \to Y$ in $\mathbf{H}$ be the [[categorical semantics]] of the [[syntax]]

\begin{displaymath}
x \colon X \; \vdash \; f(x) \colon Y
  \,.
\end{displaymath}
Then the syntax for the [[infinity-image|image]] $i_f \colon im(f) \hookrightarrow Y$ is

\begin{displaymath}
\vdash\;
   \left(
     \sum_{y \colon Y} \exists_{x \colon X} \left(f\left(x\right) = y\right)
   \right)
   \colon
   Type
  \,.
\end{displaymath}
\end{prop}
Here $\exists_{\cdots} \cdots =_{def} \left[ \sum_{\cdots} \cdot\right]$ is the [[bracket type]] of the [[dependent sum type]].

Accordingly the syntax for the smooth moduli space of differential $n$-forms, def. \ref{SmoothSpaceOfFormsOnSmoothSpace}, on a smooth space $X$,

\begin{displaymath}
\sum_{\omega \colon \sharp [X, \Omega^n]}
  \exists_{\lambda \colon [X,\Omega^n]}
  (\omega = DeCoh_X(\lambda)) 
  \,.
\end{displaymath}
(\ldots{})



\end{document}