Smooth pullback of differential forms

A C^(n+1) map pulls a C^n fixed-coefficient differential form back to a C^n form. The relative theorem uses derivatives within the source set, so it applies at boundary and corner points. No invertibility, finite dimensionality, or completeness is required.

For smooth maps, SmoothForm.mpullback bundles this operation as a linear map on smooth forms. Its underlying rough form is the existing TauCeti.mpullback. Pullback along a smooth map with a smooth right inverse, such as a vector bundle projection, is injective. The diffeomorphisms of M preserving a smooth form form a subgroup of the diffeomorphism group, its stabilizer (TauCeti.SmoothForm.diffeomorphStabilizer).

Conversely, regularity descends along a local section: if s is a C^n local section of f through x, a form is C^m near f x exactly when its pullback along f is C^m near x, for m + 1 ≤ n (TauCeti.contMDiffAt_mpullback_form_iff_of_section).

In tangent coordinates, pullback precomposes the form's coordinates with those of Mathlib's mfderivWithin, via ContinuousAlternatingMap.compContinuousLinearMap. This expresses pullback regularity in terms of maps between fixed model fibres. For bundle-valued forms, the file provides the coordinate identity inCoordinates_bundleMpullbackWithin.

References

• John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Chapter 14.

theorem TauCeti.inCoordinates_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} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] {k : ℕ} {V' : M' → Type u_8} [(y : M') → AddCommGroup (V' y)] [(y : M') → Module ℝ (V' y)] [(y : M') → TopologicalSpace (V' y)] [TopologicalSpace (Bundle.TotalSpace F V')] [FiberBundle F V'] [VectorBundle ℝ F V'] (ω : RoughBundleForm I' M' V' k) (f : M → M') (s : Set M) (x y : M) (hyT : f y ∈ (trivializationAt E' (TangentSpace I') (f x)).baseSet) : ContinuousAlternatingMap.inCoordinates E F x y (f x) (f y) (bundleMpullbackWithin I I' f s ω y) = (ContinuousAlternatingMap.inCoordinates E' F (f x) (f y) (f x) (f y) (ω (f y))).compContinuousLinearMap (inTangentCoordinates I I' id f (mfderiv[s] f) x y)

Read with the coefficient trivialization of V' at f x and the tangent trivializations at x and f x, a bundle-valued pullback is the form's coordinates precomposed with the coordinates of mfderivWithin. The target tangent trivialization must be valid at f y.

theorem TauCeti.RoughForm.inCoordinates_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} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] {k : ℕ} (ω : RoughForm I' M' F k) (f : M → M') (s : Set M) (x y : M) (hy : f y ∈ (trivializationAt E' (TangentSpace I') (f x)).baseSet) : ContinuousAlternatingMap.inCoordinates E F x y x y (mpullbackWithin I I' f s ω y) = (ContinuousAlternatingMap.inCoordinates E' F (f x) (f y) (f x) (f y) (ω (f y))).compContinuousLinearMap (inTangentCoordinates I I' id f (mfderiv[s] f) x y)

In fibre coordinates, pullback precomposes the form's coordinates with the derivative's coordinates. The target tangent trivialization must be valid at f y.

theorem ContMDiffWithinAt.mpullbackWithin_form {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] {k : ℕ} {m n : WithTop ℕ∞} {f : M → M'} {s : Set M} {t : Set M'} {x : M} {ω : TauCeti.RoughForm I' M' F k} (hω : ContMDiffWithinAt I' (I'.prod (modelWithCornersSelf ℝ (E' [⋀^Fin k]→L[ℝ] F))) m (fun (y : M') => ⟨y, ω y⟩) t (f x)) (hf : ContMDiffWithinAt I I' n f s x) (hmn : m + 1 ≤ n) (hst : Set.MapsTo f s t) (hx : x ∈ s) (hs : UniqueMDiff[s]) : ContMDiffWithinAt I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin k]→L[ℝ] F))) m (fun (y : M) => ⟨y, TauCeti.mpullbackWithin I I' f s ω y⟩) s x

A form of regularity C^m pulls back to a C^m section along a C^n map when m + 1 ≤ n. The derivative defining pullback is taken within the unique-differentiability set s.

theorem ContMDiffOn.mpullbackWithin_form {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] {k : ℕ} {m n : WithTop ℕ∞} {f : M → M'} {s : Set M} {t : Set M'} {ω : TauCeti.RoughForm I' M' F k} (hω : ContMDiffOn I' (I'.prod (modelWithCornersSelf ℝ (E' [⋀^Fin k]→L[ℝ] F))) m (fun (y : M') => ⟨y, ω y⟩) t) (hf : ContMDiffOn I I' n f s) (hmn : m + 1 ≤ n) (hst : Set.MapsTo f s t) (hs : UniqueMDiff[s]) : ContMDiffOn I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin k]→L[ℝ] F))) m (fun (y : M) => ⟨y, TauCeti.mpullbackWithin I I' f s ω y⟩) s

Pullback within a unique-differentiability set preserves C^m sections when the map is C^n and m + 1 ≤ n.

theorem ContMDiffAt.mpullback_form {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] {k : ℕ} {m n : WithTop ℕ∞} {f : M → M'} {x : M} {ω : TauCeti.RoughForm I' M' F k} (hω : ContMDiffAt I' (I'.prod (modelWithCornersSelf ℝ (E' [⋀^Fin k]→L[ℝ] F))) m (fun (y : M') => ⟨y, ω y⟩) (f x)) (hf : ContMDiffAt I I' n f x) (hmn : m + 1 ≤ n) : ContMDiffAt I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin k]→L[ℝ] F))) m (fun (y : M) => ⟨y, TauCeti.mpullback I I' f ω y⟩) x

Pointwise regularity of the pullback of a form.

theorem TauCeti.contMDiffAt_mpullback_form_iff_of_section {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] {k : ℕ} {m n : WithTop ℕ∞} {f : M → M'} {x : M} {ω : RoughForm I' M' F k} {s : M' → M} {U : Set M'} (hU : IsOpen U) (hxU : f x ∈ U) (hsx : s (f x) = x) (hs : ContMDiffOn I' I n s U) (hfs : ∀ y ∈ U, f (s y) = y) (hf : ContMDiffAt I I' n f x) (hmn : m + 1 ≤ n) : ContMDiffAt I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin k]→L[ℝ] F))) m (fun (y : M) => ⟨y, mpullback I I' f ω y⟩) x ↔ ContMDiffAt I' (I'.prod (modelWithCornersSelf ℝ (E' [⋀^Fin k]→L[ℝ] F))) m (fun (y : M') => ⟨y, ω y⟩) (f x)

Let f be C^n at x, m + 1 ≤ n, and let s be a C^n local section of f through x over an open neighbourhood U of f x. Then a form is a C^m section near f x exactly when its pullback along f is a C^m section near x: near f x, the form is the pullback of its pullback along s. Local inverses of local diffeomorphisms and local sections of submersions are such sections.

theorem TauCeti.IsSmoothBundleForm.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} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] {k : ℕ} {m n : WithTop ℕ∞} {f : M → M'} {ω : RoughForm I' M' F k} (hω : IsSmoothBundleForm I' F (Bundle.Trivial M' F) m ω) (hf : ContMDiff I I' n f) (hmn : m + 1 ≤ n) : IsSmoothBundleForm I F (Bundle.Trivial M F) m (TauCeti.mpullback I I' f ω)

Pullback of a fixed-coefficient C^m form along a C^n map is C^m for m + 1 ≤ n. In particular, smooth maps pull smooth forms back to smooth forms.

theorem TauCeti.IsSmoothForm.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} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] {k : ℕ} {m : WithTop ℕ∞} {f : M → M'} {ω : RoughForm I' M' F k} (hω : IsSmoothForm I' m ω) (hf : ContMDiff I I' (m + 1) f) : IsSmoothForm I m (TauCeti.mpullback I I' f ω)

