Issue with Module.neg_one_smul?

Stream: new members

[Arien Malec]

What's the issue here?

import Mathlib.Algebra.Module.Basic

variable [Field F] [AddCommGroup V] [Module F V]

example {a: V}: -1 • a = -a := neg_one_smul a

I get a universe issue with a

application type mismatch
  @neg_one_smul a
argument
  a
has type
  V : Type ?u.718
but is expected to have type
  Type ?u.2678 : Type (?u.2678 + 1)

Being explicit about the universes of F and V doesn't work either...

[llllvvuu]

According to by exact? you should use neg_one_zsmul instead of neg_one_smul. I believe the error message represents not a universe issue but a unification issue. Or perhaps you mean to cast the -1:

example (a: V) : (-1 : F) • a = -a := neg_one_smul F a

[Shreyas Srinivas]

import Mathlib

variable [Field F] [AddCommGroup V] [Module F V]

example {a: V}: -1 • a = -a := neg_one_smul ℤ a

[Shreyas Srinivas]

The ring type parameter (ℤ) of neg_one_smul is not implicit. That's the error

[Shreyas Srinivas]

I suspect you mean what @llllvvuu wrote, but in your statement, the {a : V} doesn't affect that the type of (-1) is inferred ℤ since it is a negated numeric literal.

[Arien Malec]

Huh... This works:

example {a: V}: (-1 : F) • a = -a := neg_one_smul F a

[Arien Malec]

Ah, which is what @llllvvuu wrote...

[Arien Malec]

I guess I don't understand why R is explicit and M is implicit here...

[llllvvuu]

M is inferred from a which is inferred from {a : V}

[Arien Malec]

It's intentional, or at least seems so:

variable (R)

theorem neg_one_smul (x : M) : (-1 : R) • x = -x := by simp
#align neg_one_smul neg_one_smul

variable {R}

[llllvvuu]

The reason most likely is that, if I were to have neg_one_smul a in a vacuum, it would be ambiguous what the return type should be

[Arien Malec]

I see this is a common pattern in the foo_smul theorems. I guess I could naively expect an error that the inferred type of -1 doesn't match the module's type, but I'd expect that specifying that type would Just Work rather than having to specify it twice. :man_shrugging:

[Arien Malec]

Weirdly I can make R implicit and recompile Mathlib with no issues...

[Arien Malec]

And when I do so, the code above works... -1 is naively inferred as ℤ which works, but if I specify F, it also works correctly.

[Yaël Dillies]

Not all carefully chosen arguments are used in mathlib, but here the intent is certainly to keep the argument explicit.