Path-integral naturality (jacobian-functoriality §4) #
Unit: jacobian-functoriality. IsPrimitiveAlongMap.pullback_comp (a general reusable lemma: a
primitive of η along f ∘ K pulls back to a primitive of Form1.pullback f hf η along K)
and its corollary pathIntegral_pullback (naturality of pathIntegral under pullback).
theorem
RS.IsPrimitiveAlongMap.pullback_comp
{X : Type u_1}
[TopologicalSpace X]
[ChartedSpace ℂ X]
[IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X]
{Y : Type u_2}
[TopologicalSpace Y]
[ChartedSpace ℂ Y]
[IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y]
{α : Type u_3}
[TopologicalSpace α]
{f : X → Y}
(hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f)
{K : α → X}
{s : Set α}
(hK : ContinuousOn K s)
{η : Form1 Y}
{F : α → ℂ}
(h : IsPrimitiveAlongMap (f ∘ K) η F s)
:
IsPrimitiveAlongMap K ((Form1.pullback f hf) η) F s
A primitive of η along f ∘ K pulls back to a primitive of Form1.pullback f hf η
along K (§4.2).
Naturality of pathIntegral #
theorem
RS.pathIntegral_pullback
{X : Type u_1}
[TopologicalSpace X]
[ChartedSpace ℂ X]
[IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X]
{Y : Type u_2}
[TopologicalSpace Y]
[ChartedSpace ℂ Y]
[IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y]
{x y : X}
{f : X → Y}
(hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f)
(γ : Path x y)
(η : Form1 Y)
: