Lean4
/-- In the context of localization of categories, if a functor
is induced by a functor which commutes with the shift, then
this functor commutes with the shift. -/
noncomputable def commShiftOfLocalization : F'.CommShift A
where
iso := commShiftOfLocalization.iso L W F F'
zero := by
ext1
apply natTrans_ext L W
intro X
dsimp
simp only [commShiftOfLocalization.iso_hom_app, comp_obj, commShiftIso_zero, CommShift.isoZero_inv_app, map_comp,
CommShift.isoZero_hom_app, Category.assoc, ← NatTrans.naturality_assoc, ← NatTrans.naturality]
dsimp
simp only [← Functor.map_comp_assoc, ← Functor.map_comp, Iso.inv_hom_id_app, id_obj, map_id, Category.id_comp,
Iso.hom_inv_id_app_assoc]
add a
b := by
ext1
apply natTrans_ext L W
intro X
dsimp
simp only [commShiftOfLocalization.iso_hom_app, comp_obj, commShiftIso_add, CommShift.isoAdd_inv_app, map_comp,
CommShift.isoAdd_hom_app, Category.assoc]
congr 1
rw [← cancel_epi (F'.map ((shiftFunctor D b).map ((L.commShiftIso a).hom.app X))), ← F'.map_comp_assoc, ← map_comp,
Iso.hom_inv_id_app, map_id, map_id, Category.id_comp]
conv_lhs =>
erw [← NatTrans.naturality_assoc]
dsimp
rw [← Functor.map_comp_assoc, ← map_comp_assoc, Category.assoc, ← map_comp, Iso.inv_hom_id_app]
dsimp
rw [map_id, Category.comp_id, ← NatTrans.naturality]
dsimp
conv_rhs =>
erw [← NatTrans.naturality_assoc]
dsimp
rw [← Functor.map_comp_assoc, ← map_comp, Iso.hom_inv_id_app]
dsimp
rw [map_id, map_id, Category.id_comp, commShiftOfLocalization.iso_hom_app, Category.assoc, Category.assoc,
Category.assoc, ← map_comp_assoc, Iso.inv_hom_id_app, map_id, Category.id_comp]
