geometry of physics -- differential forms

This entry contains one chapter of the material at geometry of physics.

previous chapter: smooth sets

next chapter: integration



physics, mathematical physics, philosophy of physics

Surveys, textbooks and lecture notes

theory (physics), model (physics)

experiment, measurement, computable physics

Differential geometry

synthetic differential geometry


from point-set topology to differentiable manifolds

geometry of physics: coordinate systems, smooth spaces, manifolds, smooth homotopy types, supergeometry



smooth space


The magic algebraic facts




tangent cohesion

differential cohesion

graded differential cohesion

id id fermionic bosonic bosonic Rh rheonomic reduced infinitesimal infinitesimal & étale cohesive ʃ discrete discrete continuous * \array{ && id &\dashv& id \\ && \vee && \vee \\ &\stackrel{fermionic}{}& \rightrightarrows &\dashv& \rightsquigarrow & \stackrel{bosonic}{} \\ && \bot && \bot \\ &\stackrel{bosonic}{} & \rightsquigarrow &\dashv& Rh & \stackrel{rheonomic}{} \\ && \vee && \vee \\ &\stackrel{reduced}{} & \Re &\dashv& \Im & \stackrel{infinitesimal}{} \\ && \bot && \bot \\ &\stackrel{infinitesimal}{}& \Im &\dashv& \& & \stackrel{\text{étale}}{} \\ && \vee && \vee \\ &\stackrel{cohesive}{}& ʃ &\dashv& \flat & \stackrel{discrete}{} \\ && \bot && \bot \\ &\stackrel{discrete}{}& \flat &\dashv& \sharp & \stackrel{continuous}{} \\ && \vee && \vee \\ && \emptyset &\dashv& \ast }


Lie theory, ∞-Lie theory

differential equations, variational calculus

Chern-Weil theory, ∞-Chern-Weil theory

Cartan geometry (super, higher)



We introduce the standard concept of differential forms in Model Layer, adding to the traditional discussion a precise version of the statement that differential forms are equivalently “incremental smooth nn-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 Ω Smooth0Type\Omega^\in \in Smooth0Type of differential forms. This has the special property that it is, for n1n \geq 1, a non-concrete smooth space. In 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 concretification of the smooth mapping space [X,Ω n][X,\Omega^n] for any smooth space XX is the smooth (moduli) space of differential forms on XX. Below in Action functionals for Chern-Simons type gauge theories the theory of concretification in a local topos is a central ingredient in the canonical existence of certain action functionals.

The process of concretification involves the general abstract notion of images. The type-theory of this notion we discuss in Syntactic Layer here.

Model Layer

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

But moreover, dynamics in physics is encoded by functionals on such trajectories: by “action functionals”. In the simplest case these are for instance homomorphisms of smooth spaces

S:[I,X], S \colon \left[I, X\right] \to \mathbb{R} \,,

where II \hookrightarrow \mathbb{R} is the standard unit interval.

Such action functionals we discuss in their own right in Variational calculus below. Here we first examine in detail a fundamental property they all have: they are supposed to be local.

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

S(γ)=S(γ 1)+S(γ 2). S(\gamma) = S(\gamma_1) + S(\gamma_2) \,.

As one takes this property to the limit of iterative subdivision, one finds that action functionals are entirely determined by their value on infinitesimal displacements along the worldline. If γ:X\gamma \colon \mathbb{R} \to X denotes a path and “γ˙(x)\dot \gamma(x)” denotes the corresponding “infinitesimal path” at worldline parameter xx, then the value of the action functional on such an infinitesimal path is traditionally written as

dS(γ˙) x, \mathbf{d}S(\dot \gamma)_x \in \mathbb{R} \,,

to be read as “the small change dS\mathbf{d}S of SS along the infinitesimal path γ˙ x\dot \gamma_x”.

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

We define smooth differential forms on Cartesian spaces in

Then we discuss how this induces a notion of smooth differential forms on general smooth spaces in

Further below we provide a precise version of the statement that “Differential 1-forms are differential measures along paths.” in

Differential forms on abstract coordinate systems

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


For nn \in \mathbb{N} a smooth differential 1-form ω\omega on a Cartesian space n\mathbb{R}^n is an nn-tuple

