English
If CompHausLike P has explicit pullbacks and explicit finite coproducts, and surjectivity holds for effective epis, then CompHausLike P is precoherent.
Русский
Если у CompHausLike P есть явные пулбэки и явные конечные копроизведения, и верна сюръективность для эффективных эпиморфизмов, то CompHausLike P является прецерогерентной.
LaTeX
$$$[HasExplicitPullbacks P] \\;[HasExplicitFiniteCoproducts P] \\; (\\forall X,Y,f, \\ \\text{EffectiveEpi}(f) \\Rightarrow \\operatorname{Surjective}(\\underline{f})) \\Rightarrow \\mathrm{Precoherent}(\\mathrm{CompHausLike} P)$$$
Lean4
theorem precoherent [HasExplicitPullbacks P] [HasExplicitFiniteCoproducts.{0} P]
(hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective f) :
Precoherent (CompHausLike P) :=
by
have : Preregular (CompHausLike P) := preregular hs
infer_instance
