isColimitLocallyConstantPresheafDiagram_desc_apply

English

Descent map for the LocallyConstantPresheaf diagram along a Profinite is given by the standard cocone desc formula; it coincides with the projection ι.

Русский

Расхождение колимита для диаграммы LocallyConstantPresheaf вдоль Profinite задаётся стандартной формулой desc для коконо и совпадает с отображением ι.

LaTeX

$$$((Condensed.isColimitLocallyConstantPresheaf c X hc).desc s (LocallyConstant.comap (TopCat.Hom.hom (c.\\pi.app i)) f)) = s.\\ι.app { unop := i } f$$$

Lean4

@[simp]
theorem isColimitLocallyConstantPresheafDiagram_desc_apply (S : Profinite)
    (s : Cocone (S.diagram.op ⋙ locallyConstantPresheaf X)) (i : DiscreteQuotient S)
    (f : LocallyConstant (S.diagram.obj i) X) :
    (isColimitLocallyConstantPresheafDiagram X S).desc s (f.comap (S.asLimitCone.π.app i).hom) = s.ι.app ⟨i⟩ f :=
  isColimitLocallyConstantPresheaf_desc_apply S.asLimitCone X S.asLimit s i f

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