adjointifyη — Mathlib

Lean4
/-- If `η : 𝟭 C ≅ F ⋙ G` is part of a (not necessarily half-adjoint) equivalence, we can upgrade it
to a refined natural isomorphism `adjointifyη η : 𝟭 C ≅ F ⋙ G` which exhibits the properties
required for a half-adjoint equivalence. See `Equivalence.mk`. -/
def adjointifyη : 𝟭 C ≅ F ⋙ G := by
  calc
    𝟭 C ≅ F ⋙ G := η
    _ ≅ F ⋙ 𝟭 D ⋙ G := (isoWhiskerLeft F (leftUnitor G).symm)
    _ ≅ F ⋙ (G ⋙ F) ⋙ G := (isoWhiskerLeft F (isoWhiskerRight ε.symm G))
    _ ≅ F ⋙ G ⋙ F ⋙ G := (isoWhiskerLeft F (associator G F G))
    _ ≅ (F ⋙ G) ⋙ F ⋙ G := (associator F G (F ⋙ G)).symm
    _ ≅ 𝟭 C ⋙ F ⋙ G := (isoWhiskerRight η.symm (F ⋙ G))
    _ ≅ F ⋙ G := leftUnitor (F ⋙ G)
Похожие утверждения