Commit 2025-02-03 16:47 fc39d3b8

View on Github →

feat(Algebra/Category): ConcreteCategory instance for Semigrp (#21368) Very straightforward, essentially copypasting the design of MonCat back onto MagmaCat and Semigrp. We can probably do without this amount of dsimp lemmas, they should all be pretty easy to prove from generic ConcreteCategory results, but it doesn't hurt to have them in any case.

Estimated changes

added structure AddMagmaCat.Hom
added structure AddMagmaCat
added structure AddSemigrp.Hom
added structure AddSemigrp
added structure MagmaCat.Hom
added theorem MagmaCat.coe_comp
added theorem MagmaCat.coe_id
modified theorem MagmaCat.coe_of
added theorem MagmaCat.comp_apply
added theorem MagmaCat.ext
added theorem MagmaCat.forget_map
added theorem MagmaCat.hom_comp
added theorem MagmaCat.hom_ext
added theorem MagmaCat.hom_id
added theorem MagmaCat.hom_inv_apply
added theorem MagmaCat.hom_ofHom
added theorem MagmaCat.id_apply
added theorem MagmaCat.inv_hom_apply
deleted def MagmaCat.of
deleted def MagmaCat.ofHom
modified theorem MagmaCat.ofHom_apply
added theorem MagmaCat.ofHom_comp
added theorem MagmaCat.ofHom_hom
added theorem MagmaCat.ofHom_id
added structure MagmaCat
deleted def MagmaCat
added structure Semigrp.Hom
added theorem Semigrp.coe_comp
added theorem Semigrp.coe_id
modified theorem Semigrp.coe_of
added theorem Semigrp.comp_apply
added theorem Semigrp.comp_def
added theorem Semigrp.ext
added theorem Semigrp.forget_map
added theorem Semigrp.hom_comp
added theorem Semigrp.hom_ext
added theorem Semigrp.hom_id
added theorem Semigrp.hom_inv_apply
added theorem Semigrp.hom_ofHom
added theorem Semigrp.id_apply
added theorem Semigrp.inv_hom_apply
deleted def Semigrp.of
deleted def Semigrp.ofHom
modified theorem Semigrp.ofHom_apply
added theorem Semigrp.ofHom_comp
added theorem Semigrp.ofHom_hom
added theorem Semigrp.ofHom_id
added structure Semigrp
deleted def Semigrp