Timeouts with Ext

Stream: maths

[Amelia Livingston]

Hiya! Could anyone explain why I get timeouts whenever I try and use Ext :( for example:

import category_theory.abelian.ext
universes v u
open category_theory
noncomputable theory
variables (R : Type u) [ring R] (C : Type u) [category.{u} C] [abelian C] [linear R C]
  [enough_projectives C] (n : ℕ) (X : Cᵒᵖ) (Y : C)

def Ext_def : ((Ext R C n).obj X).obj Y ≅
  (((linear_yoneda R C).obj Y).right_op.left_derived n).left_op.obj X := sorry

I've been working around this by just using the thing on the RHS instead of the whole functor, but I'm getting other timeouts now that are possibly related.
Apologies if there's information about use of Ext elsewhere in the chat - I don't know how to search case-sensitively and there are a lot of results for ext :)

Edit: I couldn't reproduce this in online Lean so I thought updating my mathlib would fix it, but it hasn't (phew, this post isn't pointless). Hence resolving/unresolving the topic.

[Notification Bot]

Amelia Livingston has marked this topic as resolved.

[Notification Bot]

Amelia Livingston has marked this topic as unresolved.

[Adam Topaz]

Just to confirm -- I'm getting the same issue on my machine.

[Adam Topaz]

But lean is happy if you fill in the sorry

def Ext_def : ((Ext R C n).obj X).obj Y ≅
  (((linear_yoneda R C).obj Y).right_op.left_derived n).left_op.obj X := eq_to_iso rfl

[Amelia Livingston]

oh wow! thank you!

[Adam Topaz]

I don't know why it times out with the sorry though... it's not great.

[Adam Topaz]

I hope someone who knows how to troubleshoot timeouts better than me will chime in.

[Eric Rodriguez]

this seems to be the lemma/def sorry issue; make it a lemma until you fill it in

[Bryan Gin-ge Chen]

Is this lemma/def sorry issue documented somewhere? (If I've heard of it before, I've already forgotten about it...)

[Eric Rodriguez]

not sure, it definitely should be. the idea is that lemma doesn't try to be clever about the type (I want to say elaborate but not sure) but def can make it dependent on the output, so for example def my_def : 1 = 1 := @rfl rat 1 should work, but I don't think the same would work for a lemma

[Amelia Livingston]

thank you very much! I've met this issue in other contexts without realising it...

[Reid Barton]

eq_to_iso rfl is better known as the identity map right? or does that not work for some reason?

[Kevin Buzzard]

Does the force_noncomputable trick solve this issue?

[Adam Topaz]

If you replace the iso symbol with equality then there is no issue (and the two sides are defeq). I haven't tried manually filling in the structure fields with identity, but I suppose that would work as well.

[Amelia Livingston]

maybe I should rename this topic to "lemma/def sorry issue"? unfortunate that it's in #maths

[Reid Barton]

ah I guess I meant docs#category_theory.iso.refl

[Eric Wieser]

Maintainers can move messages between streams (out of #maths) if you ask :)