The sum of two forms on a product of manifolds: π₁^* α + π₂^* β #
Category: 1-Mathlib (CSD-free; upstream target Mathlib.Geometry.Manifold).
Given a form α on M and a form β on N of the same degree, the product M × N carries
π₁^* α + π₂^* β. This module builds it on the product charted over E × F
(ProductSelfModel.lean) and proves the three facts the symplectic predicate needs:
ContinuousAlternatingMap.prodSum α β— the flat version onE × F,α ∘ fst + β ∘ snd, withprodSum_compContinuousLinearMap_prodMap(it pulls back along a block map factorwise);DifferentialForm.prodFamily α β— the family(x, y) ↦ prodSum (α x) (β y), with ★localRep_prodFamily(its local representative in a product chart is theprodSumof the factors' local representatives, byfderiv_chart_transition_prod), andcontMDiff_prodFamily(smooth when the factors are);- ★
DifferentialForm.prodForm α β— the bundledC^∞form onM × N; - ★★
mextDerivFamily_prodFamily—d (π₁^* α + π₂^* β) = π₁^* dα + π₂^* dβ, from the flat naturalityextDeriv_pullbackalong the two projections; - ★★
IsSymplectic.prodForm— the product of two symplectic manifolds is symplectic; contMDiff_zeroFamily,mextDerivFamily_zeroFamily— the zero family on any manifold over a self model is a smooth section with zero exterior derivative (used with the product to read constant interior products on a product).
Honest scope #
⚠️ Same degree on both factors, valued in the same G. That is what the sum needs. Wedge
products of forms of different degrees across the factors are not built (the corpus's
WedgeForm.lean wedges forms on one manifold).
⚠️ Nothing about the top power or volumes. That (π₁^* α + π₂^* β)^{m+n} is a multiple of
π₁^* α^m ∧ π₂^* β^n (the binomial identity for commuting even forms) is not stated; the
Liouville theorem of HamiltonianFlowVolume.lean applies to the product form's own top-power
measure, which is not here identified with a product measure. (FormInvariance.lean gives the
product form the invariances a consumer needs to identify that measure by uniqueness instead; for
the sum of the Fubini–Study form and the torus area form the top power is computed on the
product basis, by a weighted pair-tuple count rather than the binomial identity,
Instances/ProjectiveSpaceTorusVolume.lean.)
References: Geometry/Manifold/ProductSelfModel.lean (the product charts and their transition
derivatives); Geometry/Manifold/ExteriorDerivative.lean (localRep, trivializationAt_snd,
contDiffAt_localRep); Mathlib/Analysis/Calculus/DifferentialForm/Basic.lean
(extDeriv_pullback, extDeriv_add); Geometry/Manifold/TranslationAtlasForm.lean (the torus
factor); specs/BACKLOG.md (R-016′).
The flat sum #
def
ContinuousAlternatingMap.prodSum
{E : Type u_1}
{F : Type u_2}
{G : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{ι : Type u_4}
(α : E [⋀^ι]→L[ℝ] G)
(β : F [⋀^ι]→L[ℝ] G)
:
π₁^* α + π₂^* β on E × F: the alternating map v ↦ α (v.1) + β (v.2).
Equations
- α.prodSum β = α.compContinuousLinearMap (ContinuousLinearMap.fst ℝ E F) + β.compContinuousLinearMap (ContinuousLinearMap.snd ℝ E F)
Instances For
theorem
ContinuousAlternatingMap.prodSum_apply
{E : Type u_1}
{F : Type u_2}
{G : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{ι : Type u_4}
(α : E [⋀^ι]→L[ℝ] G)
(β : F [⋀^ι]→L[ℝ] G)
(v : ι → E × F)
:
@[simp]
theorem
ContinuousAlternatingMap.prodSum_zero_zero
{E : Type u_1}
{F : Type u_2}
{G : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{ι : Type u_4}
:
theorem
ContinuousAlternatingMap.prodSum_pair
{E : Type u_1}
{F : Type u_2}
{G : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
(a : E [⋀^Fin 2]→L[ℝ] G)
(b : F [⋀^Fin 2]→L[ℝ] G)
(v w : E × F)
:
The prodSum of two 2-forms evaluated on a pair of pairs.
theorem
ContinuousAlternatingMap.prodSum_compContinuousLinearMap_prodMap
{E : Type u_1}
{F : Type u_2}
{G : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{ι : Type u_4}
{E' : Type u_5}
{F' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
[NormedAddCommGroup F']
[NormedSpace ℝ F']
(α : E [⋀^ι]→L[ℝ] G)
(β : F [⋀^ι]→L[ℝ] G)
(L : E' →L[ℝ] E)
(K : F' →L[ℝ] F)
:
(α.prodSum β).compContinuousLinearMap (L.prodMap K) = (α.compContinuousLinearMap L).prodSum (β.compContinuousLinearMap K)
★ The sum pulls back factorwise along a block map.
The family on a product of manifolds #
def
DifferentialForm.prodFamily
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{M : Type u_3}
{N : Type u_4}
[TopologicalSpace M]
[ChartedSpace E M]
[TopologicalSpace N]
[ChartedSpace F N]
{G : Type u_5}
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{ι : Type u_6}
(α : (x : M) → TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ι]→L[ℝ] Bundle.Trivial M G x)
(β : (y : N) → TangentSpace (modelWithCornersSelf ℝ F) y [⋀^ι]→L[ℝ] Bundle.Trivial N G y)
(p : M × N)
:
The family (x, y) ↦ π₁^* (α x) + π₂^* (β y) on the tangent spaces of M × N.
Equations
- DifferentialForm.prodFamily α β p = (DifferentialForm.toFlat (α p.1)).prodSum (DifferentialForm.toFlat (β p.2))
Instances For
theorem
DifferentialForm.prodFamily_apply
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{M : Type u_3}
{N : Type u_4}
[TopologicalSpace M]
[ChartedSpace E M]
[TopologicalSpace N]
[ChartedSpace F N]
{G : Type u_5}
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{ι : Type u_6}
(α : (x : M) → TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ι]→L[ℝ] Bundle.Trivial M G x)
(β : (y : N) → TangentSpace (modelWithCornersSelf ℝ F) y [⋀^ι]→L[ℝ] Bundle.Trivial N G y)
(p : M × N)
:
theorem
DifferentialForm.trivializationAt_prodFamily_snd
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{M : Type u_3}
{N : Type u_4}
[TopologicalSpace M]
[ChartedSpace E M]
[TopologicalSpace N]
[ChartedSpace F N]
[IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M]
[IsManifold (modelWithCornersSelf ℝ F) (↑⊤) N]
{G : Type u_5}
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{ι : Type u_6}
[Fintype ι]
(α : (x : M) → TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ι]→L[ℝ] Bundle.Trivial M G x)
(β : (y : N) → TangentSpace (modelWithCornersSelf ℝ F) y [⋀^ι]→L[ℝ] Bundle.Trivial N G y)
(x₀ : M)
(y₀ : N)
{p : M × N}
(hp : p ∈ (chartAt (E × F) (x₀, y₀)).source)
:
(↑(trivializationAt ((E × F) [⋀^ι]→L[ℝ] G)
(fun (q : M × N) => TangentSpace (modelWithCornersSelf ℝ (E × F)) q [⋀^ι]→L[ℝ] Bundle.Trivial (M × N) G q)
(x₀, y₀))
⟨p, prodFamily α β p⟩).2 = (↑(trivializationAt (E [⋀^ι]→L[ℝ] G)
(fun (x : M) => TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ι]→L[ℝ] Bundle.Trivial M G x) x₀)
⟨p.1, α p.1⟩).2.prodSum
(↑(trivializationAt (F [⋀^ι]→L[ℝ] G)
(fun (y : N) => TangentSpace (modelWithCornersSelf ℝ F) y [⋀^ι]→L[ℝ] Bundle.Trivial N G y) y₀)
⟨p.2, β p.2⟩).2
★ Through the tangent trivialisation at (x₀, y₀), the family reads as the prodSum of
the factors' trivialised values: the coordinate change of a product chart is the block map of
the factors' coordinate changes.
theorem
DifferentialForm.localRep_prodFamily
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{M : Type u_3}
{N : Type u_4}
[TopologicalSpace M]
[ChartedSpace E M]
[TopologicalSpace N]
[ChartedSpace F N]
[IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M]
[IsManifold (modelWithCornersSelf ℝ F) (↑⊤) N]
{G : Type u_5}
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{ι : Type u_6}
[Fintype ι]
(α : (x : M) → TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ι]→L[ℝ] Bundle.Trivial M G x)
(β : (y : N) → TangentSpace (modelWithCornersSelf ℝ F) y [⋀^ι]→L[ℝ] Bundle.Trivial N G y)
(x₀ : M)
(y₀ : N)
{w : E × F}
(hw : w ∈ (chartAt (E × F) (x₀, y₀)).target)
:
★ The local representative of the sum in a product chart is the prodSum of the factors'
local representatives.
theorem
DifferentialForm.contMDiff_prodFamily
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{M : Type u_3}
{N : Type u_4}
[TopologicalSpace M]
[ChartedSpace E M]
[TopologicalSpace N]
[ChartedSpace F N]
[IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M]
[IsManifold (modelWithCornersSelf ℝ F) (↑⊤) N]
{G : Type u_5}
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{ι : Type u_6}
[Fintype ι]
{α : (x : M) → TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ι]→L[ℝ] Bundle.Trivial M G x}
{β : (y : N) → TangentSpace (modelWithCornersSelf ℝ F) y [⋀^ι]→L[ℝ] Bundle.Trivial N G y}
(hα :
ContMDiff (modelWithCornersSelf ℝ E) ((modelWithCornersSelf ℝ E).prod (modelWithCornersSelf ℝ (E [⋀^ι]→L[ℝ] G))) ↑⊤
fun (x : M) => ⟨x, α x⟩)
(hβ :
ContMDiff (modelWithCornersSelf ℝ F) ((modelWithCornersSelf ℝ F).prod (modelWithCornersSelf ℝ (F [⋀^ι]→L[ℝ] G))) ↑⊤
fun (y : N) => ⟨y, β y⟩)
:
ContMDiff (modelWithCornersSelf ℝ (E × F))
((modelWithCornersSelf ℝ (E × F)).prod (modelWithCornersSelf ℝ ((E × F) [⋀^ι]→L[ℝ] G))) ↑⊤ fun (p : M × N) =>
⟨p, prodFamily α β p⟩
The sum of two C^∞ families is a C^∞ section on the product.
def
DifferentialForm.prodForm
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{M : Type u_3}
{N : Type u_4}
[TopologicalSpace M]
[ChartedSpace E M]
[TopologicalSpace N]
[ChartedSpace F N]
[IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M]
[IsManifold (modelWithCornersSelf ℝ F) (↑⊤) N]
{G : Type u_5}
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{ι : Type u_6}
[Fintype ι]
(α : DifferentialForm (modelWithCornersSelf ℝ E) M (↑⊤) ι G)
(β : DifferentialForm (modelWithCornersSelf ℝ F) N (↑⊤) ι G)
:
DifferentialForm (modelWithCornersSelf ℝ (E × F)) (M × N) (↑⊤) ι G
★ π₁^* α + π₂^* β as a C^∞ form on the product.
Equations
- α.prodForm β = { toFun := DifferentialForm.prodFamily (fun (x : M) => α x) fun (y : N) => β y, contMDiff_toFun := ⋯ }
Instances For
@[simp]
theorem
DifferentialForm.prodForm_apply
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{M : Type u_3}
{N : Type u_4}
[TopologicalSpace M]
[ChartedSpace E M]
[TopologicalSpace N]
[ChartedSpace F N]
[IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M]
[IsManifold (modelWithCornersSelf ℝ F) (↑⊤) N]
{G : Type u_5}
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{ι : Type u_6}
[Fintype ι]
(α : DifferentialForm (modelWithCornersSelf ℝ E) M (↑⊤) ι G)
(β : DifferentialForm (modelWithCornersSelf ℝ F) N (↑⊤) ι G)
(p : M × N)
:
The exterior derivative of the sum #
theorem
DifferentialForm.extDeriv_prodSum_comp
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G : Type u_5}
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
{a : E → E [⋀^Fin k]→L[ℝ] G}
{b : F → F [⋀^Fin k]→L[ℝ] G}
{w : E × F}
(ha : DifferentiableAt ℝ a w.1)
(hb : DifferentiableAt ℝ b w.2)
:
The flat sum of two form-valued functions on the factors, pulled back to E × F.
theorem
DifferentialForm.mextDerivFamily_prodFamily
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{M : Type u_3}
{N : Type u_4}
[TopologicalSpace M]
[ChartedSpace E M]
[TopologicalSpace N]
[ChartedSpace F N]
[IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M]
[IsManifold (modelWithCornersSelf ℝ F) (↑⊤) N]
{G : Type u_5}
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
{α : (x : M) → TangentSpace (modelWithCornersSelf ℝ E) x [⋀^Fin k]→L[ℝ] Bundle.Trivial M G x}
{β : (y : N) → TangentSpace (modelWithCornersSelf ℝ F) y [⋀^Fin k]→L[ℝ] Bundle.Trivial N G y}
(hα :
ContMDiff (modelWithCornersSelf ℝ E) ((modelWithCornersSelf ℝ E).prod (modelWithCornersSelf ℝ (E [⋀^Fin k]→L[ℝ] G)))
↑⊤ fun (x : M) => ⟨x, α x⟩)
(hβ :
ContMDiff (modelWithCornersSelf ℝ F) ((modelWithCornersSelf ℝ F).prod (modelWithCornersSelf ℝ (F [⋀^Fin k]→L[ℝ] G)))
↑⊤ fun (y : N) => ⟨y, β y⟩)
(p : M × N)
:
mextDerivFamily (prodFamily α β) p = (toFlat (mextDerivFamily α p.1)).prodSum (toFlat (mextDerivFamily β p.2))
★★ d (π₁^* α + π₂^* β) = π₁^* dα + π₂^* dβ, pointwise, for C^∞ factors.
theorem
DifferentialForm.prodForm_mextDeriv
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{M : Type u_3}
{N : Type u_4}
[TopologicalSpace M]
[ChartedSpace E M]
[TopologicalSpace N]
[ChartedSpace F N]
[IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M]
[IsManifold (modelWithCornersSelf ℝ F) (↑⊤) N]
{G : Type u_5}
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
(α : DifferentialForm (modelWithCornersSelf ℝ E) M (↑⊤) (Fin k) G)
(β : DifferentialForm (modelWithCornersSelf ℝ F) N (↑⊤) (Fin k) G)
:
★★ d (prodForm α β) = prodForm (dα) (dβ).
The zero family #
theorem
DifferentialForm.trivializationAt_zero_snd
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace E M]
[IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M]
{G : Type u_5}
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{ι : Type u_6}
[Fintype ι]
(x₀ y : M)
(hy : y ∈ (chartAt E x₀).source)
:
(↑(trivializationAt (E [⋀^ι]→L[ℝ] G)
(fun (x : M) => TangentSpace (modelWithCornersSelf ℝ E) x [⋀^ι]→L[ℝ] Bundle.Trivial M G x) x₀)
⟨y, 0⟩).2 = 0
The zero family reads as zero through every tangent trivialisation.
theorem
DifferentialForm.localRep_zeroFamily
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace E M]
[IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M]
{G : Type u_5}
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{ι : Type u_6}
[Fintype ι]
(x₀ : M)
{w : E}
(hw : w ∈ (chartAt E x₀).target)
:
theorem
DifferentialForm.contMDiff_zeroFamily
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace E M]
[IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M]
{G : Type u_5}
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{ι : Type u_6}
[Fintype ι]
:
ContMDiff (modelWithCornersSelf ℝ E) ((modelWithCornersSelf ℝ E).prod (modelWithCornersSelf ℝ (E [⋀^ι]→L[ℝ] G))) ↑⊤
fun (x : M) => ⟨x, 0⟩
The zero family is a C^∞ section.
theorem
DifferentialForm.mextDerivFamily_zeroFamily
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace E M]
[IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M]
{G : Type u_5}
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{k : ℕ}
(x : M)
:
The exterior derivative of the zero family is zero.
Symplectic products #
theorem
DifferentialForm.IsSymplectic.prodForm
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{M : Type u_3}
{N : Type u_4}
[TopologicalSpace M]
[ChartedSpace E M]
[TopologicalSpace N]
[ChartedSpace F N]
[IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M]
[IsManifold (modelWithCornersSelf ℝ F) (↑⊤) N]
{α : DifferentialForm (modelWithCornersSelf ℝ E) M (↑⊤) (Fin 2) ℝ}
{β : DifferentialForm (modelWithCornersSelf ℝ F) N (↑⊤) (Fin 2) ℝ}
(hα : α.IsSymplectic)
(hβ : β.IsSymplectic)
:
(α.prodForm β).IsSymplectic
★★ The product of two symplectic manifolds is symplectic, with the form
π₁^* α + π₂^* β.