shifting triangles

Stream: condensed mathematics

[Adam Topaz]

Do we have anywhere a has_shift instance for triangle C?

[Johan Commelin]

You just pushed something, right?

[Johan Commelin]

cc @Andrew Yang

[Andrew Yang]

I don’t think so

[Adam Topaz]

Okay, yeah, I pushed a stub for this with only a few sorrys.

[Adam Topaz]

https://github.com/leanprover-community/lean-liquid/blob/master/src/for_mathlib/triangle_shift.lean

[Adam Topaz]

What I'm really after is this:

lemma shift_of_dist_triangle (T : triangle C) (hT : T ∈ dist_triang C) (i : ℤ) :
  T⟦i⟧ ∈ dist_triang C := sorry

[Matthew Ballard]

Is there an action of shift defined on triangle Calready?

[Adam Topaz]

See link above

[Johan Commelin]

How is the API for bundled triangles working out? I was a bit afraid that it would be painful, and we would need an unbundled version.

[Johan Commelin]

But I haven't worked enough with it yet to know what's best. I would be interested to hear what @Adam Topaz @Andrew Yang @Matthew Ballard think.

[Adam Topaz]

It seems fine!

[Adam Topaz]

But homology, still not so much... E.g.

def homology_shift_iso (X : 𝒦) (i : ℤ) :
  (homotopy_category.homology_functor _ _ 0).obj (X⟦i⟧) ≅
  (homotopy_category.homology_functor _ _ i).obj X :=
sorry

[Adam Topaz]

This whole game of d_from and d_to gets old really fast.

[Andrew Yang]

I have not met an issue with the current triangle API yet.

[Matthew Ballard]

I don't know enough to have opinions

[Johan Commelin]

Adam Topaz said:

This whole game of d_from and d_to gets old really fast.

At the same time, we need to do something... Unless we drop support for ℕ-indexed complexes. I think a unified definition that also works for index 0 : ℕ has benefits.

[Johan Commelin]

But I agree that it's annoying.

[Andrew Yang]

Adam Topaz said:

This whole game of d_from and d_to gets old really fast.

I have to say that they are quite frustrating to work with. I struggled with these problems so hard when constructing projective resolutions that I just gave up and some point and used heq and congr extensively to force out an iso. In particular these two proofs

This might be an option here as well.

[Johan Commelin]

Adam Topaz said:

But homology, still not so much... E.g.

def homology_shift_iso (X : 𝒦) (i : ℤ) :
  (homotopy_category.homology_functor _ _ 0).obj (X⟦i⟧) ≅
  (homotopy_category.homology_functor _ _ i).obj X :=
sorry

In this example, can you just conjugate with some homology_iso_kernel_mod_image isomorphism that hopefully exists already?

[Adam Topaz]

I don't think so... the issue is that one side is the homology of X[[i]].d_to 0 and X[[i]].d_from 0, and the other is X.d_to i and X.d_from i.

[Andrew Yang]

Is it possible to make d_from, d_to, X_prev, X_next as fields of complex_shape along with proofs that they are right to make things definitionally easier to work with?

[Adam Topaz]

That would help with some of the eq_to_hom nonsense that's involved.

[Matthew Ballard]

Would defining the n-th homology as the zeroth homology of the shift be any better?

[Johan Commelin]

Andrew Yang said:

Is it possible to make d_from, d_to, X_prev, X_next as fields of complex_shape along with proofs that they are right to make things definitionally easier to work with?

What do you mean exactly?

[Johan Commelin]

Matthew Ballard said:

Would defining the n-th homology as the zeroth homology of the shift be any better?

That doesn't work for ℕ-indexed complexes, right?

[Johan Commelin]

Or for complexes indexed by something without a 0.

[Andrew Yang]

Also, this might be helpful in these contexts

noncomputable
def foo {ι : Type*} {c : complex_shape ι} (X : homological_complex V c) (i j k : ι)
  (r₁ : c.rel i j) (r₂ : c.rel j k) :
  (homology_functor V c j).obj X ≅ homology _ _ (X.d_comp_d i j k) :=
sorry

[Matthew Ballard]

You would need some garbage values below 0. Without 0, I wouldn't know what to do

[Johan Commelin]

Adam Topaz said:

I don't think so... the issue is that one side is the homology of X[[i]].d_to 0 and X[[i]].d_from 0, and the other is X.d_to i and X.d_from i.

