Commit 2025-01-17 14:00 4335474d

chore(CategoryTheory): rename ConcreteCategory to HasForget (#20809) This is the first 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 commit was generated by find-and-replacing ConcreteCategory and concreteCategory with HasForget and hasForget respectively, making sure not to touch imports. I did not look too closely at the changes, since we should be going over everything during the redesign anyway. ConcreteCategory is now temporarily an alias for HasForget, with a deprecation warning. The ConcreteCategory namespace itself was not renamed, since we'll eventually be redoing those results for the new ConcreteCategory class.