∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {T : Type u_3} [inst_2 : CommRing T]
  [inst_3 : Algebra R T] [inst_4 : Algebra R S],
  (algebraMap R T).SurjectiveOnStalks → (algebraMap S (TensorProduct R S T)).SurjectiveOnStalks