Lean4
/-- If `e : F ≅ G` is an isomorphism of functors and if `F` commutes with the
shift, then `G` also commutes with the shift. -/
def ofIso : G.CommShift A
where
iso a := isoWhiskerLeft _ e.symm ≪≫ F.commShiftIso a ≪≫ isoWhiskerRight e _
zero := by
ext X
simp only [comp_obj, F.commShiftIso_zero A, Iso.trans_hom, isoWhiskerLeft_hom, Iso.symm_hom, isoWhiskerRight_hom,
NatTrans.comp_app, whiskerLeft_app, isoZero_hom_app, whiskerRight_app, assoc]
erw [← e.inv.naturality_assoc, ← NatTrans.naturality, e.inv_hom_id_app_assoc]
add a
b := by
ext X
simp only [comp_obj, F.commShiftIso_add, Iso.trans_hom, isoWhiskerLeft_hom, Iso.symm_hom, isoWhiskerRight_hom,
NatTrans.comp_app, whiskerLeft_app, isoAdd_hom_app, whiskerRight_app, assoc, map_comp, NatTrans.naturality_assoc,
NatIso.cancel_natIso_inv_left]
simp only [← Functor.map_comp_assoc, e.hom_inv_id_app_assoc]
simp only [← NatTrans.naturality, comp_obj, comp_map, map_comp, assoc]
