English
The inv component of lanPresheafExt is the colimMap dual to hom case; it is given by the corresponding costructuredArrow projection with inv.
Русский
Компонента inv в lanPresheafExt равна аналогичной карте колимита в обратном направлении, задаётся projection через costructuredArrow с inv.
LaTeX
$$$(lanPresheafExt i).inv.app S = \\mathrm{colimMap}(\\mathrm{whiskerLeft}(\\mathrm{CostructuredArrow.proj}\\ toProfinite.op S)\\; i.inv)$$$
Lean4
@[simp]
theorem lanPresheafExt_inv {F G : Profinite.{u}ᵒᵖ ⥤ Type (u + 1)} (S : Profinite.{u}ᵒᵖ)
(i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G) :
(lanPresheafExt i).inv.app S = colimMap (whiskerLeft (CostructuredArrow.proj toProfinite.op S) i.inv) :=
by
simp only [lanPresheaf, pointwiseLeftKanExtension_obj, lanPresheafExt, leftKanExtensionUniqueOfIso_inv,
pointwiseLeftKanExtension_desc_app]
apply colimit.hom_ext
aesop
