Epimorphisms in CommRingCat

Main results

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

theorem CommRingCat.epi_iff_epi {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] : CategoryTheory.Epi (ofHom (algebraMap R S)) ↔ Algebra.IsEpi R S

@[deprecated CommRingCat.epi_iff_epi (since := "2026-01-13")]

theorem CommRingCat.epi_iff_tmul_eq_tmul {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] : CategoryTheory.Epi (ofHom (algebraMap R S)) ↔ Algebra.IsEpi R S

Alias of CommRingCat.epi_iff_epi.

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