7. The axioms in curved spacetime and general covariance🔗

The abstract Lorentzian spacetime: exactly the structure that the curved-spacetime axioms use.

The curved Haag–Kastler axioms never look at the metric directly. They need the points of the spacetime M; the causal diamonds B = I⁺(p) ∩ I⁻(q), which are the basis sets of the Alexandrov topology; the relation "B₁ and B₂ are completely spacelike", used by Axiom 3; and the group of isometries of M connected to the identity with its action on points, used by Axiom 5. The interface records these, together with the one fact Axiom 5 needs: an isometry φ carries a basis set B to a basis set φ(B), so that α_φ : 𝔘(B) → 𝔘(φ(B)) is a map between local algebras of basis sets.

The interface imposes no other conditions on these pieces. A geometric Lorentzian spacetime (Physicslib4.Spacetime.LorentzianSpacetime: a connected four-dimensional manifold with a Lorentzian metric, a time orientation and a Hausdorff Alexandrov topology) gives an instance through Physicslib4.Spacetime.LorentzianSpacetime.toAbstractIdentityComponent, and every result proved over the interface applies to it.

Implementation note: the group structure and the action are fields, declared instances once the interface is defined, so that with open Pointwise the image φ(B) is written φ • B. The points and the isometries live in one universe u.

Blueprint: def:abstract-lorentzian-spacetime-interface

Physicslib4.AQFT.HaagKastlerCurved.LorentzianSpacetime.mk.{u}

Carrier : Type u

IsBasisSet : Set self.Carrier → Prop

IsCompletelySpacelike : Set self.Carrier → Set self.Carrier → Prop

Isom : Type u

instGroup : Group self.Isom

instAction : MulAction self.Isom self.Carrier

isBasisSet_smul : ∀ (φ : self.Isom) {B : Set self.Carrier}, self.IsBasisSet B → self.IsBasisSet (φ • B)

The abstract spacetime interface of a geometric Lorentzian spacetime L, the bridge to the curved axioms.

The pieces of the interface are read off L. The points are those of the manifold. The basis sets are the causal diamonds I⁺(p) ∩ I⁻(q) of the Alexandrov topology for the time orientation of L. Two regions are completely spacelike when every point of the one is spacelike to every point of the other. The isometry group is the group of isometries of L connected to the identity, taken as the oriented identity component: the isometries in the identity component of the isometry group that also preserve the future orientation. These isometries carry diamonds to diamonds (Spacetime.LorentzianSpacetime.isBasisSet_smul), which supplies the one axiom of the interface. Every result proved over the interface, the curved axioms included, then applies to L.

Implementation note: the oriented identity component is the group of isometries connected to the identity named in the blueprint. That an isometry connected to the identity preserves the future orientation needs a Myers–Steenrod-type rigidity theorem that Mathlib does not provide, so orientation preservation is included in the definition of the group rather than proved.

Blueprint: def:abstract-lorentzian-spacetime-interface

Axiom 1 in curved spacetime (local algebras): a unital C*-algebra 𝔘(B) for each region B of M.

The algebra 𝔘(B) is the abstract algebra of the observables that can be measured in the region B of the spacetime M. The regions that matter are the causal diamonds, the basis sets M.IsBasisSet of the Alexandrov topology, and the axioms that follow quantify over those only. The empty region is assigned the one-dimensional algebra ℂ·1 of multiples of the unit. The shape is that of the Minkowski net, with Minkowski space replaced by the abstract spacetime M.

Implementation note: algebra is defined on every subset of M, so that it is a plain function; its values on sets that are not basis sets are never used. The normalisation 𝔘(∅) = ℂ·1 is a *-isomorphism emptyEquivComplex onto ℂ. The algebras live in a universe v that is independent of the universe u of the points: LocalNet.{u, v} M has algebras in Type v.

Blueprint: def:local-algebras-in-curved-spacetime

Physicslib4.AQFT.HaagKastlerCurved.LocalNet.mk.{u, v}

algebra : Set M.Carrier → Type v

instCStarAlgebra : (B : Set M.Carrier) → CStarAlgebra (self.algebra B)

emptyEquivComplex : self.algebra ∅ ≃⋆ₐ[ℂ] ℂ

Axiom 2 in curved spacetime (isotony): a chosen unital *-monomorphism 𝔘(B₁) → 𝔘(B₂) for each inclusion of basis sets.

