Expected type is Type (?u.7012 + 1)?

Stream: new members

[Ryan Smith]

Why am I getting a type error that expects type (whatever) + 1?

import Mathlib
universe u

open LinearMap
variable {G : Type} [Group G] [Finite G]

-- goal not important for debugging
lemma temp (V : FDRep ℂ G) (g : G) : V.character g = 42 := by
  simp only [FDRep.character]
  rw [trace_eq_matrix_trace (V.ρ g)]

This gives the confusing type error

Application type mismatch: The argument
  V.ρ g
has type
  ↑V.V →ₗ[ℂ] ↑V.V
of sort `Type` but is expected to have type
  Type ?u.7012
of sort `Type (?u.7012 + 1)` in the application
  @trace_eq_matrix_trace (V.ρ g)

[Aaron Liu]

docs#LinearMap.trace_eq_matrix_trace wants to eat the base ring first (that's ℂ)

[Aaron Liu]

then it eats an R-basis for M (a ℂ-basis for ↑V.V)

[Aaron Liu]

then it eats the linear map (that's V.ρ g)

[Ryan Smith]

Sort of related question, for getting a basis b for that function what is the proper way?

rcases Basis.exists_basis ℂ V with ⟨b, hb⟩
-- produces
b : Set ↑V.V
hb : Nonempty (Basis ↑b ℂ ↑V.V)

The hypothesis hb is not that b is a basis, but there some basis exists using the set b? How do you summon a basis?

[Ryan Smith]

I partially answered my own question about the basis, we need another level of unpacking for rcases

lemma temp (V : FDRep ℂ G) (g : G) : V.character g = 42 := by
  simp only [FDRep.character]
  rcases Basis.exists_basis ℂ V with ⟨setb, ⟨b⟩⟩
  rw [trace_eq_matrix_trace ℂ b (V.ρ g)]

What does failed to synthesize DecidableEq ↑setb mean?

[Kenny Lau]

Ryan Smith said:

confusing type error

it's not very confusing, if you ignore the two "sorts", it's saying V.ρ g has type ↑V.V →ₗ[ℂ] ↑V.V but is expected to have type Type ?u.7012

[Kenny Lau]

in other words, it's expecting a type but you gave it a linear map

[Ryan Smith]

I think we fixed that first problem, now it is complaining about failing to synthesize DecideableEq? This is the signature of the method that I see:

LinearMap.trace_eq_matrix_trace.{u, v, w} (R : Type u) [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M]
{ι : Type w} [DecidableEq ι] [Fintype ι] (b : Basis ι R M) (f : M →ₗ[R] M) : (trace R M) f = ((toMatrix b b) f).trace

So we need three parameters: our commutative ring ℂ, the statement that we have a basis b, and a linear map. #check V.ρ g shows that our third argument is indeed a linear map V.ρ g : ↑V.V →ₗ[ℂ] ↑V.V.

This seems like we have the correct types for all three variables? I am confused as to what it is unhappy about?

[Kevin Buzzard]

If Lean is complaining that it can't find DecidableEq foo then just add [DecidableEq foo] as a hypothesis. This is some constructivist nonsense but apparently we're stuck with it.

[Robin Arnez]

In this case, using the classical tactic might be useful too (since the Decidable is only needed in the body)

[Ryan Smith]

Could both of you elaborate on how that works specifically? Am I trying to prove something "by classical"? And for adding DecidableEq as a hypothesis, how are we justifying that to lean (surely not a sorry) and how are passing it as an argument to trace_eq_matrix_trace?

[Kenny Lau]

basically write:

theorem ... : ... := by
  classical
  simp [foo1, foo2]

[Kenny Lau]

the way to know if you need an extra [DecidableEq Foo] argument, or if you need classical, is this:

• if the statement doesn't compile, add [DecidableEq Foo]
• if it's only the proof that complains, use classical

[Ryan Smith]

Classical doesn't fix it. What does classical do normally? I have read the docs for it but found them fairly confusing in that case.

In this case the thing which it complains about is that the set of basis vectors which is introduced part way through the lemma can't synthesize DecideableEq. So what does [DecidableEq foo] mean in this particular context here?

lemma temp (V : FDRep ℂ G) (g : G) : V.character g = 42 := by
  simp only [FDRep.character]
  rcases Basis.exists_basis ℂ V with ⟨setb, ⟨b⟩⟩
  rw [trace_eq_matrix_trace ℂ b (V.ρ g)]  -- failed to synthesize DecidableEq ↑setb

[Aaron Liu]

did you try

lemma temp (V : FDRep ℂ G) (g : G) : V.character g = 42 := by
  classical
  simp only [FDRep.character]
  rcases Basis.exists_basis ℂ V with ⟨setb, ⟨b⟩⟩
  rw [trace_eq_matrix_trace ℂ b (V.ρ g)] -- hopefully no error or a different error

[Ryan Smith]

Yes I tried , full working example:

import Mathlib
universe u

open LinearMap
open Module Module.End

variable {G : Type} [Group G] [Finite G]

lemma temp (V : FDRep ℂ G) (g : G) : V.character g = 42 := by
  classical
  simp only [FDRep.character]
  rcases Basis.exists_basis ℂ V with ⟨setb, ⟨b⟩⟩
  rw [trace_eq_matrix_trace ℂ b (V.ρ g)]  -- no change

[Aaron Liu]

so there's a different error now

[Aaron Liu]

failed to synthesize
  Fintype ↑setb

[Aaron Liu]

definitely not no change

[Ryan Smith]

You're right. In general failure to synthesize just means "lean can't figure out how to justify some requirement"?

So that is it being unhappy it doesn't know why the basis is finite?

[Ryan Smith]

Is the correct way to handle this to pass a 4th argument to the trace_eq_matrix_trace method somehow? It makes sense in a way that I started with a finite dim vector space but called a function which doesn't require finite dim so the resulting basis has no assumption of finiteness on the index set, but if the theorem I want to invoke doesn't require that as an argument how do we communicate it?