(ω iCartSp( n,)) i=1 n \left(\omega_i \in CartSp\left(\mathbb{R}^n,\mathbb{R}\right)\right)_{i = 1}^n

of smooth functions, which we think of equivalently as the coefficients of a formal linear combination

ω= i=1 nf idx i \omega = \sum_{i = 1}^n f_i \mathbf{d}x^i

on a set {dx 1,dx 2,,dx n}\{\mathbf{d}x^1, \mathbf{d}x^2, \cdots, \mathbf{d}x^n\} of cardinality nn.


Ω 1( k)CartSp( k,) ×kSet \Omega^1(\mathbb{R}^k) \simeq CartSp(\mathbb{R}^k, \mathbb{R})^{\times k}\in Set

for the set of smooth differential 1-forms on k\mathbb{R}^k.


We think of dx i\mathbf{d} x^i as a measure for infinitesimal displacements along the x ix^i-coordinate of a Cartesian space. This idea is made precise below in Differential 1-forms are smooth increnemental path measures.

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


For ϕ: k˜ k\phi \colon \mathbb{R}^{\tilde k} \to \mathbb{R}^k a smooth function, the pullback of differential 1-forms along ϕ\phi is the function

ϕ *:Ω 1( k)Ω 1( k˜) \phi^* \colon \Omega^1(\mathbb{R}^{k}) \to \Omega^1(\mathbb{R}^{\tilde k})

between sets of differential 1-forms, def. 1, which is defined on basis-elements by

ϕ *dx i j=1 k˜ϕ ix˜ jdx˜ j \phi^* \mathbf{d} x^i \coloneqq \sum_{j = 1}^{\tilde k} \frac{\partial \phi^i}{\partial \tilde x^j} \mathbf{d}\tilde x^j

and then extended linearly by

ϕ *ω =ϕ *( iω idx i) i=1 k(ϕ *ω) i j=1 k˜ϕ ix˜ jdx˜ j = i=1 k j=1 k˜(ω iϕ)ϕ ix˜ jdx˜ j. \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} \,.

The term “pullback” in pullback of differential forms is not really related, certainly not historically, to the term 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.

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

  1. The set Ω 1( k)\Omega^1(\mathbb{R}^k) is naturally an abelian group with addition given by componentwise addition

    ω+λ = i=1 kω idx i+ j=1 kλ jdx j = i=1 k(ω i+λ i)dx j, \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^j \end{aligned} \,,
  2. The abelian group Ω 1( k)\Omega^1(\mathbb{R}^k) is naturally equipped with the structure of a module over the ring C ( k,)=CartSp( k,)C^\infty(\mathbb{R}^k,\mathbb{R}) = CartSp(\mathbb{R}^k, \mathbb{R}) of smooth functions, where the action C ( k,)×Ω 1( k)Ω 1( k)C^\infty(\mathbb{R}^k,\mathbb{R}) \times\Omega^1(\mathbb{R}^k) \to \Omega^1(\mathbb{R}^k) is given by componentwise multiplication

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

More abstractly, this just says that Ω 1( k)\Omega^1(\mathbb{R}^k) is the free module over C ( k)C^\infty(\mathbb{R}^k) on the set {dx i} i=1 k\{\mathbf{d}x^i\}_{i = 1}^k.

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

dx jdx i=dx idx j \mathbf{d}x^j \wedge \mathbf{d}x^i = - \mathbf{d}x^i \wedge \mathbf{d} x^j

being the same infinitesimal measure with orientation reversed.


For k,nk,n \in \mathbb{N}, the smooth differential forms on k\mathbb{R}^k is the exterior algebra

Ω ( k) C ( k) Ω 1( k) \Omega^\bullet(\mathbb{R}^k) \coloneqq \wedge^\bullet_{C^\infty(\mathbb{R}^k)} \Omega^1(\mathbb{R}^k)

over the ring C ( k)C^\infty(\mathbb{R}^k) of smooth functions of the module Ω 1( k)\Omega^1(\mathbb{R}^k) of smooth 1-forms, prop. 3.

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


