# Zulip Chat Archive

## 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:42):

docs#category_theory.adjunction

#### 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.

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

#### 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:

https://github.com/leanprover-community/mathlib/blob/de46349366376fe12530dc56a99244a7ca405cae/src/category_theory/adjunction/basic.lean

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

So for example, if you want to lift a function from `S \to A`

where `A`

is an `R`

-algebra, you could use `adj.hom_equiv.symm`

or something like that. I'm not too familiar with the adjunction API, so someone else might be more helpful. @Bhavik Mehta ?

Last updated: May 09 2021 at 19:11 UTC