messing around with categories

Stream: general

[Eric Rodriguez]

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

import algebra.category.Module.abelian

variables {R S : Type*} [ring R] [ring S]

@[simps]
def restriction_of_scalars (f : R →+* S) (M : Module S) : Module R :=
{ carrier := M.carrier,
  is_add_comm_group := infer_instance,
  is_module := { smul := λ r x, (f r) • x,
                 smul_add := λ r, smul_add (f r),
                 add_smul := λ r s x, by simp only [add_smul, ring_hom.map_add],
                 mul_smul := λ r s x, by simp only [mul_smul, ring_hom.map_mul],
                 one_smul := λ x, by simp only [one_smul, ring_hom.map_one],
                 zero_smul := λ x, by simp only [ring_hom.map_zero, zero_smul],
                 smul_zero := λ r, smul_zero (f r) } }


def restriction_of_scalars' (f : R →+* S) : Module S ⥤ Module R :=
{ obj := restriction_of_scalars f,
  map := λ M₁ M₂ φ, { to_fun := φ,
                      map_add' := linear_map.map_add φ,
                      map_smul' := λ r x, by { change φ ((f r) • x) = _, simp } },
  map_id' := λ X, by { ext, simp },
  map_comp' := λ X Y Z φ ψ, by { ext, simp } }

-- #print restriction_of_scalars_is_module_to_distrib_mul_action_to_mul_action_to_has_scalar_smul

/- lemma restriction_of_scalars.smul_apply {f : R →+* S} {M : Module S}
    (r : R) (x : restriction_of_scalars f M) : r • x = f r • x := rfl -/

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]

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]

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]

There is some kind of defeq abuse going on there.

[Eric Rodriguez]

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]

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

[Eric Rodriguez]

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

[Adam Topaz]

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

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