sheafificationWhiskerRightIso — Mathlib

English

The inverse components of the whisker-right isomorphism coincide with the inverse components of the corresponding sheafification composition isomorphism.

Русский

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

LaTeX

$$$((J.sheafification\_WhiskerRightIso F).inv).app\;P = (J.sheafifyCompIso F P).inv$$

Lean4

/-- The isomorphism between the sheafification of `P` composed with `F` and
the sheafification of `P ⋙ F`, functorially in `P`. -/
noncomputable def sheafificationWhiskerRightIso :
    J.sheafification D ⋙ (whiskeringRight _ _ _).obj F ≅ (whiskeringRight _ _ _).obj F ⋙ J.sheafification E :=
  by
  refine associator _ _ _ ≪≫ ?_
  refine isoWhiskerLeft (J.plusFunctor D) (J.plusFunctorWhiskerRightIso _) ≪≫ ?_
  refine ?_ ≪≫ associator _ _ _
  refine (associator _ _ _).symm ≪≫ ?_
  exact isoWhiskerRight (J.plusFunctorWhiskerRightIso _) (J.plusFunctor E)

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