equivalence₂CounitIso — Mathlib

Lean4
/-- The counit isomorphism of the equivalence `equivalence₂` between `A` and `B`. -/
@[simps!]
def equivalence₂CounitIso : (eB.functor ⋙ e'.inverse ⋙ eA.inverse) ⋙ F ⋙ eB.inverse ≅ 𝟭 B :=
  calc
    (eB.functor ⋙ e'.inverse ⋙ eA.inverse) ⋙ F ⋙ eB.inverse ≅ eB.functor ⋙ (e'.inverse ⋙ eA.inverse) ⋙ F ⋙ eB.inverse :=
      associator _ _ _
    _ ≅ eB.functor ⋙ ((e'.inverse ⋙ eA.inverse) ⋙ F) ⋙ eB.inverse := (isoWhiskerLeft _ (associator _ _ _).symm)
    _ ≅ eB.functor ⋙ 𝟭 _ ⋙ eB.inverse := (isoWhiskerLeft _ (isoWhiskerRight (equivalence₁CounitIso hF) _))
    _ ≅ eB.functor ⋙ eB.inverse := (isoWhiskerLeft _ (leftUnitor _))
    _ ≅ 𝟭 B := eB.unitIso.symm
Похожие утверждения