Commit 2023-05-12 11:43 237c33e0
View on Github →chore: refactor of concrete categories (#3900) I think the ports
- https://github.com/leanprover-community/mathlib4/pull/2902 (MonCat)
- https://github.com/leanprover-community/mathlib4/pull/3036 (GroupCat)
- https://github.com/leanprover-community/mathlib4/pull/3260 (ModuleCat) didn't quite get things right, and also have some variation between them. This PR tries to straighten things out. Major changes:
- Have the coercion to type be via
X.\a, and put attribute@[coe]on this. - Make sure the coercion from morphisms to functions means that simp lemmas about the underlying bundled morphisms apply directly.
- This means we drop lemmas like
lemma Hom.map_mul {X Y : MonCat} (f : X ⟶ Y) (x y : X) : ((forget MonCat).map f) (x * y) = f x * f y- But at the expense of adding lemmas like
lemma coe_comp {X Y Z : MonCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
Overall I'm pretty happy, and it allows me to unstick the long stuck https://github.com/leanprover-community/mathlib4/pull/3105. This is not everything I want to do to refactor these files, but once I was satisfied that I can move forward with RingCat, I want to get this merged so we can unblock porting progress. I'll promise to come back to this soon! :-)