plusCompIso_inv_eq_plusLift — Mathlib

English

The isomorphism between P⁺ and P⁺ after whiskering on the right with F is compatible with whiskering of maps on the right.

Русский

Изоморфизм P⁺ → ((P)⁺) после правого whisker с F совместим с правым whisker-ом отображений.

LaTeX

$$$J.plusFunctor D ⋙ whiskeringRight _.obj F ≅ whiskeringRight _.obj F ⋙ J.plusFunctor E$$$

Lean4

theorem plusCompIso_inv_eq_plusLift (hP : Presheaf.IsSheaf J (J.plusObj P ⋙ F)) :
    (J.plusCompIso F P).inv = J.plusLift (whiskerRight (J.toPlus _) _) hP :=
  by
  apply J.plusLift_unique
  simp

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