Module over algebra is a module over base ring

Stream: Is there code for X?

[Gareth Ma]

Is the following statement missing or wrong?

import Mathlib.RepresentationTheory.Character
import Mathlib.RingTheory.RootsOfUnity.Basic
import Mathlib.RingTheory.SimpleModule
import Mathlib.CategoryTheory.Simple
import Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

open LinearMap Module Submodule Representation FiniteDimensional CategoryTheory

universe u
variable {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A]

example {V : Type u} [AddCommGroup V] [Module A V] : Module k V := by
  sorry

(sorry for the many imports lol)

[Gareth Ma]

Since you can embed k into A (via algebraMap) and the axioms should work out

[Brendan Seamas Murphy]

The way mathlib's typeclass hierarchy is designed is such that this instance doesn't exist. The reasoning here is that we might have a preexisting typeclass instance [Module k V] not definitionally equal to the one you're thinking of here, and having multiple instances of typeclasses floating around is a massive headache. Instead, when we want to consider a V which is compatibly a k-module and an A-module we add both typeclass assumptions [Module k V] and [Module A V] as well as the assumption [IsScalarTower k A V]. This last typeclass basically says that the restriction of scalars of V as an A-module to a k-module gives the existing k-module structure. But since it's a proposition instead of a required definitional equality it behaves much better

[Gareth Ma]

Ahh okay, I will have a look at the IsScalarTower API, thanks!

[Junyan Xu]

Module.compHom exists but it can't be made an instance for obvious reasons (no way to infer S, even if the RingHom is replaced by Algebra).

[Adam Topaz]

docs#Module.restrictScalars never mind… that’s for ModuleCat and it indeed restricts scalars with what Junyan suggested