[Merged by Bors] - feat(Topology/Algebra/Group/Matrix): refactor; continuity of maps on GL(n) and SL(n)

Mathlib/Analysis/Complex/Basic.lean

@@ -436,11 +436,13 @@ theorem isometry_intCast : Isometry ((↑) : ℤ → ℂ) :=
   Isometry.of_dist_eq <| by simp_rw [← Complex.ofReal_intCast,
     Complex.isometry_ofReal.dist_eq, Int.dist_cast_real, implies_true]
 
-theorem closedEmbedding_intCast : IsClosedEmbedding ((↑) : ℤ → ℂ) :=
+theorem isClosedEmbedding_intCast : IsClosedEmbedding ((↑) : ℤ → ℂ) :=
   isometry_intCast.isClosedEmbedding
 
+@[deprecated (since := "2026-04-15")] alias closedEmbedding_intCast := isClosedEmbedding_intCast
+
 lemma isClosed_range_intCast : IsClosed (Set.range ((↑) : ℤ → ℂ)) :=
-  Complex.closedEmbedding_intCast.isClosed_range
+  Complex.isClosedEmbedding_intCast.isClosed_range
 
 lemma isOpen_compl_range_intCast : IsOpen (Set.range ((↑) : ℤ → ℂ))ᶜ :=
   Complex.isClosed_range_intCast.isOpen_compl

Mathlib/Analysis/Normed/Group/Uniform.lean

