From e792f1a37f72a65d3f6748d98bf15f141dfe6a8d Mon Sep 17 00:00:00 2001
From: zstone1 <zstonex@gmail.com>
Date: Sat, 9 Nov 2024 22:51:22 -0500
Subject: [PATCH] Homeomorphisms for (X*Y)*Z -> X*(Y*Z) and X*Y -> Y*X (#1367)

* homeomorphims for products

---------

Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>
---
 CHANGELOG_UNRELEASED.md                     |  5 ++++
 classical/mathcomp_extra.v                  | 24 ++++++++++++++++-
 theories/topology_theory/product_topology.v | 30 +++++++++++++++++++++
 3 files changed, 58 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 92c340e0d..d48bcd8dc 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -71,6 +71,11 @@
   + lemma `countable_measurable`
 - in `realfun.v`:
   + lemma `cvgr_dnbhsP`
+  + new definitions `prodA`, and `prodAr`.
+  + new lemmas `prodAK`, `prodArK`, and `swapK`.
+- in file `product_topology.v`,
+  + new lemmas `swap_continuous`, `prodA_continuous`, and 
+    `prodAr_continuous`.
 
 ### Changed
 
diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
index 2c72f25ca..f0ecf3733 100644
--- a/classical/mathcomp_extra.v
+++ b/classical/mathcomp_extra.v
@@ -18,6 +18,8 @@ From mathcomp Require Import finset interval.
 (*                           {in A &, {mono f : x y /~ x <= y}}               *)
 (*             sigT_fun f := lifts a family of functions f into a function on *)
 (*                           the dependent sum                                *)
+(*                prodA x := sends (X * Y) * Z to X * (Y * Z)                 *)
+(*               prodAr x := sends X * (Y * Z) to (X * Y) * Z                 *)
 (* ```                                                                        *)
 (*                                                                            *)
 (******************************************************************************)
@@ -373,7 +375,27 @@ Lemma real_ltr_distlC [R : numDomainType] [x y : R] (e : R) :
   x - y \is Num.real -> (`|x - y| < e) = (x - e < y < x + e).
 Proof. by move=> ?; rewrite distrC real_ltr_distl// -rpredN opprB. Qed.
 
-Definition swap (T1 T2 : Type) (x : T1 * T2) := (x.2, x.1).
+Definition swap {T1 T2 : Type} (x : T1 * T2) := (x.2, x.1).
+
+Section reassociate_products.
+Context {X Y Z : Type}.
+
+Definition prodA (xyz : (X * Y) * Z) : X * (Y * Z) :=
+  (xyz.1.1, (xyz.1.2, xyz.2)).
+
+Definition prodAr (xyz : X * (Y * Z)) : (X * Y) * Z :=
+  ((xyz.1, xyz.2.1), xyz.2.2).
+
+Lemma prodAK : cancel prodA prodAr.
+Proof. by case; case. Qed.
+
+Lemma prodArK : cancel prodAr prodA.
+Proof. by case => ? []. Qed.
+
+End reassociate_products.
+
+Lemma swapK {T1 T2 : Type} : cancel (@swap T1 T2) (@swap T2 T1).
+Proof. by case=> ? ?. Qed.
 
 Definition map_pair {S U : Type} (f : S -> U) (x : (S * S)) : (U * U) :=
   (f x.1, f x.2).
diff --git a/theories/topology_theory/product_topology.v b/theories/topology_theory/product_topology.v
index 8e2984d35..4755458fc 100644
--- a/theories/topology_theory/product_topology.v
+++ b/theories/topology_theory/product_topology.v
@@ -231,3 +231,33 @@ by apply: (ngPr (b, a, i)); split => //; exact: N1N2N.
 Unshelve. all: by end_near. Qed.
 #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `compact_setX`")]
 Notation compact_setM := compact_setX (only parsing).
+
+Lemma swap_continuous {X Y : topologicalType} : continuous (@swap X Y).
+Proof.
+case=> a b W /= [[U V]][] /= Ub Va UVW; exists (V, U); first by split.
+by case => //= ? ? [] ? ?; exact: UVW.
+Qed.
+
+Section reassociate_continuous.
+Context {X Y Z : topologicalType}.
+
+Lemma prodA_continuous : continuous (@prodA X Y Z).
+Proof.
+move=> [] [a b] c U [[/= P V]] [Pa] [][/= Q R][ Qb Rc] QRV PVU.
+exists ((P `*` Q), R); first split.
+- exists (P, Q); first by [].
+  by case=> x y /= [Px Qy].
+- by [].
+- by move=> [[x y] z] [] [] ? ? ?; apply: PVU; split => //; exact: QRV.
+Qed.
+
+Lemma prodAr_continuous : continuous (@prodAr X Y Z).
+Proof.
+case=> a [b c] U [[V R]] [/= [[P Q /=]]] [Pa Qb] PQV Rc VRU.
+exists (P, (Q `*` R)); first split => //.
+- exists (Q, R); first by [].
+  by case=> ? ? /= [].
+- by case=> x [y z] [? [? ?]]; apply: VRU; split => //; exact: PQV.
+Qed.
+
+End reassociate_continuous.