English
For K: J ⥤ C^{op} and A: C^{op} ⥤ Type, if CostructuredArrow yoneda A is filtered, then limit.post K A is an isomorphism.
Русский
Для K: J ⥤ C^{op} и A: C^{op} ⥤ Type, если CostructuredArrow yoneda A фильтрована, то limit.post K A является изоморфизмом.
LaTeX
$$$\operatorname{IsFiltered}(\operatorname{CostructuredArrow}(\mathrm{yoneda}, A)) \Rightarrow \operatorname{IsIso}(\operatorname{limit.post}(K, A))$$$
Lean4
theorem iso_hom [IsFiltered (CostructuredArrow yoneda A)] : (iso A K).hom = limit.post K A := by
-- We will have to use `ι_colimitLimitIso_limit_π` eventually, so let's start by
-- transforming the goal into something from a colimit to a limit so that we can apply
-- `limit.hom_ext` and `colimit.hom_ext`.
dsimp [iso, -Iso.app_hom]
simp only [Category.assoc]
rw [Eq.comm, ← Iso.inv_comp_eq, ← Iso.inv_comp_eq]
refine limit.hom_ext (fun j => colimit.hom_ext (fun i => ?_))
simp only [Category.assoc]
-- `simp` is not too helpful here because we will need to apply `NatTrans.comp_app_assoc`
-- backwards at certain points, so we rewrite the term manually.
rw [HasLimit.isoOfNatIso_hom_π, HasLimit.isoOfNatIso_hom_π_assoc, limit.post_π,
colimitObjIsoColimitCompEvaluation_ι_inv_assoc (CostructuredArrow.proj yoneda A ⋙ yoneda), Iso.app_inv, ←
NatTrans.comp_app_assoc, colimit.comp_coconePointUniqueUpToIso_inv, Presheaf.tautologicalCocone_ι_app,
HasColimit.isoOfNatIso_ι_hom_assoc, HasLimit.isoOfNatIso_hom_π_assoc, HasColimit.isoOfNatIso_ι_hom_assoc,
HasColimit.isoOfNatIso_ι_hom_assoc, HasColimit.isoOfNatIso_ι_hom_assoc, ι_colimitLimitIso_limit_π_assoc,
isoAux_hom_app, ← NatTrans.comp_app_assoc, ← NatTrans.comp_app_assoc, Category.assoc, HasLimit.isoOfNatIso_hom_π,
preservesLimitIso_hom_π_assoc, Iso.symm_hom, ← NatTrans.comp_app_assoc, HasColimit.isoOfNatIso_ι_hom, ←
NatTrans.comp_app_assoc, Category.assoc, ι_colimitCompWhiskeringLeftIsoCompColimit_hom, NatTrans.comp_app,
Category.assoc, isoWhiskerLeft_hom, NatTrans.comp_app, Category.assoc, ← NatTrans.comp_app, ← whiskerLeft_comp,
colimit.comp_coconePointUniqueUpToIso_hom]
have := i.hom.naturality (limit.π K j)
dsimp only [yoneda_obj_obj, Functor.const_obj_obj] at this
rw [← this]
ext
simp
