equivalence₁UnitIso — Mathlib

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