whiskerRight_toSheafify_sheafifyCompIso_hom

English

Inverse-hom components of a whisker-left isomorphism match the corresponding inverse components of the coherent sheafification lift.

Русский

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

LaTeX

$$$((J.sheafificationWhiskerLeftIso P).inv).app F = (J.sheafifyCompIso F P).inv$$

Lean4

@[simp, reassoc]
theorem whiskerRight_toSheafify_sheafifyCompIso_hom :
    whiskerRight (J.toSheafify _) _ ≫ (J.sheafifyCompIso F P).hom = J.toSheafify _ :=
  by
  dsimp [sheafifyCompIso]
  erw [whiskerRight_comp, Category.assoc]
  slice_lhs 2 3 => rw [plusCompIso_whiskerRight]
  rw [Category.assoc, ← J.plusMap_comp, whiskerRight_toPlus_comp_plusCompIso_hom, ← Category.assoc,
    whiskerRight_toPlus_comp_plusCompIso_hom]
  rfl

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