Documentation

Mathlib.Algebra.Category.Ring.Epi

Epimorphisms in CommRingCat #

Main results #

source
📐 coverage
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
source
📐 coverage
@[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.

source
📐 coverage
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)
source
📐 coverage
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