Pullback of a fixed-coefficient C^m form along a C^(m+1) map is C^m. This is the form-level interface to the general bundle-section pullback theorem.

theorem TauCeti.IsSmoothForm.continuous_mpullback_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {F : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {k : ℕ} {φ : RoughForm I M F k} (hφ : IsSmoothForm I 0 φ) {u : E' → M} (hu : ContMDiff (modelWithCornersSelf ℝ E') I 1 u) (v : Fin k → E') : Continuous fun (z : E') => (TauCeti.mpullback (modelWithCornersSelf ℝ E') I u φ z) v

The pullback of a continuous form along a C¹ map u from a normed space, evaluated on fixed vectors, is continuous. For u a map of the plane this is the integrand of a rectangle integral.

theorem TauCeti.IsSmoothForm.continuous_apply_mfderiv {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {F : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {φ : RoughForm I M F 2} (hφ : IsSmoothForm I 0 φ) {u : E' → M} (hu : ContMDiff (modelWithCornersSelf ℝ E') I 1 u) (a b : E') : Continuous fun (z : E') => (φ (u z)) ![(mfderiv% u z) a, (mfderiv% u z) b]

For a continuous two-form φ and a C¹ map u from a normed space, the form evaluated on the derivatives of u along two fixed vectors, z ↦ φ (u z) (du_z a, du_z b), is continuous.

theorem TauCeti.IsSmoothForm.continuousOn_apply_mfderiv {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {F : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {φ : RoughForm I M F 2} (hφ : IsSmoothForm I 0 φ) {u : E' → M} {U : Set E'} (hU : IsOpen U) (hu : ContMDiffOn (modelWithCornersSelf ℝ E') I 1 u U) (a b : E') : ContinuousOn (fun (z : E') => (φ (u z)) ![(mfderiv% u z) a, (mfderiv% u z) b]) U

For a continuous two-form φ and a map u from a normed space which is C¹ on an open set U, the form evaluated on the derivatives of u along two fixed vectors, z ↦ φ (u z) (du_z a, du_z b), is continuous on U.

@[simp]

theorem TauCeti.mpullback_symm_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} {F : Type u_7} [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 F] [NormedSpace ℝ F] {k : ℕ} {n : WithTop ℕ∞} (hn : n ≠ 0) (φ : Diffeomorph I I' M M' n) (ω : RoughForm I' M' F k) : mpullback I' I (⇑φ.symm) (mpullback I I' (⇑φ) ω) = ω

Pulling a form back along a diffeomorphism and then along its inverse returns the form.

theorem TauCeti.mpullback_zeroSection_comp_proj {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {F' : Type u_8} [NormedAddCommGroup F'] [NormedSpace ℝ F'] {V : M → Type u_9} [TopologicalSpace (Bundle.TotalSpace F' V)] [(x : M) → AddCommMonoid (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F' V] [VectorBundle ℝ F' V] (ω : RoughForm (I.prod (modelWithCornersSelf ℝ F')) (Bundle.TotalSpace F' V) F k) : mpullback (I.prod (modelWithCornersSelf ℝ F')) (I.prod (modelWithCornersSelf ℝ F')) (Bundle.zeroSection F' V ∘ Bundle.TotalSpace.proj) ω = mpullback (I.prod (modelWithCornersSelf ℝ F')) I Bundle.TotalSpace.proj (mpullback I (I.prod (modelWithCornersSelf ℝ F')) (Bundle.zeroSection F' V) ω)

Pulling back along the retraction 0 ∘ π of a vector bundle onto its zero section factors through the restriction to the zero section.

noncomputable def TauCeti.SmoothForm.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} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] {k : ℕ} (f : M → M') (hf : ContMDiff I I' (↑⊤) f) : SmoothForm I' M' F k →ₗ[ℝ] SmoothForm I M F k

Pullback along a smooth map, as a linear map on smooth fixed-coefficient forms.

@[simp]

theorem TauCeti.SmoothForm.coe_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} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] {k : ℕ} (f : M → M') (hf : ContMDiff I I' (↑⊤) f) (φ : SmoothForm I' M' F k) : ↑((mpullback f hf) φ) = TauCeti.mpullback I I' f ↑φ

The underlying rough form of smooth pullback is rough pullback.

theorem TauCeti.SmoothForm.mpullback_cast {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] {k l : ℕ} (h : k = l) (f : M → M') (hf : ContMDiff I I' (↑⊤) f) (φ : SmoothForm I' M' F k) : (mpullback f hf) ((LinearEquiv.cast h) φ) = (LinearEquiv.cast h) ((mpullback f hf) φ)

Pullback of smooth forms commutes with transport of the degree.

theorem TauCeti.SmoothForm.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} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] {k : ℕ} (f : M → M') (hf : ContMDiff I I' (↑⊤) f) (φ : SmoothForm I' M' F k) (x : M) (v : Fin k → TangentSpace I x) : (↑((mpullback f hf) φ) x) v = (↑φ (f x)) fun (i : Fin k) => (mfderiv% f x) (v i)

Evaluation of smooth pullback on tangent vectors. Simplification also obtains this from coe_mpullback and the rough pullback's application law.

theorem TauCeti.SmoothForm.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} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] {k : ℕ} {f : M → M'} (hf : ContMDiff I I' (↑⊤) f) (hsurj : Function.Surjective f) (hdf : ∀ (x : M), Function.Surjective ⇑(mfderiv% f x)) : Function.Injective ⇑(mpullback f hf)

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

