τ₁ — Mathlib

Lean4
/-- The isomorphism `eB.functor ⋙ e'.inverse ⋙ e'.functor ≅ eB.functor` deduced
from the isomorphisms `hF : eA.functor ⋙ e'.functor ≅ F`,
`hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor` and the datum of
an isomorphism `η : G ⋙ F ≅ eB.functor`. -/
@[simps! hom_app]
def τ₁ (η : G ⋙ F ≅ eB.functor) : eB.functor ⋙ e'.inverse ⋙ e'.functor ≅ eB.functor :=
  calc
    eB.functor ⋙ e'.inverse ⋙ e'.functor ≅ (eB.functor ⋙ e'.inverse) ⋙ e'.functor := (associator _ _ _).symm
    _ ≅ (G ⋙ eA.functor) ⋙ e'.functor := (isoWhiskerRight hG _)
    _ ≅ G ⋙ eA.functor ⋙ e'.functor := (associator _ _ _)
    _ ≅ G ⋙ F := (isoWhiskerLeft _ hF)
    _ ≅ eB.functor := η
Похожие утверждения