Definition of quiver mutation

Stream: lean4

[Zheyuan Dong]

I'm trying to define quiver mutation with lean. But in my code below, it shows error failed to synthesize type class instance in line "if a = j ∧ Q.arrows j b > 0 then 0" and three lines below that.
structure quiver (vertex : Type) :=
(arrows : vertex → vertex → ℕ)
(connected_to_j (j: vertex): ∀ (v : vertex), v ≠ j → arrows v j + arrows j v > 0)
(no_circles_of_length_1 : ∀ (v : vertex), arrows v v = 0)
(no_circles_of_length_2 : ∀ (v1 v2 : vertex), v1 ≠ v2 → arrows v1 v2 = 0 → ∀ (v3 : vertex), ¬(arrows v1 v3 = 1 ∧ arrows v3 v2 = 1))

def quiver_mutate {V : Type} (j : V) (Q : quiver V) : quiver V :=
{ arrows := λ a b,
if a = j ∧ Q.arrows j b > 0 then 0
else if a = j ∧ Q.arrows b j >0 then Q.arrows b a
else if b = j ∧ Q.arrows a j >0 then 0
else if b = j ∧ Q.arrows j a >0 then Q.arrows b a
else if Q.arrows a j >0 ∧ Q.arrows j b >0 ∧ Q.arrows a b > 0 then Q.arrows a b + (Q.arrows a j) * (Q.arrows j b)
else if Q.arrows a j >0 ∧ Q.arrows j b >0 ∧ Q.arrows a b = 0 ∧ Q.arrows b a > (Q.arrows a j) * (Q.arrows j b) then 0
else if Q.arrows a j >0 ∧ Q.arrows j b >0 ∧ Q.arrows a b = 0 ∧ Q.arrows b a < (Q.arrows a j) * (Q.arrows j b) then (Q.arrows a j) * (Q.arrows j b) - Q.arrows b a
else if Q.arrows j a >0 ∧ Q.arrows b j >0 ∧ Q.arrows a b = 0 then 0
else if Q.arrows j a >0 ∧ Q.arrows b j >0 ∧ Q.arrows a b > 0 ∧ Q.arrows a b > (Q.arrows j a) * (Q.arrows b j) then Q.arrows a b - (Q.arrows j a) * (Q.arrows b j)
else if Q.arrows j a >0 ∧ Q.arrows b j >0 ∧ Q.arrows a b > 0 ∧ Q.arrows a b < (Q.arrows j a) * (Q.arrows b j) then 0
else Q.arrows a b
}
What might be the problem, thanks.

[Kevin Buzzard]

Can you please use #backticks to display lean code?

[Zheyuan Dong]

Sure. It is my first time to use the society, sorry for the inconvenience to your reading.

structure quiver (vertex : Type) :=
(arrows : vertex → vertex → ℕ)
(connected_to_j (j: vertex): ∀ (v : vertex), v ≠ j → arrows v j + arrows j v > 0)
(no_circles_of_length_1 : ∀ (v : vertex), arrows v v = 0)
(no_circles_of_length_2 : ∀ (v1 v2 : vertex), v1 ≠ v2 → arrows v1 v2 = 0 → ∀ (v3 : vertex), ¬(arrows v1 v3 = 1 ∧ arrows v3 v2 = 1))

def quiver_mutate {V : Type} (j : V) (Q : quiver V) : quiver V :=
{ arrows := λ a b,
    if a = j ∧ Q.arrows j b > 0 then 0
    else if a = j ∧ Q.arrows b j >0 then Q.arrows b a
    else if b = j ∧ Q.arrows a j >0 then 0
    else if b = j ∧ Q.arrows j a >0 then Q.arrows b a
    else if Q.arrows a j >0 ∧ Q.arrows j b >0 ∧ Q.arrows a b > 0 then Q.arrows a b + (Q.arrows a j) * (Q.arrows j b)
    else if Q.arrows a j >0 ∧ Q.arrows j b >0 ∧ Q.arrows a b = 0 ∧ Q.arrows b a > (Q.arrows a j) * (Q.arrows j b) then 0
    else if Q.arrows a j >0 ∧ Q.arrows j b >0 ∧ Q.arrows a b = 0 ∧ Q.arrows b a < (Q.arrows a j) * (Q.arrows j b) then (Q.arrows a j) * (Q.arrows j b) - Q.arrows b a
    else if Q.arrows j a >0 ∧ Q.arrows b j >0 ∧ Q.arrows a b = 0 then 0
    else if Q.arrows j a >0 ∧ Q.arrows b j >0 ∧ Q.arrows a b > 0 ∧ Q.arrows a b > (Q.arrows j a) * (Q.arrows b j) then Q.arrows a b - (Q.arrows j a) * (Q.arrows b j)
    else if Q.arrows j a >0 ∧ Q.arrows b j >0 ∧ Q.arrows a b > 0 ∧ Q.arrows a b < (Q.arrows j a) * (Q.arrows b j) then 0
    else Q.arrows a b
}

[Kevin Buzzard]

Can you post the error? I suspect that you've not posted precisely the relevant part. Guessing: does open_locale classical fix it?

[Zheyuan Dong]

Thanks, that can be solved. But there is still en error which has not been mentioned. In the line { arrows := λ a b, ,there shows arrow invalid structure value { ... }, field 'hom' was not providedandinvalid structure value { ... }, 'arrows' is not a field of structure 'quiver'
But I don't know why arrows must be a field?

[Adam Topaz]

Are you somehow also importing mathlib's quivers?

[Kevin Buzzard]

You should post a #mwe but Adam's suggestion seems to fit exactly with the symptoms

[Zheyuan Dong]

import combinatorics.quiver.basic.
Is that right? I found it is different in defining quivers. Maybe I should rewrite the definition of arrow in the corresponding environment.
Thank you very much!!!

[Kevin Buzzard]

That doesn't look like a lean 4 import. Are you posting in the right stream?

[Kevin Buzzard]

There is #mathlib4 if you are importing mathlib code and #maths if this is a lean 3 question

[Zheyuan Dong]

Maybe I use lean 3? And I should download lean4 instead?

[Alex J. Best]

Using Lean 3 is fine, and right now possibly better for this application. We just have separate streams for discussing these topics here is all

[Kevin Buzzard]

It's up to you which one you use, both can do quivers, but if this is a question involving mathlib then this stream is not the right place. I suggest you decide which one you want to use and then start a new thread posting a #mwe of your question

[Zheyuan Dong]

Thanks for your advice. If I have some problem, I will choose the right stream.