Lean4
/-- When `r : HomRel C` is compatible with the shift by an additive monoid, and
`F : C ⥤ D` is a functor which commutes with the shift and is compatible with `r`, then
the induced functor `Quotient.lift r F _ : Quotient r ⥤ D` also commutes with the shift. -/
noncomputable instance liftCommShift : (Quotient.lift r F hF).CommShift A
where
iso := LiftCommShift.iso F r hF
zero := by
ext1
apply natTrans_ext
ext X
dsimp
rw [LiftCommShift.iso_hom_app, (functor r).commShiftIso_zero, Functor.CommShift.isoZero_hom_app,
Functor.CommShift.isoZero_inv_app, Functor.map_comp, assoc, F.commShiftIso_zero,
Functor.CommShift.isoZero_hom_app, lift_map_functor_map, ← F.map_comp_assoc, Iso.inv_hom_id_app]
dsimp [lift_obj_functor_obj]
rw [F.map_id, id_comp]
add a
b := by
ext1
apply natTrans_ext
ext X
dsimp
rw [LiftCommShift.iso_hom_app, (functor r).commShiftIso_add, F.commShiftIso_add, Functor.CommShift.isoAdd_hom_app,
Functor.CommShift.isoAdd_hom_app, Functor.CommShift.isoAdd_inv_app, Functor.map_comp, Functor.map_comp,
Functor.map_comp, assoc, assoc, assoc, LiftCommShift.iso_hom_app, lift_map_functor_map]
congr 1
rw [←
cancel_epi
((shiftFunctor (Quotient r) b ⋙ lift r F hF).map (NatTrans.app (Functor.commShiftIso (functor r) a).hom X))]
erw [(LiftCommShift.iso F r hF b).hom.naturality_assoc (((functor r).commShiftIso a).hom.app X),
LiftCommShift.iso_hom_app, ← Functor.map_comp_assoc, Iso.hom_inv_id_app]
dsimp
simp only [Functor.comp_obj, assoc, ← Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.map_id, id_comp,
Iso.hom_inv_id_app, lift_obj_functor_obj]
