colimitLimitToLimitColimit_isIso — Mathlib

English

Under the stated finite and filtered hypotheses, the canonical map colimitLimitToLimitColimit F is an isomorphism.

Русский

При указанных условиях каноническое отображение colimitLimitToLimitColimit F является изоморфизмом.

LaTeX

$$HasFilteredColimitsOfSize.{max w' w₂', max w w₂} C ⟹ IsIso (colimitLimitToLimitColimit F)$$

Lean4

instance colimitLimitToLimitColimit_isIso : IsIso (colimitLimitToLimitColimit F) :=
  (isIso_iff_bijective _).mpr ⟨colimitLimitToLimitColimit_injective F, colimitLimitToLimitColimit_surjective F⟩

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