From 4ab4519f359125216bc073bcba9df1cd3bfa6b9d Mon Sep 17 00:00:00 2001
From: m13683320924-hue <m13683320924@163.com>
Date: Wed, 13 May 2026 03:58:03 +0800
Subject: [PATCH] feat: prove strict group homs are stable under Prod.map

Add section for properties of strict maps between topological groups and related theorems.
---
 Mathlib/Topology/Algebra/Group/Basic.lean | 44 +++++++++++++++++++++++
 1 file changed, 44 insertions(+)

diff --git a/Mathlib/Topology/Algebra/Group/Basic.lean b/Mathlib/Topology/Algebra/Group/Basic.lean
index 9348c7d88a3bf6..2bd8041dc21d0a 100644
--- a/Mathlib/Topology/Algebra/Group/Basic.lean
+++ b/Mathlib/Topology/Algebra/Group/Basic.lean
@@ -14,6 +14,7 @@ public import Mathlib.Order.Filter.Bases.Finite
 public import Mathlib.Topology.Algebra.Group.Defs
 public import Mathlib.Topology.Algebra.Monoid
 public import Mathlib.Topology.Homeomorph.Lemmas
+public import Mathlib.Topology.Maps.Strict.Basic
 
 /-!
 # Topological groups
@@ -913,6 +914,49 @@ lemma MonoidHom.isOpenQuotientMap_of_isQuotientMap {A : Type*} [Group A]
         use x * k, hx
         rw [map_mul, hk, mul_one]
 
+-- Section for properties of strict maps between topological groups
+section StrictMaps
+
+variable {G H : Type*} [Group G] [TopologicalSpace G] [ContinuousMul G] [Group H] [TopologicalSpace H]
+  (f : G →* H)
+
+@[to_additive]
+theorem MonoidHom.isOpenQuotientMap_of_strictMap (hf : Topology.IsStrictMap f) :
+    IsOpenQuotientMap f.rangeRestrict := by
+  refine MonoidHom.isOpenQuotientMap_of_isQuotientMap ?_
+  convert hf using 1
+
+end StrictMaps
+
+namespace Topology.IsStrictMap
+
+variable {G H K L : Type*}
+  [Group G] [TopologicalSpace G] [ContinuousMul G]
+  [Group H] [TopologicalSpace H] [ContinuousMul H]
+  [Group K] [TopologicalSpace K] [ContinuousMul K]
+  [Group L] [TopologicalSpace L] [ContinuousMul L]
+  {f : G →* H} {g : K →* L}
+
+omit [ContinuousMul H] [ContinuousMul L] in
+@[to_additive]
+theorem prodMap (hf : IsStrictMap f) (hg : IsStrictMap g) :
+    IsStrictMap (MonoidHom.prodMap f g) := by
+  have h4 : Set.range (MonoidHom.prodMap f g) = Set.range f ×ˢ Set.range g := Set.range_prodMap
+  have h5' : IsOpenQuotientMap (Set.rangeFactorization f) := by
+    convert MonoidHom.isOpenQuotientMap_of_strictMap f hf using 1
+  have h6' : IsOpenQuotientMap (Set.rangeFactorization g) := by
+    convert MonoidHom.isOpenQuotientMap_of_strictMap g hg using 1
+  have h7' : IsOpenQuotientMap (Prod.map (Set.rangeFactorization f) (Set.rangeFactorization g)) :=
+    IsOpenQuotientMap.prodMap h5' h6'
+  let e0 : (Set.range (MonoidHom.prodMap f g)) ≃ₜ (Set.range f ×ˢ Set.range g) := Homeomorph.setCongr h4
+  let e : (Set.range (MonoidHom.prodMap f g)) ≃ₜ (Set.range f × Set.range g) := e0.trans (Homeomorph.Set.prod (Set.range f) (Set.range g))
+  have h8 : IsOpenQuotientMap (e.symm ∘ Prod.map (Set.rangeFactorization f) (Set.rangeFactorization g)) :=
+    IsOpenQuotientMap.comp e.symm.isOpenQuotientMap h7'
+  rw [Topology.IsStrictMap]
+  convert h8.isQuotientMap using 1
+
+end Topology.IsStrictMap
+
 @[to_additive]
 theorem IsTopologicalGroup.ext {G : Type*} [Group G] {t t' : TopologicalSpace G}
     (tg : @IsTopologicalGroup G t _) (tg' : @IsTopologicalGroup G t' _)