Generalizing over morphisms

Stream: general

[Eric Wieser]

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]

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]

docs#category_theory.adjunction

[Adam Topaz]

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

[Adam Topaz]

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]

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]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Eric Wieser]

I think I'm done for the day anyway

[Eric Wieser]

But will take a look tomorrow, thanks!

[Adam Topaz]

@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]

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

[Adam Topaz]

#4620

[Eric Wieser]

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]

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]

So for example, if you want to lift a function from S \to Awhere A is an R-algebra, you could use adj.hom_equiv.symmor something like that. I'm not too familiar with the adjunction API, so someone else might be more helpful. @Bhavik Mehta ?