Lean4
/-- If `F : C ⥤ D` commutes with the shifts on `C` and `D`, then `PullbackShift.functor F φ`
commutes with their pullbacks by an additive map `φ`.
-/
noncomputable instance commShiftPullback : (PullbackShift.functor φ F).CommShift A
where
iso
a :=
isoWhiskerRight (pullbackShiftIso C φ a (φ a) rfl) F ≪≫
F.commShiftIso (φ a) ≪≫ isoWhiskerLeft _ (pullbackShiftIso D φ a (φ a) rfl).symm
zero := by
ext
dsimp
simp only [F.commShiftIso_zero' (A := B) (φ 0) (by rw [map_zero]), CommShift.isoZero'_hom_app, assoc,
CommShift.isoZero_hom_app, pullbackShiftFunctorZero'_hom_app, map_comp, pullbackShiftFunctorZero'_inv_app]
rfl
add _
_ := by
ext
simp only [PullbackShift.functor, comp_obj, Iso.trans_hom, isoWhiskerRight_hom, isoWhiskerLeft_hom, Iso.symm_hom,
NatTrans.comp_app, whiskerRight_app, whiskerLeft_app, CommShift.isoAdd_hom_app, map_comp, assoc]
rw [F.commShiftIso_add' (φ.map_add _ _).symm, ← shiftFunctorAdd'_eq_shiftFunctorAdd, ←
shiftFunctorAdd'_eq_shiftFunctorAdd, pullbackShiftFunctorAdd'_hom_app φ _ _ _ _ rfl _ _ _ rfl rfl rfl,
pullbackShiftFunctorAdd'_inv_app φ _ _ _ _ rfl _ _ _ rfl rfl rfl]
simp only [CommShift.isoAdd'_hom_app, assoc, map_comp, NatTrans.naturality_assoc, Iso.inv_hom_id_app_assoc]
slice_rhs 9 10 => rw [← map_comp, Iso.inv_hom_id_app, map_id]
simp only [comp_obj, id_comp]
rw [← Functor.comp_map F (shiftFunctor D _), ← (F.commShiftIso _).hom.naturality_assoc]
slice_rhs 4 5 => rw [← map_comp, (pullbackShiftIso C φ _ _ rfl).hom.naturality, map_comp]
slice_rhs 3 4 => rw [← map_comp, Iso.inv_hom_id_app, map_id]
simp only [comp_obj, id_comp, comp_map, assoc]
slice_rhs 3 4 => rw [← map_comp, ← map_comp, Iso.inv_hom_id_app, map_id, map_id]
rw [id_comp, assoc, assoc]
rfl