theorem TauCeti.SmoothForm.mpullback_apply_eq_smul_of_mpullback_eq_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} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] {k : ℕ} {f : M → M'} {hf : ContMDiff I I' (↑⊤) f} {φ' : SmoothForm I' M' F k} {φ : SmoothForm I M F k} {c : ℝ} (h : (mpullback f hf) φ' = c • φ) (x : M) : TauCeti.mpullback I I' f (↑φ') x = c • ↑φ x

A pullback equation mpullback f hf φ' = c • φ of smooth forms, read at the point x as an equation of the underlying rough forms.

theorem TauCeti.SmoothForm.mpullback_neg_apply_eq_neg_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} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] {k : ℕ} {f : M → M'} {hf : ContMDiff I I' (↑⊤) f} {φ' : SmoothForm I' M' F k} {φ : SmoothForm I M F k} {x : M} {c : ℝ} (h : ↑((mpullback f hf) φ') x = c • ↑φ x) : ↑((mpullback f hf) (-φ')) x = -c • ↑φ x

If the pullback of φ' is c times φ at x, then the pullback of -φ' is -c times φ at x.

theorem TauCeti.SmoothForm.eval₂_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} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] (f : M → M') (hf : ContMDiff I I' (↑⊤) f) (φ : SmoothForm I' M' F 2) (x : M) (v w : TangentSpace I x) : SmoothBundleForm.eval₂ ((mpullback f hf) φ) x v w = SmoothBundleForm.eval₂ φ (f x) ((mfderiv% f x) v) ((mfderiv% f x) w)

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

