§10.5 Spacetime and causal structure (pp. 250–289)

146 items (Definitions 330–475), building the entire causal and topological apparatus the axioms are indexed on. The trips underlying the chronological and causal relations \(\ll\) and \(\prec\) are genuine geodesics of the Levi-Civita connection of the metric, which the section constructs for an arbitrary pseudo-Riemannian metric on top of Mathlib’s covariant derivatives. It proceeds in nine layers.

Spacetime, tangent-vector causality, and curves (pp. 250–256, items 330–357). Gives precise definitions of spacetime (Definition 330) and standard Minkowski spacetime (Definition 331); classifies tangent vectors as timelike, spacelike, or null (Definition 332) and proves the trichotomy (Lemma 333), the reverse Cauchy–Schwarz and reverse triangle inequalities for timelike vectors (Lemmas 334–335), and the cone geometry—orientation of pointing vectors, the sign lemma, definiteness of the spacelike complement of a timelike vector, and convexity of the cones (Lemmas 342–345)—alongside time orientations (Definition 340) and future- and past-pointing vectors (Definition 341). The Lorentz, proper and orthochronous transformations of standard Minkowski spacetime are defined (Definition 336); orthochronous Lorentz transformations preserve the future cone (Lemma 337), the identity is Lorentz, proper and orthochronous and each condition is closed under composition and inversion, so that \(SO(1,3)^{\uparrow}\) is a group (Lemma 338), and the inhomogeneous Lorentz group is built on top of it (Definition 339). Then paths, curves, and oriented curves are defined as equivalence classes of paths up to reparametrisation (Definitions 346–351), with causal type and future/past orientation each shown well-defined on the quotient (Theorems 350 and 352) and a forgetful projection from oriented to unoriented curves (Theorem 353). Endpoints (Definition 354), shown to be well defined on curves and smooth curves (Lemma 355), come with two point-set lemmas—an extremal parameter lies in the frontier, and two endpoints force a compact parameter interval (Lemmas 356–357).
The Levi-Civita connection and geodesics (pp. 256–260, items 358–373). Pseudo-Riemannian metrics (Definition 358) are smooth, symmetric, non-degenerate families of bilinear forms, with no signature condition, so everything here applies to every spacetime. Covariant derivatives are Mathlib’s IsCovariantDerivativeOn; metric compatibility and the Levi-Civita condition (compatible and torsion-free) are defined on top of them (Definitions 359–360). The musical isomorphism \(v \mapsto g_x(v, \cdot)\) is a linear isomorphism at each point (Lemma 361), and its inverse is a smooth section of \(\mathrm{Hom}(T^*M, TM)\) (Lemma 362). The Koszul formula (Lemma 363), the tensoriality of the Koszul expression (Lemma 364), and the verification that the Koszul connection is a covariant derivative (Lemma 365) that is Levi-Civita (Lemma 366) give existence and uniqueness of the Levi-Civita connection (Theorem 367). Five lemmas about smooth paths—a function vanishing along a path has zero derivative along it, the covariant derivative along a curve is local, local vector fields globalise, a smooth path has a local left inverse, and its velocity extends to a smooth vector field (Lemmas 368–372)—make the geodesic condition chart-free, well defined and non-vacuous. A geodesic (Definition 373) is then an affinely parametrised smooth path \(\mu\) in a spacetime with \((\nabla_X X)(\mu(s)) = 0\) at every interior parameter, for every smooth vector field \(X\) extending the velocity near \(s\).
Trips, futures and pasts (pp. 260–262, items 374–382). Trips and causal trips (Definitions 374–375) are finite chains of future-oriented timelike (respectively causal) geodesic segments, geodesic in the sense of Definition 373, with matching past and future endpoints. Chronological and causal precedence are transitive (Theorem 376); the causality condition (Definition 377) makes them a strict partial order (Theorem 378); and chronological and causal futures and pasts (Definitions 379–380) come with their basic inclusion and monotonicity properties (Lemmas 381–382).
§10.5.1 Causal diamonds (p. 262, items 383–398). Introduces the causal diamond \(J^+(p) \cap J^-(q)\) and the chronological (Alexandrov) diamond \(I^+(p) \cap I^-(q)\) (Definition 383), with the structural properties of the causal diamond—monotonicity under endpoint spread, causal convexity, and that nonemptiness forces \(p \prec q\) (Lemma 384)—and the containment of chronological diamonds in causal ones, together with the identification of the Alexandrov basis as exactly the chronological diamonds (Theorem 385). It then develops spacelike separation of points and of regions (Definitions 386–387, Lemmas 388–389), shows that any map preserving causal precedence in both directions preserves spacelike separation of points and complete spacelike separation of regions (Lemma 390), and introduces the spacelike complement \(\mathbf{B}^\perp\) (Definition 391) and its order structure—antitone, extensive on the double complement, with the triple complement collapsing, making complementation the Galois connection attached to the spacelike-separation relation (Lemma 392). The double complement is packaged as the causal closure operator (Definition 393, Lemma 394), whose fixed points are the causally complete regions (Definition 395). These form a complete lattice—meets are intersections, joins are causal closures of unions—on which the causal complement is an order-reversing involution (Theorem 396); the set-level De Morgan laws (Lemma 397) then lift to full binary and infinitary De Morgan laws on the lattice (Theorem 398). The blueprint is careful to record what does not hold: the full orthocomplement law \(\mathbf{B} \wedge \mathbf{B}^\perp = \bot\) fails at this generality, because the trip-based causal relation is irreflexive and so a point is spacelike-separated from itself.
§10.5.2 Causal convexity (p. 267, items 399–401). Defines a causally convex region as one containing every point causally between two of its own points (Definition 399), shows causal diamonds are causally convex (Lemma 400), and shows every spacelike complement—hence every causally complete region—is causally convex (Theorem 401).
§10.5.3 Causal convexity: closure structure, and the Alexandrov basis theorems (p. 267, items 402–425). The causally convex regions are shown to form a closure system (Lemma 402), giving the causal-convex hull (Definition 403) as a genuine closure operator whose closed sets are exactly the causally convex regions (Lemmas 404, Theorem 405). The subsection then turns to the Alexandrov topology (Definition 406): every diamond is open (Lemma 407); chronological futures and pasts are open under an explicit “no endpoints” hypothesis (Lemma 408) and unconditionally on standard Minkowski spacetime, where the coordinate-cone description discharges the hypothesis (Lemma 409). On standard Minkowski spacetime the componentwise directional derivative is a Levi-Civita connection (Lemma 410), hence the Levi-Civita connection is flat (Lemma 411) and affinely parametrised straight lines are geodesics (Lemma 412), so trips there are the familiar straight-line segments. Minkowski spacetime and Lorentzian spacetime are then defined (Definitions 413–414, the latter as a spacetime whose Alexandrov topology is Hausdorff), with a bundled form of spacelike separation and basis openness (Lemma 415). A point lying in no diamond is pathological: its only Alexandrov neighbourhood is the whole space (Lemma 416), and the Hausdorff assumption rules this out, forcing the diamonds to cover the space (Lemma 417). Given downward-directedness the diamonds form a genuine topological basis (Theorem 418); past and future interpolation on standard Minkowski (Lemmas 419–420) supply downward-directedness there (Lemma 421), and common chronological predecessors and successors supply upward-directedness (Lemmas 422–424), so on standard Minkowski the diamonds are an unconditional basis (Theorem 425). Upward-directedness is what the quasilocal colimit of §10.6.1 later consumes.
§10.5.4 Dilations are causal automorphisms but not isometries (p. 274, items 426–428). The dilations \(x \mapsto \lambda x\) preserve the Minkowski cones (Lemma 426) and are therefore causal automorphisms (Theorem 427), yet scale the metric by \(\lambda^2\) and so are not isometries for \(\lambda \neq 1\) (Theorem 428). This is the counterexample that forces the general-covariance morphism of §10.8 to be specified geometrically rather than causally.
§10.5.5 Isometries and basis-set preservation (p. 274, items 429–443). Single-metric transport: isometries preserve the causal classification of tangent vectors (Lemma 429), paths have unique differentials and well-defined pushforwards (Lemmas 430–431), and isometries respect the Levi-Civita structure: pullbacks of vector fields and of the metric pairing, their derivatives and Lie brackets transform naturally (Lemmas 432–434), so an isometry preserves the Levi-Civita connection (Lemma 435) and maps geodesics to geodesics and back (Lemma 436). The inhomogeneous Lorentz group acts on smooth paths by pushforward (Definition 437), carrying future-oriented causal paths to future-oriented causal paths (Lemma 438), so causal precedence (Theorem 439) and spacelike separation (Corollary 440) are Lorentz invariant. Future-orientation-preserving isometries preserve chronology (Lemma 441) and map Alexandrov-basis diamonds to diamonds (Lemma 442), which is exactly the well-definedness condition for the Axiom 5 action (Lemma 443).
§10.5.6 Pullback metrics and cross-metric isometries (p. 277, items 444–475). The single-metric lemmas above compare a spacetime with itself; general covariance instead compares two different metrics on one carrier, so the transport statements are redone cross-metric. This subsection defines the pullback \(\psi^* g\) of a spacetime metric as a bundled family of continuous bilinear forms (Definition 444) and verifies every obligation in turn: the differential of a diffeomorphism is a linear equivalence (Lemma 445), with the two round-trip cancellation identities for a global Diffeomorph (Lemmas 446–448); the pullback metric is symmetric, non-degenerate, Lorentzian, and a smooth section of the bilinear-form bundle (Lemmas 449–452), so the pullback of a spacetime is a spacetime (Theorem 453). Two-sided preservation of future orientation is then defined (Definition 454) and the pullback time orientation is shown to be bundle-smooth, nowhere vanishing, and everywhere timelike (Lemmas 455–458), with transport of future-pointing timelike and null vectors (Lemmas 459–460) giving two-sided orientation preservation (Lemma 461). Cross-metric isometries are defined (Definition 462) and shown closed under inverses (Lemma 463), to preserve causal classification (Lemma 464), to push paths forward preserving the timelike/causal conditions and endpoints (Lemmas 465–468), and to transport chronological precedence and the chronological future and past (Lemmas 469–471), hence to preserve Alexandrov-basis sets (Lemma 472). A general topological lemma—a bijection matching generating families is a homeomorphism (Lemma 473)—then identifies the pullback Alexandrov topology (Lemma 474) and yields that the pullback of a Lorentzian spacetime is again a Lorentzian spacetime (Theorem 475). Without Theorem 475 the phrase “the net over \(\psi^*(M,g)\)” in §10.8 would have no referent.

