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>

Author: adamtopaz

src/algebra/category/Algebra/basic.lean

@@ -5,6 +5,7 @@ Authors: Scott Morrison
 -/
 import algebra.algebra.basic
 import algebra.algebra.subalgebra
+import algebra.free_algebra
 import algebra.category.CommRing.basic
 import algebra.category.Module.basic
 
@@ -69,6 +70,28 @@ variables {R} {M N U : Module.{v} R}
 @[simp] lemma coe_comp (f : M ⟶ N) (g : N ⟶ U) :
   ((f ≫ g) : M → U) = g ∘ f := rfl
 
+variables (R)
+/-- The "free algebra" functor, sending a type `S` to the free algebra on `S`. -/
+@[simps]
+def free : Type* ⥤ Algebra R :=
+{ obj := λ S,
+  { carrier := free_algebra R S,
+    is_ring := algebra.semiring_to_ring R },
+  map := λ S T f, free_algebra.lift _ $ (free_algebra.ι _) ∘ f }
+
+/-- The free/forget ajunction for `R`-algebras. -/
+@[simps]
+def adj : free R ⊣ forget (Algebra R) :=
+{ hom_equiv := λ X A,
+  { to_fun := λ f, f ∘ (free_algebra.ι _),
+    inv_fun := λ f, free_algebra.lift _ f,
+    left_inv := by tidy,
+    right_inv := by tidy },
+  unit := { app := λ S, free_algebra.ι _ },
+  counit :=
+  { app := λ S, free_algebra.lift _ $ id,
+    naturality' := by {intros, ext, simp} } } -- tidy times out :(
+
 end Algebra
 
 variables {R}