feat: inclusion maps into finite coproducts in Stonean are open embeddings (#6774)

... both the explicit and the abstract one.

- [x] depends on: #6771 

Co-authored-by: Riccardo Brasca @riccardobrasca [riccardo.brasca@gmail.com](mailto:riccardo.brasca@gmail.com)
Co-authored-by: Filippo A E Nuccio @faenuccio [filippo.nuccio@univ-st-etienne.fr](mailto:filippo.nuccio@univ-st-etienne.fr)

Author: dagurtomas

Mathlib/Topology/Category/Stonean/Limits.lean

@@ -126,6 +126,21 @@ def coproductIsoCoproduct : finiteCoproduct X ≅ ∐ X :=
 Limits.IsColimit.coconePointUniqueUpToIso
   (finiteCoproduct.isColimit' X) (Limits.colimit.isColimit _)
 
+/-- The inclusion maps into the explicit finite coproduct are open embeddings. -/
+lemma finiteCoproduct.openEmbedding_ι {α : Type} [Fintype α] (Z : α → Stonean.{u}) (a : α) :
+    OpenEmbedding (finiteCoproduct.ι Z a) :=
+  openEmbedding_sigmaMk (σ := fun a => (Z a))
+
+/-- The inclusion maps into the abstract finite coproduct are open embeddings. -/
+lemma Sigma.openEmbedding_ι {α : Type} [Fintype α] (Z : α → Stonean.{u}) (a : α) :
+    OpenEmbedding (Sigma.ι Z a) := by
+  refine' OpenEmbedding.of_comp _ (homeoOfIso (coproductIsoCoproduct Z).symm).openEmbedding _
+  convert finiteCoproduct.openEmbedding_ι Z a
+  ext x
+  change ((Sigma.ι Z a) ≫ (coproductIsoCoproduct Z).inv) x = _
+  simp only [coproductIsoCoproduct, colimit.comp_coconePointUniqueUpToIso_inv,
+    finiteCoproduct.explicitCocone_pt, finiteCoproduct.explicitCocone_ι, Discrete.natTrans_app]
+
 end FiniteCoproducts
 
 end Stonean