feat(SeparationQuotient): add missing instances

Mathlib/Topology/Algebra/SeparationQuotient.lean

@@ -3,8 +3,9 @@ Copyright (c) 2024 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Topology.Algebra.Module.Basic
 import Mathlib.LinearAlgebra.Basis.VectorSpace
+import Mathlib.Topology.Algebra.Module.Basic
+import Mathlib.Topology.Maps.OpenQuotient
 
 /-!
 # Algebraic operations on `SeparationQuotient`
@@ -63,6 +64,12 @@ instance instIsScalarTower [SMul M N] [ContinuousConstSMul N X] [IsScalarTower M
 
 end SMul
 
+instance instContinuousSMul {M X : Type*} [SMul M X] [TopologicalSpace M] [TopologicalSpace X]
+    [ContinuousSMul M X] : ContinuousSMul M (SeparationQuotient X) where
+  continuous_smul := by
+    rw [(IsOpenQuotientMap.id.prodMap isOpenQuotientMap_mk).quotientMap.continuous_iff]
+    exact continuous_mk.comp continuous_smul
+
 instance instSMulZeroClass {M X : Type*} [Zero X] [SMulZeroClass M X] [TopologicalSpace X]
     [ContinuousConstSMul M X] : SMulZeroClass M (SeparationQuotient X) :=
   ZeroHom.smulZeroClass ⟨mk, mk_zero⟩ mk_smul
@@ -190,6 +197,17 @@ instance instCommGroup [CommGroup G] [TopologicalGroup G] : CommGroup (Separatio
 
 end Group
 
+section UniformGroup
+
+@[to_additive]
+instance instUniformGroup {G : Type*} [Group G] [UniformSpace G] [UniformGroup G] :
+    UniformGroup (SeparationQuotient G) where
+  uniformContinuous_div := by
+    rw [uniformContinuous_dom₂]
+    exact uniformContinuous_mk.comp uniformContinuous_div
+
+end UniformGroup
+
 section MonoidWithZero
 
 variable {M₀ : Type*} [TopologicalSpace M₀]
@@ -391,6 +409,14 @@ theorem mk_outCLM (x : SeparationQuotient E) : mk (outCLM K E x) = x :=
 @[simp]
 theorem mk_comp_outCLM : mk ∘ outCLM K E = id := funext (mk_outCLM K)
 
+variable {K} in
+theorem postcomp_mkCLM_surjective {L : Type*} [Semiring L] (σ : L →+* K)
+    (F : Type*) [AddCommMonoid F] [Module L F] [TopologicalSpace F] :
+    Function.Surjective ((mkCLM K E).comp : (F →SL[σ] E) → (F →SL[σ] SeparationQuotient E)) := by
+  intro f
+  use (outCLM K E).comp f
+  rw [← ContinuousLinearMap.comp_assoc, mkCLM_comp_outCLM, ContinuousLinearMap.id_comp]
+
 /-- The `SeparationQuotient.outCLM K E` map is a topological embedding. -/
 theorem outCLM_embedding : Embedding (outCLM K E) :=
   Function.LeftInverse.embedding (mk_outCLM K) continuous_mk (map_continuous _)

Mathlib/Topology/Inseparable.lean

@@ -548,6 +548,9 @@ theorem preimage_image_mk_open (hs : IsOpen s) : mk ⁻¹' (mk '' s) = s := by
 theorem isOpenMap_mk : IsOpenMap (mk : X → SeparationQuotient X) := fun s hs =>
   quotientMap_mk.isOpen_preimage.1 <| by rwa [preimage_image_mk_open hs]
 
+theorem isOpenQuotientMap_mk : IsOpenQuotientMap (mk : X → SeparationQuotient X) :=
+  ⟨surjective_mk, continuous_mk, isOpenMap_mk⟩
+
 theorem preimage_image_mk_closed (hs : IsClosed s) : mk ⁻¹' (mk '' s) = s := by
   refine Subset.antisymm ?_ (subset_preimage_image _ _)
   rintro x ⟨y, hys, hxy⟩