feat(logic/equiv, topology/homeomorph): split a product at a coordina…

…te (#16210)

+ Add `equiv.pi_split_at` and `homeomorph.pi_split_at`: for every "coordinate" `i : α`, the bijection/homeomorphism between a product `Π j : α, β j` of types/topological spaces and the binary product of the type/space `β i` at that coordinate and the product `Π j : {j // j ≠ i}, β j` over all other coordinates.

+ Specialize to get the non-dependent versions, which concerns a product of copies of the same type/topological space, in which case non-dependent versions are friendlier to unification. Moreover, separate definitions allow the use of `@[simps]` to generate lemmas in which type casts are automatically removed.

Prerequisite of #15681, where we deal with cubes, which are products of copies of the unit interval, for the purpose of showing commutativity of homotopy groups.

src/logic/equiv/basic.lean

@@ -1600,6 +1600,20 @@ depending on whether they satisfy a predicate `p` or not. -/
       refl },
   end }
 
+/-- A product of types can be split as the binary product of one of the types and the product
+  of all the remaining types. -/
+@[simps] def pi_split_at {α : Type*} [decidable_eq α] (i : α) (β : α → Type*) :
+  (Π j, β j) ≃ β i × Π j : {j // j ≠ i}, β j :=
+{ to_fun := λ f, ⟨f i, λ j, f j⟩,
+  inv_fun := λ f j, if h : j = i then h.symm.rec f.1 else f.2 ⟨j, h⟩,
+  right_inv := λ f, by { ext, exacts [dif_pos rfl, (dif_neg x.2).trans (by cases x; refl)] },
+  left_inv := λ f, by { ext, dsimp only, split_ifs, { subst h }, { refl } } }
+
+/-- A product of copies of a type can be split as the binary product of one copy and the product
+  of all the remaining copies. -/
+@[simps] def fun_split_at {α : Type*} [decidable_eq α] (i : α) (β : Type*) :
+  (α → β) ≃ β × ({j // j ≠ i} → β) := pi_split_at i _
+
 end
 
 section subtype_equiv_codomain

src/topology/homeomorph.lean

@@ -470,6 +470,38 @@ def set.univ (α : Type*) [topological_space α] : (univ : set α) ≃ₜ α :=
   continuous_inv_fun := (continuous_subtype_coe.fst'.prod_mk
     continuous_subtype_coe.snd').subtype_mk _ }
 
+section
+
+variable {ι : Type*}
+
+/-- The topological space `Π i, β i` can be split as a product by separating the indices in ι
+  depending on whether they satisfy a predicate p or not.-/
+@[simps] def pi_equiv_pi_subtype_prod (p : ι → Prop) (β : ι → Type*) [Π i, topological_space (β i)]
+  [decidable_pred p] : (Π i, β i) ≃ₜ (Π i : {x // p x}, β i) × Π i : {x // ¬p x}, β i :=
+{ to_equiv := equiv.pi_equiv_pi_subtype_prod p β,
+  continuous_to_fun := by apply continuous.prod_mk; exact continuous_pi (λ j, continuous_apply j),
+  continuous_inv_fun := continuous_pi $ λ j, begin
+    dsimp only [equiv.pi_equiv_pi_subtype_prod], split_ifs,
+    exacts [(continuous_apply _).comp continuous_fst, (continuous_apply _).comp continuous_snd],
+  end }
+
+variables [decidable_eq ι] (i : ι)
+
+/-- A product of topological spaces can be split as the binary product of one of the spaces and
+  the product of all the remaining spaces. -/
+@[simps] def pi_split_at (β : ι → Type*) [Π j, topological_space (β j)] :
+  (Π j, β j) ≃ₜ β i × Π j : {j // j ≠ i}, β j :=
+{ to_equiv := equiv.pi_split_at i β,
+  continuous_to_fun := (continuous_apply i).prod_mk (continuous_pi $ λ j, continuous_apply j),
+  continuous_inv_fun := continuous_pi $ λ j, by { dsimp only [equiv.pi_split_at],
+    split_ifs, subst h, exacts [continuous_fst, (continuous_apply _).comp continuous_snd] } }
+
+/-- A product of copies of a topological space can be split as the binary product of one copy and
+  the product of all the remaining copies. -/
+@[simps] def fun_split_at : (ι → β) ≃ₜ β × ({j // j ≠ i} → β) := pi_split_at i _
+
+end
+
 end homeomorph
 
 /-- An inducing equiv between topological spaces is a homeomorphism. -/