theorem TauCeti.SmoothForm.mpullback_fst_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} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] {k : ℕ} (φ : SmoothForm I M F k) (p : M × M') (v : Fin k → TangentSpace (I.prod I') p) : (↑((mpullback Prod.fst ⋯) φ) p) v = (↑φ p.1) fun (i : Fin k) => ((Manifold.tangentSpaceProdEquiv p) (v i)).1

Evaluation of the pullback along the first projection of a product reads the first components of the tangent vectors.

theorem TauCeti.SmoothForm.mpullback_snd_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} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] {k : ℕ} (φ : SmoothForm I' M' F k) (p : M × M') (v : Fin k → TangentSpace (I.prod I') p) : (↑((mpullback Prod.snd ⋯) φ) p) v = (↑φ p.2) fun (i : Fin k) => ((Manifold.tangentSpaceProdEquiv p) (v i)).2

Evaluation of the pullback along the second projection of a product reads the second components of the tangent vectors.

theorem TauCeti.SmoothForm.eval₂_mpullback_fst {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] (φ : SmoothForm I M F 2) (p : M × M') (v w : TangentSpace (I.prod I') p) : SmoothBundleForm.eval₂ ((mpullback Prod.fst ⋯) φ) p v w = SmoothBundleForm.eval₂ φ p.1 ((Manifold.tangentSpaceProdEquiv p) v).1 ((Manifold.tangentSpaceProdEquiv p) w).1

The pullback of a two-form along the first projection of a product, evaluated on two tangent vectors, reads their first components.

theorem TauCeti.SmoothForm.eval₂_mpullback_snd {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] (φ : SmoothForm I' M' F 2) (p : M × M') (v w : TangentSpace (I.prod I') p) : SmoothBundleForm.eval₂ ((mpullback Prod.snd ⋯) φ) p v w = SmoothBundleForm.eval₂ φ p.2 ((Manifold.tangentSpaceProdEquiv p) v).2 ((Manifold.tangentSpaceProdEquiv p) w).2

The pullback of a two-form along the second projection of a product, evaluated on two tangent vectors, reads their second components.

theorem TauCeti.SmoothForm.mpullback_graph_mpullback_fst_sub_mpullback_snd {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] {k : ℕ} {f : M → M'} {x : M} (α : SmoothForm I M F k) (β : SmoothForm I' M' F k) (hf : MDiffAt f x) : TauCeti.mpullback I (I.prod I') (fun (y : M) => (y, f y)) (↑((mpullback Prod.fst ⋯) α - (mpullback Prod.snd ⋯) β)) x = ↑α x - TauCeti.mpullback I I' f (↑β) x

