English
In Stonean, a morphism is an epi if and only if it is surjective.
Русский
В категории Stonean морфизм является эпиморфизмом тогда и только тогда, когда он сюръективен.
LaTeX
$$$\mathrm{Epi}(f) \iff \operatorname{Surjective}(f)$$$
Lean4
/-- A morphism in `Stonean` is an epi iff it is surjective.
-/
theorem epi_iff_surjective {X Y : Stonean} (f : X ⟶ Y) : Epi f ↔ Function.Surjective f :=
by
refine ⟨?_, fun h => ConcreteCategory.epi_of_surjective f h⟩
dsimp [Function.Surjective]
intro h y
by_contra! hy
let C := Set.range f
have hC : IsClosed C := (isCompact_range f.hom.continuous).isClosed
let U := Cᶜ
have hUy : U ∈ 𝓝 y := by simp only [U, C, Set.mem_range, hy, exists_false, not_false_eq_true, hC.compl_mem_nhds]
obtain ⟨V, hV, hyV, hVU⟩ := isTopologicalBasis_isClopen.mem_nhds_iff.mp hUy
classical
let g : Y ⟶ mkFinite (ULift (Fin 2)) :=
TopCat.ofHom ⟨(LocallyConstant.ofIsClopen hV).map ULift.up, LocallyConstant.continuous _⟩
let h : Y ⟶ mkFinite (ULift (Fin 2)) := TopCat.ofHom ⟨fun _ => ⟨1⟩, continuous_const⟩
have H : h = g := by
rw [← cancel_epi f]
ext x
apply ULift.ext
change
1 =
ite _ _
_ -- why is `dsimp` not getting me here?
rw [if_neg]
refine
mt (hVU ·)
?_ -- what would be an idiomatic tactic for this step?
simpa only [U, Set.mem_compl_iff, Set.mem_range, not_exists, not_forall, not_not] using exists_apply_eq_apply f x
apply_fun fun e => (e y).down at H
change 1 = ite _ _ _ at H
rw [if_pos hyV] at H
exact one_ne_zero H
