Commit 2025-11-15 10:39 d07fa9a7

feat: free groupoid on a category, free-forgetful adjunction (#29279)

• define CategoryTheory.FreeGroupoid
• show the universal property of this construction, as the initial category localizing all maps in the category. These are the defs of, lift, and their related theorems
• Show that this construction is functorial CategoryTheory.FreeGroupoid.map
• Convert this to a functor CategoryTheory.Grpd.free from Cat to Grpd, and show that it is left adjoint to the forgetful functor
• CategoryTheory.Grpd.freeForgetAdjunction