lanPresheafIso_hom — Mathlib

English

The hom component of lanPresheafIso is given by a canonical colimit description, i.e., the universal morphism out of a cocone.

Русский

Гом-компонента lanPresheafIso задаётся каноническим колимитным отображением.

LaTeX

$$$(\\text{lanPresheafIso } hF).\\mathrm{hom} = \\operatorname{colimit.desc}\\; (\\text{CostructuredArrow.proj } FintypeCat.toLightProfinite.op { unop := S }).(\\text{comp} (FintypeCat.toLightProfinite.op.comp F))\\; (\\text{LightProfinite.Extend.cocone } F S)$$$

Lean4

@[simp]
theorem lanPresheafIso_hom (hF : IsColimit <| F.mapCocone (coconeRightOpOfCone S.asLimitCone)) :
    (lanPresheafIso hF).hom = colimit.desc _ (LightProfinite.Extend.cocone _ _) :=
  by
  simp [lanPresheafIso, Final.colimitIso]
  rfl

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