Commit 2025-01-30 07:11 132efc70

feat(Algebra/Category): concrete category refactor for Grp (#21192) This is a step towards a concrete category redesign, as outlined in this Zulip post: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Concrete.20category.20class.20redesign/near/493903980 This PR updates the concrete category definitions of Grp, AddGrp, CommGrp and AddCommGrp to match the standard set by AlgebraCat, ModuleCat and RingCat:

• Package objects and homs into structures.
• Replace HasForget with ConcreteCategory.
• Set up a good @[simp] set.
• Ensure constructors and projections are reducible. See MathlibTest/CategoryTheory/ConcreteCategory/Grp.lean for the specification of all the new functionality. In particular, we can drop coe_of from the @[simp] set, which means we can re-enable some @[simps] attributes downstream. (I did the ones I came across, but we'd need to go through the library more carefully to get them all.) Overall I think we get a good cleanup, even if there are a handful of places where we have to fight more against the HasForget/ConcreteCategory non-reducible defeq. Those should go away as HasForget is obsoleted further. I have not tried to look for code that can be cleaned up now, only at what broke. I want to get started on cleanup when the other concrete category instances are in.