English
Under the same assumptions as before, the inverse of plusCompIso F P equals the plusLift constructed from whiskerRight (J.toPlus P) F.
Русский
При тех же предпосылках, обратный образ plusCompIso F P равен plusLift, построенному из whiskerRight (J.toPlus P) F.
LaTeX
$$(J.plusCompIso F P).inv = J.plusLift (whiskerRight (J.toPlus P) F)$$
Lean4
@[reassoc (attr := simp)]
theorem plusCompIso_whiskerLeft {F G : D ⥤ E} (η : F ⟶ G) (P : Cᵒᵖ ⥤ D)
[∀ X : C, PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
[∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F]
[∀ X : C, PreservesColimitsOfShape (J.Cover X)ᵒᵖ G]
[∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan G] :
whiskerLeft _ η ≫ (J.plusCompIso G P).hom = (J.plusCompIso F P).hom ≫ J.plusMap (whiskerLeft _ η) :=
by
ext X
apply (isColimitOfPreserves F (colimit.isColimit (J.diagram P X.unop))).hom_ext
intro W
dsimp [plusObj, plusMap]
simp only [ι_plusCompIso_hom, ι_colimMap, whiskerLeft_app, ι_plusCompIso_hom_assoc, NatTrans.naturality_assoc,
GrothendieckTopology.diagramNatTrans_app]
simp only [← Category.assoc]
congr 1
cat_disch
