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