Commit 2025-05-17 22:59 e1e4c88c

View on Github →

chore: rename AlgebraCat to AlgCat (#23721) and its friends too. The new names:

  • are shorter
  • match MonCat, CommMonCat and (almost) match Grp, CommGrp
  • are what people would write on paper The existing name is too much of a mouthful to be usefully included in declaration names. For example, BialgebraCat.hasForgetToAlgebra wasn't named BialgebraCat.hasForgetToAlgebraCat.

Estimated changes

modified structure CSA
added structure AlgCat.Hom
added def AlgCat.adj
added theorem AlgCat.coe_of
added theorem AlgCat.comp_apply
added theorem AlgCat.forget_map
added theorem AlgCat.forget_obj
added def AlgCat.free
added theorem AlgCat.hom_comp
added theorem AlgCat.hom_ext
added theorem AlgCat.hom_id
added theorem AlgCat.hom_inv_apply
added theorem AlgCat.hom_ofHom
added theorem AlgCat.id_apply
added theorem AlgCat.inv_hom_apply
added theorem AlgCat.ofHom_apply
added theorem AlgCat.ofHom_comp
added theorem AlgCat.ofHom_hom
added theorem AlgCat.ofHom_id
added def AlgCat.ofSelfIso
added structure AlgCat
deleted structure AlgebraCat.Hom
deleted def AlgebraCat.adj
deleted theorem AlgebraCat.coe_of
deleted theorem AlgebraCat.comp_apply
deleted theorem AlgebraCat.forget_map
deleted theorem AlgebraCat.forget_obj
deleted def AlgebraCat.free
deleted theorem AlgebraCat.hom_comp
deleted theorem AlgebraCat.hom_ext
deleted theorem AlgebraCat.hom_id
deleted theorem AlgebraCat.hom_inv_apply
deleted theorem AlgebraCat.hom_ofHom
deleted theorem AlgebraCat.id_apply
deleted theorem AlgebraCat.inv_hom_apply
deleted theorem AlgebraCat.ofHom_apply
deleted theorem AlgebraCat.ofHom_comp
deleted theorem AlgebraCat.ofHom_hom
deleted theorem AlgebraCat.ofHom_id
deleted structure AlgebraCat
added theorem AlgCat.hasLimitsOfSize
added structure BialgCat.Hom
added theorem BialgCat.hom_ext
added def BialgCat.of
added theorem BialgCat.of_comul
added theorem BialgCat.of_counit
added theorem BialgCat.toBialgHom_id
added structure BialgCat
deleted structure BialgebraCat.Hom
deleted theorem BialgebraCat.hom_ext
deleted def BialgebraCat.of
deleted theorem BialgebraCat.of_comul
deleted theorem BialgebraCat.of_counit
deleted structure BialgebraCat
added structure CoalgCat.Hom
added theorem CoalgCat.forget₂_map
added theorem CoalgCat.forget₂_obj
added theorem CoalgCat.hom_ext
added theorem CoalgCat.of_comul
added theorem CoalgCat.of_counit
added theorem CoalgCat.toCoalgHom_id
added structure CoalgCat
deleted structure CoalgebraCat.Hom
deleted theorem CoalgebraCat.hom_ext
deleted theorem CoalgebraCat.of_comul
deleted theorem CoalgebraCat.of_counit
deleted structure CoalgebraCat
added def CoalgCat.ofComon
added def CoalgCat.toComon
added structure HopfAlgCat.Hom
added theorem HopfAlgCat.hom_ext
added theorem HopfAlgCat.of_comul
added theorem HopfAlgCat.of_counit
added structure HopfAlgCat
deleted structure HopfAlgebraCat.Hom
deleted theorem HopfAlgebraCat.hom_ext
deleted theorem HopfAlgebraCat.of_comul
deleted theorem HopfAlgebraCat.of_counit
deleted structure HopfAlgebraCat