feat: add sumPiEquivProdPi and piUnique (#20195)

From FLT. Add topological and algebraic versions of `Equiv.sumPiEquivProdPi` and `Equiv.piUnique`.

Author: kbuzzard

Mathlib/Algebra/Module/Equiv/Basic.lean

@@ -11,6 +11,7 @@ import Mathlib.Algebra.Module.Equiv.Defs
 import Mathlib.Algebra.Module.Hom
 import Mathlib.Algebra.Module.LinearMap.End
 import Mathlib.Algebra.Module.Pi
+import Mathlib.Algebra.Module.Prod
 
 /-!
 # Further results on (semi)linear equivalences.
@@ -698,4 +699,36 @@ end LinearEquiv
 
 end FunLeft
 
+section Pi
+
+namespace LinearEquiv
+
+/-- The product over `S ⊕ T` of a family of modules is isomorphic to the product of
+(the product over `S`) and (the product over `T`).
+
+This is `Equiv.sumPiEquivProdPi` as a `LinearEquiv`.
+-/
+def sumPiEquivProdPi (R : Type*) [Semiring R] (S T : Type*) (A : S ⊕ T → Type*)
+    [∀ st, AddCommMonoid (A st)] [∀ st, Module R (A st)] :
+    (Π (st : S ⊕ T), A st) ≃ₗ[R] (Π (s : S), A (.inl s)) × (Π (t : T), A (.inr t)) where
+  __ := Equiv.sumPiEquivProdPi _
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
+
+/-- The product `Π t : α, f t` of a family of modules is linearly isomorphic to the module
+`f ⬝` when `α` only contains `⬝`.
+
+This is `Equiv.piUnique` as a `LinearEquiv`.
+-/
+@[simps (config := .asFn)]
+def piUnique {α : Type*} [Unique α] (R : Type*) [Semiring R] (f : α → Type*)
+    [∀ x, AddCommMonoid (f x)] [∀ x, Module R (f x)] : (Π t : α, f t) ≃ₗ[R] f default where
+  __ := Equiv.piUnique _
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
+
+end LinearEquiv
+
+end Pi
+
 end AddCommMonoid

Mathlib/Topology/Algebra/Module/Equiv.lean

@@ -567,6 +567,45 @@ def arrowCongrEquiv (e₁₂ : M₁ ≃SL[σ₁₂] M₂) (e₄₃ : M₄ ≃SL[
     ContinuousLinearMap.ext fun x => by
       simp only [ContinuousLinearMap.comp_apply, apply_symm_apply, coe_coe]
 
+section Pi
+
+/-- Combine a family of linear equivalences into a linear equivalence of `pi`-types.
+This is `Equiv.piCongrLeft` as a `ContinuousLinearEquiv`.
+-/
+def piCongrLeft (R : Type*) [Semiring R] {ι ι' : Type*}
+    (φ : ι → Type*) [∀ i, AddCommMonoid (φ i)] [∀ i, Module R (φ i)]
+    [∀ i, TopologicalSpace (φ i)]
+    (e : ι' ≃ ι) : ((i' : ι') → φ (e i')) ≃L[R] (i : ι) → φ i where
+  __ := Homeomorph.piCongrLeft e
+  __ := LinearEquiv.piCongrLeft R φ e
+
+/-- The product over `S ⊕ T` of a family of topological modules
+is isomorphic (topologically and alegbraically) to the product of
+(the product over `S`) and (the product over `T`).
+
+This is `Equiv.sumPiEquivProdPi` as a `ContinuousLinearEquiv`.
+-/
+def sumPiEquivProdPi (R : Type*) [Semiring R] (S T : Type*)
+    (A : S ⊕ T → Type*) [∀ st, AddCommMonoid (A st)] [∀ st, Module R (A st)]
+    [∀ st, TopologicalSpace (A st)] :
+    ((st : S ⊕ T) → A st) ≃L[R] ((s : S) → A (Sum.inl s)) × ((t : T) → A (Sum.inr t)) where
+  __ := LinearEquiv.sumPiEquivProdPi R S T A
+  __ := Homeomorph.sumPiEquivProdPi S T A
+
+/-- The product `Π t : α, f t` of a family of topological modules is isomorphic
+(both topologically and algebraically) to the space `f ⬝` when `α` only contains `⬝`.
+
+This is `Equiv.piUnique` as a `ContinuousLinearEquiv`.
+-/
+@[simps! (config := .asFn)]
+def piUnique {α : Type*} [Unique α] (R : Type*) [Semiring R] (f : α → Type*)
+    [∀ x, AddCommMonoid (f x)] [∀ x, Module R (f x)] [∀ x, TopologicalSpace (f x)] :
+    (Π t, f t) ≃L[R] f default where
+  __ := LinearEquiv.piUnique R f
+  __ := Homeomorph.piUnique f
+
+end Pi
+
 section piCongrRight
 
 variable {ι : Type*} {M : ι → Type*} [∀ i, TopologicalSpace (M i)] [∀ i, AddCommMonoid (M i)]

Mathlib/Topology/Basic.lean

@@ -1365,6 +1365,12 @@ theorem IsOpen.preimage (hf : Continuous f) {t : Set Y} (h : IsOpen t) :
     IsOpen (f ⁻¹' t) :=
   hf.isOpen_preimage t h
 
+lemma Equiv.continuous_symm_iff (e : X ≃ Y) : Continuous e.symm ↔ IsOpenMap e := by
+  simp_rw [continuous_def, ← Set.image_equiv_eq_preimage_symm, IsOpenMap]
+
+lemma Equiv.isOpenMap_symm_iff (e : X ≃ Y) : IsOpenMap e.symm ↔ Continuous e := by
+  simp_rw [← Equiv.continuous_symm_iff, Equiv.symm_symm]
+
 theorem continuous_congr {g : X → Y} (h : ∀ x, f x = g x) :
     Continuous f ↔ Continuous g :=
   .of_eq <| congrArg _ <| funext h

Mathlib/Topology/Homeomorph.lean

@@ -427,11 +427,7 @@ theorem locallyCompactSpace_iff (h : X ≃ₜ Y) :
 @[simps toEquiv]
 def homeomorphOfContinuousOpen (e : X ≃ Y) (h₁ : Continuous e) (h₂ : IsOpenMap e) : X ≃ₜ Y where
   continuous_toFun := h₁
-  continuous_invFun := by
-    rw [continuous_def]
-    intro s hs
-    convert ← h₂ s hs using 1
-    apply e.image_eq_preimage
+  continuous_invFun := e.continuous_symm_iff.2 h₂
   toEquiv := e
 
 /-- If a bijective map `e : X ≃ Y` is continuous and closed, then it is a homeomorphism. -/
@@ -671,6 +667,28 @@ def homeomorphOfUnique [Unique X] [Unique Y] : X ≃ₜ Y :=
     continuous_toFun := continuous_const
     continuous_invFun := continuous_const }
 
+/-- The product over `S ⊕ T` of a family of topological spaces
+is homeomorphic to the product of (the product over `S`) and (the product over `T`).
+
+This is `Equiv.sumPiEquivProdPi` as a `Homeomorph`.
+-/
+def sumPiEquivProdPi (S T : Type*) (A : S ⊕ T → Type*)
+    [∀ st, TopologicalSpace (A st)] :
+    (Π (st : S ⊕ T), A st) ≃ₜ (Π (s : S), A (.inl s)) × (Π (t : T), A (.inr t)) where
+  __ := Equiv.sumPiEquivProdPi _
+  continuous_toFun := Continuous.prod_mk (by fun_prop) (by fun_prop)
+  continuous_invFun := continuous_pi <| by rintro (s | t) <;> simp <;> fun_prop
+
+/-- The product `Π t : α, f t` of a family of topological spaces is homeomorphic to the
+space `f ⬝` when `α` only contains `⬝`.
+
+This is `Equiv.piUnique` as a `Homeomorph`.
+-/
+@[simps! (config := .asFn)]
+def piUnique {α : Type*} [Unique α] (f : α → Type*) [∀ x, TopologicalSpace (f x)] :
+    (Π t, f t) ≃ₜ f default :=
+  homeomorphOfContinuousOpen (Equiv.piUnique f) (continuous_apply default) (isOpenMap_eval _)
+
 end prod
 
 /-- `Equiv.piCongrLeft` as a homeomorphism: this is the natural homeomorphism