question about design of Module

Stream: general

[Tomas Skrivan]

Why I have to separately introduce AddCommMonoid M and Module R M when I want to have a module M? Why Module R M does not extend AddCommMonoid M ?

Is this because I might want to have Module R M and Module S M ? and this would introduce two different additions on M and that would be a problem?

I'm just wondering to what kind of trouble I'm getting into if I just introduce a class

class Vec (K : Type _) [IsROrC K] (X : Type _)
  extends
    AddCommGroup X,
    Module K X,
    TopologicalSpace X,
    TopologicalAddGroup X

as my library really does not care about so much generality. However, at some point I might want to consider X as complex vector space and as real vector space at the same time.

[Kevin Buzzard]

Yes you definitely want things to be modules over more than one ring, for example the complexes are a 1D vector space over the complexes and also a 2D vector space over the reals

[Eric Wieser]

https://arxiv.org/pdf/2202.01629.pdf#page=8 (section 5.1) has an explanation of this example

[Tomas Skrivan]

Ahh I should read this pdf every sunday before lunch for couple of months straight. It contains so much wisdom and I always seem to forget it/it does not stick until I need it.

[Tomas Skrivan]

Interestingly, with [NormedField K] the class Vec warns me with cannot find synthesization order for instance Vec.toAddCommGroup with type, but with [IsROrC K] this does not happen because K is marked as semiOutParam. I wander if Vec.toAddCommGroup is still dangerous in that case.

[Jireh Loreaux]

No, it wouldn't be dangerous if you restrict to IsROrC because that class only has two instances (per the name). So it can't send Lean on a wild goose chase.

[Tomas Skrivan]

I'm still worried that Vec ℝ X and Vec ℂ X would introduce two different additions on X, but probably those will be defeq and I do not have to worry about it.

I really do not want to define Vec as

class Vec (K : Type _) [IsROrC K] (X : Type _) [AddCommGroup X] [TopologicalSpace X] [TopologicalAddGroup X]
  extends
    Module K X,
    ContinuousSMul K X

It is tedious to write and makes type signature of every function that depends on few Vec super long and unreadable.

[Patrick Massot]

This is also explained in the hierarchy chapter of Mathematics in Lean.

[Yury G. Kudryashov]

While AddCommGroup instances may be defeq in all your applications, if you write [Vec K X] [Vec K' X], there is no guarantee that AddCommGroup projections agree.

[Denis Gorbachev]

Solution for "Cannot find synthesization order" (for those coming from search)