Commit 2025-01-27 16:24 c6ea3e1e

feat(Algebra/Category): ConcreteCategory instance for ModuleCat (#21125) 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 ModuleCat. It also replaces the Hom.hom structure projection with an alias for ConcreteCategory.hom. Sadly ModuleCat.restrictScalars and PresheafOfModules do not appreciate subtle changes in elaboration/defeq, and quite a few declarations need subtle fixes. Maybe a more structural fix exists? 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.