instPreservesSheafification — Mathlib

English

Under suitable assumptions, there is an instance giving PreservesSheafification for F.

Русский

При должных предположениях существует инстанс PreservesSheafification для F.

LaTeX

$$$[\text{PreservesSheafification } J F]$$$

Lean4

instance : PreservesSheafification J F :=
  by
  rw [preservesSheafification_iff_of_adjunctions_of_hasSheafCompose _ _ (plusPlusAdjunction J D)
      (plusPlusAdjunction J E)]
  infer_instance

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