English
A technical auxiliary lemma: locally constant maps into α-indexed Finite values decompose along the cofiltered diagram.
Русский
Техническая вспомогательная лемма: локально константные отображения в α-значения распадаются вдоль кофильтрованной диаграммы.
LaTeX
$$$\\exists j:\\,J,\\exists g:\\mathrm{LocallyConstant}(F(j),(\\alpha\\to\\mathrm{Fin}\\,2)),\\ (f.map\\;\\iota)= g\\circ (C.\\pi.app j).hom$$$
Lean4
theorem exists_locallyConstant_finite_aux {α : Type*} [Finite α] (hC : IsLimit C) (f : LocallyConstant C.pt α) :
∃ (j : J) (g : LocallyConstant (F.obj j) (α → Fin 2)),
(f.map fun a b => if a = b then (0 : Fin 2) else 1) = g.comap (C.π.app _).hom :=
by
cases nonempty_fintype α
let ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
let ff := (f.map ι).flip
have hff := fun a : α => exists_locallyConstant_fin_two _ hC (ff a)
choose j g h using hff
let G : Finset J := Finset.univ.image j
obtain ⟨j0, hj0⟩ := IsCofiltered.inf_objs_exists G
have hj : ∀ a, j a ∈ (Finset.univ.image j : Finset J) := by grind
let fs : ∀ a : α, j0 ⟶ j a := fun a => (hj0 (hj a)).some
let gg : α → LocallyConstant (F.obj j0) (Fin 2) := fun a => (g a).comap (F.map (fs _)).hom
let ggg := LocallyConstant.unflip gg
refine ⟨j0, ggg, ?_⟩
have : f.map ι = LocallyConstant.unflip (f.map ι).flip := by simp
rw [this]; clear this
have :
LocallyConstant.comap (C.π.app j0).hom ggg =
LocallyConstant.unflip (LocallyConstant.comap (C.π.app j0).hom ggg).flip :=
by simp
rw [this]; clear this
congr 1
ext1 a
change ff a = _
rw [h]
dsimp
ext1 x
change _ = (g a) ((C.π.app j0 ≫ F.map (fs a)) x)
rw [C.w]; rfl
