English
For a diagram c:Cone(F ⋙ toProfinite) and an isColimit c, the desc map in the LocallyConstantPresheaf diagram yields the expected evaluation against the cocone; i.e., the desc map equals s.ι.app ⟨i⟩ f.
Русский
Для диаграммы c: Cone(F ⋙ toProfinite) и изколимита c отображение desc в диаграмме LocallyConstantPresheaf даёт ожидаемую оценку через когон; то есть desc равен s.ι.app ⟨i⟩ f.
LaTeX
$$$\\forall S\\ f,\\; (isColimitLocallyConstantPresheaf c X hc).desc s (f.\\mathrm{comap}(c.\\pi.app i).hom) = s.\\iota.app \\langle i \\rangle f$$$
Lean4
@[simp]
theorem isColimitLocallyConstantPresheaf_desc_apply (hc : IsLimit c) [∀ i, Epi (c.π.app i)]
(s : Cocone ((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X)) (i : I)
(f : LocallyConstant (toProfinite.obj (F.obj i)) X) :
(isColimitLocallyConstantPresheaf c X hc).desc s (f.comap (c.π.app i).hom) = s.ι.app ⟨i⟩ f :=
by
change
((((locallyConstantPresheaf X).mapCocone c.op).ι.app ⟨i⟩) ≫ (isColimitLocallyConstantPresheaf c X hc).desc s) _ = _
rw [(isColimitLocallyConstantPresheaf c X hc).fac]