An observable measurable in a basis set B₁ is also measurable in any larger basis set B₂ ⊇ B₁. Since the local algebras are abstract, this is expressed by a map i(B₁, B₂) : 𝔘(B₁) → 𝔘(B₂), which is a unital *-homomorphism and injective. The maps are coherent: i(B, B) is the identity, and i(B₂, B₃) ∘ i(B₁, B₂) = i(B₁, B₃) for B₁ ⊆ B₂ ⊆ B₃. In other words B ↦ 𝔘(B) is a functor on the basis sets ordered by inclusion. The hypothesis is the non-strict inclusion B₁ ⊆ B₂; the case B₁ = B₂ is what makes the identity law expressible.

The family is data, not an existence statement, exactly as in Minkowski spacetime: the identity and composition laws are equations between the maps themselves, so they can only be stated once the maps are fixed. They are required rather than derived, since nothing about the spacetime constrains which monomorphism a net chooses. Curved spacetime has no quasilocal algebra, so statements about nested regions B₁ ⊆ B₂ ⊆ B are made inside a common containing algebra 𝔘(B); the composition law makes the embedding of 𝔘(B₁) in 𝔘(B) factor through 𝔘(B₂) for every net. Axiom 3 uses this same family.

Implementation note: a unital *-homomorphism is Mathlib's StarAlgHom, which preserves the unit because it is an algebra homomorphism.

Blueprint: def:isotony-in-curved-spacetime

Physicslib4.AQFT.HaagKastlerCurved.Isotony.mk.{u_1, u_2}

map : ⦃B₁ B₂ : Set M.Carrier⦄ → M.IsBasisSet B₁ → M.IsBasisSet B₂ → B₁ ⊆ B₂ → U.algebra B₁ →⋆ₐ[ℂ] U.algebra B₂

injective : ∀ ⦃B₁ B₂ : Set M.Carrier⦄ (h₁ : M.IsBasisSet B₁) (h₂ : M.IsBasisSet B₂) (h : B₁ ⊆ B₂),
  Function.Injective ⇑(self.map h₁ h₂ h)

map_self : ∀ ⦃B : Set M.Carrier⦄ (h : M.IsBasisSet B), self.map h h ⋯ = StarAlgHom.id ℂ (U.algebra B)

map_comp : ∀ ⦃B₁ B₂ B₃ : Set M.Carrier⦄ (h₁ : M.IsBasisSet B₁) (h₂ : M.IsBasisSet B₂) (h₃ : M.IsBasisSet B₃) (h₁₂ : B₁ ⊆ B₂)
  (h₂₃ : B₂ ⊆ B₃), (self.map h₂ h₃ h₂₃).comp (self.map h₁ h₂ h₁₂) = self.map h₁ h₃ ⋯

Axiom 3 in curved spacetime (local commutativity): observables of completely spacelike basis sets commute in every basis set containing both.

Let B₁ and B₂ be completely spacelike basis sets. To multiply an element of 𝔘(B₁) by one of 𝔘(B₂), both must lie in one algebra. As in Minkowski spacetime, the axiom takes any basis set B containing both, and asks that for all a₁ ∈ 𝔘(B₁) and a₂ ∈ 𝔘(B₂) the equation

i(B₁, B)(a₁) i(B₂, B)(a₂) = i(B₂, B)(a₂) i(B₁, B)(a₁)

holds in 𝔘(B), where i is the isotony family of Axiom 2. The difference from Minkowski spacetime is that such a B need not exist, and there is no quasilocal algebra to fall back on. When no common containing basis set exists the condition is vacuous: the two algebras do not lie in a common algebra, so their commutation is not a meaningful question.

The axiom asserts only the commutation. The embeddings, their injectivity and their identity and composition laws belong to Axiom 2, whose family is a parameter here, so results that factor a three-fold inclusion B₁ ⊆ B₂ ⊆ B need no separate coherence hypothesis.

Blueprint: def:local-commutativity-in-curved-spacetime

A local observable of a representation π of 𝔘(B): an operator π(a) with a self-adjoint in 𝔘(B).

