sheafComposeNatTrans_fac — Mathlib

English

The sheafComposeNatTrans J F adj₁ adj₂ is an isomorphism.

Русский

SheafComposeNatTrans является изоморфизмом.

LaTeX

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

Lean4

theorem sheafComposeNatTrans_fac (P : Cᵒᵖ ⥤ A) :
    adj₂.unit.app (P ⋙ F) ≫ (sheafToPresheaf J B).map ((sheafComposeNatTrans J F adj₁ adj₂).app P) =
      whiskerRight (adj₁.unit.app P) F :=
  by simp [sheafComposeNatTrans, -sheafToPresheaf_obj, -sheafToPresheaf_map, Adjunction.homEquiv_counit]

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