module maps induced by ring homs

Stream: maths

[Apurva Nakade]

What is a good way to define a map between modules induced by ring homomorphisms? Here's an mwe:

import Mathlib.Algebra.Module.Submodule.Basic

variable {R : Type*} [Ring R]
variable {S : Type*} [Ring S]

variable {E : Type*} [AddCommGroup E] [Module S E]
variable {F : Type*} [AddCommGroup F] [Module S F]

variable (φ : R →+* S)

-- instance : Module R E := Module.compHom E φ
#check Module.compHom E φ -- typechecks!

-- instance : Module R F := Module.compHom F φ
#check Module.compHom F φ -- typechecks!

example (f : E →ₗ[S] F) : E →ₗ[R] F := by sorry

Thanks,

[Apurva Nakade]

The case I'm interested is when φ is an inclusion of subrings.

[Apurva Nakade]

(Also, VSCode parses \phi as \varphi and \varphi as \phi lol)

[Alex J. Best]

Does docs#LinearMap.restrictScalars work?

[Apurva Nakade]

This is exactly what I want! Thanks!!

I'm having issues with inducing the second module structure though. This line gives an error even though it typechecks:

-- instance : Module R E := Module.compHom E φ
#check Module.compHom E φ -- typechecks!

The error is:

cannot find synthesization order for instance @instModuleToSemiringToAddCommMonoid with type
  {R : Type u_1} →
    [inst : Ring R] →
      {S : Type u_2} →
        [inst_1 : Ring S] → {E : Type u_3} → [inst_2 : AddCommGroup E] → [inst_3 : Module S E] → (R →+* S) → Module R E
all remaining arguments have metavariables:
  Ring ?S
  @Module ?S E Ring.toSemiring AddCommGroup.toAddCommMonoid

[Kevin Buzzard]

What's a #mwe for the error?

[Apurva Nakade]

The same as above:

import Mathlib.Algebra.Module.Submodule.Basic

variable {R : Type*} [Ring R]
variable {S : Type*} [Ring S]

variable {E : Type*} [AddCommGroup E] [Module S E]
variable {F : Type*} [AddCommGroup F] [Module S F]

variable (φ : R →+* S)

-- instance : Module R E := Module.compHom E φ
#check Module.compHom E φ -- typechecks!

[Kevin Buzzard]

The instance doesn't really make sense. $\phi$ is just a variable. What if I have two ring homomorphisms $R\to S$? So the system is complaining that the instance is not mathematically meaningful.

[Kevin Buzzard]

Mathematically if you want to say "there is one and only one canonical map from R to S, and I want to fix that one" then you can use [Algebra R S] and then you can make E into an R-module with [Module R E] [IsScalarTower R S E]

[Apurva Nakade]

I see, thanks! I will try this out.

[Kevin Buzzard]

I think I have a more precise explanation of the error. variable (φ : R →+* S) doesn't mean "let $\phi$ be a ring homomorphism from $R$ to $S$". It rather means "do nothing, but if a user ever mentions $\phi$ then just put "for all $\phi:R\to S$ in front of what they're writing". So what Module.compHom E \phi unfolds to is "for all rings R and S, and for all S-modules E, and for all ring homs phi:R->S, here's an R-module structure on E". Now if you make this an instance, then when the typeclass inference system sees Module R E it can figure out what to choose for R and E, but now it has no clue what to let S be, so it gives up.

[Apurva Nakade]

I see. So I need a better way to create the _specific_ ring hom I'm interested in.

[Kevin Buzzard]

If you have a specific ring hom in mind which won't change then Algebra R S is the way to go.

[Apurva Nakade]

Yes, it's just an inclusion of rings.

[Apurva Nakade]

Great, I'll switch to using [Algebra R S]