SMul borks with SubNegMonoid

Stream: new members

[Arien Malec]

I'm back at pushing through Linear Algebra Done Right, after getting a bit discouraged before the holiday.

Right now, I want vectors that subtract, but I've discovered that if I do:

import Mathlib.Algebra.Module.Basic
import Mathlib.Data.Real.Basic

variable (V: Type _)
variable [SubNegMonoid V] [AddCommMonoid V] [Module ℝ V]

variable (r: ℝ) (v: V)
#check r • v

I get

failed to synthesize instance
  HSMul ℝ V ?m.120

But this works just fine without the assertion [SubNegMonoid V] -- is there a different typeclass I should be using for an additive commutative monoid with negation and subtraction?

[Arien Malec]

(In addition to that, is there any documentation for the tower of algebraic typeclasses in Mathlib?)

[Arien Malec]

Ah, scratch that, I've discovered SubtractionCommMonoid -- was looking for SubCommMonoid on the analogy of SubNegMonoid

[Eric Rodriguez]

You had two additive structures on your V, I think

[Kevin Buzzard]

If you're trying to say "let V be an R-vector space" then it's just variable (V : Type*) [AddCommGroup V] [Module ℝ V]

[Arien Malec]

I need the vectors to subtract.

[Riccardo Brasca]

AddCommGroup V implies you can do subtraction.

[Arien Malec]

But not negation?

[Eric Rodriguez]

You should be able to, yes.

[Riccardo Brasca]

Yes, you can also negate

[Jireh Loreaux]

Arien, try this:

import Mathlib

variable {V : Type*} [AddCommGroup V]

#synth SubtractionCommMonoid V

This will tell you that AddCommGroup has an instance of SubtractionCommMonoid

[Riccardo Brasca]

variable (V: Type*) [AddCommGroup V] [Module ℝ V] is the translation of "let $V$ be an $\mathbb{R}$ vector space"

[Arien Malec]

Yeesh, I must have gone wrong somewhere else then.

[Arien Malec]

import Mathlib.Algebra.Module.Basic
import Mathlib.Data.Real.Basic

variable (V: Type _)
variable [AddCommMonoid V] [Module ℝ V]

variable (r: ℝ) (v: V)
#check -v

failed to synthesize instance Neg V

[Jireh Loreaux]

Monoid ≠ Group

[Arien Malec]

Lightbulb goes on.

[Jireh Loreaux]

(Aside: you should write V : Type*, not V : Type _ because of performance reasons; likely this is minor, but it's worth getting into that habit.)

[Arien Malec]

Ah, I thought Type* was a Lean3ism.

[Jireh Loreaux]

Originally it was, but then we found out there were issues, and so we added Type* back in. Basically, Type _ creates a metavariable for the universe level whereas Type* creates an fresh universe level as an implicit variable. The problem with the former is that Lean sometimes has to solve universe constraints that arise because of the metavariables, and that takes time. However, most of the time we just want all our universes to be arbitrary, so we actually want the Type* behavior. It is rare that this is not the case, at least in most of the library (exceptions probably includ things involving Cardinal or Category).