English
In TopCat, effective epimorphisms are exactly quotient maps. If π: X ⟶ B is effective epi, then π is a quotient map, and conversely.
Русский
В TopCat эффективные эпиморфизмы совпадают с кратными отображениями (квотиентами).
LaTeX
$$$\\mathrm{EffectiveEpi}(\\pi) \\iff \\mathrm{IsQuotientMap}(\\pi)$$$
Lean4
/-- The effective epimorphisms in `TopCat` are precisely the quotient maps. -/
theorem effectiveEpi_iff_isQuotientMap {B X : TopCat.{u}} (π : X ⟶ B) : EffectiveEpi π ↔ IsQuotientMap π := by
/- The backward direction is given by `effectiveEpiStructOfQuotientMap` above. -/
refine
⟨fun _ ↦ ?_, fun hπ ↦ ⟨⟨effectiveEpiStructOfQuotientMap π hπ⟩⟩⟩
/- Since `TopCat` has pullbacks, `π` is in fact a `RegularEpi`. This means that it exhibits `B` as
a coequalizer of two maps into `X`. It suffices to prove that `π` followed by the isomorphism to
an arbitrary coequalizer is a quotient map. -/
have hπ : RegularEpi π := inferInstance
exact isQuotientMap_of_isColimit_cofork _ hπ.isColimit
