Commit 2025-01-27 12:48 41fd6951

feat(Algebra/Category): ConcreteCategory instance for AlgebraCat (#21121) 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 adds a ConcreteCategory instance for AlgebraCat. It also replaces the Hom.hom structure projection with an alias for ConcreteCategory.hom. Apparently this went perfectly well and everything stays working nicely. :) 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.