English
In LightProfinite, a morphism f is epi if and only if its underlying map is surjective.
Русский
В LightProfinite морфизм f является эпиморфизмом тогда и только тогда, когда соответствующая карта по значению изображения сюръективна.
LaTeX
$$$\text{Epi } f \Leftrightarrow \text{Surjective}(f)$$$
Lean4
theorem epi_iff_surjective {X Y : LightProfinite.{u}} (f : X ⟶ Y) : Epi f ↔ Function.Surjective f :=
by
constructor
· -- Note: in mathlib3 `contrapose` saw through `Function.Surjective`.
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 := CompHausLike.ofHom _ ⟨(LocallyConstant.ofIsClopen hV).map ULift.up, LocallyConstant.continuous _⟩
let h : Y ⟶ Z := CompHausLike.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, 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 LightProfinite).epi_of_epi_map
