∀ (x : CommSemiRingCat),
  CommGrpCat.ofHom (CommRing.Pic.mapRingHom (CommSemiRingCat.Hom.hom (CategoryTheory.CategoryStruct.id x))) =
    CategoryTheory.CategoryStruct.id (CommGrpCat.of (CommRing.Pic ↑x))