hasColimit_iff_small_quot — Mathlib

English

Same as above, in a variant form, relating HasColimit F to Small(Quot F).

Русский

Те же идеи в другой формулировке: HasColimit F эквивално Small(Quot F).

LaTeX

$$$ \\mathrm{HasColimit} F \\iff \\mathrm{Small}(\\mathrm{Quot} F) $$$

Lean4

/-- A functor `F : J ⥤ AddCommGrpCat.{w}` has a colimit if and only if `Colimits.Quot F` is
`w`-small.
-/
theorem hasColimit_iff_small_quot [DecidableEq J] : HasColimit F ↔ Small.{w} (Quot F) :=
  ⟨fun _ ↦
    Small.mk ⟨_, ⟨(Equiv.ofBijective _ ((isColimit_iff_bijective_desc (colimit.cocone F)).mp ⟨colimit.isColimit _⟩))⟩⟩,
    hasColimit_of_small_quot F⟩

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