@@ -468,3 +468,20 @@ theorem LipschitzWith.norm_div_le_of_le {f : E → F} {C : ℝ≥0} {a b : E} {r
   (h.norm_div_le _ _).trans <| by gcongr
 
 end SeminormedCommGroup
+
+namespace Real
+open Topology
+
+theorem isometry_intCast : Isometry ((↑) : ℤ → ℝ) :=
+  Isometry.of_dist_eq <| by tauto
+
+theorem isClosedEmbedding_intCast : IsClosedEmbedding ((↑) : ℤ → ℝ) :=
+  isometry_intCast.isClosedEmbedding
+
+lemma isClosed_range_intCast : IsClosed (Set.range ((↑) : ℤ → ℝ)) :=
+  isClosedEmbedding_intCast.isClosed_range
+
+lemma isOpen_compl_range_intCast : IsOpen (Set.range ((↑) : ℤ → ℝ))ᶜ :=
+  Real.isClosed_range_intCast.isOpen_compl
+
+end Real

Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean

@@ -132,7 +132,7 @@ lemma HasProdUniformlyOn_sineTerm_prod_on_compact (hZ2 : Z ⊆ ℂ_ℤ)
 lemma HasProdLocallyUniformlyOn_euler_sin_prod :
     HasProdLocallyUniformlyOn (fun n : ℕ => fun z : ℂ => (1 + sineTerm z n))
     (fun x => (Complex.sin (π * x) / (π * x))) ℂ_ℤ := by
-  apply hasProdLocallyUniformlyOn_of_forall_compact isOpen_compl_range_intCast
+  apply hasProdLocallyUniformlyOn_of_forall_compact Complex.isOpen_compl_range_intCast
   exact fun _ hZ hZC => HasProdUniformlyOn_sineTerm_prod_on_compact hZ hZC
 
 /-- `sin π z` is non vanishing on the complement of the integers in `ℂ`. -/
@@ -270,7 +270,7 @@ lemma eqOn_iteratedDerivWithin_cotTerm_integerComplement (d : ℕ) :
       (iteratedDerivWithin k (fun z ↦ cotTerm z d) ℂ_ℤ)
       (fun z ↦ (-1) ^ k * k ! * ((z + (d + 1)) ^ (-1 - k : ℤ) + (z - (d + 1)) ^ (-1 - k : ℤ)))
       ℂ_ℤ := by
-  apply Set.EqOn.trans (iteratedDerivWithin_of_isOpen isOpen_compl_range_intCast)
+  apply Set.EqOn.trans (iteratedDerivWithin_of_isOpen Complex.isOpen_compl_range_intCast)
   exact eqOn_iteratedDeriv_cotTerm ..
 
 lemma eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet (d : ℕ) :

Mathlib/Topology/Algebra/Constructions.lean

@@ -178,4 +178,18 @@ lemma isOpenMap_map {f : M →* N} (hf_inj : Function.Injective f) (hf : IsOpenM
     fun ⟨x, hxV, hx⟩ ↦ ⟨x, x.inv, by simp [hxV, ← hx]⟩⟩
   all_goals simp_all
 
+@[to_additive]
+lemma _root_.Topology.IsInducing.units_map {f : M →* N} (hf : IsInducing f) :
+    IsInducing (map f) := by
+  refine .of_comp (continuous_map hf.continuous) continuous_embedProduct ?_
+  exact hf.prodMap (opHomeomorph.isInducing.comp <| hf.comp opHomeomorph.symm.isInducing)
+    |>.comp isInducing_embedProduct
+
+@[to_additive]
+lemma _root_.Topology.IsEmbedding.units_map {f : M →* N} (hf : IsEmbedding f) :
+    IsEmbedding (map f) := by
+  refine .of_comp (continuous_map hf.continuous) continuous_embedProduct ?_
+  exact hf.prodMap (opHomeomorph.isEmbedding.comp <| hf.comp opHomeomorph.symm.isEmbedding)
+    |>.comp isEmbedding_embedProduct
+
 end Units

Mathlib/Topology/Algebra/Group/Basic.lean

@@ -1335,6 +1335,12 @@ theorem isClosedEmbedding_embedProduct [T1Space α] [ContinuousMul α] :
     refine .inter (isClosed_singleton.preimage ?_) (isClosed_singleton.preimage ?_) <;>
     fun_prop
 
+lemma _root_.Topology.IsClosedEmbedding.units_map [ContinuousMul α] [T1Space α] {f : α →* β}
+    (hf : IsClosedEmbedding f) : IsClosedEmbedding (map f) := by
+  refine .of_comp isEmbedding_embedProduct ?_
+  exact (hf.prodMap (opHomeomorph.isClosedEmbedding.comp
+    <| hf.comp opHomeomorph.symm.isClosedEmbedding)).comp isClosedEmbedding_embedProduct
+
 @[to_additive]
 instance [T1Space α] [ContinuousMul α] [CompactSpace α] : CompactSpace αˣ :=
   isClosedEmbedding_embedProduct.compactSpace

Mathlib/Topology/Algebra/Group/Matrix.lean

@@ -7,6 +7,7 @@ Authors: David Loeffler
 module
 
 public import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
+public import Mathlib.Topology.Algebra.Algebra
 public import Mathlib.Topology.Algebra.Group.Pointwise
 public import Mathlib.Topology.Instances.Matrix
 
@@ -19,25 +20,42 @@ topological ring `R`.
 
 @[expose] public section
 
-open Matrix
+open Matrix Topology
 
-variable {n R : Type*}
+variable {n R S : Type*} [Fintype n] [DecidableEq n]
+  [CommRing R] [TopologicalSpace R] [CommRing S] [TopologicalSpace S] {f : R →+* S}
 
-/-! ### Lemmas about matrix groups -/
-
-section MatrixGroups
-
-variable [Fintype n] [DecidableEq n] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
+/-!
+### Topology of the general linear group
+-/
 
 namespace Matrix.GeneralLinearGroup
 
-omit [IsTopologicalRing R] in
 @[fun_prop]
 theorem continuous_apply {α : Type*} [TopologicalSpace α]
     (f : α → GL n R) (hf : Continuous f) (i : n) :
     Continuous (fun x ↦ f x i) :=
   (by fun_prop : Continuous fun A : Matrix n n R ↦ A i).comp <| by fun_prop
 
+@[fun_prop]
+lemma _root_.Continuous.generalLinearGroup_map (hf : Continuous f) :
+    Continuous (map (n := n) f) :=
+  (continuous_id.matrix_map hf).units_map
+
+lemma _root_.Topology.IsInducing.generalLinearGroup_map (hf : IsInducing f) :
+    IsInducing (map (n := n) f) :=
+  hf.matrix_map.units_map
+
+lemma _root_.Topology.IsEmbedding.generalLinearGroup_map (hf : IsEmbedding f) :
+    IsEmbedding (map (n := n) f) :=
+  hf.matrix_map.units_map
+
+variable [IsTopologicalRing R]
+
+lemma _root_.Topology.IsClosedEmbedding.generalLinearGroup_map [T0Space R]
+    (hf : IsClosedEmbedding f) : IsClosedEmbedding (map (n := n) f) :=
+  hf.matrix_map.units_map
+
 /-- The determinant is continuous as a map from the general linear group to the units. -/
 @[continuity, fun_prop] protected lemma continuous_det :
     Continuous (det : GL n R → Rˣ) := by
@@ -55,52 +73,79 @@ lemma continuous_upperRightHom {R : Type*} [Ring R] [TopologicalSpace R] [IsTopo
 
 end Matrix.GeneralLinearGroup
 
+/-!
+### Topology of the special linear group
+-/
 namespace Matrix.SpecialLinearGroup
 
 local notation "SL" => SpecialLinearGroup
 
-omit [IsTopologicalRing R] in
 instance : TopologicalSpace (SL n R) :=
   inferInstanceAs <| TopologicalSpace (Subtype _)
 
-omit [IsTopologicalRing R] in
 @[fun_prop]
 theorem continuous_apply {α : Type*} [TopologicalSpace α]
     (f : α → SL n R) (hf : Continuous f) (i) :
     Continuous (fun x ↦ f x i) :=
   (by fun_prop : Continuous fun A : Matrix n n R ↦ A i).comp <| by fun_prop
 
+/-- The topology on `SL n R` is functorial in `R`. -/
+@[fun_prop]
+lemma _root_.Continuous.specialLinearGroup_map (hf : Continuous f) :
+    Continuous (map (n := n) f) := by
+  refine IsInducing.subtypeVal.continuous_iff.mpr ?_
+  exact (continuous_id.matrix_map hf).comp continuous_subtype_val
+
+lemma _root_.Topology.IsInducing.specialLinearGroup_map (hf : IsInducing f) :
+    IsInducing (map (n := n) f) :=
+  (hf.matrix_map.comp .subtypeVal).of_comp (by fun_prop) continuous_subtype_val
+
+lemma _root_.Topology.IsEmbedding.specialLinearGroup_map (hf : IsEmbedding f) :
+    IsEmbedding (map (n := n) f) :=
+  (hf.matrix_map.comp .subtypeVal).of_comp (by fun_prop) continuous_subtype_val
+
+variable [IsTopologicalRing R]
+
 /-- If `R` is a commutative ring with the discrete topology, then `SL(n, R)` has the discrete
 topology. -/
 instance [DiscreteTopology R] : DiscreteTopology (SL n R) :=
   inferInstanceAs <| DiscreteTopology (Subtype _)
 
 lemma isClosedEmbedding_val [T1Space R] :
-    Topology.IsClosedEmbedding ((↑) : SL n R → Matrix n n R) :=
+    IsClosedEmbedding ((↑) : SL n R → Matrix n n R) :=
   (isClosed_singleton.preimage continuous_id.matrix_det).isClosedEmbedding_subtypeVal
 
-set_option backward.isDefEq.respectTransparency false in
+lemma _root_.Topology.IsClosedEmbedding.specialLinearGroup_map [T1Space R]
+    (hf : IsClosedEmbedding f) : IsClosedEmbedding (map (n := n) f) :=
+  (hf.matrix_map.comp isClosedEmbedding_val).of_comp .subtypeVal
+
+instance instT1Space [T1Space R] : T1Space (SL n R) := isClosedEmbedding_val.isEmbedding.t1Space
+
 /-- The special linear group over a topological ring is a topological group. -/
 instance topologicalGroup : IsTopologicalGroup (SL n R) where
-  continuous_inv := by simpa [continuous_induced_rng] using continuous_induced_dom.matrix_adjugate
-  continuous_mul := by simpa only [continuous_induced_rng] using
+  continuous_inv := continuous_induced_rng.mpr continuous_induced_dom.matrix_adjugate
+  continuous_mul := continuous_induced_rng.mpr <|
     (continuous_induced_dom.comp continuous_fst).mul (continuous_induced_dom.comp continuous_snd)
 
-section toGL -- results on the map from `SL` to `GL`
+/-!
+### Mapping `SL(n, R)` to `GL(n, R)`
+-/
+section toGL
 
 /-- The natural map from `SL n A` to `GL n A` is continuous. -/
+@[fun_prop]
 lemma continuous_toGL : Continuous (toGL : SL n R → GL n R) := by
   simp_rw [Units.continuous_iff, ← map_inv]
   constructor <;> fun_prop
 
 /-- The natural map from `SL n A` to `GL n A` is inducing, i.e. the topology on
 `SL n A` is the pullback of the topology from `GL n A`. -/
-lemma isInducing_toGL : Topology.IsInducing (toGL : SL n R → GL n R) :=
-  .of_comp continuous_toGL Units.continuous_val (Topology.IsInducing.induced _)
+lemma isInducing_toGL : IsInducing (toGL : SL n R → GL n R) :=
+  .of_comp continuous_toGL Units.continuous_val (IsInducing.induced _)
 
 /-- The natural map from `SL n A` in `GL n A` is an embedding, i.e. it is an injection and
 the topology on `SL n A` coincides with the subspace topology from `GL n A`. -/
-lemma isEmbedding_toGL : Topology.IsEmbedding (toGL : SL n R → GL n R) :=
+lemma isEmbedding_toGL : IsEmbedding (toGL : SL n R → GL n R) :=
   ⟨isInducing_toGL, toGL_injective⟩
 
 theorem range_toGL {A : Type*} [CommRing A] :
@@ -109,33 +154,39 @@ theorem range_toGL {A : Type*} [CommRing A] :
   simpa [Units.ext_iff] using ⟨fun ⟨y, hy⟩ ↦ by simp [← hy], fun hx ↦ ⟨⟨x, hx⟩, rfl⟩⟩
 
 /-- The natural inclusion of `SL n A` in `GL n A` is a closed embedding. -/
-lemma isClosedEmbedding_toGL [T0Space R] : Topology.IsClosedEmbedding (toGL : SL n R → GL n R) :=
+lemma isClosedEmbedding_toGL [T0Space R] : IsClosedEmbedding (toGL : SL n R → GL n R) :=
   ⟨isEmbedding_toGL, by simpa [range_toGL] using isClosed_singleton.preimage <| by fun_prop⟩
 
 end toGL
 
 section mapGL
 
-variable {n : Type*} [Fintype n] [DecidableEq n]
-  {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
-  [TopologicalSpace A] [TopologicalSpace B] [IsTopologicalRing B]
+/-!
+### Shortcuts for the composite `SL(n, R) → GL(n, S)`
+-/
+variable [Algebra R S] [IsTopologicalRing S]
+
+omit [IsTopologicalRing R]
+
+lemma continuous_mapGL [ContinuousSMul R S] : Continuous (mapGL S : SL n R → _) :=
+  continuous_toGL.comp
+    (continuous_algebraMap_iff_smul R S |>.2 continuous_smul).specialLinearGroup_map
+
+lemma isInducing_mapGL (h : IsInducing (algebraMap R S)) :
+    IsInducing (mapGL S : SL n R → _) :=
+  isInducing_toGL.comp h.specialLinearGroup_map
 
-set_option backward.isDefEq.respectTransparency false in
-lemma isInducing_mapGL (h : Topology.IsInducing (algebraMap A B)) :
-    Topology.IsInducing (mapGL B : SL n A → GL n B) := by
-  -- TODO: add `IsInducing.units_map` and deduce `IsInducing.generalLinearGroup_map`
-  refine isInducing_toGL.comp ?_
-  refine .of_comp ?_ continuous_induced_dom (h.matrix_map.comp (Topology.IsInducing.induced _))
-  rw [continuous_induced_rng]
-  exact continuous_subtype_val.matrix_map h.continuous
+lemma isEmbedding_mapGL (h : IsEmbedding (algebraMap R S)) :
+    IsEmbedding (mapGL S : SL n R → _) :=
+  isEmbedding_toGL.comp h.specialLinearGroup_map
 
-lemma isEmbedding_mapGL (h : Topology.IsEmbedding (algebraMap A B)) :
-    Topology.IsEmbedding (mapGL B : SL n A → GL n B) :=
-  haveI : FaithfulSMul A B := (faithfulSMul_iff_algebraMap_injective _ _).mpr h.2
-  ⟨isInducing_mapGL h.isInducing, mapGL_injective⟩
+lemma isClosedEmbedding_mapGL [IsTopologicalRing R] [T1Space R] [T1Space S]
+    (h : IsClosedEmbedding (algebraMap R S)) :
+    IsClosedEmbedding (mapGL S : SL n R → _) :=
+  isClosedEmbedding_toGL.comp h.specialLinearGroup_map
 
 end mapGL
 
 end Matrix.SpecialLinearGroup
 
-end MatrixGroups
+end

Mathlib/Topology/Constructions/SumProd.lean

@@ -593,6 +593,12 @@ protected lemma Topology.IsOpenEmbedding.prodMap {f : X → Y} {g : Z → W} (hf
     (hg : IsOpenEmbedding g) : IsOpenEmbedding (Prod.map f g) :=
   .of_isEmbedding_isOpenMap (hf.1.prodMap hg.1) (hf.isOpenMap.prodMap hg.isOpenMap)
 
+protected lemma Topology.IsClosedEmbedding.prodMap {f : X → Y} {g : Z → W}
+    (hf : IsClosedEmbedding f) (hg : IsClosedEmbedding g) :
+    IsClosedEmbedding (Prod.map f g) :=
+  { hf.isEmbedding.prodMap hg.isEmbedding with
+    isClosed_range := range_prodMap ▸ hf.isClosed_range.prod hg.isClosed_range }
+
 lemma isEmbedding_graph {f : X → Y} (hf : Continuous f) : IsEmbedding fun x => (x, f x) :=
   .of_comp (continuous_id.prodMk hf) continuous_fst .id
 

Mathlib/Topology/Maps/Basic.lean

@@ -226,6 +226,7 @@ lemma tendsto_nhds_iff {f : ι → Y} {l : Filter ι} {y : Y} (hg : IsEmbedding
 lemma continuous_iff (hg : IsEmbedding g) : Continuous f ↔ Continuous (g ∘ f) :=
   hg.isInducing.continuous_iff
 
+@[fun_prop]
 lemma continuous (hf : IsEmbedding f) : Continuous f := hf.isInducing.continuous
 
 lemma closure_eq_preimage_closure_image (hf : IsEmbedding f) (s : Set X) :