Lean4
/-- Given an isomorphism of functors `e : L ⋙ F ≅ G` relating functors `L : C ⥤ D`,
`F : D ⥤ A` and `G : C ⥤ A`, an additive monoid `M`, a family of functors `F' : M → D ⥤ A`
equipped with isomorphisms `e' : ∀ m, L ⋙ F' m ≅ G.shift m`, this is the shift sequence
induced on `F` induced by a shift sequence for the functor `G`, provided that
the functor `(whiskeringLeft C D A).obj L` of precomposition by `L` is fully faithful. -/
noncomputable def induced : F.ShiftSequence M where
sequence := F'
isoZero := induced.isoZero e M F' e'
shiftIso := induced.shiftIso L G M F' e'
shiftIso_zero
a := by
ext1
apply ((whiskeringLeft C D A).obj L).map_injective
ext K
dsimp
simp only [induced.shiftIso_hom_app_obj, shiftIso_zero_hom_app, id_obj, NatTrans.naturality, comp_map,
Iso.hom_inv_id_app_assoc, comp_id, ← Functor.map_comp, L.commShiftIso_zero, CommShift.isoZero_inv_app, assoc,
Iso.inv_hom_id_app, Functor.map_id]
shiftIso_add n m a a' a'' ha'
ha'' := by
ext1
apply ((whiskeringLeft C D A).obj L).map_injective
ext K
dsimp
simp only [id_comp, induced.shiftIso_hom_app_obj, G.shiftIso_add_hom_app n m a a' a'' ha' ha'', L.commShiftIso_add,
comp_obj, CommShift.isoAdd_inv_app, (F' a).map_comp, assoc, ← (e' a).hom.naturality_assoc, comp_map]
simp only [← NatTrans.naturality_assoc, induced.shiftIso_hom_app_obj, ← Functor.map_comp_assoc, ← Functor.map_comp,
Iso.inv_hom_id_app, comp_obj, Functor.map_id, id_comp]
dsimp
simp only [Functor.map_comp, assoc, Iso.inv_hom_id_app_assoc]
