is_iso dist triang

Stream: Is there code for X?

[Adam Topaz]

I just want to verify that we don't have the following lemma
https://stacks.math.columbia.edu/tag/014A
before I start using docs#category_theory.abelian.is_iso_of_is_iso_of_is_iso_of_is_iso_of_is_iso :)

[Adam Topaz]

Ping @Andrew Yang @Johan Commelin @Matthew Ballard

[Matthew Ballard]

I just thought that name was a joke...

[Adam Topaz]

That's the five lemma :rofl:

[Andrew Yang]

I don’t think we have that yet

[Adam Topaz]

Okay. I'll prove it later today. I already added the stub to LTE.

[Matthew Ballard]

I think you need to know that $\operatorname{Hom}(X,-)$ is homological as a prereq to stacks#014A

[Adam Topaz]

We did that last week!

[Matthew Ballard]

Is it in mathlib? :stuck_out_tongue:

[Adam Topaz]

Ah, no.

[Adam Topaz]

@Andrew Yang how's it going with projective replacements? Did you see some of the stuff in the recent for_mathlib/derived folder from LTE?

[Matthew Ballard]

I think that is the main missing piece. The rest is Yoneda + repeat 5 is_iso

[Andrew Yang]

All the data are constructed but I’m struggling to show that it is quasi iso despite having finished all the diagram chasing parts because of some dependent type issues. I have a busy day tomorrow, so I hope I’ll be able to finish it the day after.

[Andrew Yang]

I noticed there’s quite a lot going on in that directory, but I have yet to look into it.

[Adam Topaz]

We defined is_quasi_iso there. It would be useful to know how you formulate boundedness so that I can add that condition to one of the theorems

[Andrew Yang]

There’s also docs#quasi_iso that seems to have the same definition.
For boundedness I simply used
“forall i > a, is_iso (0 : X.X i -> 0)”
(sorry, on a phone now)

[Adam Topaz]

Ah ok. Yeah, the one in for_mathlib/derived is for the homotopy category, but it's essentially the same yes.