preservesFiniteColimits_of_coflat

English

Representably Coflat F preserves finite colimits; equivalently, representably flat F preserves finite limits under dualities.

Русский

Representably Coflat F сохраняет конечные колимиты; эквивалентно тому, что representably flat F сохраняет конечные пределы под двойственностями.

LaTeX

$$PreservesFiniteColimits F$$

Lean4

/-- Representably coflat functors preserve finite colimits. -/
theorem preservesFiniteColimits_of_coflat (F : C ⥤ D) [RepresentablyCoflat F] : PreservesFiniteColimits F :=
  letI _ := preservesFiniteLimits_of_flat F.op
  preservesFiniteColimits_of_op _

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