feat: more API specific to strict group homs (#41238)

* Move the section of `Topology.Maps.Strict.Basic` about group homs to a new file `Topology.Maps.Strict.Group`
* add more criterions for strictness of group homs
* the first isomorphism theorem holds for strict group homs, yielding a [ContinuousMulEquiv](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Algebra/ContinuousMonoidHom.html#ContinuousMulEquiv)
* various tweaks to namespaces and variables throughout the two files.

Author: ADedecker

Mathlib.lean

@@ -7986,6 +7986,7 @@ public import Mathlib.Topology.Maps.Proper.Basic
 public import Mathlib.Topology.Maps.Proper.CompactlyGenerated
 public import Mathlib.Topology.Maps.Proper.UniversallyClosed
 public import Mathlib.Topology.Maps.Strict.Basic
+public import Mathlib.Topology.Maps.Strict.Group
 public import Mathlib.Topology.MetricSpace.Algebra
 public import Mathlib.Topology.MetricSpace.Antilipschitz
 public import Mathlib.Topology.MetricSpace.Basic

Mathlib/Topology/Maps/Strict/Basic.lean

@@ -9,7 +9,6 @@ public import Mathlib.Topology.Maps.Basic
 public import Mathlib.Topology.Homeomorph.Quotient
 public import Mathlib.Topology.Constructions
 public import Mathlib.Data.Setoid.Basic
-public import Mathlib.Topology.Algebra.Group.Quotient
 
 /-!
 # Bourbaki Strict Maps
@@ -35,18 +34,6 @@ We provide several equivalent ways to characterize a strict map `f`:
   the canonical bijection `Quotient (Setoid.ker f) ≃ Set.range f` is a homeomorphism.
 * `Topology.isStrictMap_iff_isEmbedding_kerLift`: `f` is strict if and only if
   the canonical injection `Quotient (Setoid.ker f) → Y` (`Setoid.kerLift f`) is an embedding.
-
-### Group homomorphisms
-
-In general, the product (in the sense of `Prod.map`) of two strict maps need not be strict.
-But thanks to `MonoidHom.isOpenQuotientMap_of_isQuotientMap`, we can replace `IsQuotientMap`
-by `IsOpenQuotientMap` in the setting of group homomorphisms. Therefore we provide several
-important properties of strict group homomorphisms :
-
-* `isStrictMap_iff_isOpenQuotientMap_rangeRestrict`: `f` is a strict group homomorphism if
-  and only if the `rangeRestrict` of `f` is an open quotient map.
-* `isStrictMap_prodMap`: The product (in the sense of Prod.map) of strict group homomorphisms
-  is strict.
 -/
 
 @[expose] public section
@@ -56,8 +43,9 @@ open Function Set Topology Setoid
 namespace Topology
 
 variable {X Y Z : Type*} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]
-  (f : X → Y) {g : Y → Z}
+  {f : X → Y} {g : Y → Z}
 
+variable (f) in
 /-- A map is a strict map in the sense of Bourbaki if the natural map to its image
 is a quotient map. -/
 def IsStrictMap : Prop :=
@@ -67,8 +55,6 @@ lemma isStrictMap_iff_isQuotientMap_rangeFactorization :
     IsStrictMap f ↔ IsQuotientMap (Set.rangeFactorization f) :=
   Iff.rfl
 
-variable {f}
-
 /-- A map is a strict map if and only if the canonical bijection
 `Quotient (Setoid.ker f) ≃ Set.range f` is a homeomorphism. -/
 theorem isStrictMap_iff_isHomeomorph_quotientKerEquivRange :
@@ -80,10 +66,13 @@ theorem isStrictMap_iff_isHomeomorph_quotientKerEquivRange :
 
 /-- The homeomorphism `Quotient (Setoid.ker f) ≃ₜ Set.range f` given by a strict map `f`.
 This is the homeomorphism obtained from the first isomorphism theorem. -/
-noncomputable def Homeomorph.quotientKerEquivRange (hf : IsStrictMap f) :
+noncomputable def _root_.Homeomorph.quotientKerEquivRange (hf : IsStrictMap f) :
     Quotient (Setoid.ker f) ≃ₜ Set.range f :=
   (isStrictMap_iff_isHomeomorph_quotientKerEquivRange.mp hf).homeomorph
 
+@[deprecated (since := "2026-07-10")] protected alias Homeomorph.quotientKerEquivRange :=
+  Homeomorph.quotientKerEquivRange
+
 /-- A map is a strict map if and only if the canonical injection `Quotient (Setoid.ker f) → Y`
 (`Setoid.kerLift f`) is an embedding. -/
 theorem isStrictMap_iff_isEmbedding_kerLift :
@@ -98,24 +87,33 @@ lemma IsStrictMap.continuous {f : X → Y} (hf : IsStrictMap f) : Continuous f :
   exact continuous_rangeFactorization_iff.mp hf.continuous
 
 /-- A open continuous map is a strict map. -/
-lemma IsOpenMap.isStrictMap (ho : IsOpenMap f) (h_cont : Continuous f) :
+lemma _root_.IsOpenMap.isStrictMap (ho : IsOpenMap f) (h_cont : Continuous f) :
     IsStrictMap f := by
   rw [isStrictMap_iff_isQuotientMap_rangeFactorization]
   exact (ho.subtype_mk fun x => ⟨x, rfl⟩).isQuotientMap
     h_cont.rangeFactorization Set.rangeFactorization_surjective
 
+@[deprecated (since := "2026-07-10")] protected alias IsOpenMap.isStrictMap :=
+  IsOpenMap.isStrictMap
+
 /-- A closed continuous map is a strict map. -/
-lemma IsClosedMap.isStrictMap (hc : IsClosedMap f) (h_cont : Continuous f) :
+lemma _root_.IsClosedMap.isStrictMap (hc : IsClosedMap f) (h_cont : Continuous f) :
     IsStrictMap f := by
   rw [isStrictMap_iff_isQuotientMap_rangeFactorization]
   exact (hc.subtype_mk fun x => ⟨x, rfl⟩).isQuotientMap
     h_cont.rangeFactorization Set.rangeFactorization_surjective
 
+@[deprecated (since := "2026-07-10")] protected alias IsClosedMap.isStrictMap :=
+  IsClosedMap.isStrictMap
+
 /-- A homeomorphism is a strict map. -/
-lemma IsHomeomorph.isStrictMap (f_homeo : IsHomeomorph f) :
+lemma _root_.IsHomeomorph.isStrictMap (f_homeo : IsHomeomorph f) :
     IsStrictMap f :=
   f_homeo.isOpenMap.isStrictMap f_homeo.continuous
 
+@[deprecated (since := "2026-07-10")] protected alias IsHomeomorph.isStrictMap :=
+  IsHomeomorph.isStrictMap
+
 /-- The identity is a strict map. -/
 lemma IsStrictMap.id : IsStrictMap (id : X → X) := IsHomeomorph.id.isStrictMap
 
@@ -174,45 +172,19 @@ lemma isHomeomorph_iff_isStrictMap_bijective :
     and_assoc]
 
 /-- Strict maps are preserved when precomposing with a homeomorphism. -/
