English
The hom component of lanPresheafExt is given by colimMap whiskerLeft of i.hom.
Русский
Гом-компонента lanPresheafExt задаётся как colimMap whiskerLeft от i.hom.
LaTeX
$$$(\\text{lanPresheafExt } i).\\mathrm{hom.app} S = \\operatorname{colimMap}(\\text{whiskerLeft}(\\text{CostructuredArrow.proj } toLightProfinite.op S) i.hom)$$$
Lean4
@[simp]
theorem lanPresheafExt_hom {F G : LightProfinite.{u}ᵒᵖ ⥤ Type u} (S : LightProfinite.{u}ᵒᵖ)
(i : toLightProfinite.op ⋙ F ≅ toLightProfinite.op ⋙ G) :
(lanPresheafExt i).hom.app S = colimMap (whiskerLeft (CostructuredArrow.proj toLightProfinite.op S) i.hom) :=
by
simp only [lanPresheaf, pointwiseLeftKanExtension_obj, lanPresheafExt, leftKanExtensionUniqueOfIso_hom,
pointwiseLeftKanExtension_desc_app]
apply colimit.hom_ext
aesop
