## Stream: general

### Topic: Generalizing over morphisms

#### Eric Wieser (Oct 14 2020 at 16:39):

To do the cleanups in #4616, it would be nice to generalize across the various ιs and lifts. To do that, I need to be able to generalize across the type of ι, which is X → _ in free_algebra, X →ₗ[R] _ in tensor_algebra, {f : X →ₗ[R] _ // ∀ x, f x * f x} in exterior_algebra, etc.

Naively, I tried to do this here by adding a (hom_α : Type u₃ → Type*) argument to my struct. I can't seem to use has_coe_to_fun instances in my argument list, and end up needing some obviously questionable instances like has_coe (α → β) (α → β) instead.

Is there a better way to generalize over "any object that has a coercion to a given function type"?

#### Adam Topaz (Oct 14 2020 at 16:42):

I don't know whether you want to actually go this route, but the "correct" generalization (from the category theoretic point of view) is to construct adjunctions between suitable categories.

#### Adam Topaz (Oct 14 2020 at 16:46):

I guess you could make a bundle which essentially encodes the same data as an adjunction, without mentioning category theory.

#### Adam Topaz (Oct 14 2020 at 16:48):

One disadvantage over using adjunctions from category theory is that you will have to put restrictions on the universe levels of the objects involved. I don't know if there is a way around it...

#### Eric Wieser (Oct 14 2020 at 16:49):

Yeah, being forced to constrain universe levels was one of the things I ran into. I don't know how to start with your suggestion though - I don't know what C and D should be for one.

#### Adam Topaz (Oct 14 2020 at 16:50):

For the free algebra, you would take the forgetful functor from the category of R-algebras to the category of types.

#### Adam Topaz (Oct 14 2020 at 16:50):

The free_algebra construction is the left adjoint, and the forgetful functor is the right adjoint.

#### Adam Topaz (Oct 14 2020 at 16:50):

I have to lecture in 10 minutes, but I will try to sketch an example after that.

#### Eric Wieser (Oct 14 2020 at 16:50):

I think I'm done for the day anyway

#### Eric Wieser (Oct 14 2020 at 16:51):

But will take a look tomorrow, thanks!

#### Adam Topaz (Oct 14 2020 at 18:23):

@Eric Wieser See below. I can PR this if people are interested.

import algebra.free_algebra
import algebra.category.Algebra.basic

open category_theory

variables (R : Type*) [comm_ring R]

@[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 } 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 :(

#### Adam Topaz (Oct 14 2020 at 18:23):

Note that the category of R-algebras in mathlib assumes R to be a commutative ring.

#4620

#### Eric Wieser (Oct 14 2020 at 19:02):

Thanks for doing that - I think the piece I'm missing is how to actually apply that adj definition, and whether the extra lemmas about lift and iota can be expressed in terms of it

#### Adam Topaz (Oct 14 2020 at 19:04):

I think the gist is all in this file: