Zulip Chat Archive

Stream: general

Topic: Generalizing over morphisms


view this post on Zulip 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"?

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Oct 14 2020 at 16:42):

docs#category_theory.adjunction

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Oct 14 2020 at 16:50):

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

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Oct 14 2020 at 16:50):

I think I'm done for the day anyway

view this post on Zulip Eric Wieser (Oct 14 2020 at 16:51):

But will take a look tomorrow, thanks!

view this post on Zulip 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 :(

view this post on Zulip Adam Topaz (Oct 14 2020 at 18:23):

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

view this post on Zulip Adam Topaz (Oct 14 2020 at 18:39):

#4620

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Oct 14 2020 at 19:07):

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 ?


Last updated: May 09 2021 at 19:11 UTC