Zulip Chat Archive

Stream: general

Topic: messing around with categories

Eric Rodriguez (Sep 25 2021 at 14:47):

This weekend, I've been messing a little with categories in Lean. I ended up making this:

Firstly — where is this functor in mathlib? I imagine it's presented as a general results in terms of <some name> categories, but I couldn't seem to find it.

More to the point, however; how come I can't write the commented out lemma? No matter how way I write it, I end up getting some missing typeclass. If I try to use the monstrosity just above it (helpfully made by @[simps]) it tells me it's not there (from the name, I'm guessing different typeclass routes). Is the right solution just to define the module instance separately? Or should I be using algebra and stuff instead. Having to use change feels wrong :(

Thirdly; is this even the right to do category stuff in mathlib? I originally had the universe stuff, but it didn't seem to matter that much there; am I also missing other idiomatic things?

Eric Rodriguez (Sep 25 2021 at 14:56):

ahh, the change line can be replaced with λ r, linear_map.map_smul φ (f r), but that seems to basically just be hiding the change

Reid Barton (Sep 25 2021 at 15:05):

The lemma looks kind of bad just taken at face value--I mean you could have R = S but f not the identity, for example.

Reid Barton (Sep 25 2021 at 15:05):

There is some kind of defeq abuse going on there.

Eric Rodriguez (Sep 25 2021 at 15:12):

the left smul should be the restriction_of_scalars one, whilst the right one is the "standard" smul from the Module S structure; I get why you say that but I can't see another way to write it

Reid Barton (Sep 25 2021 at 15:13):

I guess you need some explicit function going from M to restriction_of_scalars f M or vice versa

Eric Rodriguez (Sep 25 2021 at 15:14):

yeah, that makes sense actually, and it makes it clearer what's going on too

Adam Topaz (Sep 25 2021 at 15:45):

@Eric Rodriguez docs#restrict_scalars works by using an [algebra R S] instance. So one possible definition of this functor could be this:

import algebra.algebra.restrict_scalars
import algebra.category.Module.adjunctions

variables (R S : Type*) [comm_ring R] [comm_ring S]

def foo [algebra R S] : Module S  Module R :=
{ obj := λ M, Module.of R $ restrict_scalars R S M,
  map := λ M N f, f.restrict_scalars _ }

def bar (f : R →+* S) : Module S  Module R :=
by letI : algebra R S := f.to_algebra ; exact foo R S

Adam Topaz (Sep 25 2021 at 15:46):

(note that I had to assume that the rings are commutative to use the docs#ring_hom.to_algebra )

Last updated: Dec 20 2023 at 11:08 UTC