Explicitly this means that a differential n-form ωΩ n( k)\omega \in \Omega^n(\mathbb{R}^k) on k\mathbb{R}^k is a formal linear combination over C ( k)C^\infty(\mathbb{R}^k) of basis elements of the form dx i 1dx i n\mathbf{d} x^{i_1} \wedge \cdots \wedge \mathbf{d}x^{i_n} for i 1<i 2<<i ni_1 \lt i_2 \lt \cdots \lt i_n:

ω= 1i 1<i 2<<i n<kω i 1,,i ndx i 1dx i n. \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} \,.

The pullback of differential 1-forms of def. 1 extends as an C ( k)C^\infty(\mathbb{R}^k)-algebra homomorphism to Ω n()\Omega^n(-), given for a smooth function f: k˜ kf \colon \mathbb{R}^{\tilde k} \to \mathbb{R}^k on basis elements by

f *(dx i 1dx i n)=(f *dx i 1f *dx i n). 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) \,.

Differential forms on smooth spaces

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


The assignment of differential nn-forms

Ω n(): kΩ n( k) \Omega^n(-) \colon \mathbb{R}^k \mapsto \Omega^n(\mathbb{R}^k)

of def. 5 together with the pullback of differential forms-functions of def. 6

k 1 Ω 1( k 1) f f * k 2 Ω 1( k 2) \array{ \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}) }

defines a smooth space in the sense of def. \ref{SmoothSpace}:

Ω n()Smooth0Type. \Omega^n(-) \in Smooth0Type \,.

We call this

Ω n:Smooth0Type \Omega^n \colon Smooth0Type

the universal smooth moduli space of differential nn-forms.

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


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

Ω n( k)Hom( k,Ω 1) \Omega^n(\mathbb{R}^k) \simeq Hom(\mathbb{R}^k, \Omega^1)

between the set of smooth nn-forms on n\mathbb{R}^n according to def. 1 and the set of homomorphism of smooth spaces, kΩ 1\mathbb{R}^k \to \Omega^1, according to def. \ref{HomomorphismOfSmoothSpaces}.

In view of this we have the following elegant definition of smooth nn-forms on an arbitrary smooth space.


For XSmooth0TypeX \in Smooth0Type a smooth space, def. \ref{SmoothSpace}, a differential n-form on XX is a homomorphism of smooth spaces of the form

ω:XΩ n(). \omega \colon X \to \Omega^n(-) \,.

Accordingly we write

Ω n(X)Smooth0Type(X,Ω n) \Omega^n(X) \coloneqq Smooth0Type(X,\Omega^n)

for the set of smooth nn-forms on XX.

We may unwind this definition to a very explicit description of differential forms on smooth spaces. This we do in a moment in remark 4.

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


Ω 0\Omega^0 \simeq \mathbb{R}


For f:XYf \colon X \to Y a homomorphism of smooth spaces, def. \ref{HomomorphismOfSmoothSpaces}, the pullback of differential forms along ff is the function

f *:Ω n(Y)Ω n(X) f^* \colon \Omega^n(Y) \to \Omega^n(X)

given by the hom-functor into the smooth space Ω n\Omega^n of def. 7:

f *Hom(,Ω n). f^* \coloneqq Hom(-, \Omega^n) \,.

This means that it sends an nn-form ωΩ n(Y)\omega \in \Omega^n(Y) which is modulated by a homomorphism YΩ nY \to \Omega^n to the nn-form f *ωΩ n(X)f^* \omega \in \Omega^n(X) which is modulated by the composite XfYΩ nX \stackrel{f}{\to} Y \to \Omega^n.


For X= k˜X = \mathbb{R}^{\tilde k} and Y= kY = \mathbb{R}^{k} definition 9 reproduces def. 6.


Again by the Yoneda lemma.


Using def. 9

Unwinding def. 8 yields the following explicit description:

a differential nn-form ωΩ n(X)\omega \in \Omega^n(X) on a smooth space XX is

  1. for each way ϕ: kX\phi \colon \mathbb{R}^k \to X of laying out a coordinate system k\mathbb{R}^k in XX a differential nn-form

    ϕ *ωΩ n( k) \phi^* \omega \in \Omega^n(\mathbb{R}^k)

    on the abstract coordinate system, as given by def. 5;

  2. for each abstract coordinate transformation f: k 2 k 1f \colon \mathbb{R}^{k_2} \to \mathbb{R}^{k_1} a corresponding compatibility condition between local differential forms ϕ 1: k 1X\phi_1 \colon \mathbb{R}^{k_1} \to X and ϕ 2: k 2X\phi_2 \colon \mathbb{R}^{k_2} \to X of the form

    f *ϕ 1 *ω=ϕ 2 *ω. f^* \phi_1^* \omega = \phi_2^* \omega \,.

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.