Where the Lean lives: Physicslib4/Geometry/PseudoRiemannian/ (Basic, LeviCivita, Flat), Physicslib4/Spacetime/ (Causality, Curves, AlongPath, CausalComplement, CausalStructure, Minkowski, MinkowskiDirected, LorentzianSpacetime, IsometryCausality, …)

Items

Each blueprint subsection below is collapsed; click a heading to see its items. Every entry links to its node in the web blueprint and names the principal Lean declaration.

§10.5 opening run — spacetime, tangent-vector causality, curves, the Levi-Civita connection and geodesics, trips, futures and pasts (p. 250) — 53 items

Definition 330 — Spacetime · Physicslib4.Spacetime
Definition 331 — Standard Minkowski Spacetime · Physicslib4.StandardMinkowskiSpacetime
Definition 332 — Timelike, Spacelike, or Null Vectors · Physicslib4.Spacetime.IsTimelike (+2 more)
Lemma 333 — Causal Classification · Physicslib4.Spacetime.isTimelike_or_isNull_or_isSpacelike (+5 more)
Lemma 334 — Reverse Cauchy–Schwarz for Timelike Vectors · Physicslib4.reverse_cauchy_schwarz_of_lorentzianAt (+1 more)
Lemma 335 — Timelike Cone Convexity and Reverse Triangle Inequality · Physicslib4.add_isTimelike_of_lorentzianAt (+3 more)
Definition 336 — Lorentz, Proper and Orthochronous Transformations · Physicslib4.IsLorentz (+2 more)
Lemma 337 — Orthochronous Lorentz Transformations Preserve the Future Cone · Physicslib4.isOrthochronous_pos_time_of_timelike
Lemma 338 — Closure of the Lorentz Conditions · Physicslib4.isLorentz_refl (+8 more)
Definition 339 — Inhomogeneous Lorentz Group · Physicslib4.AQFT.HaagKastler.InhomogeneousLorentzGroup
Definition 340 — Time Orientation · Physicslib4.Spacetime.TimeOrientation (+1 more)
Definition 341 — Future and Past Pointing Vectors · Physicslib4.Spacetime.IsFuturePointing (+1 more)
Lemma 342 — Orientation of Pointing Vectors · Physicslib4.Spacetime.isTimelike_or_isNull_of_isFuturePointing (+2 more)
Lemma 343 — Sign Lemma for the Future Cone · Physicslib4.nonneg_of_orthogonal_timelike (+4 more)
Lemma 344 — Definiteness of the Spacelike Complement · Physicslib4.eq_zero_of_forall_bilin_eq_zero (+2 more)
Lemma 345 — Convexity of the Future Cone · Physicslib4.Spacetime.isFuturePointing_add (+10 more)
Definition 346 — Paths · Physicslib4.Spacetime.Path (+1 more)
Definition 347 — Curves · Physicslib4.Spacetime.Curve (+1 more)
Definition 348 — Timelike and Causal Smooth Curves · Physicslib4.Spacetime.IsTimelikeSmoothCurve (+1 more)
Definition 349 — Future and Past Oriented Smooth Curves · Physicslib4.Spacetime.IsFutureOrientedSmoothCurve (+1 more)
Theorem 350 — Reparametrisation-Invariance of the Causal Type · Physicslib4.Spacetime.isTimelikeSmoothCurve_ofPath_iff (+1 more)
Definition 351 — Oriented Smooth Curve · Physicslib4.Spacetime.OrientedSmoothCurve
Theorem 352 — Reparametrisation-Invariance of Orientation · Physicslib4.Spacetime.isFutureOrientedCurve_ofPath_iff (+1 more)
Theorem 353 — The Forgetful Projection of Oriented Curves · Physicslib4.Spacetime.OrientedSmoothCurve.toSmoothCurve (+1 more)
Definition 354 — Endpoints · Physicslib4.Spacetime.IsEndpoint (+2 more)
Lemma 355 — Endpoints of curves are well defined · Physicslib4.Spacetime.IsCurveEndpoint (+5 more)
Lemma 356 — An extremal parameter lies in the frontier · Physicslib4.Spacetime.mem_frontier_of_isMin (+3 more)
Lemma 357 — Two endpoints force a compact parameter interval · Physicslib4.Spacetime.parameterSpace_eq_Icc_of_endpoints
Definition 358 — Pseudo-Riemannian Metric · Physicslib4.Geometry.PseudoRiemannianMetric (+1 more)
Definition 359 — Covariant Derivative; Metric Compatibility · Physicslib4.Geometry.CovariantDerivative.IsMetricCompatibleWith
Definition 360 — Levi-Civita Connection · Physicslib4.Geometry.CovariantDerivative.IsLeviCivitaFor
Lemma 361 — Musical Isomorphism · Physicslib4.Geometry.PseudoRiemannianMetric.bijective_val
Lemma 362 — Smoothness of the Inverse Musical Isomorphism · Physicslib4.Geometry.PseudoRiemannianMetric.contMDiff_flatEquiv_symm (+1 more)
Lemma 363 — Koszul Formula · Physicslib4.Geometry.CovariantDerivative.IsLeviCivitaFor.koszul
Lemma 364 — Tensoriality of the Koszul Expression · Physicslib4.Geometry.PseudoRiemannianMetric.tensorialAt_koszulAux₁ (+2 more)
Lemma 365 — The Koszul Connection is a Covariant Derivative · Physicslib4.Geometry.PseudoRiemannianMetric.isCovariantDerivativeOn_leviCivitaAux
Lemma 366 — The Koszul Connection is Levi-Civita · Physicslib4.Geometry.PseudoRiemannianMetric.isMetricCompatibleWith_koszulConnection (+1 more)
Theorem 367 — Existence and Uniqueness of the Levi-Civita Connection · Physicslib4.Geometry.PseudoRiemannianMetric.exists_isLeviCivitaFor (+3 more)
Lemma 368 — A Function Vanishing Along a Path has Zero Derivative Along It · Physicslib4.Spacetime.SmoothPath.mfderiv_apply_tangent_eq_zero
Lemma 369 — Covariant Derivative Along a Curve is Local · Physicslib4.Spacetime.SmoothPath.covDeriv_eq_of_eventuallyEq
Lemma 370 — Local Vector Fields Globalise · Physicslib4.Spacetime.exists_contMDiff_vectorField_eventuallyEq
Lemma 371 — Local Left Inverse of a Smooth Path · Physicslib4.Spacetime.SmoothPath.exists_localLeftInverse
Lemma 372 — The Velocity of a Smooth Path Extends to a Vector Field · Physicslib4.Spacetime.SmoothPath.exists_vectorField_eq_tangent
Definition 373 — Geodesic · Physicslib4.Spacetime.IsGeodesic
Definition 374 — Trip · Physicslib4.Spacetime.IsTripSegment (+2 more)
Definition 375 — Causal Trip · Physicslib4.Spacetime.IsCausalTripSegment (+2 more)
Theorem 376 — Transitivity of chronological and causal precedence · Physicslib4.Spacetime.chronologicallyPrecedes_trans (+1 more)
Definition 377 — No Closed Causal Curve (Causality Condition) · Physicslib4.Spacetime.NoClosedCausalCurve
Theorem 378 — Irreflexivity and Antisymmetry under Causality · Physicslib4.Spacetime.chronologicallyPrecedes_irrefl (+2 more)
Definition 379 — Chronological Future and Chronological Past · Physicslib4.Spacetime.chronologicalFuture (+3 more)
Definition 380 — Causal Future and Causal Past · Physicslib4.Spacetime.causalFuture (+3 more)
Lemma 381 — Chronological Precedence Implies Causal Precedence · Physicslib4.Spacetime.isCausal_of_isTimelike (+3 more)
Lemma 382 — Monotonicity of Futures and Pasts · Physicslib4.Spacetime.chronologicalFutureSet_mono (+3 more)

