Zulip Chat Archive

Stream: condensed mathematics

Topic: for_mathlib/acyclic


Kevin Buzzard (May 28 2022 at 19:10):

My partner's away, my kids are out, and I'm sick of marking, so I'm going to do some LTE work. The stuff in for_mathlib/acyclic looks pretty straightforward to knock off (hopefully) -- is anyone else working on this? I'm trying the sorrys now.

Adam Topaz (May 28 2022 at 19:24):

Johan and I were hacking on this yesterday

Adam Topaz (May 28 2022 at 19:25):

I think this will be a bit of a challlenge:
https://github.com/leanprover-community/lean-liquid/blob/edc56f03a7883d9ebe76a8b31e18e0212fa7df2f/src/for_mathlib/acyclic.lean#L430

Adam Topaz (May 28 2022 at 19:25):

And a few of the sorries in Ext_compute_with_acyclic_naturality will probably also be a little challenging.

Kevin Buzzard (May 28 2022 at 19:28):

This stuff is quite good fun :-)

Kevin Buzzard (May 28 2022 at 19:28):

I'll take a look at your challenge! The night is young.

Kevin Buzzard (May 28 2022 at 19:31):

Have you done anything with this file which isn't currently on master? I was working on the sorry in cochain_complex.hom_to_single_of_hom

Kevin Buzzard (May 28 2022 at 19:31):

I really like these kinds of levels

Kevin Buzzard (May 28 2022 at 19:32):

Can you imagine life without widgets? I can just dive into each of these goals thinking "I haven't even read the question but I know this is some diagram in category theory and it's really easy to draw it on paper because I can just query the goal state"

Kevin Buzzard (May 28 2022 at 19:36):

Shall I just push directly to master?

Johan Commelin (May 28 2022 at 19:40):

Yes please

Kevin Buzzard (May 28 2022 at 19:46):

Do we have this?

import category_theory.abelian.exact

open category_theory category_theory.limits

example {𝓐 : Type}
  [category 𝓐]
  [abelian 𝓐]
  (X Y : 𝓐)
  (hY : is_zero Y) :
  subsingleton (X  Y) :=
begin
  admit,
end

Kevin Buzzard (May 28 2022 at 19:47):

I think I find abelian category theory much more fun than category theory :-)

Adam Topaz (May 28 2022 at 19:50):

docs#category_theory.limits.is_zero.eq_of_tgt

Adam Topaz (May 28 2022 at 19:50):

(or something like that...)

Adam Topaz (May 28 2022 at 19:50):

There is also a eq_of_src variant

Kevin Buzzard (May 28 2022 at 19:58):

lemma is_zero.subsingleton_right {𝓐 : Type*} [category 𝓐] [abelian 𝓐]
  (X : 𝓐) {Y : 𝓐} (hY : is_zero Y) : subsingleton (X  Y) :=
λ a b, begin
  rcases hY with -, hY⟩,
  obtain ⟨⟨_, h⟩⟩ := hY X,
  exact (h a).trans (h b).symm,
end

Kevin Buzzard (May 28 2022 at 19:58):

I just took it all apart :-) I'm learning how it all works.

Riccardo Brasca (May 28 2022 at 19:59):

@unique.subsingleton _ (hY.unique_from X).some should also work

Riccardo Brasca (May 28 2022 at 19:59):

and abelian is not needed :grinning:

Adam Topaz (May 28 2022 at 20:00):

I think it would be generally easier to use eq_of_src and eq_of_tgt instead of adding various subsingleton instances using haveI or whatnot inside tactic blocks.

Kevin Buzzard (May 28 2022 at 20:05):

I'm just experimenting with this stuff for the first time and would be very happy to hear style comments! I thought the subsingleton approach was all abstract and cool :-)

Kevin Buzzard (May 28 2022 at 20:12):

I like that I can use

#print prefix category_theory.limits.is_zero

to get the API for this concept I've not really used before

Kevin Buzzard (May 28 2022 at 20:23):