Pullback along a graph. Along the graph y ↦ (y, f y) of a map f differentiable at x, the form pr₁^*α - pr₂^*β on M × M' pulls back at x to α - f^*β.

@[simp]

theorem TauCeti.SmoothForm.mpullback_id {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {k : ℕ} : mpullback id ⋯ = LinearMap.id

Pullback by the identity is the identity linear map.

theorem TauCeti.SmoothForm.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} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] {k : ℕ} {E'' : Type u_8} {H'' : Type u_9} {M'' : Type u_10} [NormedAddCommGroup E''] [NormedSpace ℝ E''] [TopologicalSpace H''] [TopologicalSpace M''] [ChartedSpace H'' M''] {I'' : ModelWithCorners ℝ E'' H''} [IsManifold I'' 1 M''] (f : M → M') (g : M' → M'') (hf : ContMDiff I I' (↑⊤) f) (hg : ContMDiff I' I'' (↑⊤) g) : mpullback (g ∘ f) ⋯ = mpullback f hf ∘ₗ mpullback g hg

Pullback reverses composition of smooth maps.

theorem TauCeti.SmoothForm.mpullback_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} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] {k : ℕ} {E'' : Type u_8} {H'' : Type u_9} {M'' : Type u_10} [NormedAddCommGroup E''] [NormedSpace ℝ E''] [TopologicalSpace H''] [TopologicalSpace M''] [ChartedSpace H'' M''] {I'' : ModelWithCorners ℝ E'' H''} [IsManifold I'' 1 M''] (f : M → M') (g : M' → M'') (hf : ContMDiff I I' (↑⊤) f) (hg : ContMDiff I' I'' (↑⊤) g) (β : SmoothForm I'' M'' F k) : (mpullback f hf) ((mpullback g hg) β) = (mpullback (g ∘ f) ⋯) β

Pulling a form back along g and then along f is pulling it back along g ∘ f.

theorem TauCeti.SmoothForm.mpullback_injective_of_rightInverse {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] {k : ℕ} {f : M → M'} {g : M' → M} (hf : ContMDiff I I' (↑⊤) f) (hg : ContMDiff I' I (↑⊤) g) (hfg : Function.RightInverse g f) : Function.Injective ⇑(mpullback f hf)

Pullback along a smooth map with a smooth right inverse is injective.

theorem TauCeti.SmoothForm.mpullback_proj_injective {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {k : ℕ} {F' : Type u_11} [NormedAddCommGroup F'] [NormedSpace ℝ F'] {V : M → Type u_12} [TopologicalSpace (Bundle.TotalSpace F' V)] [(x : M) → AddCommMonoid (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [FiberBundle F' V] [VectorBundle ℝ F' V] [IsManifold (I.prod (modelWithCornersSelf ℝ F')) 1 (Bundle.TotalSpace F' V)] : Function.Injective ⇑(mpullback Bundle.TotalSpace.proj ⋯)

Pullback along the projection of a smooth vector bundle is injective: the zero section is a smooth right inverse of the projection.

theorem TauCeti.SmoothForm.mpullback_symm_eq_of_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} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] {k : ℕ} {φ : Diffeomorph I I' M M' ↑⊤} {α : SmoothForm I M F k} {β : SmoothForm I' M' F k} (h : (mpullback ⇑φ ⋯) β = α) : (mpullback ⇑φ.symm ⋯) α = β

If a diffeomorphism φ pulls β back to α, then its inverse pulls α back to β.

@[simp]

theorem TauCeti.SmoothForm.mpullback_mpullback_symm {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] {k : ℕ} (φ : Diffeomorph I I' M M' ↑⊤) (β : SmoothForm I M F k) : (mpullback ⇑φ ⋯) ((mpullback ⇑φ.symm ⋯) β) = β

Pulling a form back along the inverse of a diffeomorphism φ and then along φ gives the form back.

@[simp]

theorem TauCeti.SmoothForm.mpullback_symm_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} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] {k : ℕ} (φ : Diffeomorph I I' M M' ↑⊤) (β : SmoothForm I' M' F k) : (mpullback ⇑φ.symm ⋯) ((mpullback ⇑φ ⋯) β) = β

Pulling a form back along a diffeomorphism φ and then along its inverse gives the form back.

