ι_colimitLimitIso_limit_π — Mathlib

English

If forgetful functor preserves limits and filtered colimits and C has finite limits, then colim preserves finite limits.

Русский

Если забывающий функтор сохраняет пределы и фильтрованные колимиты, иC имеет конечные пределы, то colim сохраняет конечные пределы.

LaTeX

$$[PreservesFiniteLimits (forget C)] [PreservesColimitsOfShape K (forget C)] [HasFiniteLimits C] [HasColimitsOfShape K C] ⇒ PreservesFiniteLimits colim$$

Lean4

@[reassoc (attr := simp)]
theorem ι_colimitLimitIso_limit_π (F : J ⥤ K ⥤ C) (a) (b) :
    colimit.ι (limit F) a ≫ (colimitLimitIso F).hom ≫ limit.π (colimit F.flip) b =
      (limit.π F b).app a ≫ (colimit.ι F.flip a).app b :=
  by
  dsimp [colimitLimitIso]
  simp only [Functor.mapCone_π_app, Iso.symm_hom, Limits.limit.conePointUniqueUpToIso_hom_comp_assoc,
    Limits.limit.cone_π, Limits.colimit.ι_map_assoc, Limits.colimitFlipIsoCompColim_inv_app, assoc,
    Limits.HasLimit.isoOfNatIso_hom_π]
  congr 1
  simp only [← Category.assoc, Iso.comp_inv_eq, Limits.colimitObjIsoColimitCompEvaluation_ι_app_hom,
    Limits.HasColimit.isoOfNatIso_ι_hom]
  simp

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