instPreservesSheafificationOfIsLeftAdjoint

English

If G is left adjoint, then J.PreservesSheafification G holds, giving the left adjoint preservation in sheafification.

Русский

Если G является левым сопряженным, то J.PreservesSheafification G имеет место, обеспечивая сохранение шейфикации левым сопряженным.

LaTeX

$$$[G.IsLeftAdjoint]\\;\\Rightarrow\\; J.PreservesSheafification G$$$

Lean4

instance [G.IsLeftAdjoint] : J.PreservesSheafification G :=
  preservesSheafification_of_adjunction J (Adjunction.ofIsLeftAdjoint G)

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