§10.5.1 Causal diamonds, spacelike complement, and causal closure (p. 262) — 16 items

Definition 383 — Causal and chronological diamonds · Physicslib4.Spacetime.causalDiamond (+3 more)
Lemma 384 — Structural properties of the causal diamond · Physicslib4.Spacetime.causalDiamond_subset_of (+2 more)
Theorem 385 — Chronological diamonds inside causal diamonds · Physicslib4.Spacetime.chronologicalDiamond_subset_causalDiamond (+1 more)
Definition 386 — Spacelike Related · Physicslib4.Spacetime.IsSpacelikeRelated
Definition 387 — Completely Spacelike · Physicslib4.Spacetime.IsCompletelySpacelike
Lemma 388 — Symmetry of Spacelike Separation · Physicslib4.Spacetime.isSpacelikeRelated_comm (+1 more)
Lemma 389 — Structural Properties of Complete Spacelike Separation · Physicslib4.Spacetime.isCompletelySpacelike_mono (+9 more)
Lemma 390 — Precedence-Preserving Maps Preserve Spacelike Separation · Physicslib4.Spacetime.isSpacelikeRelated_congr (+1 more)
Definition 391 — Spacelike Complement of a Region · Physicslib4.Spacetime.LorentzianSpacetime.spacelikeComplement
Lemma 392 — Order Structure of the Spacelike Complement · Physicslib4.Spacetime.LorentzianSpacetime.spacelikeComplement_antitone (+3 more)
Definition 393 — Causal closure operator · Physicslib4.Spacetime.LorentzianSpacetime.causalClosure
Lemma 394 — The Causal Closure is a Closure Operator · Physicslib4.Spacetime.LorentzianSpacetime.causalClosure (+1 more)
Definition 395 — Causally complete region · Physicslib4.Spacetime.LorentzianSpacetime.IsCausallyComplete
Theorem 396 — Lattice of causally complete regions · Physicslib4.Spacetime.LorentzianSpacetime.CausallyCompleteRegion (+8 more)
Lemma 397 — De Morgan Laws for the Spacelike Complement · Physicslib4.Spacetime.LorentzianSpacetime.spacelikeComplement_union (+1 more)
Theorem 398 — De Morgan Laws for the Causal Complement · Physicslib4.Spacetime.LorentzianSpacetime.causalComplement_antitone (+6 more)

