cannot find synthesization order for instance

Stream: new members

[Ali Ramsey]

Hi, I'm trying to show that a module M over a k-algebra A is also a vector space over k, but I keep getting the error in the title. My code so far is

instance {F : Type u₁} [Field F] {H : Type u₂} [Ring H] [Algebra F H] {M : Type u₃} [AddCommGroup M] [Module H M] : Module F M where

I've tried permuting the orders of things around a bit, but nothing seems to make a difference...

[Junyan Xu]

This can't be an instance since Lean has no way to figure out what H is looking only at the goal Module F M. However, if you bake H into the type M, then it can be an instance, see docs#RestrictScalars.module. If you don't want to change the type M, you can use docs#Module.compHom, which is a def as it can't be an instane, and it's used to define docs#ModuleCat.RestrictScalars.obj'.

By the way, the usual mathlib way to work in your situation is

instance {F H M} [Field F] [Ring H] [Algebra F H] [AddCommGroup M] [Module F M] [Module H M] [IsScalarTower F H M]

but it depends on your purposes.

[Ali Ramsey]

Thank you! I was trying to make an instance because I'm trying to show that the category A-mod has a monoidal structure (imitating the way the monoidal structure of R-mod is built up in ModuleCat.Monoidal.Basic), but when I started with something like

def tensorObj' {F : Type u₁} {H : Type u₂} [Field F] [Ring H] [Algebra F H] (M N : ModuleCat H) : ModuleCat H :=
  ModuleCat.of H (M ⊗[F] N)

I would get the error failed to synthesize instance Module F ↑M so I figured Lean didn't know M was also a vector space over F. I've now changed it to be

def tensorObj' {F : Type u₁} {H : Type u₂} [Field F] [Ring H] [Algebra F H] (M N : ModuleCat H) [Module F M] [Module F N] [IsScalarTower F H M] [IsScalarTower F H N] : ModuleCat H :=
  ModuleCat.of H (M ⊗[F] N)

which doesn't throw any errors, but it just seems a little strange to have something like [Module F M] which looks like an assumption when it should just be true. Am I going about this the right way?

[Eric Wieser]

I think you might need a dedicated AModuleCat R A type

[Eric Wieser]

You'll need it anyway for the monoidal structure to be unambiguous against the existing one

[Kevin Buzzard]

You can think of [Module F M] as "initialise the notation f • m" and [IsScalarTower F H M] to mean "and furthermore define f • m to mean the obvious thing".

[Eric Wieser]

Something like

structure AModuleCat (R A : Type*) [CommRing R] [Ring A] [Algebra R A] extends ModuleCat A where
   toBaseModule : Module R carrier
   tower : IsScalarTower R A carrier

attribute [instance] AModuleCat.toBaseModule AModuleCat.tower

[Eric Wieser]

Maybe @Scott Morrison can tell you if that's reasonable

[Eric Wieser]

You should then be able to copy the approach used by docs#QuadraticModuleCat.instMonoidalCategory to get the monoidal category on AModuleCat