Isomorphisms with the homology

Stream: condensed mathematics

[Joël Riou]

With the current API, I am unable to remove the last sorry in the proof of homology_iso in exact_functor.lean, which is (F.obj (homology f g w) ≅ homology (F.map f) (F.map g) w' for an exact functor F. What we have to prove is completely nonsensical, the difficulty is that we have to do computations with kernels and cokernels while we have several candidates for some limit (co)cones: the one that is chosen in the API of kernel/cokernel, and those that are obtained by applying the functor F to (co)limit (co)cones. The only mathematical content is that up to unique isomorphisms, F preserves kernels and cokernels.

In order to construct isomorphisms with an homology object, I suggest introducing what I have named homology_iso_predatum and homology_iso_datum attached to morphisms f : X ⟶ Y and g : X ⟶ Z such that f ≫ g = 0: such datum consists of a diagram including a map ι : K ⟶ Y which is a kernel for g and a map π : K ⟶ H which is a cokernel for the obvious map f' : X ⟶ K. From this datum, I construct an isomorphism H ≅ homology f g w. Then, the lemma homology_iso mentionned above becomes trivial, once we know that homology_iso_datum are preserved by exact functors. A first draft of this is https://github.com/leanprover-community/lean-liquid/commit/98ff40ccfd8fdfe29366bb1970a9a8301e2a3748

I believe this gives some flexibility in order to construct very formal isomorphisms on homology and do computations. If this API is slightly developped, I presume that it should also help in the verification of the naturality of the isomorphisms we construct, like in homology_functor_iso, also in exact_functor.lean. Please let me know if I may proceed with this approach.

[Johan Commelin]

@Joël Riou Do you know about has_homology?

[Johan Commelin]

It's an LTE only thing, but it should move to mathlib at some point.

[Johan Commelin]

It might help here.

[Johan Commelin]

It might be very similar to your homology_iso_datum.

[Joël Riou]

I did not know about has_homology! The structure I suggest is more flexible because in has_homology the homologue of the object K I mention above must kernel g (and not any object K which is a kernel). I will see if has_homology is flexible enough to get the commutation of homology and exact functor.

[Johan Commelin]

Agreed. Adam also suggested this generalization to me a while ago.

[Johan Commelin]

@Joël Riou Did you already settle on a solution for this isomorphism?

[Johan Commelin]

has_homology_aux2.lean also has some sorries that are harder than they should be.

[Joël Riou]

I already have a no-sorry draft version of the homology_isoin exact_functor.lean. I am working on cleaning a little bit my API (and proving a few more lemmas), and then most of these sorries could be removed (even though, I may require changing some defs).

[Johan Commelin]

Ok, cool! Looking forward to your push.
Thanks a lot for your help!

[Joël Riou]

I have developed significantly my API. homology_iso is now sorry free. I redefined homology_functor_iso, for which only the naturality remains to be proven (this broke the unfinished proof in ab5.lean, but this should not be a serious problem). At the end of homology_iso_datum.lean, I have defined the homology_iso_datum that computes the homology of a complex, which is basically what you need for the sorries in has_homology_aux2.lean: the last basic step is to complete the constructon of

def homology_iso_datum.has_homology (h : homology_iso_datum f g H) : has_homology f g H := sorry

(I believe I know at least an ugly way to do this: starting from the "canonical" has_homology f g (homology f g)given by homology.has and transport everything by the isomorphisms I have constructed...)

[Johan Commelin]

Very nice!

[Johan Commelin]

Feel free to turn has_homology_aux2.lean upside down (-;

[Johan Commelin]

If you have an (easy) way to kill those 12 sorries, that would be awesome :lol:

[Joël Riou]

Johan Commelin said:

If you have an (easy) way to kill those 12 sorries, that would be awesome :lol:

Done! (It was not as ugly as I expected.)

[Johan Commelin]

Awesome!

[Joël Riou]

For eval_functor_homology_iso in homological_complex2.lean, I would have a very drastic simplification of the proof:

instance (x : X) : preserves_finite_limits ((evaluation X 𝒜).obj x) :=
⟨by { intro J, introI, introI, apply limits.evaluation_preserves_limits_of_shape, }⟩

instance (x : X) : preserves_finite_colimits ((evaluation X 𝒜).obj x) :=
⟨by { intro J, introI, introI, apply limits.evaluation_preserves_colimits_of_shape, }⟩

def functor_eval_homology_iso (G : homological_complex (X ⥤ 𝒜) c) (i) :
  G.homology i ≅ functor_eval.flip.obj G ⋙ homology_functor _ c i :=
nat_iso.of_components (λ x, (functor.homology_functor_iso ((evaluation X 𝒜).obj x) c i).app G)
begin
  sorry,
end

def eval_functor_homology_iso (F : X ⥤ homological_complex 𝒜 c) (i) :
  F ⋙ homology_functor _ c i ≅ (eval_functor.obj F).homology i :=
iso_whisker_right (eval_functor_equiv.unit_iso.app F) (homology_functor 𝒜 c i) ≪≫
  (functor_eval_homology_iso ((@eval_functor _ X 𝒜 _ _ _ c).obj F) i).symm

The only sorry here is the naturality of a map, which should easily follow from the general naturality of the constructions I made in homology_iso_datum. (More precisely it would be the naturality of homology_functor_iso with respect to a natural transformation between exact functors.)

[Johan Commelin]

Does the rest of the project compile if you use that definition?

[Johan Commelin]

Or do changed defeqs mess up other parts of LTE?

[Joël Riou]

I think it does compile: it is used only in for_mathlib/ab5.lean in an unfinished proof. Anyway, I have to check the naturality mentioned above in order to remove the last sorry in the proof of homology_functor_isoin exact_functor.lean.

[Johan Commelin]

Ok, cool. Feel free to push this already.

[Johan Commelin]

I will stop working on that file until you release it :wink:

[Johan Commelin]

I'm testing your API in breen_deligne/main.lean

[Johan Commelin]

@Joël Riou I've been trying to finish off the sorries at the bottom of the file. But I guess I'm missing tricks on how to use your API, because it's not really going anywhere.

[Joël Riou]

About the very last sorry in breen_deligne/main.lean, I do not know all the details, but it looks like a compatibility of homology_functor_iso with respect to natural transformations between exact functors (it is not stated nor proved yet in exact_functor.lean), and here the natural transformation would come from the tautological endomorphism on objects in endomorphisms A. Does that make sense?

[Johan Commelin]

It makes sense mathematically, but Lean doesn't play ball

[Johan Commelin]

Wait, do you mean the sorry in hH0_endo? I don't think all the functors involved are exact. But would you need that? I think they just need to play nice with endomorphisms.

[Joël Riou]

I am not sure. Now, I am doing my best to stabilize my definitions. There is still some work to do on functor_homology_iso. For now, I suggest you do not rely on the datum in the definition of functor_homology_iso, but you may write some sorried equational lemmas for the basic general compatibilities you need; in principle, I should be able to prove these.

[Johan Commelin]

Well, for the next 4 hours, I'm offline anyway (-; Will keep an eye on what you push.

[Joël Riou]

For the next 4 hours, I teach dance!

[Joël Riou]

Now, the natural isomorphism homology_functor_iso which expresses that homology of complexes commutes with exact functors is almost sorry free (it relies only on one basic sorry in homology_map_datum.lean. To do that, I introduced the category short_complex C of complexes X ⟶ Y ⟶ Z, and defined the functor which basically sends a K : homological_complex C c to the complex K.X_prev i ⟶ K.X i ⟶ K.X_next i. As the homology of such short_complexes are functorialy well behaved with respect to exact functors (because of homology_nat_iso : (short_complex.homology_functor : short_complex A ⥤ A) ⋙ F ≅ F.map_short_complex ⋙ short_complex.homology_functor), it sufficed to check that the short complex K.X_prev i ⟶ K.X i ⟶ K.X_next i is mapped by F to the corresponding complex for F.map_homological_complex K, which is annoying only because F may not send the chosen 0 to the chosen 0. Eventually, homology_functor_iso is now a composition of 7 natural isomorphisms, 5 of which is basically iso.refl on objects.

I will work now on the last sorry in homology_map_datum.lean, and for that, I will have to prove some equational lemmas relating my constructions will homology.desc', etc, which should also be helpful in order to proceed with the computations...

[Joël Riou]

The file for_mathlib/exact_functor.lean is now completely sorry free, and I have established the appropriate equational lemmas iso_hom and iso_inv in homology_map_iso. I believe that what is still missing in order to do computations are basic equational lemmas like homology_functor_iso_hom that would compute homology_functor_iso (this would basically be showing consistency with the first tentative approach to the definition of homology_functor). I shall not do anything more today, but it should be easy to at least state these in the cases that are needed for the computations (depending whether the index i has a given prev and next, or only one of these, etc.).

[Johan Commelin]

I'm about to leave on a road trip to NL. Will be back on Saturday.

[Johan Commelin]

Thanks for what you've done.

[Johan Commelin]

You posted a sketch for the stuff in src/for_mathlib/homological_complex2.lean. I guess you can push that to master now?

[Johan Commelin]

Seemed like that would help a lot with those sorries.

[Joël Riou]

Yes, the last sorry in homological_complex2.leanshould be very easy now. I shall try to complete this tomorrow.

[Johan Commelin]

@Joël Riou It's amazing to see all those sorries vanish. Great job!

Could you please also take a look at this one?
https://github.com/leanprover-community/lean-liquid/blob/00154e0cab9a03c476ac40224c1b626ce5641682/src/breen_deligne/main.lean#L494

[Johan Commelin]

I just closed the other sorry above it.

[Joël Riou]

I will try to see what I can do for this. (I may have to translate some defs from has_homology to homology_map_datum, but I will try not to break anything...)
By the way, do we need for_mathlib/derived/homology.lean which does not seem to be imported by any other file? (I could certainly handle these sorries, but not sure if it is worth?).

[Johan Commelin]

Yes, I was just looking into that question

[Johan Commelin]

I think we might need it for something like https://github.com/leanprover-community/lean-liquid/blob/master/src/condensed/bd_lemma.lean#L210

[Johan Commelin]

But maybe we can prove that in a different way as well.

[Joël Riou]

With the commutation of filtered colimits and homology that I just finished, we have already this in for_mathlib/ab5.lean:

noncomputable
instance homology_functor_preserves_filtered_colimit
  {M : Type} (c : complex_shape M) (i : M)
  (F : J ⥤ homological_complex A c) :
  preserves_colimit F (homology_functor A c i) :=
preserves_colimit_of_nat_iso F (short_complex.homology_functor_iso A c i).symm

Then, it seems it would sufficient to prove (BD.eval' (forget AddCommGroup.{u+1} ⋙ AddCommGroup.free) commutes with filtered colimits.

[Johan Commelin]

Cool, can you make

prove (BD.eval' (forget AddCommGroup.{u+1} ⋙ AddCommGroup.free) commutes with filtered colimits

into a new sorry, and close the old one? Then I think we can remove derived/homology.lean.

[Joël Riou]

Ok, I will do that after I handle the sorry you mentioned about the naturality of eval'_homology.

[Johan Commelin]

Merci!

[Joël Riou]

It seems that I am not able to handle the explicit universe parameters to make this work, but I assume it would not be difficult for you.

[Johan Commelin]

But the sorry is gone, right?

[Johan Commelin]

Did it move to another place?

[Joël Riou]

What I was trying to say is that I was not able to deduce preserves_filtered_colimits (BD.eval' (forget AddCommGroup.{u+1} ⋙ AddCommGroup.free) ⋙ homology_functor AddCommGroup.{u+1} (complex_shape.up ℤ) i)
from a sorried preserves_filtered_colimits (BD.eval' (forget AddCommGroup.{u+1} ⋙ AddCommGroup.free) even though we have preserves_filtered_colimits homology_functor AddCommGroup.{u+1} (complex_shape.up ℤ) i), only because I was not able to handle universe parameters with comp_preserves_filtered_colimits.

[Johan Commelin]

ooh, ok. Let me try

[Adam Topaz]

The universe strikes back!

[Adam Topaz]

It will be some subpermutation of .{u+2 u u+1}

[Johan Commelin]

I now get

preserves_finite_colimits.{u+1 u+2 u+2}
    (homology_functor.{u+1 u+2 0} AddCommGroup.{u+1} (complex_shape.up.{0} ℤ) i)

[Adam Topaz]

That works?

[Johan Commelin]

Wait, something very weird is happening

[Adam Topaz]

where is the 0 coming from?

[Adam Topaz]

oh the Z

[Johan Commelin]

Oops, I meant

preserves_filtered_colimits.{u+1 u+2 u+2}
    (BD.eval' (forget.{u+2 u+1 u+1} AddCommGroup.{u+1} ⋙ AddCommGroup.free.{u+1}))

but same problem

[Johan Commelin]

@Joël Riou You added that somewhere, right?

[Joël Riou]

I do not think I have added anything about AddCommGroup! I have only proved the preserves_colimit F (homology_functor A c i) from for_mathlib/ab5.lean.

[Johan Commelin]

Ok, gotcha

[Adam Topaz]

But that sorry should be easy with what we already have.

[Adam Topaz]

There's the lemma that reduces it to showing that forget.{u+2 u+1 u+1} AddCommGroup.{u+1} ⋙ AddCommGroup.free.{u+1}) preserves filtered colimits, and that's again true by because each of the two functors in the composition preserves such colimits.

[Johan Commelin]

And

preserves_filtered_colimits.{u+1 u+2 u+2}
    (homology_functor.{u+1 u+2 0} AddCommGroup.{u+1} (complex_shape.up.{0} ℤ) i)

is that conclusion done somewhere?

[Adam Topaz]

That should follow from the AB5 file.

[Adam Topaz]

I suppose TC should just pick it up?

[Adam Topaz]

if not the isntance is called category_theory.homology_functor_preserves_filtered_colimits

[Johan Commelin]

I pushed something that breaks the sorry into pieces.

[Johan Commelin]

ok, I'm now importing AB5. Let's see if that helps.

[Johan Commelin]

hmm, it aint working, we are missing some instances

[Johan Commelin]

We also need

preserves_filtered_colimits.{u+1 u+2 u+2} (homological_complex.embed.{0 0 u+2 u+1} complex_shape.embedding.nat_down_int_up)

[Adam Topaz]

Oh that might actually be missing

[Joël Riou]

If we have/had a kind of eval_jointly_reflects_colimits or something, it should be easy using embed_comp_eval in complex_extend.lean that I have added today.