colimitLimitToLimitColimitCone_iso

English

For suitable J, K, and F, the cone colimitLimitToLimitColimitCone F is an isomorphism.

Русский

Для подходящих J, K и F конус colimitLimitToLimitColimitCone является изоморфизмом.

LaTeX

$$IsIso (colimitLimitToLimitColimitCone F)$$

Lean4

instance colimitLimitToLimitColimitCone_iso (F : J ⥤ K ⥤ Type v) : IsIso (colimitLimitToLimitColimitCone F) :=
  by
  have : IsIso (colimitLimitToLimitColimitCone F).hom :=
    by
    suffices
      IsIso (colimitLimitToLimitColimit (uncurry.obj F) ≫ lim.map (whiskerRight (currying.unitIso.app F).inv colim)) by
      apply IsIso.comp_isIso
    infer_instance
  apply Cones.cone_iso_of_hom_iso

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