filtered_colim_preservesFiniteLimits_of_types

English

The cone iso associated to colimit-limit-to-limit-colimit is invertible; thus the cone is an isomorphism.

Русский

Конусная изоморфность, связанная с переходом пределов, оборотима; следовательно конус является изоморфизмом.

LaTeX

$$$IsIso(\mathrm{colimitLimitToLimitColimitCone} F)$$$

Lean4

noncomputable instance filtered_colim_preservesFiniteLimits_of_types :
    PreservesFiniteLimits (colim : (K ⥤ Type v) ⥤ _) :=
  by
  apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize.{v₂}
  intro J _ _
  refine ⟨fun {F} => ⟨fun {c} hc => ⟨IsLimit.ofIsoLimit (limit.isLimit _) ?_⟩⟩⟩
  symm
  trans colim.mapCone (limit.cone F)
  · exact Functor.mapIso _ (hc.uniqueUpToIso (limit.isLimit F))
  · exact asIso (colimitLimitToLimitColimitCone F)

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