Commit 2020-10-15 16:29 abaf3c29

View on Github →

feat(algebra/category/Algebra/basic): Add free/forget adjunction. (#4620) This PR adds the usual free/forget adjunction for the category of R-algebras.

Estimated changes

Modified src/algebra/category/Algebra/basic.lean

added def Algebra.adj

added def Algebra.free