sheafificationWhiskerLeftIso_inv_app

English

The hom-components of the whisker-right isomorphism agree with the corresponding components of the sheafification composition isomorphism.

Русский

Гом-компоненты изоморфизма whisker-right совпадают с соответствующими компонентами изоморфизма композиции шейфификации.

LaTeX

$$$((J.sheafification\_WhiskerRightIso F).hom)\_{{}.app\;P} = (J.sheafifyCompIso F P).hom$$

Lean4

@[simp]
theorem sheafificationWhiskerLeftIso_inv_app (P : Cᵒᵖ ⥤ D) (F : D ⥤ E)
    [∀ (F : D ⥤ E) (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
    [∀ (F : D ⥤ E) (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F] :
    (sheafificationWhiskerLeftIso J P).inv.app F = (J.sheafifyCompIso F P).inv :=
  by
  dsimp [sheafificationWhiskerLeftIso, sheafifyCompIso]
  erw [Category.id_comp]

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