Fix a region B and a *-representation π of its local algebra 𝔘(B) by bounded operators on a Hilbert space H; the blueprint's case is the GNS representation π_ω of a state ω on 𝔘(B) (gns_construction). A bounded operator T on H is a local observable when T = π(a) for some self-adjoint a ∈ 𝔘(B). Such a T is self-adjoint (IsLocalObservable.isSelfAdjoint), since π preserves the adjoint, so it is an observable in the quantum-mechanical sense, and it is measured in B. Conversely, every self-adjoint operator in the range of π is a local observable (isLocalObservable_iff).

Implementation note: π is any unital *-homomorphism 𝔘(B) → B(H), not only a GNS representation.

Blueprint: def:local-observable

Axiom 4 in curved spacetime (local completeness): each observable of a local representation is a local observable.

The blueprint's axiom says that all observables are local observables. Curved spacetime has no quasilocal algebra, so there is no single algebra in which "all observables" live; the axiom is read locally instead. For every basis set B, every *-representation π of 𝔘(B) on a Hilbert space H, and every self-adjoint operator T in the range of π, T is a local observable: T = π(a) for a self-adjoint a ∈ 𝔘(B).

Read this way the axiom holds for every local net (localAlgebra_of): if T = π(b) is self-adjoint, then T is also the image of the self-adjoint part (b + b*)/2 of b.

Implementation note: the Hilbert spaces H range over Type v, the universe of the local algebras, which is where gns_construction puts the GNS spaces of their states (as in the Minkowski net). π is any unital *-homomorphism 𝔘(B) → B(H).

Blueprint: def:local-completeness-in-curved-spacetime

Axiom 5 in curved spacetime (isometric covariance): the isometries connected to the identity act on the net, compatibly with isotony.

In curved spacetime the Poincaré group of the Minkowski axioms is replaced by the symmetries the spacetime actually has: the group M.Isom of isometries of M connected to the identity. A generic spacetime has no isometries other than the identity, and then the axiom says little. The axiom asks for a unital *-isomorphism α_φ : 𝔘(B) → 𝔘(φ(B)) for every such isometry φ and every region B, where φ(B) is the image of B under φ, such that

1. α_1 is the identity;

