English
The hom component of the plusCompIso is compatible with colimits and whiskering in the expected way, i.e., the natural diagrams commute with F, P, and the plus constructions.
Русский
Гом-компонента plusCompIso совместима с колимитами и взятыми за whisker, диаграммы естественны и совместимы с F, P и конструкциями plus.
LaTeX
$$$(J.plusCompIso F P).hom$ is compatible with whiskering and colimits in the expected way.$$
Lean4
@[reassoc (attr := simp)]
theorem plusCompIso_whiskerRight {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) :
whiskerRight (J.plusMap η) F ≫ (J.plusCompIso F Q).hom = (J.plusCompIso F P).hom ≫ J.plusMap (whiskerRight η F) :=
by
ext X
apply (isColimitOfPreserves F (colimit.isColimit (J.diagram P X.unop))).hom_ext
intro W
dsimp [plusObj, plusMap]
simp only [ι_colimMap, whiskerRight_app, ι_plusCompIso_hom_assoc, GrothendieckTopology.diagramNatTrans_app]
simp only [← Category.assoc, ← F.map_comp]
dsimp [colimMap, IsColimit.map]
simp only [colimit.ι_desc]
dsimp [Cocones.precompose]
simp only [Functor.map_comp, Category.assoc, ι_plusCompIso_hom]
simp only [← Category.assoc]
congr 1
dsimp only [diagram] -- Need to unfold `diagram` before `ext` applies.
ext a
dsimp
simp only [diagramCompIso_hom_ι_assoc, Multiequalizer.lift_ι, diagramCompIso_hom_ι, Category.assoc]
simp only [← F.map_comp, Multiequalizer.lift_ι]