theorem TauCeti.SmoothForm.mpullback_trans {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] {k : ℕ} {E'' : Type u_8} {H'' : Type u_9} {M'' : Type u_10} [NormedAddCommGroup E''] [NormedSpace ℝ E''] [TopologicalSpace H''] [TopologicalSpace M''] [ChartedSpace H'' M''] {I'' : ModelWithCorners ℝ E'' H''} [IsManifold I'' 1 M''] (φ : Diffeomorph I I' M M' ↑⊤) (ψ : Diffeomorph I' I'' M' M'' ↑⊤) (γ : SmoothForm I'' M'' F k) : (mpullback ⇑(φ.trans ψ) ⋯) γ = (mpullback ⇑φ ⋯) ((mpullback ⇑ψ ⋯) γ)

Pullback along a composite of diffeomorphisms is the composite of the pullbacks.

theorem TauCeti.SmoothForm.mpullback_apply_eq_smul_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} {F : Type u_7} [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 F] [NormedSpace ℝ F] [IsManifold I 1 M] [IsManifold I' 1 M'] {k : ℕ} (φ : Diffeomorph I I' M M' ↑⊤) (α β : SmoothForm I' M' F k) (c : ℝ) (x : M) : ↑((mpullback ⇑φ ⋯) α) x = c • ↑((mpullback ⇑φ ⋯) β) x ↔ ↑α (φ x) = c • ↑β (φ x)

Pullback along a diffeomorphism φ transports pointwise proportionality: at x, the pullback of α is c times the pullback of β exactly when α is c times β at φ x.

def TauCeti.SmoothForm.diffeomorphStabilizer {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {k : ℕ} (σ : SmoothForm I M F k) : Subgroup (Diffeomorph I I M M ↑⊤)

The stabilizer of a smooth form σ in the diffeomorphism group of M: the smooth diffeomorphisms φ with φ^* σ = σ. For a symplectic form ω this is the group of symplectomorphisms Symp(M, ω), and for a volume form the group of volume-preserving diffeomorphisms.

@[simp]

theorem TauCeti.SmoothForm.mem_diffeomorphStabilizer {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {k : ℕ} {σ : SmoothForm I M F k} {φ : Diffeomorph I I M M ↑⊤} : φ ∈ σ.diffeomorphStabilizer ↔ (mpullback ⇑φ ⋯) σ = σ

A diffeomorphism lies in the stabilizer of σ exactly when it pulls σ back to itself.

theorem TauCeti.SmoothForm.mem_diffeomorphStabilizer_iff_forall {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {k : ℕ} {σ : SmoothForm I M F k} {φ : Diffeomorph I I M M ↑⊤} : φ ∈ σ.diffeomorphStabilizer ↔ ∀ (x : M), TauCeti.mpullback I I (⇑φ) (↑σ) x = ↑σ x

A diffeomorphism preserves a smooth form exactly when it preserves its value at every point: (φ^* σ)_x = σ_x for all x.

theorem TauCeti.SmoothForm.mpullback_zpow_eq_self {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F] [NormedSpace ℝ F] [IsManifold I 1 M] {k : ℕ} {φ : Diffeomorph I I M M ↑⊤} {σ : SmoothForm I M F k} (hσ : (mpullback ⇑φ ⋯) σ = σ) (j : ℤ) : (mpullback ⇑(φ ^ j) ⋯) σ = σ

A smooth form preserved by a diffeomorphism φ is preserved by every integer power of φ.

theorem TauCeti.SmoothForm.mpullback_wedgeWith {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'} [IsManifold I 1 M] [IsManifold I' 1 M'] {F₁ : Type u_11} {F₂ : Type u_12} {F₃ : Type u_13} [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] {k l : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (f : M → M') (hf : ContMDiff I I' (↑⊤) f) (φ : SmoothForm I' M' F₁ k) (ψ : SmoothForm I' M' F₂ l) : (mpullback f hf) (((wedgeWith μ) φ) ψ) = ((wedgeWith μ) ((mpullback f hf) φ)) ((mpullback f hf) ψ)

Smooth pullback is a homomorphism for every fixed continuous coefficient pairing.

theorem TauCeti.SmoothForm.mpullback_wedge {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'} [IsManifold I 1 M] [IsManifold I' 1 M'] {k l : ℕ} (f : M → M') (hf : ContMDiff I I' (↑⊤) f) (φ : SmoothForm I' M' ℝ k) (ψ : SmoothForm I' M' ℝ l) : (mpullback f hf) ((wedge φ) ψ) = (wedge ((mpullback f hf) φ)) ((mpullback f hf) ψ)

Smooth real-valued pullback is a homomorphism for the usual wedge.