colim_preservesTerminal_of_isSifted

English

The canonical product comparison map is an isomorphism when C is sifted.

Русский

Каноническое сравнение произведений является изоморфизмом при ситообразной C.

LaTeX

$$IsIso (CartesianMonoidalCategory.prodComparison colim X Y)$$

Lean4

/-- If `C` is sifted, the `colimit` functor `(C ⥤ Type) ⥤ Type` preserves terminal objects -/
instance colim_preservesTerminal_of_isSifted : PreservesLimit (Functor.empty.{0} (C ⥤ Type u)) colim :=
  by
  apply preservesTerminal_of_iso
  symm
  apply (_ : ⊤_ (Type u) ≅ PUnit.{u + 1}).trans
  · apply_rules [(Types.colimitConstPUnitIsoPUnit C).symm.trans, HasColimit.isoOfNatIso,
      IsTerminal.uniqueUpToIso _ terminalIsTerminal, evaluationJointlyReflectsLimits]
    exact fun _ ↦ isLimitChangeEmptyCone _ Types.isTerminalPunit _ <| Iso.refl _
  · exact Types.isTerminalEquivIsoPUnit (⊤_ (Type u)) |>.toFun terminalIsTerminal

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