natIsoComp — Mathlib

Lean4
/-- The natural isomorphism between the pullback of `F ⋙ G` and the
composition of the pullbacks of `F` and `G`.
-/
def natIsoComp : PullbackShift.functor φ (F ⋙ G) ≅ PullbackShift.functor φ F ⋙ PullbackShift.functor φ G :=
  Iso.refl
    _
      /-
      Suppose that `F` and `G` have `CommShift` structure by `B`. This expresses the
      compatibility between two `CommShift` structures by `A` on (synonyms of) `F ⋙ G`:
      the `CommShift` structure on `PullbackShift.functor (F ⋙ G) φ` (i.e the pullback of the
      composition of `CommShift` structures by `B` on `F` and `G`), and that on
      `PullbackShift.functor F φ ⋙ PullbackShift.functor G φ` (i.e. the one coming from
      the composition of the pulled back `CommShift` structures on `F` and `G`).
      -/
Похожие утверждения