Hey! cochain_complex.hom_to_single_of_hom : computer says no.
Here's the first case I can't do:

𝓐 : Type u_1,
_inst_1 : category 𝓐,
_inst_2 : abelian 𝓐,
_inst_3 : enough_projectives 𝓐,
C : cochain_complex 𝓐 ,
B : 𝓐,
j : ,
f : C.X (j.add 1)  B
 0 = C.d j (j.add 1)  f  (homological_complex.single_iso B _).inv

Kevin Buzzard (May 28 2022 at 20:24):

This is the j + 1 = i branch.

Kevin Buzzard (May 28 2022 at 20:26):

I pushed to master, I'll try and fathom out the mathematical assertion I'm making.

Kevin Buzzard (May 28 2022 at 20:28):

I'm now quite confused. I would ignore me for a while.

Kevin Buzzard (May 28 2022 at 20:31):

Yeah I think my proof has gone astray ;-)

Kevin Buzzard (May 28 2022 at 20:35):

I now understand my mistake. I had lost information about f. The definition looks like this:

def cochain_complex.hom_to_single_of_hom
  (C : cochain_complex 𝓐 ) (B : 𝓐) (i : ) (f : C.X i  B) :
  C  (homological_complex.single _ _ i).obj B :=
{ f := λ j, if h : j = i then eq_to_hom (by rw h)  f  (homological_complex.single_iso _ h).inv
    else 0,
  comm' := begin
    sorry
  end }

but if you look at the goal state in the comm' proof then there's no mention of the definition of f!

Kevin Buzzard (May 28 2022 at 20:37):

oh this is an actual problem: I don't know how to get to the definition of f in that proof.

Adam Topaz (May 28 2022 at 20:38):

change ite _ _ _ doesn't work?

Kevin Buzzard (May 28 2022 at 20:47):

oh lol there are two fs

Kevin Buzzard (May 28 2022 at 20:52):

OK so here is the issue. You want to define a morphism of complexes, from a general complex C to a "skyscraper" complex with only one term B in position i. You want to magic this up from a map from a map from C[i] to B in the the obvious way. The problem: one of the squares doesn't commute. That map from C[i] to B had better be zero on the image of C[i-1] for this construction to work, right?

Kevin Buzzard (May 28 2022 at 20:52):

@Adam Topaz @Johan Commelin do you agree that this is a false sorry?

Kevin Buzzard (May 28 2022 at 20:53):

I mean, before I started messing with it on master.

Adam Topaz (May 28 2022 at 20:56):

Yeah it's false

Kevin Buzzard (May 28 2022 at 20:56):

I propose this modification:

