English
A morphism between profinite spaces is an epimorphism in Profinite if and only if the underlying function is surjective.
Русский
Гомоморфизм между профинидальными пространствами является эпиморфизмом в Profinite тогда и только тогда, когда соответствующая функция сюръективна.
LaTeX
$$$\\forall X,Y\\in \\mathrm{Profinite},\\forall f:X\\to Y,\\ \\mathrm{Epi}(f)\\iff \\mathrm{Surjective}(f).$$$
Lean4
theorem epi_iff_surjective {X Y : Profinite.{u}} (f : X ⟶ Y) : Epi f ↔ Function.Surjective f :=
by
constructor
· dsimp [Function.Surjective]
contrapose!
rintro ⟨y, hy⟩ hf
let C := Set.range f
have hC : IsClosed C := (isCompact_range f.hom.continuous).isClosed
let U := Cᶜ
have hyU : y ∈ U := by
refine Set.mem_compl ?_
rintro ⟨y', hy'⟩
exact hy y' hy'
have hUy : U ∈ 𝓝 y := hC.compl_mem_nhds hyU
obtain ⟨V, hV, hyV, hVU⟩ := isTopologicalBasis_isClopen.mem_nhds_iff.mp hUy
classical
let Z := of (ULift.{u} <| Fin 2)
let g : Y ⟶ Z := ofHom _ ⟨(LocallyConstant.ofIsClopen hV).map ULift.up, LocallyConstant.continuous _⟩
let h : Y ⟶ Z := ofHom _ ⟨fun _ => ⟨1⟩, continuous_const⟩
have H : h = g := by
rw [← cancel_epi f]
ext x
dsimp [g, LocallyConstant.ofIsClopen]
rw [ContinuousMap.coe_mk, ContinuousMap.coe_mk, ConcreteCategory.hom_ofHom, ContinuousMap.coe_mk,
Function.comp_apply, if_neg]
refine mt (fun α => hVU α) ?_
simp [U, C]
apply_fun fun e => (e y).down at H
dsimp [g, LocallyConstant.ofIsClopen] at H
rw [ContinuousMap.coe_mk, ContinuousMap.coe_mk, Function.comp_apply, if_pos hyV] at H
exact top_ne_bot H
· rw [← CategoryTheory.epi_iff_surjective]
apply (forget Profinite).epi_of_epi_map
