feat: API and proof of isStrictMap_prodMap (#38937)

Co-authored-by: Oliver Nash <github@olivernash.org>
Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Co-authored-by: ADedecker <anatolededecker@gmail.com>
Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>

Author: 5 people

Mathlib/Topology/Algebra/Group/Basic.lean

@@ -914,6 +914,13 @@ lemma MonoidHom.isOpenQuotientMap_of_isQuotientMap {A : Type*} [Group A]
         use x * k, hx
         rw [map_mul, hk, mul_one]
 
+@[to_additive]
+lemma MonoidHom.isOpenQuotientMap_iff_isQuotientMap {A : Type*} [Group A]
+    [TopologicalSpace A] [ContinuousMul A] {B : Type*} [Group B] [TopologicalSpace B]
+    {F : Type*} [FunLike F A B] [MonoidHomClass F A B] {φ : F} :
+    IsOpenQuotientMap φ ↔ IsQuotientMap φ :=
+  ⟨fun hf => hf.isQuotientMap, MonoidHom.isOpenQuotientMap_of_isQuotientMap⟩
+
 @[to_additive]
 theorem IsTopologicalGroup.ext {G : Type*} [Group G] {t t' : TopologicalSpace G}
     (tg : @IsTopologicalGroup G t _) (tg' : @IsTopologicalGroup G t' _)

Mathlib/Topology/Maps/Strict/Basic.lean

@@ -9,6 +9,8 @@ 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
 
@@ -33,6 +35,18 @@ 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
@@ -153,4 +167,39 @@ lemma isEmbedding_iff_isStrictMap_injective :
     (Homeomorph.Quotient.congrRight <| by simp [f_inj.eq_iff]).trans Homeomorph.quotientBot
   exact f_strict.comp Φ.symm.isEmbedding
 
+/-- Strict maps are preserved when precomposing with a homeomorphism. -/
+lemma Homeomorph.isStrictMap_comp_iff (e : X ≃ₜ Y) {f : Y → Z} :
+    IsStrictMap (f ∘ e) ↔ IsStrictMap f :=
+  e.isQuotientMap.isStrictMap_iff.symm
+
+/-- Strict maps are preserved when postcomposing with a homeomorphism. -/
+lemma 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']
+
+/-- 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) := by
+  rw [isStrictMap_iff_isOpenQuotientMap_rangeRestrict] at hf hg ⊢
+  let aux : (f.prodMap g).range ≃ₜ f.range × g.range :=
+    (Homeomorph.setCongr (by simp [Subgroup.coe_prod])).trans (Homeomorph.Set.prod _ _)
+  exact aux.symm.isOpenQuotientMap.comp (hf.prodMap hg)
+
+-- TODO Add the lemma `isStrictMap_piMap` once `MonoidHom.piMap` has been defined.
+
+end MonoidHom