2. α_(φ'φ) = α_φ' ∘ α_φ; and

3. α_φ commutes with the isotony family i of Axiom 2: whenever B₁ ⊆ B₂ are basis sets, α_φ ∘ i(B₁, B₂) = i(φ(B₁), φ(B₂)) ∘ α_φ.

In condition 3, φ(B₁) and φ(B₂) are basis sets with φ(B₁) ⊆ φ(B₂) because isometries preserve basis sets (the interface field LorentzianSpacetime.isBasisSet_smul) and images preserve inclusions (Set.smul_set_mono), so no further hypothesis is needed. The predicate takes the isotony family as a parameter, so the action respects the net's own embeddings. HaagKastlerNet.covEquiv chooses the maps α_φ. There is no quasilocal algebra for them to act on; on a region fixed by φ they give automorphisms of its algebra (HaagKastlerNet.stabAut).

Implementation note: 𝔘(1 • B) and 𝔘(B), and 𝔘((φ'φ) • B) and 𝔘(φ' • (φ • B)), are different types that are equal only propositionally, so conditions 1 and 2 transport along those equalities (one_smul, mul_smul) with Eq.mp. For a geometric spacetime, M.Isom is the oriented identity component of its isometry group (toAbstractIdentityComponent).

Blueprint: def:isometric-covariance-in-curved-spacetime

A Haag–Kastler net on a curved spacetime M: a net of local algebras satisfying Axioms 1 to 5.

The structure bundles the local algebras B ↦ 𝔘(B) of Axiom 1, the isotony family of Axiom 2, and proofs of local commutativity (Axiom 3), local completeness (Axiom 4) and isometric covariance (Axiom 5). Theorems about a theory on M take a HaagKastlerNet M as hypothesis and use each axiom as a field. Unlike the Minkowski net, there is no quasilocal algebra: results are stated in the algebra 𝔘(B) of a basis set B containing the regions involved, or in a representation of it. Axiom 4, read locally, is a field here and holds for every net (localAlgebra_of). nonempty_haagKastlerNet shows that the axioms are consistent over every spacetime.

Implementation note: HaagKastlerNet.{u, v} M has its spacetime M in universe u and its local algebras in universe v, independent of u.

Blueprint: def:haag-kastler-net-in-curved-spacetime

Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.mk.{u, v}

U : LocalNet M

isotony : Isotony self.U

localCommutativity : LocalCommutativity self.U self.isotony

localAlgebra : LocalAlgebra self.U

isometricCovariance : IsometricCovariance self.U self.isotony

The local von Neumann algebra R(B') = π(𝔘(B'))'' of a basis set B' ⊆ B, as a von Neumann algebra.

The local operators π(𝔘(B')) form a self-adjoint set, since π and the isotony embedding preserve the adjoint, and the bicommutant of a self-adjoint set is a von Neumann algebra (Physicslib4.GNS.vonNeumannOfSelfAdjoint). This is that algebra, an element of Mathlib's VonNeumannAlgebra; its underlying set is localVonNeumann (coe_localVonNeumannAlgebra). Microcausality and isotony are stated for it with the order ≤ and VonNeumannAlgebra.commutant.

Blueprint: def:local-von-neumann-algebra-in-curved-spacetime

The stabilizer automorphism α̂_φ of 𝔘(B), for an isometry φ that fixes the region B.

The covariance isomorphisms α_φ : 𝔘(B) → 𝔘(φ(B)) of Axiom 5 map between different local algebras, and curved spacetime has no quasilocal algebra on which they could act together. When φ(B) = B, however, α_φ maps 𝔘(B) back to itself, and so is a *-automorphism α̂_φ of the single algebra 𝔘(B). The isometries fixing B form its stabilizer subgroup Stab(B), on which these automorphisms form a group action (stabAut_one, stabAut_mul). Physically Stab(B) stands in for the global symmetry group. The motivating examples are Killing flows, such as the stationary flow of a black-hole exterior or the boost of a de Sitter static patch. Those regions are not diamonds (basis sets), and no such flow fixes a nonempty diamond, so the axioms as stated place no constraint on their algebras: the examples motivate the definition but are not instances of it.

Implementation note: α̂_φ is covEquiv φ B followed by the identification 𝔘(φ • B) = 𝔘(B) along the hypothesis h : φ • B = B (algCongr). stabAutHom is the same map indexed by elements of MulAction.stabilizer M.Isom B.

Blueprint: def:stabilizer-action-in-curved-spacetime

The stabilizer action g ↦ α̂_g as a group homomorphism from Stab(B) to the group of *-automorphisms of 𝔘(B).

This bundles the action laws stabAutHom_one and stabAutHom_mul: Stab(B) acts on the single algebra 𝔘(B) by *-automorphisms. It is the curved counterpart of the Minkowski actionHom, which acts on the quasilocal algebra; here the action is on one region's algebra only.

Implementation note: the group law of the automorphisms is composition, f * g = g.trans f (StarAlgEquiv.aut). The structure is a MonoidHom, which for groups is a group homomorphism.

Blueprint: the group action of lmm:stabilizer-action-laws-in-curved-spacetime

Conjugation by a unitary implementing a stabilizer element g, as a *-isomorphism R(B₁) ≅ R(g · B₁) of local von Neumann algebras.

Suppose g fixes the basis set B (g ∈ Stab(B), so g · B = B), π is a representation of 𝔘(B), and U is a unitary on H with U π(a) U⁻¹ = π(α̂_g a) for all a ∈ 𝔘(B), where α̂_g is the stabilizer automorphism of 𝔘(B); the stabilizer GNS unitaries (exists_gns_unitary_stabilizer) are such unitaries. For a basis set B₁ ⊆ B, conjugation T ↦ U T U⁻¹ is a *-automorphism of the bounded operators on H, and by geometric covariance (lieConj_image_localVonNeumann) it maps R(B₁) onto R(g · B₁). This is its restriction, a *-isomorphism between the two algebras.

Implementation note: the isomorphism is between the underlying *-subalgebras (VonNeumannAlgebra.toStarSubalgebra).

Blueprint: thrm:von-neumann-covariance-iso-in-curved-spacetime

A covariant family of local states: a state ω_B on each 𝔘(B), carried into one another by the isometries.

The family assigns to every region B a state ω_B on its local algebra 𝔘(B). It is covariant when ω_B(a) = ω_(φ(B))(α_φ a) for every isometry φ connected to the identity, every region B and every a ∈ 𝔘(B), where α_φ is the covariance isomorphism of Axiom 5 (covEquiv). Expectation values in a region and in its image under a symmetry of the spacetime are then the same. Curved spacetime has no quasilocal algebra, hence no single global state to be invariant; this local family is the available form of a covariant state. Mathematically, on a region fixed by φ the condition makes ω_B invariant under the stabilizer automorphism of 𝔘(B) (stabAut); the library has no separate lemma for this.

Implementation note: the family is indexed by all subsets of M; only its values on basis sets are meaningful.

Blueprint: def:covariant-state-family-in-curved-spacetime

A state ω on a local algebra 𝔘(B) is a KMS state at inverse temperature β for a Killing flow t ↦ φ_t fixing B.

The Kubo–Martin–Schwinger condition characterises thermal equilibrium: for all a, b the correlation function t ↦ ω(a τ_t(b)) extends to a bounded continuous function on the strip 0 ≤ Im z ≤ β, holomorphic inside, whose values on Im z = β are ω(τ_t(b) a). This definition is the general KMS condition AQFT.IsKMSState for the automorphisms τ_t = α̂_(φ_t) of 𝔘(B) (flowAut). Curved spacetime has no quasilocal algebra, so the dynamics must act on the algebra of a single region, which is why the flow takes values in the stabilizer of B. The Hartle–Hawking state of a Schwarzschild exterior and the Bunch–Davies state on a de Sitter static patch, KMS at the Hawking and Gibbons–Hawking temperatures, are the motivating examples. Those regions are not diamonds (basis sets), and no such flow fixes a nonempty diamond, so the axioms as stated place no constraint on their algebras: the examples motivate the definition but are not instances of it, and the library constructs neither state. When t ↦ φ_t is a one-parameter subgroup and β > 0, a KMS state is invariant under the flow; if moreover the functions t ↦ ω(a* τ_t(b)) are continuous, its GNS space carries a strongly continuous unitary group implementing the flow (IsKMSStateForFlow.exists_gns_unitary_strongContinuous).

Blueprint: def:kms-state-for-flow-in-curved-spacetime

A ground state for a Killing flow t ↦ φ_t fixing B: a flow-invariant state on 𝔘(B) in which the flow has a positive generator.

A state ω on 𝔘(B) is a ground state for t ↦ φ_t when

1. ω(τ_t a) = ω(a) for all t and a, where τ_t = α̂_(φ_t) (flowAut); and

2. there is a representation (K, π, Ω) reproducing ω, with unitaries U(t) that fix Ω and implement the flow, U(t)π(a)Ω = π(τ_t a)Ω, such that t ↦ U(t) has positive energy (AQFT.IsPositiveEnergy): it is strongly continuous with positive generator.

The generator is the local Hamiltonian of the Killing flow. The ground state is the zero-temperature counterpart of the KMS states of IsKMSStateForFlow. Two consequences do not use the positivity of the generator: a ground state is flow-invariant (IsGroundStateForFlow.invariant) and its unitary group is strongly continuous (IsGroundStateForFlow.exists_strongContinuous_unitary).

Implementation note: the representation space K ranges over Type v, the universe of the local algebras.

Blueprint: def:ground-state-for-flow-in-curved-spacetime

An equivalence of two Haag–Kastler nets along a bijection e of their spacetimes: *-isomorphisms Θ_B : 𝔘₁(B) → 𝔘₂(e(B)) compatible with isotony.

Let M₁ and M₂ be spacetimes, e a bijection from the points of M₁ to those of M₂ that maps basis sets to basis sets (hypothesis he), and N₁, N₂ Haag–Kastler nets over M₁ and M₂. An equivalence of N₁ and N₂ along e chooses, for each basis set B of M₁, a unital *-isomorphism

Θ_B : 𝔘₁(B) → 𝔘₂(e(B)),

which makes sense because e(B) is a basis set of M₂. The isomorphisms must be compatible with the isotony embeddings i₁ and i₂ of the two nets (HaagKastlerNet.commIsotony): whenever B₁ ⊆ B₂ are basis sets of M₁,

Θ_(B₂) ∘ i₁(B₁, B₂) = i₂(e(B₁), e(B₂)) ∘ Θ_(B₁).

The two nets then describe the same physics, with the region B of M₁ corresponding to the region e(B) of M₂.

The family Θ is data, not an existence statement, since the square refers to the chosen maps. The definition mentions no metric and no isometry: all it asks of e is that it carry basis sets to basis sets. The square is attached to a single inclusion, so no coherence hypothesis is needed; Axiom 2 carries the identity and composition laws of the embeddings in any case.

Implementation note: the spacetimes are related by the bijection e rather than by an equality of their carriers, which would be an equality of types and could not be transported along.

Blueprint: def:net-equivalence-in-curved-spacetime

Physicslib4.AQFT.HaagKastlerCurved.NetEquivalence.mk.{u_1, u_2, u_3, u_4}

theta : ⦃B : Set M₁.Carrier⦄ → M₁.IsBasisSet B → N₁.algebra B ≃⋆ₐ[ℂ] N₂.algebra (⇑e '' B)

naturality : ∀ ⦃B₁ B₂ : Set M₁.Carrier⦄ (h₁ : M₁.IsBasisSet B₁) (h₂ : M₁.IsBasisSet B₂) (h : B₁ ⊆ B₂) (a : N₁.algebra B₁),
  (self.theta h₂) ((N₁.commIsotony h₁ h₂ h) a) = (N₂.commIsotony ⋯ ⋯ ⋯) ((self.theta h₁) a)

A net theory: a choice of Haag–Kastler net 𝔘_L over every geometric Lorentzian spacetime L.

A quantum field theory in curved spacetime is not one net but a rule assigning a net to each background. Here the rule is a function L ↦ 𝔘_L from geometric Lorentzian spacetimes to nets over the abstract interfaces they induce (toAbstractIdentityComponent). Quantifying over all Lorentzian spacetimes, rather than over the metrics on one fixed manifold, is what makes general covariance (IsGenerallyCovariant) a statement about the theory: the pullback of any L is again a Lorentzian spacetime, so both nets that general covariance compares are values of the same function.

Implementation note: the spacetimes have their points in Type, and the nets of a net theory share one universe for their local algebras, the universe parameter of NetTheory.

Blueprint: def:general-covariance-in-curved-spacetime

The relabelling bijection of general covariance: a diffeomorphism ψ of M, read as a map from the points of ψ*L to the points of L.

The pullback ψ*L has the same manifold as L, with the pulled-back metric ψ*g and time orientation ψ*t. As a map from ψ*L to L, the diffeomorphism ψ is an isometry, and it carries the causal diamonds of ψ*L to those of L (toAbstractIdentityComponent_pullback_isBasisSet). It is ψ, not its inverse, that does this. General covariance compares the nets over ψ*L and over L along this bijection.

Implementation note: the two carriers are definitionally equal (pullback changes only the metric and the time orientation), but the blueprint relates the two spacetimes by data rather than by a type equality, and this is that datum. The type is stated with .Carrier rather than .toAbstractIdentityComponent.Carrier: the two are definitionally equal, but toAbstractIdentityComponent_Carrier is a simp lemma, so only the former leaves pullbackCarrierEquiv_apply in simp-normal form.

Blueprint: def:general-covariance-in-curved-spacetime

General covariance: a net theory assigns equivalent nets to diffeomorphism-related backgrounds.

The gauge group of general relativity is the diffeomorphism group of M, acting on all fields, the metric included. For a Lorentzian spacetime L with manifold M, metric g and time orientation t, and a smooth diffeomorphism ψ of M, the pullback ψ*L, with metric ψ*g and time orientation ψ*t, differs from L only by a relabelling of the points. A net theory 𝔘 is generally covariant when the nets 𝔘_(ψ*L) and 𝔘_L are equivalent (NetEquivalence) for every such L and ψ, along ψ read as a bijection from the points of ψ*L to those of L (pullbackCarrierEquiv). That ψ carries the diamonds of ψ*L to those of L is toAbstractIdentityComponent_pullback_isBasisSet.

This is a postulate, not a consequence of Axioms 1 to 5, which each constrain a single net over a single spacetime. It encodes Leibniz equivalence, the resolution of the hole argument: the choice of representative within a diffeomorphism class is gauge and can have no observable consequences. It is a property of the theory L ↦ 𝔘_L, not an extra field of HaagKastlerNet, and it says nothing about backgrounds that are not related by a diffeomorphism. Unlike Axiom 5, it is not restricted to diffeomorphisms connected to the identity, since it compares two nets rather than making a group act on one.

Blueprint: def:general-covariance-in-curved-spacetime