preservesFiniteColimits_iff_coflat

English

Representably Coflat F iff PreservesFiniteColimits F.

Русский

Representably Coflat F эквивалентно сохранению конечных колимитов F.

LaTeX

$$RepresentablyCoflat F \iff PreservesFiniteColimits F$$

Lean4

/-- If `C` is finitely cocomplete, then `F : C ⥤ D` is representably coflat iff it preserves
finite colimits. -/
theorem preservesFiniteColimits_iff_coflat [HasFiniteColimits C] (F : C ⥤ D) :
    RepresentablyCoflat F ↔ PreservesFiniteColimits F :=
  ⟨fun _ => preservesFiniteColimits_of_coflat F, fun _ => coflat_of_preservesFiniteColimits F⟩

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