for_mathlib/acyclic

Stream: condensed mathematics

[Kevin Buzzard]

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]

Johan and I were hacking on this yesterday

[Adam Topaz]

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]

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

[Kevin Buzzard]

This stuff is quite good fun :-)

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

I really like these kinds of levels

[Kevin Buzzard]

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]

Shall I just push directly to master?

[Johan Commelin]

Yes please

[Kevin Buzzard]

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]

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

[Adam Topaz]

docs#category_theory.limits.is_zero.eq_of_tgt

[Adam Topaz]

(or something like that...)

[Adam Topaz]

There is also a eq_of_src variant

[Kevin Buzzard]

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]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

and abelian is not needed :grinning:

[Adam Topaz]

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]

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]

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]

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]

This is the j + 1 = i branch.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Yeah I think my proof has gone astray ;-)

[Kevin Buzzard]

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]

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

[Adam Topaz]

change ite _ _ _ doesn't work?

[Kevin Buzzard]

oh lol there are two fs

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Adam Topaz]

Yeah it's false

[Kevin Buzzard]

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]

Oops!

[Kevin Buzzard]

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

[Adam Topaz]

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

[Adam Topaz]

Sorry we got the map in the wrong direction

[Adam Topaz]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

OK, I'll keep digging :-)

[Kevin Buzzard]

Oh I think I understand. Fixing it up.

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

Doesn't that mean duplicating the entire category library?

[Johan Commelin]

It is already duplicating all the limits stuff into colimits.

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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

[Johan Commelin]

But you will need 4 definitions of composition of functor.

[Johan Commelin]

And I guess they can't share notation

[Kevin Buzzard]

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]

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

[Johan Commelin]

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

[Kevin Buzzard]

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]

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

[Johan Commelin]

Yeah we need it in Lbar/ext.lean

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Johan Commelin]

Yes

[Kevin Buzzard]

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]

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]

@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]

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

[Adam Topaz]

I'm working on it now.

[Kevin Buzzard]

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

[Adam Topaz]

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]

The three smaller naturality sorries are in for_mathlib/acyclic.

[Kevin Buzzard]

I'm about to start hacking on this again

[Adam Topaz]

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

[Adam Topaz]

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]

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

[Kevin Buzzard]

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

[Adam Topaz]

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]

docs#eq_of_homotopy (modulo some namespace)

[Adam Topaz]

That's not quite what I need

[Adam Topaz]

I have two maps $f,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]

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

[Johan Commelin]

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

[Adam Topaz]

I'm doing that now.

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

Indeed: docs#functor.map_homotopy

[Adam Topaz]

(mod namespaces)

[Adam Topaz]

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]

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]

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