coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π

English

For each index i, the composition of the isomorphism’s hom with the i-th projection equals the coyoneda-map of the colimit injection at i.

Русский

Для каждого индекса i композиция гом-праобраза из изоморфизма с i-й проекцией равна отображению coyoneda соответствующего инъекта колимита на i.

LaTeX

$$$ (\text{coyonedaOpColimitIsoLimitCoyoneda}(F)).\mathrm{hom} \; \limfunc{π}_{F,i} = \mathrm{coyoneda}(\mathrm{colimit}.\mathrm{ι}F i).op. $$$

Lean4

@[reassoc (attr := simp)]
theorem coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π (i : I) :
    (coyonedaOpColimitIsoLimitCoyoneda F).hom ≫ limit.π (F.op.comp coyoneda) ⟨i⟩ = coyoneda.map (colimit.ι F i).op := by
  simp only [coyonedaOpColimitIsoLimitCoyoneda, Functor.mapIso_symm, Iso.trans_hom, Iso.symm_hom, Functor.mapIso_inv,
    Category.assoc, preservesLimitIso_hom_π, ← Functor.map_comp, limitOpIsoOpColimit_inv_comp_π]

Похожие утверждения