mathlib

abaf3c29 - feat(algebra/category/Algebra/basic): Add free/forget adjunction. (#4620)

feat(algebra/category/Algebra/basic): Add free/forget adjunction. (#4620) This PR adds the usual free/forget adjunction for the category of `R`-algebras. Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>