A product of manifolds, charted on the product normed space

Category: 1-Mathlib (CSD-free; upstream target Mathlib.Geometry.Manifold).

Mathlib charts M × N on the type synonym ModelProd E F with the model 𝓘(ℝ, E).prod 𝓘(ℝ, F), and deliberately keeps that apart from the normed space E × F with its self model 𝓘(ℝ, E × F) (modelWithCornersSelf_prod is the bridge, and its docstring says why it is kept separate). The corpus's form layer (DifferentialForm.lean … HamiltonianFlowVolume.lean) is stated for self models only, so to write a form on a product it needs the product charted on E × F.

This module supplies exactly that, by the same product charts:

• Prod.instChartedSpaceSelf — ChartedSpace (E × F) (M × N), the chart at (x, y) being (chartAt E x).prod (chartAt F y) (chartAt_prod, definitional);
• Prod.instIsManifoldSelf — IsManifold 𝓘(ℝ, E × F) n (M × N) from the factors, through Mathlib's product instance and modelWithCornersSelf_prod;
• ★ fderiv_chart_transition_prod — the derivative of a product chart transition is the product of the factors' derivatives (ContinuousLinearMap.prodMap), which is what the local-representative machinery of ExteriorDerivative.lean reads on a product;
• contMDiff_fst_self, contMDiff_snd_self, hasMFDerivAt_fst_self, hasMFDerivAt_snd_self, ContMDiff.prodMk_self, HasMFDerivAt.prodMk_self — the projections and pairings are smooth, with the expected derivatives, for the self model (Mathlib's statements, read through the bridge);
• ChartCover.prod — a finite chart cover of each factor gives one of the product.

Honest scope

⚠️ Two charted-space instances on M × N, keyed on the distinct model types ModelProd E F and E × F. Instance search never confuses them; a lemma stated for one is not automatically available for the other, which is why the transfer lemmas at the end exist.

⚠️ modelWithCornersSelf_prod is a propositional equality between models over different Hs. The instance proofs rewrite along it and finish with the factor instances; nothing here depends on the identification being definitional.

References: Mathlib/Geometry/Manifold/IsManifold/Basic.lean (modelWithCornersSelf_prod, ModelProd); Geometry/Manifold/ExteriorDerivative.lean (tangent_symmL_eq_fderiv, contDiffAt_chart_transition); Geometry/Manifold/ProductForm.lean (the consumer); specs/BACKLOG.md (R-016′).

The charted space and the manifold structure

@[instance_reducible]

instance Prod.instChartedSpaceSelf {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {M : Type u_3} {N : Type u_4} [TopologicalSpace M] [ChartedSpace E M] [TopologicalSpace N] [ChartedSpace F N] : ChartedSpace (E × F) (M × N)

★ The product charted on the normed space E × F, by the product charts.

Equations

• Prod.instChartedSpaceSelf = prodChartedSpace E M F N

theorem Prod.chartAt_prod {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {M : Type u_3} {N : Type u_4} [TopologicalSpace M] [ChartedSpace E M] [TopologicalSpace N] [ChartedSpace F N] (x : M) (y : N) : chartAt (E × F) (x, y) = (chartAt E x).prod (chartAt F y)

theorem Prod.chartAt_prod_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {M : Type u_3} {N : Type u_4} [TopologicalSpace M] [ChartedSpace E M] [TopologicalSpace N] [ChartedSpace F N] (x : M) (y : N) (p : M × N) : ↑(chartAt (E × F) (x, y)) p = (↑(chartAt E x) p.1, ↑(chartAt F y) p.2)

theorem Prod.chartAt_prod_symm_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {M : Type u_3} {N : Type u_4} [TopologicalSpace M] [ChartedSpace E M] [TopologicalSpace N] [ChartedSpace F N] (x : M) (y : N) (w : E × F) : ↑(chartAt (E × F) (x, y)).symm w = (↑(chartAt E x).symm w.1, ↑(chartAt F y).symm w.2)

theorem Prod.chartAt_prod_source {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {M : Type u_3} {N : Type u_4} [TopologicalSpace M] [ChartedSpace E M] [TopologicalSpace N] [ChartedSpace F N] (x : M) (y : N) : (chartAt (E × F) (x, y)).source = (chartAt E x).source ×ˢ (chartAt F y).source

theorem Prod.chartAt_prod_target {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {M : Type u_3} {N : Type u_4} [TopologicalSpace M] [ChartedSpace E M] [TopologicalSpace N] [ChartedSpace F N] (x : M) (y : N) : (chartAt (E × F) (x, y)).target = (chartAt E x).target ×ˢ (chartAt F y).target

theorem Prod.chart_transition_prod {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {M : Type u_3} {N : Type u_4} [TopologicalSpace M] [ChartedSpace E M] [TopologicalSpace N] [ChartedSpace F N] (x x' : M) (y y' : N) : ↑(chartAt (E × F) (x', y')) ∘ ↑(chartAt (E × F) (x, y)).symm = map (↑(chartAt E x') ∘ ↑(chartAt E x).symm) (↑(chartAt F y') ∘ ↑(chartAt F y).symm)

The chart transition on a product is the product of the chart transitions.

instance Prod.instIsManifoldSelf {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {M : Type u_3} {N : Type u_4} [TopologicalSpace M] [ChartedSpace E M] [TopologicalSpace N] [ChartedSpace F N] [NormedSpace ℝ E] [NormedSpace ℝ F] {n : WithTop ℕ∞} [IsManifold (modelWithCornersSelf ℝ E) n M] [IsManifold (modelWithCornersSelf ℝ F) n N] : IsManifold (modelWithCornersSelf ℝ (E × F)) n (M × N)

★ The product of manifolds is a manifold over the product normed space.

The derivative of a product transition

theorem Prod.fderiv_chart_transition_prod {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {M : Type u_3} {N : Type u_4} [TopologicalSpace M] [ChartedSpace E M] [TopologicalSpace N] [ChartedSpace F N] [NormedSpace ℝ E] [NormedSpace ℝ F] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] [IsManifold (modelWithCornersSelf ℝ F) (↑⊤) N] (x x' : M) (y y' : N) {w : E × F} (hw₁ : w.1 ∈ (chartAt E x).target) (hx' : ↑(chartAt E x).symm w.1 ∈ (chartAt E x').source) (hw₂ : w.2 ∈ (chartAt F y).target) (hy' : ↑(chartAt F y).symm w.2 ∈ (chartAt F y').source) : fderiv ℝ (↑(chartAt (E × F) (x', y')) ∘ ↑(chartAt (E × F) (x, y)).symm) w = (fderiv ℝ (↑(chartAt E x') ∘ ↑(chartAt E x).symm) w.1).prodMap (fderiv ℝ (↑(chartAt F y') ∘ ↑(chartAt F y).symm) w.2)

★ The derivative of a product chart transition is the product of the factors' derivatives, at every point where both factor transitions are defined.

Smoothness of the projections and of pairings, for the self model

theorem Prod.contMDiff_fst_self {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {M : Type u_3} {N : Type u_4} [TopologicalSpace M] [ChartedSpace E M] [TopologicalSpace N] [ChartedSpace F N] [NormedSpace ℝ E] [NormedSpace ℝ F] {n : WithTop ℕ∞} : ContMDiff (modelWithCornersSelf ℝ (E × F)) (modelWithCornersSelf ℝ E) n fst

theorem Prod.contMDiff_snd_self {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {M : Type u_3} {N : Type u_4} [TopologicalSpace M] [ChartedSpace E M] [TopologicalSpace N] [ChartedSpace F N] [NormedSpace ℝ E] [NormedSpace ℝ F] {n : WithTop ℕ∞} : ContMDiff (modelWithCornersSelf ℝ (E × F)) (modelWithCornersSelf ℝ F) n snd

theorem Prod.hasMFDerivAt_fst_self {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {M : Type u_3} {N : Type u_4} [TopologicalSpace M] [ChartedSpace E M] [TopologicalSpace N] [ChartedSpace F N] [NormedSpace ℝ E] [NormedSpace ℝ F] (p : M × N) : HasMFDerivAt% fst p (ContinuousLinearMap.fst ℝ E F)

The manifold derivative of the first projection, for the self model.

theorem Prod.hasMFDerivAt_snd_self {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {M : Type u_3} {N : Type u_4} [TopologicalSpace M] [ChartedSpace E M] [TopologicalSpace N] [ChartedSpace F N] [NormedSpace ℝ E] [NormedSpace ℝ F] (p : M × N) : HasMFDerivAt% snd p (ContinuousLinearMap.snd ℝ E F)

The manifold derivative of the second projection, for the self model.

theorem HasMFDerivAt.congr_deriv {E : Type u_1} [NormedAddCommGroup E] {M : Type u_3} [TopologicalSpace M] [ChartedSpace E M] [NormedSpace ℝ E] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] {P : Type u_6} [TopologicalSpace P] [ChartedSpace G P] {f : P → M} {x : P} {df df' : TangentSpace (modelWithCornersSelf ℝ G) x →L[ℝ] TangentSpace (modelWithCornersSelf ℝ E) (f x)} (h : HasMFDerivAt% f x df) (h' : df = df') : HasMFDerivAt% f x df'

Replace the derivative in a HasMFDerivAt by an equal one. Stated once so that the equality is used at a site where the two continuous linear maps have syntactically the same type; at a use site exact h.congr_deriv h' lets unification identify the instance paths.

theorem HasMFDerivAt.prodMk_self {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {M : Type u_3} {N : Type u_4} [TopologicalSpace M] [ChartedSpace E M] [TopologicalSpace N] [ChartedSpace F N] [NormedSpace ℝ E] [NormedSpace ℝ F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] {P : Type u_6} [TopologicalSpace P] [ChartedSpace G P] {f : P → M} {g : P → N} {x : P} {df : TangentSpace (modelWithCornersSelf ℝ G) x →L[ℝ] TangentSpace (modelWithCornersSelf ℝ E) (f x)} (hf : HasMFDerivAt% f x df) {dg : TangentSpace (modelWithCornersSelf ℝ G) x →L[ℝ] TangentSpace (modelWithCornersSelf ℝ F) (g x)} (hg : HasMFDerivAt% g x dg) : HasMFDerivAt% (fun (y : P) => (f y, g y)) x (df.prod dg)

The manifold derivative of a pairing, for the self model on the product.

theorem ContMDiff.prodMk_self {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {M : Type u_3} {N : Type u_4} [TopologicalSpace M] [ChartedSpace E M] [TopologicalSpace N] [ChartedSpace F N] [NormedSpace ℝ E] [NormedSpace ℝ F] {n : WithTop ℕ∞} {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] {P : Type u_6} [TopologicalSpace P] [ChartedSpace G P] {f : P → M} {g : P → N} (hf : ContMDiff (modelWithCornersSelf ℝ G) (modelWithCornersSelf ℝ E) n f) (hg : ContMDiff (modelWithCornersSelf ℝ G) (modelWithCornersSelf ℝ F) n g) : ContMDiff (modelWithCornersSelf ℝ G) (modelWithCornersSelf ℝ (E × F)) n fun (p : P) => (f p, g p)

Chart covers of a product

def ChartCover.prod {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {M : Type u_3} {N : Type u_4} [TopologicalSpace M] [ChartedSpace E M] [TopologicalSpace N] [ChartedSpace F N] [NormedSpace ℝ E] [NormedSpace ℝ F] (c : ChartCover E M) (c' : ChartCover F N) : ChartCover (E × F) (M × N)

A finite chart cover of each factor covers the product by the product charts.

Equations

• c.prod c' = { m := c.m * c'.m, pt := fun (k : Fin (c.m * c'.m)) => (c.pt (finProdFinEquiv.symm k).1, c'.pt (finProdFinEquiv.symm k).2), cover := ⋯ }