-lemma Homeomorph.isStrictMap_comp_iff (e : X ≃ₜ Y) {f : Y → Z} :
+lemma _root_.Homeomorph.isStrictMap_comp_iff (e : X ≃ₜ Y) {f : Y → Z} :
     IsStrictMap (f ∘ e) ↔ IsStrictMap f :=
   e.isQuotientMap.isStrictMap_iff.symm
 
+@[deprecated (since := "2026-07-10")] protected alias Homeomorph.isStrictMap_comp_iff :=
+  Homeomorph.isStrictMap_comp_iff
+
 /-- Strict maps are preserved when postcomposing with a homeomorphism. -/
-lemma Homeomorph.comp_isStrictMap_iff (e : Y ≃ₜ Z) {f : X → Y} :
+lemma _root_.Homeomorph.comp_isStrictMap_iff (e : Y ≃ₜ Z) {f : X → Y} :
     IsStrictMap (e ∘ f) ↔ IsStrictMap f :=
   e.isEmbedding.isStrictMap_iff.symm
 
-end Topology
-
-namespace MonoidHom
-
-variable {G H G' H' : Type*} [Group G'] [Group H'] [Group G] [Group H] (f : G →* H) (g : G' →* H')
-  [TopologicalSpace G] [IsTopologicalGroup G] [TopologicalSpace H]
-
-/-- A group homomorphism is strict if and only if its `rangeRestrict` is an open quotient map. -/
-@[to_additive] lemma isStrictMap_iff_isOpenQuotientMap_rangeRestrict :
-    IsStrictMap f ↔ IsOpenQuotientMap f.rangeRestrict := by
-  rw [isOpenQuotientMap_iff_isQuotientMap]
-  rfl
-
-variable {f g} [TopologicalSpace G'] [IsTopologicalGroup G'] [TopologicalSpace H']
+@[deprecated (since := "2026-07-10")] protected alias Homeomorph.comp_isStrictMap_iff :=
+  Homeomorph.comp_isStrictMap_iff
 
-/-- The product (in the sense of `Prod.map`) of group homomorphisms is strict if and only if each
-of the morphisms is strict. -/
-@[to_additive isStrictMap_prodMap_iff] lemma isStrictMap_prodMap_iff :
-    IsStrictMap (f.prodMap g) ↔ IsStrictMap f ∧ IsStrictMap g := by
-  simp_rw [isStrictMap_iff_isOpenQuotientMap_rangeRestrict]
-  let Φ : (f.prodMap g).range ≃ₜ f.range × g.range :=
-    (Homeomorph.setCongr (by simp [Subgroup.coe_prod])).trans (Homeomorph.Set.prod _ _)
-  have eq : Φ ∘ (f.prodMap g).rangeRestrict = f.rangeRestrict.prodMap g.rangeRestrict := rfl
-  rw [← Φ.comp_isOpenQuotientMap_iff, eq, MonoidHom.coe_prodMap, isOpenQuotientMap_prodMap_iff]
-
-/-- The product (in the sense of `Prod.map`) of strict group homomorphisms is strict -/
-@[to_additive isStrictMap_prodMap] lemma isStrictMap_prodMap (hf : IsStrictMap f)
-    (hg : IsStrictMap g) : IsStrictMap (f.prodMap g) :=
-  isStrictMap_prodMap_iff.mpr ⟨hf, hg⟩
-
--- TODO Add the lemma `isStrictMap_piMap` once `MonoidHom.piMap` has been defined.
-
-end MonoidHom
+end Topology

Mathlib/Topology/Maps/Strict/Group.lean

@@ -0,0 +1,104 @@
+/-
+Copyright (c) 2026 Ziyan Wei. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ziyan Wei, Anatole Dedecker
+-/
+module
+
+public import Mathlib.GroupTheory.QuotientGroup.Basic
+public import Mathlib.Topology.Algebra.ContinuousMonoidHom
+public import Mathlib.Topology.Algebra.Group.Quotient
+public import Mathlib.Topology.Maps.Strict.Basic
+
+/-!
+# Strict Group Homomorphisms
+
+In this file, we study homomorphisms of topological groups which are *strict* in the sense
+of `Topology.IsStrictMap`.
+
+We provide specialized variations of general facts about `IsStrictMap` for convenience.
+But we also show that strict group homomorphisms enjoy some extra properties compared to general
+strict maps. Namely, we provide:
+* `isStrictMap_iff_isOpenQuotientMap_rangeRestrict`: `f` is a strict group homomorphism if
+  and only if the `rangeRestrict` of `f` is an *open* quotient map. This ultimately relies
+  on `MonoidHom.isOpenQuotientMap_of_isQuotientMap`.
+* `isStrictMap_prodMap`: The product (in the sense of `MonoidHom.prodMap`) of strict group
+  homomorphisms is strict. Note that this result is false for general maps; what makes things work
+  in our context is that, unlike `IsQuotientMap`, `IsOpenQuotientMap` is stable under product.
+-/
+
+@[expose] public section
+
+open Function Set Topology QuotientGroup
+
+namespace MonoidHom
+
+variable {G H G' H' : Type*} [Group G'] [Group H'] [Group G] [Group H] {f : G →* H} {g : G' →* H'}
+  [TopologicalSpace G] [TopologicalSpace H]
+
+/-- A group homomorphism is strict if and only if its `QuotientGroup.kerLift` is an embedding. -/
+@[to_additive /-- An additive group homomorphism is strict if and only if its
+`QuotientAddGroup.kerLift` is an embedding. -/]
+protected lemma isStrictMap_iff_isEmbedding_kerLift :
+    IsStrictMap f ↔ IsEmbedding (kerLift f) := by
+  -- Note: `G ⧸ MonoidHom.ker f` and `G ⧸ Setoid.ker f` are not definitionally equal, so
+  -- using `Topology.isStrictMap_iff_isEmbedding_kerLift` is too painful here.
+  simp_rw [isEmbedding_iff_isStrictMap_injective, kerLift_injective, and_true,
+    (isQuotientMap_mk _).isStrictMap_iff]
+  rfl
+
+/-- A group homomorphism is strict if and only if the canonical isomorphism
+`G ⧸ f.ker ≃ f.range` is a homeomorphism. -/
+@[to_additive /-- An additive group homomorphism is strict if and only if the canonical isomorphism
+`G ⧸ f.ker ≃ f.range` is a homeomorphism. -/]
+protected lemma isStrictMap_iff_isHomeomorph_quotientKerEquivRange :
+    IsStrictMap f ↔ IsHomeomorph (quotientKerEquivRange f) := by
+  -- Note: `G ⧸ MonoidHom.ker f` and `G ⧸ Setoid.ker f` are not definitionally equal, so
+  -- using `Topology.isStrictMap_iff_isHomeomorph_quotientKerEquivRange` is too painful here.
+  simp_rw [isHomeomorph_iff_isStrictMap_bijective, EquivLike.bijective, and_true,
+    (isQuotientMap_mk _).isStrictMap_iff, IsEmbedding.subtypeVal.isStrictMap_iff]
+  rfl
+
+/-- The isomorphism of topological groups `G ⧸ f.ker ≃ f.range` given by a strict group
+homomorphism `f`. This is an avatar of the first isomorphism theorem. -/
+@[to_additive /-- The isomorphism of topological additive groups `G ⧸ f.ker ≃ f.range` given by a
+strict additive group homomorphism `f`. This is an avatar of the first isomorphism theorem. -/]
+noncomputable def _root_.ContinuousMulEquiv.quotientKerEquivRange
+    (hf : IsStrictMap f) : G ⧸ f.ker ≃ₜ* f.range where
+  toMulEquiv := QuotientGroup.quotientKerEquivRange f
+  __ := (f.isStrictMap_iff_isHomeomorph_quotientKerEquivRange.mp hf).homeomorph
+
+variable [IsTopologicalGroup G]
+
+/-- A group homomorphism is strict if and only if its `rangeRestrict` is an open quotient map. -/
+@[to_additive /-- An additive group homomorphism is strict if and only if its `rangeRestrict` is an
+open quotient map. -/]
+protected lemma isStrictMap_iff_isOpenQuotientMap_rangeRestrict :
+    IsStrictMap f ↔ IsOpenQuotientMap f.rangeRestrict := by
+  rw [isOpenQuotientMap_iff_isQuotientMap]
+  rfl
+
+variable [TopologicalSpace G'] [IsTopologicalGroup G'] [TopologicalSpace H']
+
+/-- The product (in the sense of `Prod.map`) of group homomorphisms is strict if and only if each
+of the homomorphisms is strict. -/
+@[to_additive isStrictMap_prodMap_iff /-- The product (in the sense of `Prod.map`) of additive group
+homomorphisms is strict if and only if each of the homomorphisms is strict. -/]
+protected lemma isStrictMap_prodMap_iff :
+    IsStrictMap (f.prodMap g) ↔ IsStrictMap f ∧ IsStrictMap g := by
+  simp_rw [MonoidHom.isStrictMap_iff_isOpenQuotientMap_rangeRestrict]
+  let Φ : (f.prodMap g).range ≃ₜ f.range × g.range :=
+    (Homeomorph.setCongr (by simp [Subgroup.coe_prod])).trans (Homeomorph.Set.prod _ _)
+  have eq : Φ ∘ (f.prodMap g).rangeRestrict = f.rangeRestrict.prodMap g.rangeRestrict := rfl
+  rw [← Φ.comp_isOpenQuotientMap_iff, eq, MonoidHom.coe_prodMap, isOpenQuotientMap_prodMap_iff]
+
+/-- The product (in the sense of `Prod.map`) of strict group homomorphisms is strict. -/
+@[to_additive isStrictMap_prodMap /-- The product (in the sense of `Prod.map`) of strict additive
+group homomorphisms is strict. -/]
+protected lemma isStrictMap_prodMap (hf : IsStrictMap f)
+    (hg : IsStrictMap g) : IsStrictMap (f.prodMap g) :=
+  MonoidHom.isStrictMap_prodMap_iff.mpr ⟨hf, hg⟩
+
+-- TODO: Add the lemma `isStrictMap_piMap` once `MonoidHom.piMap` has been defined.
+
+end MonoidHom