§10.5.2 Causal convexity (p. 267) — 3 items

Definition 399 — Causally convex region · Physicslib4.Spacetime.IsCausallyConvex
Lemma 400 — Causal diamonds are causally convex · Physicslib4.Spacetime.causalDiamond_isCausallyConvex
Theorem 401 — Causally complete regions are causally convex · Physicslib4.Spacetime.spacelikeComplement_isCausallyConvex (+2 more)

§10.5.3 Causal convexity: closure structure, and the Alexandrov basis theorems (p. 267) — 24 items

Lemma 402 — Causally convex regions form a closure system · Physicslib4.Spacetime.isCausallyConvex_univ (+4 more)
Definition 403 — Causal-convex hull · Physicslib4.Spacetime.causalConvexHull
Lemma 404 — The Causal-Convex Hull is Extensive and Causally Convex · Physicslib4.Spacetime.subset_causalConvexHull (+1 more)
Theorem 405 — The causal-convex hull is a closure operator · Physicslib4.Spacetime.causalConvexHull_minimal (+3 more)
Definition 406 — Alexandrov Topology · Physicslib4.Spacetime.alexandrovTopology
Lemma 407 — Basis Sets Are Alexandrov-Open · Physicslib4.Spacetime.isOpen_alexandrov_of_mem_basis
Lemma 408 — Openness of Chronological Futures and Pasts · Physicslib4.Spacetime.isOpen_chronologicalFuture_inter_chronologicalPast (+2 more)
Lemma 409 — Unconditional Openness of Chronological Futures and Pasts on Standard Minkowski · Physicslib4.exists_chronologicalFuture_standardMinkowski (+5 more)
Lemma 410 — The Directional Derivative is Levi-Civita on Standard Minkowski · Physicslib4.Geometry.PseudoRiemannianMetric.isLeviCivitaFor_flatConnection (+2 more)
Lemma 411 — The Minkowski Levi-Civita Connection is Flat · Physicslib4.standardMinkowski_leviCivita_apply (+1 more)
Lemma 412 — Straight Lines are Geodesics in Standard Minkowski · Physicslib4.standardMinkowskiLineSegmentPath_isGeodesic (+1 more)
Definition 413 — Minkowski Spacetime · Physicslib4.MinkowskiSpacetime
Definition 414 — Lorentzian Spacetime · Physicslib4.Spacetime.LorentzianSpacetime
Lemma 415 — Bundled Spacelike Separation and Basis Openness · Physicslib4.Spacetime.LorentzianSpacetime.isCompletelySpacelike_comm (+1 more)
Lemma 416 — No-Diamond Points Have Only the Whole Space as Neighbourhood · Physicslib4.Spacetime.alexandrov_nbhd_univ_of_no_diamond
Lemma 417 — Covering from the Hausdorff Assumption · Physicslib4.Spacetime.LorentzianSpacetime.sUnion_alexandrovBasis_eq_univ
Theorem 418 — The Alexandrov Diamonds Form a Topological Basis · Physicslib4.Spacetime.LorentzianSpacetime.isTopologicalBasis_alexandrovBasis
Lemma 419 — Past Interpolation on Standard Minkowski · Physicslib4.Spacetime.exists_past_between_standardMinkowski
Lemma 420 — Future Interpolation on Standard Minkowski · Physicslib4.Spacetime.exists_future_between_standardMinkowski
Lemma 421 — Standard Minkowski Diamonds Are Downward-Directed · Physicslib4.Spacetime.alexandrovBasis_exists_subset_inter_standardMinkowski
Lemma 422 — Common Chronological Predecessor on Standard Minkowski · Physicslib4.Spacetime.exists_common_past
Lemma 423 — Common Chronological Successor on Standard Minkowski · Physicslib4.Spacetime.exists_common_future
Lemma 424 — Standard Minkowski Diamonds Are Upward-Directed · Physicslib4.Spacetime.alexandrovBasis_directed
Theorem 425 — The Alexandrov Diamonds are a Basis on Standard Minkowski · Physicslib4.Spacetime.isTopologicalBasis_alexandrovBasis_standardMinkowski

