Euclidean charts on products

Mathlib charts a product M × N of spaces charted on H and H' on the type synonym ModelProd H H'. For spaces charted on Euclidean spaces this file reads those product charts on a single Euclidean space: TauCeti.prodEuclideanChartedSpace charts M × N on EuclideanSpace 𝕜 (Fin (n + m)) when M and N are charted on EuclideanSpace 𝕜 (Fin n) and EuclideanSpace 𝕜 (Fin m), by composing the product charts with EuclideanSpace.finAddEquivProd. TauCeti.prodEuclideanChartedSpace_chartAt describes its charts.

It is a definition rather than an instance, so that the Euclidean model can be chosen explicitly alongside Mathlib's product model.

@[instance_reducible]

noncomputable def TauCeti.prodEuclideanChartedSpace {𝕜 : Type u_1} [RCLike 𝕜] {n m : ℕ} {M : Type u_2} {N : Type u_3} [TopologicalSpace M] [TopologicalSpace N] [ChartedSpace (EuclideanSpace 𝕜 (Fin n)) M] [ChartedSpace (EuclideanSpace 𝕜 (Fin m)) N] : ChartedSpace (EuclideanSpace 𝕜 (Fin (n + m))) (M × N)

The product M × N of spaces charted on 𝕜ⁿ and 𝕜ᵐ, charted on 𝕜ⁿ⁺ᵐ: the product of charts of M and N, followed by the identification EuclideanSpace.finAddEquivProd of 𝕜ⁿ × 𝕜ᵐ with 𝕜ⁿ⁺ᵐ.

@[simp]

theorem TauCeti.prodEuclideanChartedSpace_chartAt {𝕜 : Type u_1} [RCLike 𝕜] {n m : ℕ} {M : Type u_2} {N : Type u_3} [TopologicalSpace M] [TopologicalSpace N] [ChartedSpace (EuclideanSpace 𝕜 (Fin n)) M] [ChartedSpace (EuclideanSpace 𝕜 (Fin m)) N] (x : M × N) : chartAt (EuclideanSpace 𝕜 (Fin (n + m))) x = ((chartAt (EuclideanSpace 𝕜 (Fin n)) x.1).prod (chartAt (EuclideanSpace 𝕜 (Fin m)) x.2)).trans EuclideanSpace.finAddEquivProd.symm.toHomeomorph.toOpenPartialHomeomorph

The chart of TauCeti.prodEuclideanChartedSpace at x is the product of the charts of the factors at x.1 and x.2, followed by EuclideanSpace.finAddEquivProd.symm.