preservesFiniteLimits — Mathlib

English

Assuming RepresentablyFlat G, HasWeakSheafify, etc., the sheafPullback construction preserves finite limits.

Русский

При предположении RepresentablyFlat G и наличии слабой шейфификации, конструкция sheafPullback сохраняет конечные пределы.

LaTeX

$$$\\text{PreservesFiniteLimits} (G. sheafPullback A J K)$$$

Lean4

instance preservesFiniteLimits : PreservesFiniteLimits (Functor.sheafPullback G A J K) :=
  preservesFiniteLimits_of_natIso (sheafPullbackIso G A J K).symm

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