§10.5.4 Dilations are causal automorphisms but not isometries (p. 274) — 3 items

Lemma 426 — Dilations Preserve the Minkowski Cones · Physicslib4.minkowskiForwardCone_smul (+1 more)
Theorem 427 — Dilations are Causal Automorphisms · Physicslib4.alexandrovBasis_image_smul
Theorem 428 — Dilations are Not Isometries · Physicslib4.minkowskiForm_smul (+1 more)

§10.5.5 Isometries and basis-set preservation (p. 274) — 15 items

Lemma 429 — Isometries Preserve the Causal Classification · Physicslib4.Spacetime.Isometry.preserves_self (+3 more)
Lemma 430 — Unique Differentials Along a Path · Physicslib4.Spacetime.Path.uniqueDiffOn_parameterSpace
Lemma 431 — Pushforward of a Path Under an Isometry · Physicslib4.Spacetime.Isometry.pushforwardPath (+5 more)
Lemma 432 — Pullback of Vector Fields and the Metric Under an Isometry · Physicslib4.Spacetime.Isometry.val_mpullback (+3 more)
Lemma 433 — Derivatives of Metric Pairings of Pulled-Back Fields · Physicslib4.Spacetime.Isometry.mfderiv_val_mpullback (+1 more)
Lemma 434 — Metric Pairings with Lie Brackets of Pulled-Back Fields · Physicslib4.Spacetime.Isometry.val_mlieBracket_mpullback (+1 more)
Lemma 435 — Isometries Preserve the Levi-Civita Connection · Physicslib4.Spacetime.Isometry.mfderiv_leviCivita_mpullback (+1 more)
Lemma 436 — Isometries Preserve Geodesics · Physicslib4.Spacetime.Isometry.pushforwardPath_isGeodesic (+2 more)
Definition 437 — Lorentz Pushforward of a Smooth Path · Physicslib4.lorentzPath
Lemma 438 — Lorentz Pushforward of Causal Paths · Physicslib4.lorentzPath_mfderivWithin (+4 more)
Theorem 439 — Lorentz Invariance of Causal Precedence · Physicslib4.causalSegmentPrecedes_smul (+2 more)
Corollary 440 — Lorentz Invariance of Spacelike Separation · Physicslib4.isSpacelikeRelated_smul_iff (+1 more)
Lemma 441 — Isometries Preserve Chronology · Physicslib4.Spacetime.Isometry.PreservesFutureOrientation (+8 more)
Lemma 442 — Isometries Preserve Basis Sets · Physicslib4.Spacetime.Isometry.futureOrientationPreserving (+8 more)
Lemma 443 — Axiom 5 Basis-Set Preservation · Physicslib4.Spacetime.LorentzianSpacetime.toAbstractIdentityComponent_isBasisSet_smul

