Monday, September 10, 2012

General Covariance in Homotopy Type Theory

General Covariance in Homotopy Type Theory:


MathML-enabled post (click for more details).


In physics, the term general covariance is meant to indicate the property of a physical system or model (in theoretical physics) whose configurations, action functional and equations of motion are all equivariant under the action of the diffeomorphism group on the smooth manifold underlying the spacetime or the worldvolume of the system. The archetypical example of a generally covariant system is of course Einstein-gravity / “general relativity”.

I indicate here how general covariance has a natural formalization in homotopy type theory, hence internal to any ∞-topos. For background and all details see at general covariance on the nLab, and the links given there.


MathML-enabled post (click for more details).


Of course a basic idea of traditional dependent type theory is that types A may appear in context of other types Γ. The traditional interpretation of such a dependent type

x:Γ⊢A(x):Type

is that of a Γ-parameterized family or bundle of types, whose fiber over x∈Γ is A(x).

But in homotopy type theory, types are homotopy types, of course, and, hence so are the contexts. A type in context is now in general something more refined than just a family of types. It is really a family of types equipped with equivariance structure with respect to the homotopy groups of the context type.

Specifically, if the context type is connected and pointed, then it is equivalent to the delooping Γ≃BG of an ∞-group G. One finds (this is discussed here) – that the context defined by the type BG is that of G-equivariance: every type in the context is a type in the original context, but now equipped with a G-∞-action. In a precise sense, the homotopy type theory of G-∞-actions is equivalent to plain homotopy type theory in context BG.

Consider this for the case that G is an automorphism ∞-group of a type Σ which is regarded as representing spacetime or a worldvolume. 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 Fields a moduli object for the given fields, so that a field configuration is a function ϕ:Σ→Fields, the configuration space of covariant fields is the function type (Σ→Fields) but formed in the “general covariance context” BAut(Σ). When interpreted in smooth models, Conf is the smooth groupoid of field configurations and diffeomorphism gauge transformations acting on them, the Lie integration of the BRST complex whose degree-1 elements are accordingly called the diffeomorphism ghosts.

More precisely, I show the following (and thanks again to Mike, for discussion of this here).

Definition. Consider in homotopy type theory two types ⊢Σ,Fields:Type, to be called spacetime and field moduli. Let

⊢BAut(Σ):Type

be the image of the name of Σ, with essentially unique term

⊢Σ:BAut(Σ).

Perform the canonical context extension of Σ and trivial context extension of Fields to get types in context

Σ:BAut(Σ)⊢Σ:Type

and

Σ:BAut(Σ)⊢Fields:Type.

Form then the type of field moduli “Conf≔(Σ→Fields)” in this context:

Conf≔Σ:BAut(Σ)⊢(Σ→Fields):Type.

Proposition. The categorical semantics of Conf in the model of smooth cohesion, and for Σ a smooth manifold, is given by the diffeological groupoid

Conf=[Σ,Fields]⫽Diff(Σ)

whose objects are field configurations on Σ and whose morphisms are diffeomorphism gauge transformations between them. In particular the corresponding Lie algebroid is dual to the (off-shell) BRST complex of fields with diffeomorphism ghosts in degree 1.



DIGITAL JUICE

No comments:

Post a Comment

Thank's!