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