preservesFiniteLimits_iff_flat — Mathlib

English

If C has finite limits, then F is representably flat iff F preserves finite limits.

Русский

Если C имеет конечные пределы, то F представимо плоский тогда и только тогда, когда F сохраняет конечные пределы.

LaTeX

$$$RepresentablyFlat F \iff PreservesFiniteLimits F$$$

Lean4

/-- If `C` is finitely complete, then `F : C ⥤ D` is representably flat iff it preserves
finite limits.
-/
theorem preservesFiniteLimits_iff_flat [HasFiniteLimits C] (F : C ⥤ D) :
    RepresentablyFlat F ↔ PreservesFiniteLimits F :=
  ⟨fun _ ↦ preservesFiniteLimits_of_flat F, fun _ ↦ flat_of_preservesFiniteLimits F⟩

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