instPreservesFiniteLimitsSheafSheafPullback

English

Under the stated hypotheses, the sheafPushforwardContinuous functor is right adjoint to its counterpart; i.e., pushforward is left adjoint to some pullback construction in the sheaf setting.

Русский

При заданных предпосылках отображение pushforward для sheaf является правым смежным к своей паре; т. е. переход к глобальному слою является частным случаем сопряжения в теорииSheaf.

LaTeX

$$$\\exists$ a right adjoint: $(G.sheafPushforwardContinuous)(A,J,K)\\dashv\\text{(its left adjoint)}$$$

Lean4

instance : PreservesFiniteLimits (sheafPullback G A J K) :=
  by
  have : PreservesFiniteLimits (G.op.lan ⋙ presheafToSheaf K A) := comp_preservesFiniteLimits _ _
  apply comp_preservesFiniteLimits

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