Diffeomorphisms of products

If a diffeomorphism between nonempty products has underlying map Prod.map f g, then both f and g are diffeomorphisms. No smoothness of the factor maps or their inverses is assumed: each is recovered as a slice of the product diffeomorphism or its inverse. This lets one promote separation of a smooth map into separation by bundled equivalences.

Diffeomorph.prodAssocOfModels reassociates three manifold factors with independent model vector spaces, generalizing Mathlib's Diffeomorph.prodAssoc, where the last two coincide.

The four-way exchange ((a, b), (c, d)) ↦ ((a, c), (b, d)) of a product of two products is the diffeomorphism Diffeomorph.prodProdProdComm, the smooth counterpart of Equiv.prodProdProdComm. It regroups a product of relations M₁ ⇝ N₁ and M₂ ⇝ N₂ as a relation M₁ × M₂ ⇝ N₁ × N₂.

theorem Diffeomorph.exists_factors_of_eq_prodMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_5} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {F' : Type u_8} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {G' : Type u_9} [TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_11} [TopologicalSpace N] [ChartedSpace G N] {M' : Type u_12} [TopologicalSpace M'] [ChartedSpace H' M'] {N' : Type u_13} [TopologicalSpace N'] [ChartedSpace G' N'] {n : WithTop ℕ∞} (Q : Diffeomorph (I.prod J) (I'.prod J') (M × N) (M' × N') n) [Nonempty M] [Nonempty N] (f : M → M') (g : N → N') (hQ : ⇑Q = Prod.map f g) : ∃ (φ : Diffeomorph I I' M M' n) (ψ : Diffeomorph J J' N N' n), ⇑φ = f ∧ ⇑ψ = g

The factors of a diffeomorphism whose underlying map separates are themselves C^n diffeomorphisms. Nonemptiness excludes an empty product hiding an arbitrary factor.

def Diffeomorph.prodAssocOfModels {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_5} [TopologicalSpace G] (J : ModelWithCorners 𝕜 F G) {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') (M : Type u_10) [TopologicalSpace M] [ChartedSpace H M] (N : Type u_11) [TopologicalSpace N] [ChartedSpace G N] (M' : Type u_12) [TopologicalSpace M'] [ChartedSpace H' M'] (n : WithTop ℕ∞) : Diffeomorph ((I.prod J).prod I') (I.prod (J.prod I')) ((M × N) × M') (M × N × M') n

Reassociation of three manifold factors with independent model vector spaces.

@[simp]

theorem Diffeomorph.prodAssocOfModels_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_5} [TopologicalSpace G] (J : ModelWithCorners 𝕜 F G) {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') (M : Type u_10) [TopologicalSpace M] [ChartedSpace H M] (N : Type u_11) [TopologicalSpace N] [ChartedSpace G N] (M' : Type u_12) [TopologicalSpace M'] [ChartedSpace H' M'] (n : WithTop ℕ∞) (p : (M × N) × M') : (prodAssocOfModels I J I' M N M' n) p = (p.1.1, p.1.2, p.2)

Reassociation sends ((x, y), z) to (x, (y, z)).

@[simp]

theorem Diffeomorph.prodAssocOfModels_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_5} [TopologicalSpace G] (J : ModelWithCorners 𝕜 F G) {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') (M : Type u_10) [TopologicalSpace M] [ChartedSpace H M] (N : Type u_11) [TopologicalSpace N] [ChartedSpace G N] (M' : Type u_12) [TopologicalSpace M'] [ChartedSpace H' M'] (n : WithTop ℕ∞) (p : M × N × M') : (prodAssocOfModels I J I' M N M' n).symm p = ((p.1, p.2.1), p.2.2)

Inverse reassociation sends (x, (y, z)) to ((x, y), z).

def Diffeomorph.prodProdProdComm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_5} [TopologicalSpace G] (J : ModelWithCorners 𝕜 F G) {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') {F' : Type u_8} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {G' : Type u_9} [TopologicalSpace G'] (J' : ModelWithCorners 𝕜 F' G') (M : Type u_10) [TopologicalSpace M] [ChartedSpace H M] (N : Type u_11) [TopologicalSpace N] [ChartedSpace G N] (M' : Type u_12) [TopologicalSpace M'] [ChartedSpace H' M'] (N' : Type u_13) [TopologicalSpace N'] [ChartedSpace G' N'] (n : WithTop ℕ∞) : Diffeomorph ((I.prod J).prod (I'.prod J')) ((I.prod I').prod (J.prod J')) ((M × N) × M' × N') ((M × M') × N × N') n

(M × N) × (M' × N') is diffeomorphic to (M × M') × (N × N'), by exchanging the two middle factors.

@[simp]

theorem Diffeomorph.prodProdProdComm_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_5} [TopologicalSpace G] (J : ModelWithCorners 𝕜 F G) {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') {F' : Type u_8} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {G' : Type u_9} [TopologicalSpace G'] (J' : ModelWithCorners 𝕜 F' G') (M : Type u_10) [TopologicalSpace M] [ChartedSpace H M] (N : Type u_11) [TopologicalSpace N] [ChartedSpace G N] (M' : Type u_12) [TopologicalSpace M'] [ChartedSpace H' M'] (N' : Type u_13) [TopologicalSpace N'] [ChartedSpace G' N'] (n : WithTop ℕ∞) : (prodProdProdComm I J I' J' M N M' N' n).symm = prodProdProdComm I I' J J' M M' N N' n

The inverse of the four-way exchange is the four-way exchange of the regrouped factors.

@[simp]

theorem Diffeomorph.coe_prodProdProdComm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_5} [TopologicalSpace G] (J : ModelWithCorners 𝕜 F G) {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_7} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') {F' : Type u_8} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {G' : Type u_9} [TopologicalSpace G'] (J' : ModelWithCorners 𝕜 F' G') (M : Type u_10) [TopologicalSpace M] [ChartedSpace H M] (N : Type u_11) [TopologicalSpace N] [ChartedSpace G N] (M' : Type u_12) [TopologicalSpace M'] [ChartedSpace H' M'] (N' : Type u_13) [TopologicalSpace N'] [ChartedSpace G' N'] (n : WithTop ℕ∞) : ⇑(prodProdProdComm I J I' J' M N M' N' n) = ⇑(Equiv.prodProdProdComm M N M' N')

The underlying map of the four-way exchange is Equiv.prodProdProdComm.