instIsIsoSheafAppFunctorOppositeSheafComposeNatTransPlusPlusAdjunction

English

For any P, the app of sheafComposeNatTrans is an isomorphism.

Русский

Для любого P компонент app у sheafComposeNatTrans является изоморфизмом.

LaTeX

$$$IsIso\left((\text{sheafComposeNatTrans } J F adj_1 adj_2).app P\right)$$$

Lean4

instance (P : Cᵒᵖ ⥤ D) : IsIso ((sheafComposeNatTrans J F (plusPlusAdjunction J D) (plusPlusAdjunction J E)).app P) :=
  by
  rw [← isIso_iff_of_reflects_iso _ (sheafToPresheaf J E),
    sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv]
  infer_instance

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