I don't understand why that causes a problem. Conjugating with such an isomorphism would leave you with an _ in the middle where you need to build an iso from the homology of X[[i]].d (-1) 0 and X[[i]].d 0 1 to the homology of X.d (i-1) i and X.d i (i+1).

[Johan Commelin]

Yeah, that foo from Andrew is exactly the iso that I'm talking about.

[Andrew Yang]

Johan Commelin said:

What do you mean exactly?

I meant something like this

structure complex_shape (ι : Type*) :=
(rel : ι → ι → Prop)
(next_eq : ∀ {i j j'}, rel i j → rel i j' → j = j')
(prev_eq : ∀ {i i' j}, rel i j → rel i' j → i = i')
(prev_X : ∀ (X : ι → V) (i : ι), V)
(prev_X_eq₁ : ∀ (X : ι → V) (i j : ι), rel j i → prev_X X i = X j)
(prev_X_eq₂ : ∀ (X : ι → V) (i : ι), (¬ ∃ j, rel j i) → prev_X X i = 0)
(d_to : ∀ (X : ι → V) (d : ∀ (i j : ι), X i ⟶ X j) (i : ι), prev_X X i → X i)
(d_to_eq₁ : ∀ (X : ι → V) (d : ∀ (i j : ι), X i ⟶ X j) (i j : ι) (r : rel j i),
  d_to X d i = eq_to_hom (prev_X_eq₁ X i j r) ≫ d j i)
(d_to_eq₂ : ∀ (X : ι → V) (d : ∀ (i j : ι), X i ⟶ X j) (i j : ι),
  (¬ ∃ j, rel j i) → d_to X d i = 0)

[Andrew Yang]

So that at least X.prev_X i can be defeq to X.X (i-1) when we need it to.

[Johan Commelin]

But what is V? You want to quantify over all categories?

[Andrew Yang]

Oh :(

[Andrew Yang]

That might still be an option though, if people doesn't care about complex_shape living in an unreasonably large universe. :grimacing:

[Johan Commelin]

Hmm... I think I would prefer to stick to the universe of ι. If you have a functor between two categories in different universes, then your definition would be in trouble. At least, you wouldn't be able to use the same complex_shape for complexes with values in either category.

[Adam Topaz]

Andrew Yang said:

Also, this might be helpful in these contexts

noncomputable
def foo {ι : Type*} {c : complex_shape ι} (X : homological_complex V c) (i j k : ι)
  (r₁ : c.rel i j) (r₂ : c.rel j k) :
  (homology_functor V c j).obj X ≅ homology _ _ (X.d_comp_d i j k) :=
sorry

Okay, I added this iso.

[Adam Topaz]

uuughhhh.... we also have to contend with the fact that shifting includes a $(-1)^i$.

[Johan Commelin]

Does Lean understand (-1) ^ i • iso.refl _?

[Adam Topaz]

I doubt it

[Adam Topaz]

Well, I didn't get around to obtaining the homology/shift isomorphism, but

lemma hom_K_projective_bijective {X Y : 𝒦} (P : 𝒦) [is_K_projective P]
  (f : X ⟶ Y) [hf : is_quasi_iso f] : function.bijective (λ e : P ⟶ X, e ≫ f) :=

is done (modulo that isomorphism)

If anyone wants to work on that isomorphism, it's here:

def homology_shift_iso (i : ℤ) :
  category_theory.shift_functor 𝒦 i ⋙
  homology_functor A (complex_shape.up ℤ) 0 ≅
  homology_functor A (complex_shape.up ℤ) i := sorry

In the file for_mathlib/derived/K_projective.lean.

The useful isomorphism that Andrew suggested is available (sorry-free) in for_mathlib/homology_iso.lean.

[Adam Topaz]

Concerning shifting triangles: What's the convention regarding $(-1)^n$?
Note that if $T$ is a triangle, then by defining $T[1]$ to include a negation on the morphisms, that would match T.rotate.rotate.rotate. Is this the right thing to do? What about shifting morphisms of triangles?

Maybe a more important question: does it really matter?

[Matthew Ballard]

The convention I follow is:

$$C[1]_i = C_{i+1}, d[1]_i = -d_{i+1}$$

for complexes. I though I saw the rotated triangles included adding a negation in to one of the terms?

[Adam Topaz]

Yeah, that's right.

[Adam Topaz]

But that's for complexes. What about shifting a whole triangle?

[Adam Topaz]

If we take the convention that, for a triangle $T = (A \to B \to C \to A[1])$ where $f : A \to B$, $g : B \to C$ and $h : C \to A[1]$ are the morphisms, that one has $T[1] = (A[1] \to B[1] \to C[1] \to A[2])$ with maps $-f[1]$, $-g[1]$ and $-h[1]$, then, with how we have rotation set up for triangles now, it would follow that $T[1]$ is the "same" as rotating three times.

[Adam Topaz]

OTOH, if we have a triangle $T = (A \to B \to C \to A[1])$ as above, and we apply some homological functor $H$, then we probably want to get the long exact sequence for $H$ by composing with $H(T[1])$, i.e.

$H(A) \to H(B) \to H(C) \to H(A[1]) \to H(B[1]) \to H(C[1]) \to H(A[2]) \to \cdots$

so in that sense we wouldn't want to negate (maybe?)

[Adam Topaz]

I'm confused.

[Matthew Ballard]

I usually take the action of shifts on triangles to have no signs but I am not the most careful. Neeman in his book takes the negative of all maps after one shift of the triangle (as you did) and mathlib adds in one negative at a time for a shift.

If you pretend a triangle is like a big cochain complex, then negating everything after one shift seems best. But I think anything can probably be made to work.

[Andrew Yang]

Adam Topaz said:

If anyone wants to work on that isomorphism, it's here:

I could work on that later today.

[Andrew Yang]

Should be done now.

[Adam Topaz]

Thanks!

[Adam Topaz]

@Andrew Yang I will add this lemma you wrote

lemma π'_ι : π' f g w ≫ ι f g w =
  kernel.ι _ ≫ cokernel.π _ :=
by { dsimp [π', ι, homology_iso_kernel_desc], simp }

to my PR #12171

I'm inclined to make it a simp lemma too. Any objections to tagging with simp?

[Adam Topaz]

Also re

-- we seem to be missing loads of simp lemmas :(

I think the issue is that most of the homology involves homology.map, which is kind of a pain to use. You can convert it to homology.desc' using homology.map_eq_left (or some other variant) and I think simp should be more effective like this.

[Adam Topaz]

Although simp only [category.assoc] seems to get stuck for some reason.

[Andrew Yang]

The main problem should be that the newly added maps does not have corresponding simp lemmas, and the erw are just unfolding them until homology.map or homology.desc' comes up.
IMO, I don't really find homology.map as quite a source of pain though.

[Adam Topaz]

Are there some lemmas that might be missing from #12171 that might be helpful?

[Adam Topaz]

If so I should add those before that PR gets merged.

[Andrew Yang]

I left some comments on the PR regarding my thoughts.
I also think π'_ι should be a simp lemma.

[Adam Topaz]

I'm perfectly happy with the renames (and it's already done), but I'm not convinced about the simp lemmas involving the isomorphism

[Adam Topaz]

I think the issue with this particular proof can be summarized in the fact that there is no good way to write a general simp lemma for the following

kernel.lift (d_from Y (j + i)) (kernel.ι (Y.d (j + i) (j + 1 + i))) _

because what's there is essentially a kernel.map, although in this special case it involves some eq_to_homs while in general you have to compose kernel.\iota with a map on the right to obtain the general form of kernel.map.

[Adam Topaz]

So I think a solution would be change the definition of homology_iso to use kernel.map, and prove a general simp lemma about homology.desc' _ _ _ (kernel.map _ _ _ _ _) _ \gg homology.\iota _ _ _ = ...

[Adam Topaz]

@Andrew Yang This seems to work with just one additional lemma about homology, and some dsimp lemma for the shift functor itself

@[simp, reassoc]
lemma homology.π'_ι {X Y Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : f ≫ g = 0) :
  homology.π' f g w ≫ homology.ι f g w = kernel.ι g ≫ cokernel.π f :=
by { delta homology.π' homology.ι homology_iso_kernel_desc, simp }

@[simp, reassoc]
lemma homology.desc'_ι {X X' Y Z Z' : A} (f : X ⟶ Y) (g : Y ⟶ Z) (w : f ≫ g = 0)
  (f' : X' ⟶ Y) (g' : Y ⟶ Z') (w' : f' ≫ g' = 0) (h₁) (h₂) (h₃) :
  homology.desc' _ _ w (kernel.lift _ (kernel.ι _) h₁ ≫ homology.π' _ _ _) h₂ ≫
  homology.ι _ _ w' = homology.ι _ _ _ ≫ cokernel.desc _ (cokernel.π _) h₃ :=
by { ext, simp, }

variable (A)

@[simp]
lemma foobar (V : Type*) [category V] [preadditive V] (i) :
  homological_complex.shift_functor V i = category_theory.shift_functor _ i := rfl

noncomputable
def homology_shift_iso (i j : ℤ) :
  shift_functor _ i ⋙ homology_functor A (complex_shape.up ℤ) j ≅
    homology_functor A (complex_shape.up ℤ) (j + i) :=
nat_iso.of_components (λ X, homology_shift_obj_iso X i j : _)
begin
  intros X Y f,
  ext,
  dsimp [homology_shift_obj_iso, homology_iso, homology.map_iso],
  simp,
end

[Adam Topaz]

Where would be the natural place for foobar?

[Adam Topaz]

In for_mathlib/homological_complex_shift?

[Adam Topaz]

Well, I'll just leave it there for now.

[Andrew Yang]

I think so.
What should the direction be?
If this is the correct direction, it probably means that homological_complex.shift_functor is probably an implementation detail and we should hide it better.
In particular, if every shift_functor in the definitions were changed into category_theory.shift_functor, would that proof work without the lemma?

[Adam Topaz]

I don't know which direction should be preferred. I suppose if we build a bunch of general API for general shift functors, then we should prefer category_theory.shift_functor.

[Adam Topaz]

We now have a more-or-less complete proof that Ext for complexes (well, bounded above complexes) is homological in both variables. That's essentially the LES in either variable (modulo some general shifting calculus which needs to be done).

[Adam Topaz]

I guess we also need to relate a SES of complexes to triangles, but that should be straightforward I hope.

[Kevin Buzzard]

Wow -- well done! What about Tor?

[Adam Topaz]

We can now (essentially) do most things that involve the bounded above derived category (in the case with enough projectives). If you want to give me a construction of tensor products of complexes, i will give you tor!

[Reid Barton]

Does that proof for Ext involve double complexes?

[Adam Topaz]

Not directly. I proved that Hom(-,-) is homological in both variables, and that (almost immediately) implies that Ext(-,-) is homological in the second var. For the first var, it involved showing that taking K-projective replacements of the terms of a distinguished triangle yields another distinguished triangle

[Adam Topaz]

I should mention that we still don't have the comparison with mathlib's Ext.

[Reid Barton]

oh maybe I don't actually know what these words mean

[Adam Topaz]

I should mention a huge thanks to @Andrew Yang for proving that projective replacements exist!

[Johan Commelin]

I'm working on

lemma shift_of_dist_triangle (T : triangle C) (hT : T ∈ dist_triang C) (i : ℤ) :
  T⟦i⟧ ∈ dist_triang C :=
begin
  induction i using int.induction_on with i IH i IH,
  { exact isomorphic_distinguished T hT _ (shift_zero _ _), },
  { suffices : T⟦(i+1 : ℤ)⟧ ≅ T⟦(i:ℤ)⟧.rotate.rotate.rotate,
    { refine isomorphic_distinguished _ _ _ this,
      repeat { refine rot_of_dist_triangle _ _ _ },
      exact IH },
    refine shift_add _ _ _ ≪≫ _,
    refine triangle.iso.of_components (iso.refl _) (-iso.refl _) (iso.refl _) _ _ _, -- we might need to do something more subtle here
    { dsimp, simp only [category.id_comp, category.comp_id, comp_neg, neg_neg], },
    { dsimp, simp only [category.id_comp, category.comp_id, neg_comp, neg_neg], },
    { dsimp, simp only [category.id_comp, category.comp_id, neg_comp, neg_neg],
      simp only [functor.map_comp, assoc, category_theory.functor.map_id, comp_id],
      -- getting stuck
 }, },
end

[Adam Topaz]

What's the goal here?

[Adam Topaz]

@Johan Commelin can you push what you have?

[Adam Topaz]

It's possible that the definition of the shift of a triangle by $i$ is missing some $(-1)^i$?

[Matthew Ballard]

suffices : T⟦(i+1 : ℤ)⟧ ≅ T⟦(i:ℤ)⟧.rotate.rotate.rotate,

[Matthew Ballard]

It looks like the signs haven't been adjusted for that

[Adam Topaz]

Isn't it enough to change

refine triangle.iso.of_components (iso.refl _) (-iso.refl _) (iso.refl _) _ _ _, -

to

refine triangle.iso.of_components (- iso.refl _) (iso.refl _) (- iso.refl _) _ _ _, -

???

[Adam Topaz]

ah, no the last square won't commutee.

[Adam Topaz]

Perhaps we need to do the following:

def triangle_shift_obj (T : triangle C) (i : ℤ) : triangle C :=
triangle.mk C
  ((shift_functor _ i).map T.mor₁)
  (((shift_functor _ i).map T.mor₂))
  (i.neg_one_pow • ((shift_functor C i).map T.mor₃ ≫ (shift_comm _ _ _).hom))

[Adam Topaz]

Or add a $(-1)^i$ to all three maps

[Matthew Ballard]

If I think of a triangle as like a complex then the $(-1)^i$ for all lines up

[Adam Topaz]

:face_palm: https://github.com/leanprover-community/lean-liquid/blob/a540ac19005bb6a786f925c695239c5698903fc9/src/for_mathlib/triangle_shift.lean#L21

[Matthew Ballard]

Yeah. That's how I remembered!

[Matthew Ballard]

Well commented code

[Adam Topaz]

Now where is that AI that will convert my comment into lean?

[Johan Commelin]

Adam Topaz said:

Johan Commelin can you push what you have?

Done

[Johan Commelin]

Is there a convention in the literature? Or do people typically not shift triangles at all, but just repeatedly rotate?

[Matthew Ballard]

Can you just say shifting a triangle by $i$ is rotating $3i$ as the definition?

[Johan Commelin]

That would lead to bad defeqs, I think

[Matthew Ballard]

The convention is to work $\mathbb{Z}/2\mathbb{Z}$ mentally

[Matthew Ballard]

But in googling around I found two different conventions for the signs for rotate as an example

[Adam Topaz]

Why do we negate in rotate again?

[Matthew Ballard]

stacks vs Neeman pg 30

[Johan Commelin]

Adam Topaz said:

Why do we negate in rotate again?

I think because we negate in f[1]. And we want to undo it. Because T.rotate should be the same "long sequence" as T, but just "literally shifted" one place.

[Matthew Ballard]

You have to choose some signs for the cone complex to be a complex. Adding in negative signs for the morphisms in a shift is the usual way

[Johan Commelin]

Otherwise you start to get signs appearing mod 3, which is probably bad.

[Matthew Ballard]

Does shift act with a sign on morphisms?

[Johan Commelin]

f⟦1⟧'.f i = -f.f (i+1) (unless that + should be a -)

[Matthew Ballard]

Just want to be sure I am clear: it negates the chain maps in addition to the differentials?

[Adam Topaz]

Okay, I'll try to add some $(-1)^i$ and see what breaks.

[Johan Commelin]

Matthew Ballard said:

Just want to be sure I am clear: it negates the chain maps in addition to the differentials?

Yes, I think that's what we have in mathlib atm.

[Johan Commelin]

Is that good or bad?

[Matthew Ballard]

Neither?

[Matthew Ballard]

It runs contra to Stacks

[Matthew Ballard]

If you want good interop with Stacks then I would probably hug them

[Johan Commelin]

Hmm, but the proof I'm working on is actually for arbitrary pretriangulated cats. It doesn't have anything to do with how shift is defined on complexes.

[Adam Topaz]

I pushed a WIP fix @Johan Commelin

[Adam Topaz]

@[simps]
def triangle_shift_obj (T : triangle C) (i : ℤ) : triangle C :=
triangle.mk C
  (i.neg_one_pow • ((shift_functor _ i).map T.mor₁))
  (i.neg_one_pow • (((shift_functor _ i).map T.mor₂)))
  (i.neg_one_pow • ((shift_functor C i).map T.mor₃ ≫ (shift_comm _ _ _).hom))

[Adam Topaz]

and

lemma shift_of_dist_triangle (T : triangle C) (hT : T ∈ dist_triang C) (i : ℤ) :
  T⟦i⟧ ∈ dist_triang C :=
begin
  induction i using int.induction_on with i IH i IH,
  { exact isomorphic_distinguished T hT _ (shift_zero _ _), },
  { suffices : T⟦(i+1 : ℤ)⟧ ≅ T⟦(i:ℤ)⟧.rotate.rotate.rotate,
    { refine isomorphic_distinguished _ _ _ this,
      repeat { refine rot_of_dist_triangle _ _ _ },
      exact IH },
    refine shift_add _ _ _ ≪≫ _,
    refine triangle.iso.of_components (iso.refl _) (iso.refl _) (iso.refl _) _ _ _,
    { dsimp, simp only [category.id_comp, category.comp_id, comp_neg, neg_one_smul], },
    { dsimp, simp only [category.id_comp, category.comp_id, neg_comp, neg_one_smul], },
    { dsimp, simp only [category.id_comp, category.comp_id, neg_comp, neg_one_smul],
      simp only [functor.map_comp, assoc, category_theory.functor.map_id, comp_id,
        functor.map_zsmul, preadditive.zsmul_comp, preadditive.comp_zsmul],
      congr' 2,
      sorry }, },
  sorry
end

[Adam Topaz]

This now looks doable.

[Matthew Ballard]

Johan Commelin said:

Hmm, but the proof I'm working on is actually for arbitrary pretriangulated cats. It doesn't have anything to do with how shift is defined on complexes.

Yeah. I think the conventions for a general one are less painful until you want to prove that the homotopy category of chain complexes is (pre)triangulated

[Johan Commelin]

Those last two sorrys are now filled in. So the shift of a distinguished triangle is distinguished.

[Johan Commelin]

Other sorries remain...

[Johan Commelin]

The remaining sorry's are horrible. Do people actually work with lax monoidal functors in real life? Or do they cheat and work with monoid homomorphisms instead?

[Matthew Ballard]

:up: :up: :down: :down: :left: :right: :left: :right: :b: :a: :b: :a: :start:

[Matthew Ballard]

Cheat or perhaps more graciously elide the details

[Kevin Buzzard]

Perhaps the more relevant question then is whether we have to work with lax monoidal functors in LTE or whether we can get away with monoid homomorphisms instead?

[Kevin Buzzard]

Johan I've already mentioned to you that in just over a week's time my term will be over and I'd like to lunge into a Lean project. Could you do with some help here?

[Eric Rodriguez]

help us finish flt-regular ;b

[Kevin Buzzard]

My instinct is LTE first and flt-regular after.

[Johan Commelin]

@Kevin Buzzard We can certainly use your help! Do you want a lot of category theory, or even more category theory?

[Johan Commelin]

There's stuff left about homological algebra, or computations with condensed abelian groups.

[Johan Commelin]

Another option is to attack one of the fundamental short exact sequences that we need.

[Johan Commelin]

https://leanprover-community.github.io/liquid/dep_graph_section_2.html is pretty accurate. So I would just click around if I were you, and see if there's a topic that you like.

[Johan Commelin]

Be sure to coordinate here, to check how it fits with what others are doing.

[Adam Topaz]

Johan Commelin said:

The remaining sorry's are horrible. Do people actually work with lax monoidal functors in real life? Or do they cheat and work with monoid homomorphisms instead?

Don't folks usually draw these so-called string diagrams for such things?

[Adam Topaz]

@Scott Morrison is probably the person to ask.

[Bhavik Mehta]

Where can I see these sorries?

[Adam Topaz]

for_mathlib/triangle_shift

[Johan Commelin]

@Bhavik Mehta I just pushed some stuff

[Andrew Yang]

What is remaining for homological algebra? I'll have a fair amount of spare time to spend starting from tomorrow and I could contribute some stuff if there are still todos within my scope of knowledge.

[Johan Commelin]

There certainly are!

[Johan Commelin]

Apart from those triangle sorries, we have

5       src/for_mathlib/derived/example.lean
2       src/for_mathlib/derived/K_projective.lean

[Johan Commelin]

And then we are in good shape to start working on the Breen-Deligne lemma!

[Kevin Buzzard]

I just pulled master (for the first time in about two months) and got caches and there are errors for me in for_mathlib.derived.lemmas. Is that to be expected?

[Adam Topaz]

I don't know what happened, but the has_shift (triangle ...) is not being picked up anymore.
Adding

instance : has_shift (triangle 𝒦) ℤ :=
triangle.int.category_theory.has_shift (homotopy_category A (complex_shape.up ℤ))

just before is_acyclic_of_dist_triang_of_is_quasi_iso fixes this, but it would be better to figure out why typeclass search is failing to find this instance.

[Adam Topaz]

Well, I added these two lines to fix the build for now.

[Johan Commelin]

I guess we still need to go from short_exact to triangle. Or is that done?

[Adam Topaz]

Nope. Still need that.

[Adam Topaz]

But it should be straightforward with the mapping cone.... I hope...

[Kevin Buzzard]

Super Mario 64 - Tricky Triangles! 12"31 [TWR]