The following adds further explanation to the role of Ω nSmooth0Tye\Omega^n \in Smooth0Tye as a moduli space. Notice that since Ω n\Omega^n is itself a smooth space, we may speak about differential nn-forms on Ω n\Omega^n itsefl.


The universal differential nn-forms is the differential nn-form

ω univ nΩ n(Ω n) \omega^n_{univ} \in \Omega^n(\Omega^n)

which is modulated by the identity homomorphism id:Ω nΩ nid \colon \Omega^n \to \Omega^n.

With this definition we have:


For XSmooth0TypeX \in Smooth0Type any smooth space, every differential nn-form on XX, ωΩ n(X)\omega \in \Omega^n(X) is the pullback of differential forms, def. 9, of the universal differential nn-form, def. 11, along a homomorphism ff from XX into the moduli space Ω n\Omega^n of differential nn-forms:

ω=f *ω univ n. \omega = f^* \omega^n_{univ} \,.

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.


This ends the Model-layer discussion of differential forms. We now pass to a more advanced discussion of this topic in the 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 differentiation below.

Semantic Layer

Concrete smooth spaces

The smooth universal moduli space of differential forms Ω n()\Omega^n(-) from def. 7 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 kk-dimensional subspaces” for low kk. In fact


For k<nk \lt n the smooth space Ω n\Omega^n admits only a unique probe by k\mathbb{R}^k:

Hom( k,Ω n())Ω n( k)={0}. Hom(\mathbb{R}^k, \Omega^n(-)) \simeq \Omega^n(\mathbb{R}^k) = \{0\} \,.

By the Yoneda lemma a smooth morphism kΩ n\mathbb{R}^k \to \Omega^n is a differential n-form ωΩ n( k)\omega \in \Omega^n(\mathbb{R}^k). But for n>kn \gt k there is only the 0 element.

So while Ω n()\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 is supported on its probes is that of a concrete object. There is a univeral map that sends any smooth space to its concretification. The universal moduli spaces of differential forms turn out to be non-concrete in that their concetrification is the point.


Let H\mathbf{H} be a local topos. Write :HH\sharp \colon \mathbf{H} \to \mathbf{H} for the corresponding sharp modality, def. \ref{SharpModalityOfLocalTopos}. Then.

  1. An object XHX \in \mathbf{H} is called a concrete object if

    DeCoh X:XX DeCoh_X \colon X \to \sharp X

    is a monomorphism.

  2. For XHX \in \mathbf{H} any object, its concretification Conc(X)HConc(X) \in \mathbf{H} is the image factorization of DeCoh XDeCoh_X, hence the factorization into an epimorphism followed by a monomorphism

    DeCoh X:XConc(X)X. DeCoh_X : X \to Conc(X) \hookrightarrow \sharp X \,.

Hence the concretification Conc(X)Conc(X) of an object XX is itself a concrete object and it is universal with this property. (…)


Let CC be a site of definition for the local topos H\mathbf{H}, with terminal object **. Then for X:C opSetX \colon C^{op} \to Set a sheaf, DeCoh XDeCoh_X is given over UCU \in C by

X(U)YonedaH(U,X)Γ U,XSet(Γ(U),Γ(X)). X(U) \underoverset{Yoneda}{\simeq}{\to} \mathbf{H}(U, X) \stackrel{\Gamma_{U,X}}{\to} Set(\Gamma(U),\Gamma(X)) \,.

For n1n \geq 1 we have

Conc(Ω n)*. Conc(\Omega^n) \simeq * \,.

In this sense the smooth moduli space of differential nn-forms is maximally non-concrete.

Smooth moduli space of differential forms on a smooth space

We discuss the smooth space of differential forms on a fixed smooth space XX.


For XX a smooth space, the smooth mapping space [X,Ω n]Smooth0Type[X, \Omega^n] \in Smooth0Type is the smooth space whose k\mathbb{R}^k-plots are differential nn-forms on the product X× kX \times \mathbb{R}^k

