English
If CompHausLike P has explicit pullbacks and every effective epimorphism f is surjective on the underlying functions, then CompHausLike P is preregular.
Русский
Если у Cateгории CompHausLike P есть явные вычислимые пуллбэки, и любая эффективная эпиморфизм f действует как сюръекция на базовых отображениях, тогда CompHausLike P является пререгулярной.
LaTeX
$$$[\\text{HasExplicitPullbacks } P]\\;\\&\\; (\\forall X,Y,f:X\\to Y,\\ \\text{EffectiveEpi}(f) \\Rightarrow \\operatorname{Surjective}(\\underline{f})) \\Rightarrow \\mathrm{Preregular}(\\mathrm{CompHausLike} P)$$$
Lean4
theorem preregular [HasExplicitPullbacks P]
(hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective f) : Preregular (CompHausLike P)
where
exists_fac := by
intro X Y Z f π hπ
refine
⟨pullback f π, pullback.fst f π, ⟨⟨effectiveEpiStruct _ ?_⟩⟩, pullback.snd f π, (pullback.condition _ _).symm⟩
intro y
obtain ⟨z, hz⟩ := hs π hπ (f y)
exact ⟨⟨(y, z), hz.symm⟩, rfl⟩
