instIsRightAdjointSheafComposeOfHasWeakSheafify

English

If HasWeakSheafify J D and F is right adjoint, then composition with F in the sheaf context is right adjoint.

Русский

При наличии HasWeakSheafify J D и F как правого сопряженного, композиция с F в контексте шейфа является правым сопряженным.

LaTeX

$$$[HasWeakSheafify\\ J\\ D]\\ [F.IsRightAdjoint]\\Rightarrow (\\mathrm{sheafCompose}\\ J F)\\text{ is right adjoint}$$$

Lean4

instance [HasWeakSheafify J D] [F.IsRightAdjoint] : (sheafCompose J F).IsRightAdjoint :=
  (adjunction J (Adjunction.ofIsRightAdjoint F)).isRightAdjoint

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