Epimorphisms in CommRingCat

Main results

• RingHom.surjective_iff_epi_and_finite: surjective <=> epi + finite

theorem CommRingCat.epi_iff_tmul_eq_tmul {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] : CategoryTheory.Epi (CommRingCat.ofHom (algebraMap R S)) ↔ ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s

theorem RingHom.surjective_of_epi_of_finite {R S : CommRingCat} (f : R ⟶ S) [CategoryTheory.Epi f] (h₂ : RingHom.Finite f) : Function.Surjective ⇑f

theorem RingHom.surjective_iff_epi_and_finite {R S : CommRingCat} {f : R ⟶ S} : Function.Surjective ⇑f ↔ CategoryTheory.Epi f ∧ RingHom.Finite f