English
If α is finite and nonempty, any locally constant map from the limit to α factors through a stage as above.
Русский
Если α конечна и непустая, локально константное отображение из предела в α факторизуется через некоторый этап диаграммы.
LaTeX
$$$\\forall α\\,[\\text{Finite }α],\\,[\\text{Nonempty }α],\\ (hC):IsLimit C\\Rightarrow \\exists j,\\exists g:\\mathrm{LocallyConstant}(F(j),α),\\ f= g\\circ (C.\\pi.app j).hom$$$
Lean4
theorem exists_locallyConstant_finite_nonempty {α : Type*} [Finite α] [Nonempty α] (hC : IsLimit C)
(f : LocallyConstant C.pt α) : ∃ (j : J) (g : LocallyConstant (F.obj j) α), f = g.comap (C.π.app _).hom :=
by
inhabit α
obtain ⟨j, gg, h⟩ := exists_locallyConstant_finite_aux _ hC f
classical
let ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
let σ : (α → Fin 2) → α := fun f => if h : ∃ a : α, ι a = f then h.choose else default
refine ⟨j, gg.map σ, ?_⟩
ext x
simp only [Functor.const_obj_obj, LocallyConstant.coe_comap, LocallyConstant.map_apply, Function.comp_apply]
dsimp [σ]
have h1 : ι (f x) = gg (C.π.app j x) :=
by
change f.map (fun a b => if a = b then (0 : Fin 2) else 1) x = _
rw [h]
rfl
have h2 : ∃ a : α, ι a = gg (C.π.app j x) := ⟨f x, h1⟩
rw [dif_pos]
swap
· assumption
apply_fun ι
· rw [h2.choose_spec]
exact h1
· intro a b hh
have hhh := congr_fun hh a
dsimp [ι] at hhh
rw [if_pos rfl] at hhh
split_ifs at hhh with hh1
· exact hh1.symm
· exact False.elim (bot_ne_top hhh)
