Proposition 31, p. 26 — monos and epis in DSpace are the injective and surjective maps
ProvedConcreteSheaves.Quasitopos.proposition_31Let be a small category with a coverage and a terminal object (written in the paper), and suppose is a concrete site: representables are sheaves, is faithful, and covering families are jointly surjective on points. Write for the underlying set of a presheaf and , , for the underlying function of a plot .
For every map of spaces, with underlying function ,
This identifies the monomorphisms and epimorphisms of concretely and is used to analyse strong monomorphisms.
Formalization Note The site is small ( in universe , presheaves valued in ), covering families are presieves, and the terminal domain is passed explicitly as . Mono and epi are taken in the category of spaces (a full subcategory of presheaves); is the component of the natural transformation at .
import Mathlib import Definitions.Def_ConcreteSheaves_Quasitopos_Setting
namespace ConcreteSheaves.Quasitopos
open CategoryTheory CategoryTheory.Limits Opposite
universe u
variable {D : Type u} [SmallCategory D]
/-- Baez–Hoffnung, Proposition 31, p. 26. -/
theorem proposition_31 (K : Coverage D) (T : D) (hT : IsTerminal T)
(hK : IsConcreteSite K T hT) {X Y : DSpace K T} (f : X ⟶ Y) :
(Mono f ↔ Function.Injective (f.hom.app (op T))) ∧
(Epi f ↔ Function.Surjective (f.hom.app (op T))) := by sorry
end ConcreteSheaves.Quasitopos
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.