Pullback of rough bundle-valued differential forms

Pullback precomposes each alternating map with the manifold derivative. Its value fiber at x is the original fiber at f x, so it works without a trivialization of the value bundle. Both within-set and unrestricted pullbacks are total; their chain rules carry the differentiability and unique-derivative hypotheses of Mathlib's mfderivWithin. For a trivial value bundle, mpullbackWithin and mpullback retain the fixed coefficient space. On model spaces they agree with precomposition by the Fréchet derivative. Pullback at x only depends on the germ of f at x, within-set pullback at x only on the value at x and the germ within the set, and when the derivative of f at x is surjective it determines the form at f x.

This construction follows Lee, Introduction to Smooth Manifolds, second edition, Chapter 14. The proofs reuse Mathlib's manifold chain rule and alternating-map composition.

noncomputable def TauCeti.bundleMpullbackWithin {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {k : ℕ} {V : M' → Type u_10} [(y : M') → AddCommGroup (V y)] [(y : M') → Module ℝ (V y)] [(y : M') → TopologicalSpace (V y)] (I : ModelWithCorners ℝ E H) (I' : ModelWithCorners ℝ E' H') (f : M → M') (s : Set M) (ω : RoughBundleForm I' M' V k) : RoughBundleForm I M (fun (x : M) => V (f x)) k

Pullback using the derivative within s; the value bundle is pulled back along f.

@[simp]

theorem TauCeti.bundleMpullbackWithin_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {V : M' → Type u_10} [(y : M') → AddCommGroup (V y)] [(y : M') → Module ℝ (V y)] [(y : M') → TopologicalSpace (V y)] (f : M → M') (s : Set M) (ω : RoughBundleForm I' M' V k) (x : M) (v : Fin k → TangentSpace I x) : (bundleMpullbackWithin I I' f s ω x) v = (ω (f x)) fun (i : Fin k) => (mfderiv[s] f x) (v i)

Evaluation of within-set pullback on tangent vectors.

noncomputable def TauCeti.bundleMpullback {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {k : ℕ} {V : M' → Type u_10} [(y : M') → AddCommGroup (V y)] [(y : M') → Module ℝ (V y)] [(y : M') → TopologicalSpace (V y)] (I : ModelWithCorners ℝ E H) (I' : ModelWithCorners ℝ E' H') (f : M → M') (ω : RoughBundleForm I' M' V k) : RoughBundleForm I M (fun (x : M) => V (f x)) k

Pullback of a rough form, with values in the pulled-back value bundle.

@[simp]

theorem TauCeti.bundleMpullback_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {V : M' → Type u_10} [(y : M') → AddCommGroup (V y)] [(y : M') → Module ℝ (V y)] [(y : M') → TopologicalSpace (V y)] (f : M → M') (ω : RoughBundleForm I' M' V k) (x : M) (v : Fin k → TangentSpace I x) : (bundleMpullback I I' f ω x) v = (ω (f x)) fun (i : Fin k) => (mfderiv% f x) (v i)

Evaluation of pullback on tangent vectors.

@[simp]

