∀ {R : Type u_1} {S : Type u_2} [τR : TopologicalSpace R] [τS : TopologicalSpace S] [inst : Ring R] [inst_1 : Ring S]
  {A : Type u_3} [inst_2 : AddCommGroup A] [inst_3 : Module R A] [inst_4 : TopologicalSpace A] [IsModuleTopology R A]
  {B' : Type u_5} [inst_6 : AddCommGroup B'] [inst_7 : Module S B'] [τB : TopologicalSpace B'] [IsModuleTopology S B']
  {σ : R →+* S}, IsOpenQuotientMap ⇑σ → ∀ (φ : A →ₛₗ[σ] B'), Function.Surjective ⇑φ → Topology.IsQuotientMap ⇑φ