plusFunctorWhiskerLeftIso — Mathlib

English

Same as earlier inversion equality for plusCompIso with the IsSheaf hypothesis.

Русский

То же самое соотношение обращения для plusCompIso при гипотезе IsSheaf.

LaTeX

$$(J.plusCompIso F P).inv = J.plusLift (whiskerRight (J.toPlus _) F) hP$$

Lean4

/-- The isomorphism between `P⁺ ⋙ F` and `(P ⋙ F)⁺`, functorially in `F`. -/
@[simps! hom_app inv_app]
def plusFunctorWhiskerLeftIso (P : Cᵒᵖ ⥤ D) [∀ (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] :
    (whiskeringLeft _ _ E).obj (J.plusObj P) ≅ (whiskeringLeft _ _ _).obj P ⋙ J.plusFunctor E :=
  NatIso.ofComponents (fun _ => plusCompIso _ _ _) @fun _ _ _ => plusCompIso_whiskerLeft _ _ _

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