tautological — Mathlib

Lean4
/-- The tautological shift sequence on a functor. -/
noncomputable def tautological : ShiftSequence F M
    where
  sequence n := shiftFunctor C n ⋙ F
  isoZero := isoWhiskerRight (shiftFunctorZero C M) F ≪≫ F.rightUnitor
  shiftIso n a a' ha' := (Functor.associator _ _ _).symm ≪≫ isoWhiskerRight (shiftFunctorAdd' C n a a' ha').symm _
  shiftIso_zero
    a := by
    rw [shiftFunctorAdd'_zero_add]
    cat_disch
  shiftIso_add n m a a' a'' ha'
    ha'' := by
    ext X
    dsimp
    simp only [id_comp, ← Functor.map_comp]
    congr
    simpa only [← cancel_epi ((shiftFunctor C a).map ((shiftFunctorAdd C m n).hom.app X)),
      shiftFunctorAdd'_eq_shiftFunctorAdd, ← Functor.map_comp_assoc, Iso.hom_inv_id_app, Functor.map_id, id_comp] using
      shiftFunctorAdd'_assoc_inv_app m n a (m + n) a' a'' rfl ha' (by rw [← ha'', ← ha', add_assoc]) X
Похожие утверждения