Commit 2025-01-27 14:13 ed60c9dd

feat(Algebra/Category): ConcreteCategory instances for rings (#20815) 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 the categories of rings: SemiRingCat, RingCat, CommSemiRingCat and CommRingCat. It also replaces the Hom.hom structure projection with an alias for ConcreteCategory.hom. The latter requires a few fixes downstream where things get mistakenly unfolded (especially involving ModuleCat.restrictScalars) or where rw doesn't see through the definitional equality ConcreteCategory.hom (ConcreteCategory.ofHom f) = f. Finally, a few places where the proof works around the old forget <-> FunLike mismatch, and needs updating. 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.