§10.5.6 Pullback metrics and cross-metric isometries (p. 277) — 32 items

Definition 444 — Pullback of a Spacetime Metric · Physicslib4.Spacetime.bilinearPrecomp (+3 more)
Lemma 445 — The Differential of a Diffeomorphism is a Linear Equivalence · Physicslib4.Spacetime.Diffeo (+4 more)
Lemma 446 — Round-Trip Cancellation: \(d\psi\) After \(d(\psi^{-1})\) · Physicslib4.Spacetime.mfderiv_symm_cancel_left
Lemma 447 — Round-Trip Cancellation: \(d(\psi^{-1})\) After \(d\psi\) · Physicslib4.Spacetime.mfderiv_symm_cancel_right
Lemma 448 — The Formal Inverse of \(d\psi_x\) is the Inverse Equivalence · Physicslib4.Spacetime.inverse_mfderiv_eq_symm (+2 more)
Lemma 449 — The Pullback Metric is Symmetric · Physicslib4.Spacetime.pullbackVal_symm
Lemma 450 — The Pullback Metric is Non-Degenerate · Physicslib4.Spacetime.pullbackVal_nondegenerate
Lemma 451 — The Pullback Metric is Lorentzian · Physicslib4.Spacetime.pullbackVal_lorentzian
Lemma 452 — The Pullback Metric is a Smooth Section of the Bilinear-Form Bundle · Physicslib4.Spacetime.pullbackVal_contMDiff
Theorem 453 — The Pullback of a Spacetime is a Spacetime · Physicslib4.Spacetime.pullback (+4 more)
Definition 454 — Two-Sided Preservation of Future Orientation · Physicslib4.Spacetime.PreservesFutureOrientation (+1 more)
Lemma 455 — The Pullback of a Bundle-Smooth Vector Field Along a Diffeomorphism is Bundle-Smooth · Physicslib4.Spacetime.contMDiff_mpullback_vectorField
Lemma 456 — The Pullback Time Orientation is Nowhere Vanishing · Physicslib4.Spacetime.mpullback_field_ne_zero
Lemma 457 — The Pullback Time Orientation is Everywhere Timelike · Physicslib4.Spacetime.pullbackVal_mpullback_field_self (+1 more)
Lemma 458 — Pullback of a Time Orientation · Physicslib4.Spacetime.pullbackTimeOrientation (+1 more)
Lemma 459 — Transport of Future-Pointing Timelike Vectors · Physicslib4.Spacetime.pullbackVal_mpullback_field_apply (+1 more)
Lemma 460 — Transport of Future-Pointing Null Vectors · Physicslib4.Spacetime.isFuturePointing_pullback_iff_of_isNull
Lemma 461 — The Pullback Preserves the Future Orientation Two-Sidedly · Physicslib4.Spacetime.pullback_preservesFutureOrientationTwoSided
Definition 462 — Isometry Between Two Metrics on One Manifold · Physicslib4.Spacetime.CrossIsometry (+4 more)
Lemma 463 — The Inverse of a Cross-Metric Isometry is a Cross-Metric Isometry · Physicslib4.Spacetime.CrossIsometry.symm_preserves (+1 more)
Lemma 464 — Cross-Metric Isometries Preserve the Causal Classification · Physicslib4.Spacetime.CrossIsometry.preserves_self (+3 more)
Lemma 465 — The Tangent Chain Rule Along a Path · Physicslib4.Spacetime.mfderivWithin_comp_diffeo (+1 more)
Lemma 466 — Pushforward of a Path Under a Cross-Metric Isometry · Physicslib4.Spacetime.pushforwardPath (+2 more)
Lemma 467 — The Pushforward Preserves the Timelike and Causal Conditions · Physicslib4.Spacetime.CrossIsometry.pushforwardPath_isTimelike (+1 more)
Lemma 468 — The Pushforward Transports Endpoints · Physicslib4.Spacetime.pushforwardPath_isPastEndpoint (+1 more)
Lemma 469 — Cross-Metric Isometries Transport Chronological Precedence · Physicslib4.Spacetime.pushforwardPath_isFutureOriented (+2 more)
Lemma 470 — Image of the Chronological Future · Physicslib4.Spacetime.CrossIsometry.chronologicalFuture_image
Lemma 471 — Image of the Chronological Past · Physicslib4.Spacetime.CrossIsometry.chronologicalPast_image
Lemma 472 — Cross-Metric Isometries Preserve Basis Sets · Physicslib4.Spacetime.CrossIsometry.alexandrovDiamond_image (+1 more)
Lemma 473 — A Bijection Matching Generating Families is a Homeomorphism · Physicslib4.continuous_generateFrom_of_preimage_mem (+4 more)
Lemma 474 — The Pullback Alexandrov Topology · Physicslib4.Spacetime.pullback_alexandrovBasis_image (+3 more)
Theorem 475 — The Pullback of a Lorentzian Spacetime is a Lorentzian Spacetime · Physicslib4.Spacetime.LorentzianSpacetime.pullback_alexandrov_t2 (+3 more)

Home · §10.1 GNS · §10.2 Spectral · §10.3 Unbounded · §10.4 Stone · §10.5 Spacetime · §10.6 Minkowski · §10.7 Curved · §10.8 Covariance · Axioms · Guide

← §10.4 Stone · §10.6 Minkowski →