English
The hom component of lanPresheafExt is described by a colimit map along the whiskered projection from the CostructuredArrow, i.e., it encodes the universal mapping property of LanPresheafExt.
Русский
Гом-компонента lanPresheafExt задаётся через колимитное отображение, получаемое через whiskerLeft от CostructuredArrow.
LaTeX
$$$(\\text{lanPresheafExt } i).\\mathrm{hom.app} S = \\operatorname{colimMap}(\\text{whiskerLeft}(\\text{CostructuredArrow.proj toLightProfinite.op } S) i.hom)$$$
Lean4
@[simp]
theorem isColimitLocallyConstantPresheaf_desc_apply (hc : IsLimit c) [∀ i, Epi (c.π.app i)]
(s : Cocone ((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X)) (n : ℕᵒᵖ)
(f : LocallyConstant (toLightProfinite.obj (F.obj n)) X) :
(isColimitLocallyConstantPresheaf c X hc).desc s (f.comap (c.π.app n).hom) = s.ι.app ⟨n⟩ f :=
by
change
((((locallyConstantPresheaf X).mapCocone c.op).ι.app ⟨n⟩) ≫ (isColimitLocallyConstantPresheaf c X hc).desc s) _ = _
rw [(isColimitLocallyConstantPresheaf c X hc).fac]
