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 (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₂ : (CommRingCat.Hom.hom f).Finite) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)

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