[X,Ω n]: kΩ n(X× k). [X, \Omega^n] \colon \mathbb{R}^k \mapsto \Omega^n(X \times \mathbb{R}^k) \,.

This is not quite what one usually wants to regard as an k\mathbb{R}^k-parameterized of differential forms on XX. That is instead usually meant to be a differential form ω\omega on X× kX \times \mathbb{R}^k which has “no leg along k\mathbb{R}^k”. Another way to say this is that the family of forms on XX that is represented by some ω\omega on X× kX \times \mathbb{R}^k is that which over a point v:*ℝℝ kv \colon * \to \mathbb{RR}^k has the value (id X,v) *ω(id_X,v)^* \omega. Under this pullback of differential forms any components of ω\omega with “legs along k\mathbb{R}^k” are identified with the 0 differential form

This is captured by the following definition.


For XSmooth0TypeX \in Smooth0Type and nn \in \mathbb{N}, the smooth space of differential nn-forms Ω n(X)\mathbf{\Omega}^n(X) on XX is the concretification, def. 12, of the smooth mapping space [X,Ω n][X, \Omega^n], def. \ref{SmoothFunctionSpace}, into the smooth moduli space of differential nn-forms, def. 7:

Ω n(X)Conc([X,Ω n]). \mathbf{\Omega}^n(X) \coloneqq Conc([X, \Omega^n]) \,.

The k\mathbb{R}^k-plots of Ω n( k)\mathbf{\Omega}^n(\mathbb{R}^k) are indeed smooth differential nn-forms on X× kX \times \mathbb{R}^k which are such that their evaluation on vector fields tangent to k\mathbb{R}^k vanish.

Proof (sketch)

By def. \ref{Decohese}, def. 12 and prop. 5 the set of plots of Ω n(X)\mathbf{\Omega}^n(X) over k\mathbb{R}^k is the image of the function

Ω n(X× k)Hom Smooth0Type( k,[X,Ω n])Γ k,[X,Ω n]Hom Set(Γ( k),Γ[X,Ω n])Hom Set( s k,Ω n(X)), \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)) \,,

where on the right s k\mathbb{R}^k_s denotes, just for emphasis, the underlying set of s k\mathbb{R}^k_s. This function manifestly sends a smooth differential form ωΩ n(X× k)\omega \in \Omega^n(X \times \mathbb{R}^k) to the function from points vv of k\mathbb{R}^k to differential forms on XX given by

ω(v(id X,v) *ω). \omega \mapsto \left(v \mapsto (id_X, v)^* \omega \right) \,.

Under this function all components of differential forms with a “leg along” k\mathbb{R}^k are sent to the 0-form. Hence the image of this function is the collection of smooth forms on X× kX \times \mathbb{R}^k with “no leg along k\mathbb{R}^k”.


For n=0n = 0 we have (for any XSmooth0TypeX\in Smooth0Type)

Ω 0(X) Conc[X,Ω 1] Conc[X,] [X,], \begin{aligned} \mathbf{\Omega}^0(X) & \coloneqq Conc [X, \Omega^1] \\ & \simeq Conc [X, \mathbb{R}] \\ & \simeq [X, \mathbb{R}] \end{aligned} \,,

by prop. 2.

Syntactic Layer



Let a morphism f:XYf \colon X \to Y in H\mathbf{H} be the categorical semantics of the syntax

x:Xf(x):Y. x \colon X \; \vdash \; f(x) \colon Y \,.

Then the syntax for the image i f:im(f)Yi_f \colon im(f) \hookrightarrow Y is

( y:Y x:X(f(x)=y)):Type. \vdash\; \left( \sum_{y \colon Y} \exists_{x \colon X} \left(f\left(x\right) = y\right) \right) \colon Type \,.

Here = def[ ]\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 nn-forms, def. 13, on a smooth space XX,

ω:[X,Ω n] λ:[X,Ω n](ω=DeCoh X(λ)). \sum_{\omega \colon \sharp [X, \Omega^n]} \exists_{\lambda \colon [X,\Omega^n]} (\omega = DeCoh_X(\lambda)) \,.


Revised on September 19, 2017 15:34:03 by Urs Schreiber (