def cochain_complex.hom_to_single_of_hom
  (C : cochain_complex 𝓐 ) (B : 𝓐) (i : ) (f : C.X i  B)
  (h :  j : , C.d j i  f = 0):
  C  (homological_complex.single _ _ i).obj B :=
{ f := λ j, if h : j = i then eq_to_hom (by rw h)  f  (homological_complex.single_iso _ h).inv
    else 0,

Adam Topaz (May 28 2022 at 20:56):

Oops!

Kevin Buzzard (May 28 2022 at 20:58):

Ext_compute_with_acyclic_inv_eq_aux breaks -- I'm checking out the random extra goal which has now appeared :-)

Adam Topaz (May 28 2022 at 20:59):

Yeah that would have to be fixed as well...

Adam Topaz (May 28 2022 at 20:59):

Sorry we got the map in the wrong direction

Adam Topaz (May 28 2022 at 20:59):

A map on the ith term induces a map from single.obj ...

Kevin Buzzard (May 28 2022 at 21:01):

So I can try to fix this: if you want to write the new defs I can fill in the proofs, on a branch or something -- I don't really just want to blunder in as I'm only just learning about this part of the code base for the first time

Adam Topaz (May 28 2022 at 21:03):

I won't have time to work on LTE until Monday.

Kevin Buzzard (May 28 2022 at 21:11):

OK, I'll keep digging :-)

Kevin Buzzard (May 28 2022 at 21:27):

Oh I think I understand. Fixing it up.

Kevin Buzzard (May 28 2022 at 21:30):

No, this isn't true either. To make sure that the map from B to C_i induces a map from the singleton complex B[i] into C, you need that the given map is in the kernel of C_i -> C_{i+1}.

Kevin Buzzard (May 28 2022 at 21:47):

OK so after the dust has cleared: I appear to have broken the statement of Ext_compute_with_acylic_inv_eq. Here is a revised Ext_compute_with_acyclic_inv_eq_aux :

def Ext_compute_with_acyclic_inv_eq_aux (B) (i) :
  AddCommGroup.of (C  (homological_complex.single _ _ (-i)).obj B)  ((Ext i).obj (op (of' C))).obj ((single 𝓐 0).obj B) :=
{ to_fun := λ f, (of' C).π  begin
    dsimp at f,
    refine (homotopy_category.quotient _ _).map _,
    refine _  (homological_complex.single_shift _ _).inv.app _,
    refine f  _,
    refine eq_to_hom _,
    simp,
  end,
  map_zero' := sorry,
  map_add' := sorry }

The change is that the hom set we're mapping into the Ext group is now smaller; it's only the morphisms of complexes from C to B[-i] instead of the possibly larger group of morphisms C.X (-i) ⟶ B.

Kevin Buzzard (May 28 2022 at 21:55):

I think I can fix it. In the application we need to construct a map from a kernel and we were throwing away information, using kernel.\iota and instead constructing a map on a bigger space -- we were throwing away precisely what we needed to make the diagram commute.

Kevin Buzzard (May 28 2022 at 22:28):

Ha ha there is a nasty sub-boss. We have some function f which is given as some fancy object in a kernel but you know when you unravel it that the spec of it you'll get a group hom with a nice property. However just attempting to extract this and I ran into classical.choice, which was used to construct the kernel of the group homomorphism in Ab :-)

Adam Topaz (May 29 2022 at 02:39):

I think at the end of the day we're interested in the case where C is a resolution by acyclic objects, and in that case, the original construction should actually be okay, except that some hypotheses were missing. I think the version of hom_to_single_of_hom that Kevin proposed above should work.

Kevin Buzzard (May 29 2022 at 12:52):

OK so I have pushed my suggested change of route to master. @Adam Topaz you might want to have a look at it. My changes start at line 402. I slightly weaken Ext_compute_with_acyclic_inv_eq_aux. I add a new definition kernel_yoneda_complex_to_morphism_to_single saying that if you have f in the kernel of (Cⱼ₊₁ ⟶ B) ⟶ (Cⱼ ⟶ B) then you can define a map of complexes C -> B[j+1] ; I seem to have made an off by one error but I'll fix it later. In particular there might still be a false sorry but I will sort it out later; I need be disciplined and to do some solid marking for a few hours now.

Kevin Buzzard (May 29 2022 at 12:52):

Sorry -- I thought I had fixed all the false sorries; it was only when I was writing the previous message that I noticed the possible off by one error.

Kevin Buzzard (May 29 2022 at 13:02):

Near the end of the file, a rewrite broke and I now suspect that this will be because of the off by one error I've made. Will fix later (maybe 10pm UK time tonight)

Kevin Buzzard (May 30 2022 at 03:26):

OK I've made some progress (and fixed the off by one error). Things are a bit tidier than before but I still didn't finish one annoying sorry.

@Adam Topaz why are you stating such an ugly Ext_compute_with_acyclic_naturality ? One of the things you have in the
statement is

    (((preadditive_yoneda.obj B).right_op.map_homological_complex _ 
      homological_complex.unop_functor.right_op  (_root_.homology_functor _ _ (-i)).op).map f).unop

This contains no fewer than 5 op/unopisms. Is this really the form you want it to be in? I've been trying to avoid Ab^{op} completely. My refactor broke your proof but I'm wondering why you want to prove it at all!

Kevin Buzzard (May 30 2022 at 03:30):

If we had contravariant functors we wouldn't need any ops at all. You could have a Yoneda : B \func (B \contrafunc Ab), have a contra_map_homological_complex sending B-valued complexes with shape c to Ab-valued complexes with shape c.symm (note that c.symm.symm is definitionally c), you never see another op in your life. What do you think?

Johan Commelin (May 30 2022 at 04:04):

Doesn't that mean duplicating the entire category library?

Johan Commelin (May 30 2022 at 04:05):

It is already duplicating all the limits stuff into colimits.

Kevin Buzzard (May 30 2022 at 10:02):

Yeah! But then no more fighting ops so we can delete all that stuff. Right now we have two ways of talking about contravariant functor and both of them are inconvenient. The explicit op-free definition feels more natural -- we're never thinking about op c in reality, we're thinking about c but with the arrows going the other way and this is just interchanging the order of the inputs to the hom functor

Kevin Buzzard (May 30 2022 at 10:07):

For example if someone said to you "hey let's delete colimits, they're just limits in op so we don't need them" you'd be like "well I'm not so sure, that sounds like it would make a bunch of stuff a lot more fiddly". I'm looking at this op nonsense and thinking it would be less fiddly with contravariant functors. Maybe I'm wrong though, I'm a newcomer to this part of the library

Yaël Dillies (May 30 2022 at 10:14):

Analogously, we added docs#antitone lately and it makes stuff much cleaner.

Kevin Buzzard (May 30 2022 at 10:17):

The op-free definition of a contravariant functor has better definitional properties too; it's a genuinely simpler object

Johan Commelin (May 30 2022 at 10:29):

But you will need 4 definitions of composition of functor.

Johan Commelin (May 30 2022 at 10:29):

And I guess they can't share notation

Kevin Buzzard (May 30 2022 at 10:41):

Yup. And they'll all have better definitional properties than anything we have now, because we're already doing those four definitions in our code but we're filling our terms with op (o) and f.op instead. Adam's term has no fewer than five "no-op" applications in. If you like you could say I was proposing deleting all of them and doing it a new way

Johan Commelin (May 30 2022 at 10:43):

Btw, I guess I actually wrote that last decl in the file

Johan Commelin (May 30 2022 at 10:45):

Note that unop_functor is a different beast. It doesn't just disappear if you add contravariant functors.

Kevin Buzzard (May 30 2022 at 10:52):

Oh great! Why did you write it like that? Is it something that's coming up later and we need it to be in that form? I am still in marking hell but I've got my eye on it

Kevin Buzzard (May 30 2022 at 10:53):

I'm about to spend an hour hacking on this file before I start marking again

Johan Commelin (May 30 2022 at 11:03):

Yeah we need it in Lbar/ext.lean

Johan Commelin (May 30 2022 at 11:03):

But I don't really care too much about where you put the ops.

Johan Commelin (May 30 2022 at 11:04):

Because f.op.unop is defeq to f. And the same for op (unop X). So in the end, all those different ways will be defeq.

Kevin Buzzard (May 30 2022 at 11:08):

Is op X \hom op Y defeq to Y \hom X?

Johan Commelin (May 30 2022 at 11:09):

Yes

Kevin Buzzard (May 30 2022 at 12:32):

Nice! OK so I have finished the "annoying sorry" mentioned above, so a summary of my work is that the false sorry is now modified so it's true, and proved; and the consequences are that Ext_compute_with_acylic_inv_eq still compiles as well as it did before (i.e. there's a sorry in both the statement and the proof) and the proof of Ext_compute_with_acyclic_naturality is a bit more broken than it was, because a rewrite which used to work, no longer works.

Kevin Buzzard (May 30 2022 at 14:53):

OK I got the rewrite working again. I've pushed. I now have sorried data and I don't know the maths well enough to know what the data should be. I'm unlikely to work on this file for the next 6 hours or so because I need to stop doing Lean and start doing marking. Please @Johan Commelin or @Adam Topaz let me know if I'm taking things backwards! I don't really know what I'm doing, I'm just blundering in really. I've learnt tons in the last two days!

Adam Topaz (May 30 2022 at 16:09):

@Kevin Buzzard I think there is an issue with the missing data in the proof:

(preadditive_yoneda.obj B).obj (op (C₁.X (-i)))  ((Ext i).obj (op (of' C₁))).obj ((single 𝓐 0).obj B)

The natural thing here would be something simiilar to what we discussed above about hom_to_single_of_hom composed with Ext_compute_with_acyclic_inv_eq_aux, but as you noted there is a missing hypothesis which I don't think we can deduce here.

Kevin Buzzard (May 30 2022 at 17:32):

Oh interesting! So we need to sort out the mathematics here.

Adam Topaz (May 30 2022 at 17:34):

I'm working on it now.

Kevin Buzzard (May 30 2022 at 17:35):

I'll have some time later to work on this. I'd pushed all I had by the way

Adam Topaz (May 30 2022 at 18:16):

Okay, I've broken up the primary naturality proof into three smaller naturality proofs which should be doable independently.
I think this makes it much clearer what's actually goiing on here...

Adam Topaz (May 30 2022 at 18:16):

The three smaller naturality sorries are in for_mathlib/acyclic.

Kevin Buzzard (May 30 2022 at 19:06):

I'm about to start hacking on this again

Adam Topaz (May 30 2022 at 19:41):

@Kevin Buzzard there is one new sorry in for_mathlib/derived/example.lean

Adam Topaz (May 30 2022 at 19:42):

That takes care of the of the three sorries I mentioned above, I already solved the fiirst one, and I'm working on the last one now.

Adam Topaz (May 30 2022 at 19:51):

Well, I have to do other things for a little while. I'll try to finish off the third sorry later

Kevin Buzzard (May 31 2022 at 00:42):

I didn't get very far :-( I spent most of the evening learning about the area.

Adam Topaz (May 31 2022 at 12:39):

The proof I was working on turned out to be quite difficult because at some point II have to switch from equality to homotopy.
Do we have a well-establiished way to do such proofs?

Johan Commelin (May 31 2022 at 12:39):

docs#eq_of_homotopy (modulo some namespace)

Adam Topaz (May 31 2022 at 12:41):

That's not quite what I need

Adam Topaz (May 31 2022 at 12:42):

I have two maps f,gf,g and the goal is to show that the compositiion (approx) kernel.\iota d \gg f \gg cokernel.\pi d = kernell.\iota d \gg g \gg cokernel.\pi d.

Adam Topaz (May 31 2022 at 12:43):

And what I can prove that is f and g are homotopic

Johan Commelin (May 31 2022 at 12:44):

Hmm, I guess we need more API for that. Can you state a selfcontained lemma?

Adam Topaz (May 31 2022 at 12:45):

I'm doing that now.

Adam Topaz (May 31 2022 at 13:02):

Lemma added to for_mathlib/homotopy_category_lemmas... additional sorries incoming.

Adam Topaz (May 31 2022 at 13:02):

And I suppose we already know that an additive functor preserves homotopies?

Adam Topaz (May 31 2022 at 13:03):

Indeed: docs#functor.map_homotopy

Adam Topaz (May 31 2022 at 13:03):

(mod namespaces)

Adam Topaz (May 31 2022 at 13:18):

Alright, for_mathlib/acyclic is sorry-free, but there are some dependent sorries in for_mathliib/homotopy_category_lemmas and for_mathlib/derived/example

Johan Commelin (May 31 2022 at 13:26):

for_mathlib/derived/example is very slow for me. I think we should clean-up/reorganize that file. It's doing 10 things and some.

Johan Commelin (May 31 2022 at 13:26):

But I'm very glad that the bulk of this naturality proof is now done! Merci!


Last updated: Dec 20 2023 at 11:08 UTC