isColimitLocallyConstantPresheafDiagram

English

In the isColimit construction for locally constant presheaf over a right-Op cocone, the descent along the isColimit equals the expected evaluation on s.ι app.

Русский

В описании isColimit для locallyConstantPresheaf над правым cocone, descend через isColimit равняется требуемой оценки на s.ι app.

LaTeX

$$$ (\\text{isColimitLocallyConstantPresheaf } c X hc).desc\\; s\\; (f) = s.ι.app \\langle n \\rangle f $$$

Lean4

/-- `isColimitLocallyConstantPresheaf` in the case of `S.asLimit`. -/
noncomputable def isColimitLocallyConstantPresheafDiagram (S : LightProfinite) :
    IsColimit <| (locallyConstantPresheaf X).mapCocone (coconeRightOpOfCone S.asLimitCone) :=
  (Functor.Final.isColimitWhiskerEquiv (opOpEquivalence ℕ).inverse _).symm
    (isColimitLocallyConstantPresheaf _ _ S.asLimit)

Похожие утверждения