Zulip Chat Archive

Stream: condensed mathematics

Topic: shifting triangles


Adam Topaz (Feb 24 2022 at 17:08):

Do we have anywhere a has_shift instance for triangle C?

Johan Commelin (Feb 24 2022 at 17:34):

You just pushed something, right?

Johan Commelin (Feb 24 2022 at 17:34):

cc @Andrew Yang

Andrew Yang (Feb 24 2022 at 17:35):

I don’t think so

Adam Topaz (Feb 24 2022 at 17:35):

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

Adam Topaz (Feb 24 2022 at 17:36):

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

Adam Topaz (Feb 24 2022 at 17:36):

What I'm really after is this:

lemma shift_of_dist_triangle (T : triangle C) (hT : T  dist_triang C) (i : ) :
  Ti  dist_triang C := sorry

Matthew Ballard (Feb 24 2022 at 18:04):

Is there an action of shift defined on triangle Calready?

Adam Topaz (Feb 24 2022 at 18:05):

See link above

Johan Commelin (Feb 24 2022 at 18:12):

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 (Feb 24 2022 at 18:13):

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 (Feb 24 2022 at 18:13):

It seems fine!

Adam Topaz (Feb 24 2022 at 18:13):

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

def homology_shift_iso (X : 𝒦) (i : ) :
  (homotopy_category.homology_functor _ _ 0).obj (Xi) 
  (homotopy_category.homology_functor _ _ i).obj X :=
sorry

Adam Topaz (Feb 24 2022 at 18:15):

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

Andrew Yang (Feb 24 2022 at 18:16):

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

Matthew Ballard (Feb 24 2022 at 18:18):

I don't know enough to have opinions

Johan Commelin (Feb 24 2022 at 18:19):

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 (Feb 24 2022 at 18:20):

But I agree that it's annoying.

Andrew Yang (Feb 24 2022 at 18:20):

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 (Feb 24 2022 at 18:24):

Adam Topaz said:

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

