HasCardinalFilteredColimits_iff_hasFilteredColimitsOfSize

English

A category has cardinal-filtered colimits of size aleph_0 if and only if it has filtered colimits of size (the appropriate size).

Русский

У категории есть кардинально-фильтрованные колимиты размера aleph_0 тогда и только тогда, когда существуют фильтрованные колимиты соответствующего размера.

LaTeX

$$$HasCardinalFilteredColimits\ C\ \aleph_0 \iff HasFilteredColimitsOfSize C$$$

Lean4

theorem HasCardinalFilteredColimits_iff_hasFilteredColimitsOfSize :
    HasCardinalFilteredColimits.{w} C ℵ₀ ↔ HasFilteredColimitsOfSize.{w, w} C := by
  refine ⟨fun ⟨H⟩ ↦ ⟨?_⟩, fun ⟨H⟩ ↦ ⟨?_⟩⟩ <;> simp only [isCardinalFiltered_aleph0_iff] at * <;> exact H

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