unitIso — Mathlib

Lean4
/-- Implementation, see `leftExactFunctorForgetEquivalence`. -/
noncomputable def unitIso :
    𝟭 (C ⥤ₗ AddCommGrpCat) ≅ (LeftExactFunctor.whiskeringRight _ _ _).obj (LeftExactFunctor.of (forget _)) ⋙ inverse :=
  NatIso.ofComponents
    (fun F =>
      InducedCategory.isoMk
        (NatIso.ofComponents
          (fun X =>
            commGroupAddCommGroupEquivalence.counitIso.app _ ≪≫
              (CommGrpCat.toAddCommGrp.mapIso
                    (commGrpTypeEquivalenceCommGrp.counitIso.app (AddCommGrpCat.toCommGrp.obj (F.obj.obj X)))).symm ≪≫
                CommGrpCat.toAddCommGrp.mapIso (CommGrpTypeEquivalenceCommGrp.functor.mapIso (unitIsoAux F.obj X)))))
Похожие утверждения