def homology_shift_iso (X : 𝒦) (i : ) :
  (homotopy_category.homology_functor _ _ 0).obj (Xi) 
  (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 (Feb 24 2022 at 18:25):

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 (Feb 24 2022 at 18:27):

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 (Feb 24 2022 at 18:27):

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

Matthew Ballard (Feb 24 2022 at 18:27):

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

Johan Commelin (Feb 24 2022 at 18:29):

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 (Feb 24 2022 at 18:30):

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 (Feb 24 2022 at 18:30):

Or for complexes indexed by something without a 0.

Andrew Yang (Feb 24 2022 at 18:30):

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 (Feb 24 2022 at 18:31):

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

Johan Commelin (Feb 24 2022 at 18:32):

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 (Feb 24 2022 at 18:33):

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

Andrew Yang (Feb 24 2022 at 18:42):

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 (Feb 24 2022 at 18:45):

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

Johan Commelin (Feb 24 2022 at 18:46):

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

Andrew Yang (Feb 24 2022 at 18:47):

Oh :(

Andrew Yang (Feb 24 2022 at 18:51):

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

Johan Commelin (Feb 24 2022 at 19:00):

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 (Feb 24 2022 at 19:27):

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 (Feb 24 2022 at 19:37):

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

Johan Commelin (Feb 24 2022 at 19:39):

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

Adam Topaz (Feb 24 2022 at 19:41):

I doubt it

Adam Topaz (Feb 24 2022 at 22:20):

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 (Feb 24 2022 at 22:37):

Concerning shifting triangles: What's the convention regarding (1)n(-1)^n?
Note that if TT is a triangle, then by defining T[1]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 (Feb 25 2022 at 00:38):

The convention I follow is:

C[1]i=Ci+1,d[1]i=di+1C[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 (Feb 25 2022 at 00:53):

Yeah, that's right.

Adam Topaz (Feb 25 2022 at 00:54):

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

Adam Topaz (Feb 25 2022 at 00:58):

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

Adam Topaz (Feb 25 2022 at 01:02):

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

H(A)H(B)H(C)H(A[1])H(B[1])H(C[1])H(A[2])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 (Feb 25 2022 at 01:02):

I'm confused.

Matthew Ballard (Feb 25 2022 at 01:27):

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 (Feb 25 2022 at 01:39):

Adam Topaz said:

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

I could work on that later today.

Andrew Yang (Feb 25 2022 at 05:12):

Should be done now.

Adam Topaz (Feb 25 2022 at 12:00):

Thanks!

Adam Topaz (Feb 25 2022 at 13:25):

@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 (Feb 25 2022 at 14:02):

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 (Feb 25 2022 at 14:06):

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

Andrew Yang (Feb 25 2022 at 14:19):

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 (Feb 25 2022 at 14:28):

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

Adam Topaz (Feb 25 2022 at 14:28):

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

Andrew Yang (Feb 25 2022 at 14:36):

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

Adam Topaz (Feb 25 2022 at 15:05):

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 (Feb 25 2022 at 15:37):

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 (Feb 25 2022 at 15:39):

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 (Feb 25 2022 at 16:31):

@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 (Feb 25 2022 at 16:33):

Where would be the natural place for foobar?

Adam Topaz (Feb 25 2022 at 16:33):

In for_mathlib/homological_complex_shift?

Adam Topaz (Feb 25 2022 at 16:37):

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

Andrew Yang (Feb 25 2022 at 16:40):

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 (Feb 25 2022 at 16:41):

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 (Feb 27 2022 at 16:00):

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 (Feb 27 2022 at 16:02):

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

Kevin Buzzard (Feb 27 2022 at 16:18):

Wow -- well done! What about Tor?

Adam Topaz (Feb 27 2022 at 16:34):

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 (Feb 27 2022 at 18:18):

Does that proof for Ext involve double complexes?

Adam Topaz (Feb 27 2022 at 18:21):

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 (Feb 27 2022 at 18:22):

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

Reid Barton (Feb 27 2022 at 18:23):

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

Adam Topaz (Feb 27 2022 at 18:44):

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

Johan Commelin (Mar 16 2022 at 17:03):

I'm working on

lemma shift_of_dist_triangle (T : triangle C) (hT : T  dist_triang C) (i : ) :
  Ti  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 (Mar 16 2022 at 17:08):

What's the goal here?

Adam Topaz (Mar 16 2022 at 17:14):

@Johan Commelin can you push what you have?

Adam Topaz (Mar 16 2022 at 17:19):

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

Matthew Ballard (Mar 16 2022 at 17:20):

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

Matthew Ballard (Mar 16 2022 at 17:21):

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

Adam Topaz (Mar 16 2022 at 17:25):

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 (Mar 16 2022 at 17:26):

ah, no the last square won't commutee.

Adam Topaz (Mar 16 2022 at 17:30):

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 (Mar 16 2022 at 17:36):

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

Matthew Ballard (Mar 16 2022 at 17:38):

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

Adam Topaz (Mar 16 2022 at 17:39):

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

Matthew Ballard (Mar 16 2022 at 17:40):

Yeah. That's how I remembered!

Matthew Ballard (Mar 16 2022 at 17:40):

Well commented code

Adam Topaz (Mar 16 2022 at 17:42):

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

Johan Commelin (Mar 16 2022 at 17:45):

Adam Topaz said:

Johan Commelin can you push what you have?

Done

Johan Commelin (Mar 16 2022 at 17:47):

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

Matthew Ballard (Mar 16 2022 at 17:47):

Can you just say shifting a triangle by ii is rotating 3i3i as the definition?

Johan Commelin (Mar 16 2022 at 17:48):

That would lead to bad defeqs, I think

Matthew Ballard (Mar 16 2022 at 17:49):

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

Matthew Ballard (Mar 16 2022 at 17:50):

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

Adam Topaz (Mar 16 2022 at 17:51):

Why do we negate in rotate again?

Matthew Ballard (Mar 16 2022 at 17:53):

stacks vs Neeman pg 30

Johan Commelin (Mar 16 2022 at 17:54):

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 (Mar 16 2022 at 17:55):

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 (Mar 16 2022 at 17:55):

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

Matthew Ballard (Mar 16 2022 at 17:55):

Does shift act with a sign on morphisms?

Johan Commelin (Mar 16 2022 at 17:56):

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

Matthew Ballard (Mar 16 2022 at 17:56):

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

Adam Topaz (Mar 16 2022 at 17:56):

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

Johan Commelin (Mar 16 2022 at 17:57):

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 (Mar 16 2022 at 17:57):

Is that good or bad?

Matthew Ballard (Mar 16 2022 at 17:59):

Neither?

Matthew Ballard (Mar 16 2022 at 18:01):

It runs contra to Stacks

Matthew Ballard (Mar 16 2022 at 18:03):

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

Johan Commelin (Mar 16 2022 at 18:38):

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 (Mar 16 2022 at 18:38):

I pushed a WIP fix @Johan Commelin

Adam Topaz (Mar 16 2022 at 18:39):

@[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 (Mar 16 2022 at 18:39):

and

lemma shift_of_dist_triangle (T : triangle C) (hT : T  dist_triang C) (i : ) :
  Ti  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 (Mar 16 2022 at 18:39):

This now looks doable.

Matthew Ballard (Mar 16 2022 at 18:40):

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 (Mar 16 2022 at 19:43):

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

Johan Commelin (Mar 16 2022 at 19:43):

Other sorries remain...

Johan Commelin (Mar 17 2022 at 12:52):

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 (Mar 17 2022 at 14:01):

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

Matthew Ballard (Mar 17 2022 at 14:03):

Cheat or perhaps more graciously elide the details

Kevin Buzzard (Mar 17 2022 at 14:08):

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 (Mar 17 2022 at 14:08):

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 (Mar 17 2022 at 14:11):

help us finish flt-regular ;b

Kevin Buzzard (Mar 17 2022 at 14:14):

My instinct is LTE first and flt-regular after.

Johan Commelin (Mar 17 2022 at 14:21):

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

Johan Commelin (Mar 17 2022 at 14:21):

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

Johan Commelin (Mar 17 2022 at 14:22):

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

Johan Commelin (Mar 17 2022 at 14:22):

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 (Mar 17 2022 at 14:23):

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

Adam Topaz (Mar 17 2022 at 14:36):

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 (Mar 17 2022 at 14:36):

@Scott Morrison is probably the person to ask.

Bhavik Mehta (Mar 17 2022 at 14:37):

Where can I see these sorries?

Adam Topaz (Mar 17 2022 at 14:38):

for_mathlib/triangle_shift

Johan Commelin (Mar 17 2022 at 15:01):

@Bhavik Mehta I just pushed some stuff

Andrew Yang (Mar 17 2022 at 15:04):

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 (Mar 17 2022 at 15:14):

There certainly are!

Johan Commelin (Mar 17 2022 at 15:14):

Apart from those triangle sorries, we have

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

Johan Commelin (Mar 17 2022 at 15:15):

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

Kevin Buzzard (Mar 17 2022 at 20:34):

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 (Mar 17 2022 at 20:59):

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 (Mar 17 2022 at 22:23):

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

Johan Commelin (Mar 21 2022 at 15:41):

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

Adam Topaz (Mar 21 2022 at 15:43):

Nope. Still need that.

Adam Topaz (Mar 21 2022 at 15:44):

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

Kevin Buzzard (Mar 21 2022 at 15:58):

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


Last updated: Dec 20 2023 at 11:08 UTC