theorem TauCeti.bundleMpullbackWithin_univ {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {V : M' → Type u_10} [(y : M') → AddCommGroup (V y)] [(y : M') → Module ℝ (V y)] [(y : M') → TopologicalSpace (V y)] (f : M → M') (ω : RoughBundleForm I' M' V k) : bundleMpullbackWithin I I' f Set.univ ω = bundleMpullback I I' f ω

The within-set construction on the whole manifold is ordinary pullback.

@[simp]

theorem TauCeti.bundleMpullbackWithin_eq_bundleMpullback {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {V : M' → Type u_10} [(y : M') → AddCommGroup (V y)] [(y : M') → Module ℝ (V y)] [(y : M') → TopologicalSpace (V y)] {f : M → M'} {s : Set M} {x : M} (hs : UniqueMDiffAt[s] x) (hf : MDiffAt f x) (ω : RoughBundleForm I' M' V k) : bundleMpullbackWithin I I' f s ω x = bundleMpullback I I' f ω x

Within-set and ordinary pullback agree where the derivatives agree.

@[simp]

theorem TauCeti.bundleMpullbackWithin_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {V : M' → Type u_10} [(y : M') → AddCommGroup (V y)] [(y : M') → Module ℝ (V y)] [(y : M') → TopologicalSpace (V y)] (f : M → M') (s : Set M) : bundleMpullbackWithin I I' f s 0 = 0

Within-set pullback preserves the zero form.

@[simp]

theorem TauCeti.bundleMpullback_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {V : M' → Type u_10} [(y : M') → AddCommGroup (V y)] [(y : M') → Module ℝ (V y)] [(y : M') → TopologicalSpace (V y)] (f : M → M') : bundleMpullback I I' f 0 = 0

Pullback preserves the zero form.

@[simp]

theorem TauCeti.bundleMpullbackWithin_add {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {V : M' → Type u_10} [(y : M') → AddCommGroup (V y)] [(y : M') → Module ℝ (V y)] [(y : M') → TopologicalSpace (V y)] [∀ (y : M'), ContinuousAdd (V y)] (f : M → M') (s : Set M) (ω η : RoughBundleForm I' M' V k) : bundleMpullbackWithin I I' f s (ω + η) = bundleMpullbackWithin I I' f s ω + bundleMpullbackWithin I I' f s η

Within-set pullback distributes over addition.

@[simp]

theorem TauCeti.bundleMpullback_add {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {V : M' → Type u_10} [(y : M') → AddCommGroup (V y)] [(y : M') → Module ℝ (V y)] [(y : M') → TopologicalSpace (V y)] [∀ (y : M'), ContinuousAdd (V y)] (f : M → M') (ω η : RoughBundleForm I' M' V k) : bundleMpullback I I' f (ω + η) = bundleMpullback I I' f ω + bundleMpullback I I' f η

Pullback distributes over addition.

@[simp]

theorem TauCeti.bundleMpullbackWithin_smul {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {V : M' → Type u_10} [(y : M') → AddCommGroup (V y)] [(y : M') → Module ℝ (V y)] [(y : M') → TopologicalSpace (V y)] {S : Type u_11} [Monoid S] [(y : M') → DistribMulAction S (V y)] [∀ (y : M'), ContinuousConstSMul S (V y)] [∀ (y : M'), SMulCommClass ℝ S (V y)] (f : M → M') (s : Set M) (c : S) (ω : RoughBundleForm I' M' V k) : bundleMpullbackWithin I I' f s (c • ω) = c • bundleMpullbackWithin I I' f s ω

Within-set pullback commutes with scalar multiplication of the values, by any scalars acting continuously on the fibres and commuting with the real action.

@[simp]

theorem TauCeti.bundleMpullback_smul {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {V : M' → Type u_10} [(y : M') → AddCommGroup (V y)] [(y : M') → Module ℝ (V y)] [(y : M') → TopologicalSpace (V y)] {S : Type u_11} [Monoid S] [(y : M') → DistribMulAction S (V y)] [∀ (y : M'), ContinuousConstSMul S (V y)] [∀ (y : M'), SMulCommClass ℝ S (V y)] (f : M → M') (c : S) (ω : RoughBundleForm I' M' V k) : bundleMpullback I I' f (c • ω) = c • bundleMpullback I I' f ω

Pullback commutes with scalar multiplication of the values, by any scalars acting continuously on the fibres and commuting with the real action.

@[simp]

theorem TauCeti.bundleMpullbackWithin_id {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {V : M → Type u_10} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] {s : Set M} {x : M} (hs : UniqueMDiffAt[s] x) (ω : RoughBundleForm I M V k) : bundleMpullbackWithin I I id s ω x = ω x

Within-set pullback by the identity fixes a form wherever the derivative is unique.

@[simp]

theorem TauCeti.bundleMpullback_id {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {V : M → Type u_10} [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] (ω : RoughBundleForm I M V k) : bundleMpullback I I id ω = ω

Pullback by the identity fixes a rough form.

theorem TauCeti.bundleMpullbackWithin_comp_at {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {E'' : Type u_7} {H'' : Type u_8} {M'' : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} [NormedAddCommGroup E''] [NormedSpace ℝ E''] [TopologicalSpace H''] [TopologicalSpace M''] [ChartedSpace H'' M''] {I'' : ModelWithCorners ℝ E'' H''} {k : ℕ} {V : M'' → Type u_10} [(z : M'') → AddCommGroup (V z)] [(z : M'') → Module ℝ (V z)] [(z : M'') → TopologicalSpace (V z)] {f : M → M'} {g : M' → M''} {s : Set M} {t : Set M'} {x : M} (hf : MDiffAt[s] f x) (hg : MDiffAt[t] g (f x)) (hst : Set.MapsTo f s t) (hs : UniqueMDiffAt[s] x) (ω : RoughBundleForm I'' M'' V k) : bundleMpullbackWithin I I'' (g ∘ f) s ω x = bundleMpullbackWithin I I' f s (bundleMpullbackWithin I' I'' g t ω) x

The chain rule for bundle-valued pullbacks within sets.

theorem TauCeti.bundleMpullbackWithin_comp_of_preimage_mem_nhdsWithin {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {E'' : Type u_7} {H'' : Type u_8} {M'' : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} [NormedAddCommGroup E''] [NormedSpace ℝ E''] [TopologicalSpace H''] [TopologicalSpace M''] [ChartedSpace H'' M''] {I'' : ModelWithCorners ℝ E'' H''} {k : ℕ} {V : M'' → Type u_10} [(z : M'') → AddCommGroup (V z)] [(z : M'') → Module ℝ (V z)] [(z : M'') → TopologicalSpace (V z)] {f : M → M'} {g : M' → M''} {s : Set M} {t : Set M'} {x : M} (hf : MDiffAt[s] f x) (hg : MDiffAt[t] g (f x)) (hst : f ⁻¹' t ∈ nhdsWithin x s) (hs : UniqueMDiffAt[s] x) (ω : RoughBundleForm I'' M'' V k) : bundleMpullbackWithin I I'' (g ∘ f) s ω x = bundleMpullbackWithin I I' f s (bundleMpullbackWithin I' I'' g t ω) x

The chain rule for bundle-valued pullbacks when the intermediate set condition holds only locally at the base point.

theorem TauCeti.bundleMpullback_comp_at {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {E'' : Type u_7} {H'' : Type u_8} {M'' : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} [NormedAddCommGroup E''] [NormedSpace ℝ E''] [TopologicalSpace H''] [TopologicalSpace M''] [ChartedSpace H'' M''] {I'' : ModelWithCorners ℝ E'' H''} {k : ℕ} {V : M'' → Type u_10} [(z : M'') → AddCommGroup (V z)] [(z : M'') → Module ℝ (V z)] [(z : M'') → TopologicalSpace (V z)] {f : M → M'} {g : M' → M''} {x : M} (hf : MDiffAt f x) (hg : MDiffAt g (f x)) (ω : RoughBundleForm I'' M'' V k) : bundleMpullback I I'' (g ∘ f) ω x = bundleMpullback I I' f (bundleMpullback I' I'' g ω) x

The chain rule for bundle-valued pullback at one point.

theorem TauCeti.bundleMpullback_comp_on {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {E'' : Type u_7} {H'' : Type u_8} {M'' : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} [NormedAddCommGroup E''] [NormedSpace ℝ E''] [TopologicalSpace H''] [TopologicalSpace M''] [ChartedSpace H'' M''] {I'' : ModelWithCorners ℝ E'' H''} {k : ℕ} {V : M'' → Type u_10} [(z : M'') → AddCommGroup (V z)] [(z : M'') → Module ℝ (V z)] [(z : M'') → TopologicalSpace (V z)] {f : M → M'} {g : M' → M''} {s : Set M} (hf : ∀ x ∈ s, MDiffAt f x) (hg : ∀ x ∈ s, MDiffAt g (f x)) (ω : RoughBundleForm I'' M'' V k) (x : M) : x ∈ s → bundleMpullback I I'' (g ∘ f) ω x = bundleMpullback I I' f (bundleMpullback I' I'' g ω) x

The chain rule on a set, requiring differentiability only at its points and their images.

theorem TauCeti.bundleMpullback_comp {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {E'' : Type u_7} {H'' : Type u_8} {M'' : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} [NormedAddCommGroup E''] [NormedSpace ℝ E''] [TopologicalSpace H''] [TopologicalSpace M''] [ChartedSpace H'' M''] {I'' : ModelWithCorners ℝ E'' H''} {k : ℕ} {V : M'' → Type u_10} [(z : M'') → AddCommGroup (V z)] [(z : M'') → Module ℝ (V z)] [(z : M'') → TopologicalSpace (V z)] {f : M → M'} {g : M' → M''} (hf : MDiff f) (hg : MDiff g) (ω : RoughBundleForm I'' M'' V k) : bundleMpullback I I'' (g ∘ f) ω = bundleMpullback I I' f (bundleMpullback I' I'' g ω)

Pullback reverses composition of differentiable maps.

noncomputable def TauCeti.mpullbackWithin {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (I : ModelWithCorners ℝ E H) (I' : ModelWithCorners ℝ E' H') (f : M → M') (s : Set M) (ω : RoughForm I' M' F k) : RoughForm I M F k

Pullback of a fixed-coefficient form using the derivative within s.

@[simp]

theorem TauCeti.mpullbackWithin_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (f : M → M') (s : Set M) (ω : RoughForm I' M' F k) (x : M) (v : Fin k → TangentSpace I x) : (mpullbackWithin I I' f s ω x) v = (ω (f x)) fun (i : Fin k) => (mfderiv[s] f x) (v i)

Evaluation of fixed-coefficient within-set pullback on tangent vectors.

noncomputable def TauCeti.mpullback {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (I : ModelWithCorners ℝ E H) (I' : ModelWithCorners ℝ E' H') (f : M → M') (ω : RoughForm I' M' F k) : RoughForm I M F k

Pullback of a fixed-coefficient rough form along the manifold derivative.

@[simp]

theorem TauCeti.mpullback_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (f : M → M') (ω : RoughForm I' M' F k) (x : M) (v : Fin k → TangentSpace I x) : (mpullback I I' f ω x) v = (ω (f x)) fun (i : Fin k) => (mfderiv% f x) (v i)

Evaluation of fixed-coefficient pullback on tangent vectors.

theorem TauCeti.mpullback_apply_pair {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (f : M → M') (ω : RoughForm I' M' F 2) (x : M) (a b : TangentSpace I x) : (mpullback I I' f ω x) ![a, b] = (ω (f x)) ![(mfderiv% f x) a, (mfderiv% f x) b]

Evaluation of the pullback of a two-form on a pair of tangent vectors.

@[simp]

theorem TauCeti.mpullbackWithin_univ {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (f : M → M') (ω : RoughForm I' M' F k) : mpullbackWithin I I' f Set.univ ω = mpullback I I' f ω

Pullback within the whole manifold is ordinary pullback.

@[simp]

theorem TauCeti.mpullbackWithin_eq_mpullback {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {f : M → M'} {s : Set M} {x : M} (hs : UniqueMDiffAt[s] x) (hf : MDiffAt f x) (ω : RoughForm I' M' F k) : mpullbackWithin I I' f s ω x = mpullback I I' f ω x

Within-set and ordinary pullback agree where their derivatives agree.

theorem TauCeti.RoughForm.apply_tangentSpaceCast {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {ω : RoughForm I' M' F k} {a b : M'} (h : b = a) (u : Fin k → TangentSpace I' b) : ((ω a) fun (i : Fin k) => (tangentSpaceCast I' b a) (u i)) = (ω b) u

A form evaluated at a on tangent vectors at b = a moved by tangentSpaceCast is the form evaluated at b on the original vectors.

theorem Filter.EventuallyEq.mpullbackWithin_eq {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {f g : M → M'} {s : Set M} {x : M} (h : f =ᶠ[nhdsWithin x s] g) (hx : f x = g x) (ω : TauCeti.RoughForm I' M' F k) : TauCeti.mpullbackWithin I I' f s ω x = TauCeti.mpullbackWithin I I' g s ω x

Maps that agree near x within s, and at x, pull a form back within s to the same value at x.

theorem TauCeti.mpullbackWithin_congr {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {f g : M → M'} {s : Set M} {x : M} (h : Set.EqOn f g s) (hx : x ∈ s) (ω : RoughForm I' M' F k) : mpullbackWithin I I' f s ω x = mpullbackWithin I I' g s ω x

Maps that agree on s pull a form back within s to the same value at each point of s.

theorem Filter.EventuallyEq.mpullback_eq {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {f g : M → M'} {x : M} (h : f =ᶠ[nhds x] g) (ω : TauCeti.RoughForm I' M' F k) : TauCeti.mpullback I I' f ω x = TauCeti.mpullback I I' g ω x

Maps that agree near x pull a form back to the same value at x.

theorem TauCeti.mpullback_apply_eq_mpullback_apply_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {f : M → M'} {x : M} (hf : Function.Surjective ⇑(mfderiv% f x)) {ω η : RoughForm I' M' F k} : mpullback I I' f ω x = mpullback I I' f η x ↔ ω (f x) = η (f x)

If the derivative of f at x is surjective, two forms have the same pullback along f at x exactly when they agree at f x.

theorem TauCeti.mpullback_apply_eq_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {f : M → M'} {ω : RoughForm I' M' F k} {x : M} (h : ω (f x) = 0) : mpullback I I' f ω x = 0

A pullback vanishes at every point where the form vanishes at the image point.

theorem TauCeti.mpullback_injective_of_surjective {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {f : M → M'} (hsurj : Function.Surjective f) (hf : ∀ (x : M), Function.Surjective ⇑(mfderiv% f x)) : Function.Injective (mpullback I I' f)

Pullback along a surjective map whose derivatives are all surjective is injective.

@[simp]

theorem TauCeti.mpullbackWithin_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (f : M → M') (s : Set M) : mpullbackWithin I I' f s 0 = 0

Within-set pullback preserves zero.

@[simp]

theorem TauCeti.mpullback_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (f : M → M') : mpullback I I' f 0 = 0

Pullback preserves zero.

@[simp]

theorem TauCeti.mpullbackWithin_add {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousAdd F] (f : M → M') (s : Set M) (ω η : RoughForm I' M' F k) : mpullbackWithin I I' f s (ω + η) = mpullbackWithin I I' f s ω + mpullbackWithin I I' f s η

Within-set pullback preserves addition.

@[simp]

theorem TauCeti.mpullback_add {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousAdd F] (f : M → M') (ω η : RoughForm I' M' F k) : mpullback I I' f (ω + η) = mpullback I I' f ω + mpullback I I' f η

Pullback preserves addition.

@[simp]

theorem TauCeti.mpullback_sub {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] (f : M → M') (ω η : RoughForm I' M' F k) : mpullback I I' f (ω - η) = mpullback I I' f ω - mpullback I I' f η

Pullback preserves subtraction.

@[simp]

theorem TauCeti.mpullbackWithin_smul {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {S : Type u_11} [Monoid S] [DistribMulAction S F] [ContinuousConstSMul S F] [SMulCommClass ℝ S F] (f : M → M') (s : Set M) (c : S) (ω : RoughForm I' M' F k) : mpullbackWithin I I' f s (c • ω) = c • mpullbackWithin I I' f s ω

Within-set pullback respects scalar multiplication of the coefficients, by any scalars acting continuously on the coefficient space and commuting with the real action.

@[simp]

theorem TauCeti.mpullback_smul {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {S : Type u_11} [Monoid S] [DistribMulAction S F] [ContinuousConstSMul S F] [SMulCommClass ℝ S F] (f : M → M') (c : S) (ω : RoughForm I' M' F k) : mpullback I I' f (c • ω) = c • mpullback I I' f ω

Pullback respects scalar multiplication of the coefficients, by any scalars acting continuously on the coefficient space and commuting with the real action.

@[simp]

theorem TauCeti.mpullback_fun_smul {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {S : Type u_11} [Monoid S] [DistribMulAction S F] [ContinuousConstSMul S F] [SMulCommClass ℝ S F] (f : M → M') (c : M' → S) (ω : RoughForm I' M' F k) : (mpullback I I' f fun (y : M') => c y • ω y) = fun (x : M) => c (f x) • mpullback I I' f ω x

Pullback of a form multiplied pointwise by a scalar function multiplies the pullback by the composite function, for any scalars acting continuously on the coefficient space and commuting with the real action.

@[simp]

theorem TauCeti.mpullbackWithin_id {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {s : Set M} {x : M} (hs : UniqueMDiffAt[s] x) (ω : RoughForm I M F k) : mpullbackWithin I I id s ω x = ω x

Within-set pullback by the identity fixes forms wherever the derivative is unique.

@[simp]

theorem TauCeti.mpullback_id {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (ω : RoughForm I M F k) : mpullback I I id ω = ω

Pullback by the identity fixes forms.

theorem TauCeti.mpullbackWithin_comp_at {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {E'' : Type u_7} {H'' : Type u_8} {M'' : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} [NormedAddCommGroup E''] [NormedSpace ℝ E''] [TopologicalSpace H''] [TopologicalSpace M''] [ChartedSpace H'' M''] {I'' : ModelWithCorners ℝ E'' H''} {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {f : M → M'} {g : M' → M''} {s : Set M} {t : Set M'} {x : M} (hf : MDiffAt[s] f x) (hg : MDiffAt[t] g (f x)) (hst : Set.MapsTo f s t) (hs : UniqueMDiffAt[s] x) (ω : RoughForm I'' M'' F k) : mpullbackWithin I I'' (g ∘ f) s ω x = mpullbackWithin I I' f s (mpullbackWithin I' I'' g t ω) x

The within-set chain rule for fixed-coefficient forms.

theorem TauCeti.mpullbackWithin_comp_of_preimage_mem_nhdsWithin {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {E'' : Type u_7} {H'' : Type u_8} {M'' : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} [NormedAddCommGroup E''] [NormedSpace ℝ E''] [TopologicalSpace H''] [TopologicalSpace M''] [ChartedSpace H'' M''] {I'' : ModelWithCorners ℝ E'' H''} {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {f : M → M'} {g : M' → M''} {s : Set M} {t : Set M'} {x : M} (hf : MDiffAt[s] f x) (hg : MDiffAt[t] g (f x)) (hst : f ⁻¹' t ∈ nhdsWithin x s) (hs : UniqueMDiffAt[s] x) (ω : RoughForm I'' M'' F k) : mpullbackWithin I I'' (g ∘ f) s ω x = mpullbackWithin I I' f s (mpullbackWithin I' I'' g t ω) x

The within-set chain rule for fixed-coefficient forms with a local intermediate-set condition.

theorem TauCeti.mpullback_comp_at {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {E'' : Type u_7} {H'' : Type u_8} {M'' : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} [NormedAddCommGroup E''] [NormedSpace ℝ E''] [TopologicalSpace H''] [TopologicalSpace M''] [ChartedSpace H'' M''] {I'' : ModelWithCorners ℝ E'' H''} {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {f : M → M'} {g : M' → M''} {x : M} (hf : MDiffAt f x) (hg : MDiffAt g (f x)) (ω : RoughForm I'' M'' F k) : mpullback I I'' (g ∘ f) ω x = mpullback I I' f (mpullback I' I'' g ω) x

The chain rule for fixed-coefficient forms at a point.

theorem TauCeti.mpullback_comp_on {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {E'' : Type u_7} {H'' : Type u_8} {M'' : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} [NormedAddCommGroup E''] [NormedSpace ℝ E''] [TopologicalSpace H''] [TopologicalSpace M''] [ChartedSpace H'' M''] {I'' : ModelWithCorners ℝ E'' H''} {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {f : M → M'} {g : M' → M''} {s : Set M} (hf : ∀ x ∈ s, MDiffAt f x) (hg : ∀ x ∈ s, MDiffAt g (f x)) (ω : RoughForm I'' M'' F k) (x : M) : x ∈ s → mpullback I I'' (g ∘ f) ω x = mpullback I I' f (mpullback I' I'' g ω) x

The fixed-coefficient chain rule on a set.

theorem TauCeti.mpullback_comp {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {E'' : Type u_7} {H'' : Type u_8} {M'' : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} [NormedAddCommGroup E''] [NormedSpace ℝ E''] [TopologicalSpace H''] [TopologicalSpace M''] [ChartedSpace H'' M''] {I'' : ModelWithCorners ℝ E'' H''} {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {f : M → M'} {g : M' → M''} (hf : MDiff f) (hg : MDiff g) (ω : RoughForm I'' M'' F k) : mpullback I I'' (g ∘ f) ω = mpullback I I' f (mpullback I' I'' g ω)

Pullback reverses composition of differentiable maps.

theorem TauCeti.mpullback_comp_of_mdifferentiableAt_comp_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {E'' : Type u_7} {H'' : Type u_8} {M'' : Type u_9} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} [NormedAddCommGroup E''] [NormedSpace ℝ E''] [TopologicalSpace H''] [TopologicalSpace M''] [ChartedSpace H'' M''] {I'' : ModelWithCorners ℝ E'' H''} {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {f : M → M'} {g : M' → M''} (hg : MDiff g) (hfg : ∀ (x : M), MDiffAt (g ∘ f) x ↔ MDiffAt f x) (ω : RoughForm I'' M'' F k) : mpullback I I'' (g ∘ f) ω = mpullback I I' f (mpullback I' I'' g ω)

Pullback reverses composition with a differentiable map g that does not change where the inner map f is differentiable. At points where f is not differentiable, the pullbacks of a form of positive degree both vanish, as the derivative is taken to be zero there; for a form of degree zero the pullbacks agree by composition of functions.

@[simp]

theorem TauCeti.mpullback_ofFunction {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (f : M → M') (a : M' → F) : mpullback I I' f (RoughForm.ofFunction I' a) = RoughForm.ofFunction I (a ∘ f)

Pullback of a degree-zero form is composition of its underlying function.

@[simp]

theorem TauCeti.mpullbackWithin_ofFunction {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (f : M → M') (s : Set M) (a : M' → F) : mpullbackWithin I I' f s (RoughForm.ofFunction I' a) = RoughForm.ofFunction I (a ∘ f)

Within-set pullback of a degree-zero form is function composition.

theorem TauCeti.mpullbackWithin_eq_flat {E : Type u_1} {E' : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (f : E → E') (s : Set E) (ω : RoughForm (modelWithCornersSelf ℝ E') E' F k) : mpullbackWithin (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E') f s ω = fun (x : E) => (ω (f x)).compContinuousLinearMap (fderivWithin ℝ f s x)

On model spaces, within-set pullback is the flat pullback by the Fréchet derivative.

theorem TauCeti.mpullback_eq_flat {E : Type u_1} {E' : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (f : E → E') (ω : RoughForm (modelWithCornersSelf ℝ E') E' F k) : mpullback (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ E') f ω = fun (x : E) => (ω (f x)).compContinuousLinearMap (fderiv ℝ f x)

On model spaces, pullback is the flat pullback by the Fréchet derivative.

theorem TauCeti.mpullback_comp_apply_of_hasFDerivAt {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {E'' : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup E''] [NormedSpace ℝ E''] {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {u : E' → M} {L : E'' → E'} {A : E'' →L[ℝ] E'} {y : E''} (hL : HasFDerivAt L A y) (hu : MDiffAt u (L y)) (ω : RoughForm I M F k) : mpullback (modelWithCornersSelf ℝ E'') I (u ∘ L) ω y = (mpullback (modelWithCornersSelf ℝ E') I u ω (L y)).compContinuousLinearMap A

The chain rule for precomposition by a map of normed spaces: the pullback along u ∘ L, for a map L with derivative A at y, is the pullback along u at L y precomposed with A.

theorem TauCeti.mpullback_comp_clm_apply_eq_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {E'' : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup E''] [NormedSpace ℝ E''] {k : ℕ} {F : Type u_10} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (ω : RoughForm I M F k) (γ : E' → M) (P : E'' →L[ℝ] E') {z : E''} {v : Fin k → E''} {i : Fin k} (hv : P (v i) = 0) : (mpullback (modelWithCornersSelf ℝ E'') I (γ ∘ ⇑P) ω z) v = 0

The pullback of a form along γ ∘ P, for a continuous linear map P of normed spaces, vanishes on every family of vectors one of which lies in the kernel of P.

theorem TauCeti.mpullback_apply_eq_compContinuousLinearMapCLM {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {I' : ModelWithCorners ℝ E' H'} {k : ℕ} {F : Type u_10} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : M → M') (η : RoughForm I' M' F k) (x : M) : mpullback I I' f η x = (ContinuousAlternatingMap.compContinuousLinearMapCLM (mfderiv% f x)) (η (f x))

The pullback of a form at x is the form at f x composed with the differential of f, read as an operator on alternating maps of the model spaces. The two sides agree up to unfolding the tangent spaces to the model spaces; this is the form in which pullbacks are differentiated.