flat_of_preservesFiniteLimits — Mathlib

English

Representably flat functors preserve finite limits; more precisely, if F preserves finite limits, then F is representably flat, and the opposite direction holds as well via equivalences.

Русский

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

LaTeX

$$$\text{RepresentablyFlat } F \iff \text{PreservesFiniteLimits } F$$$

Lean4

theorem flat_of_preservesFiniteLimits [HasFiniteLimits C] (F : C ⥤ D) [PreservesFiniteLimits F] : RepresentablyFlat F :=
  ⟨fun X =>
    haveI : HasFiniteLimits (StructuredArrow X F) :=
      by
      apply hasFiniteLimits_of_hasFiniteLimits_of_size.{v₁} (StructuredArrow X F)
      exact fun _ _ _ => HasLimitsOfShape.mk
    IsCofiltered.of_hasFiniteLimits _⟩

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