Zulip Chat Archive

Stream: condensed mathematics

Topic: Isomorphisms with the homology


Joël Riou (Jun 27 2022 at 14:46):

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 (Jun 27 2022 at 14:59):

@Joël Riou Do you know about has_homology?

Johan Commelin (Jun 27 2022 at 14:59):

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

Johan Commelin (Jun 27 2022 at 14:59):

It might help here.

Johan Commelin (Jun 27 2022 at 14:59):

It might be very similar to your homology_iso_datum.

Joël Riou (Jun 27 2022 at 15:15):

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 (Jun 27 2022 at 15:16):

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

Johan Commelin (Jun 28 2022 at 10:24):

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

Johan Commelin (Jun 28 2022 at 11:21):

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

Joël Riou (Jun 28 2022 at 11:35):

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 (Jun 28 2022 at 11:35):

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

Joël Riou (Jun 28 2022 at 19:31):

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 (Jun 28 2022 at 19:35):

Very nice!

Johan Commelin (Jun 28 2022 at 19:36):

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

Johan Commelin (Jun 28 2022 at 19:36):

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

Joël Riou (Jun 28 2022 at 23:08):

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 (Jun 29 2022 at 03:47):

Awesome!

Joël Riou (Jun 29 2022 at 05:39):

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 (Jun 29 2022 at 05:40):

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

Johan Commelin (Jun 29 2022 at 05:40):

Or do changed defeqs mess up other parts of LTE?

Joël Riou (Jun 29 2022 at 05:47):

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 (Jun 29 2022 at 05:47):

Ok, cool. Feel free to push this already.

Johan Commelin (Jun 29 2022 at 05:49):

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

Johan Commelin (Jun 29 2022 at 06:06):

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

Johan Commelin (Jun 29 2022 at 09:46):

@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 (Jun 29 2022 at 13:23):

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 (Jun 29 2022 at 13:50):

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

Johan Commelin (Jun 29 2022 at 14:09):

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 (Jun 29 2022 at 15:29):

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 (Jun 29 2022 at 15:35):

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

Joël Riou (Jun 29 2022 at 15:56):

For the next 4 hours, I teach dance!

Joël Riou (Jun 30 2022 at 11:26):

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 (Jun 30 2022 at 13:54):

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 (Jun 30 2022 at 14:04):

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

Johan Commelin (Jun 30 2022 at 14:04):

Thanks for what you've done.

Johan Commelin (Jun 30 2022 at 14:04):

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 (Jun 30 2022 at 14:05):

Seemed like that would help a lot with those sorries.

Joël Riou (Jun 30 2022 at 14:10):

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

Johan Commelin (Jul 02 2022 at 07:45):

@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 (Jul 02 2022 at 08:13):

I just closed the other sorry above it.

Joël Riou (Jul 02 2022 at 09:02):

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 (Jul 02 2022 at 09:03):

Yes, I was just looking into that question

Johan Commelin (Jul 02 2022 at 09:04):

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 (Jul 02 2022 at 09:05):

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

Joël Riou (Jul 02 2022 at 09:13):

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 (Jul 02 2022 at 09:14):

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 (Jul 02 2022 at 09:36):

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

Johan Commelin (Jul 02 2022 at 09:40):

Merci!

Joël Riou (Jul 02 2022 at 14:19):

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 (Jul 02 2022 at 14:20):

But the sorry is gone, right?

Johan Commelin (Jul 02 2022 at 14:20):

Did it move to another place?

Joël Riou (Jul 02 2022 at 14:41):

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 (Jul 02 2022 at 14:42):

ooh, ok. Let me try

Adam Topaz (Jul 02 2022 at 14:43):

The universe strikes back!

Adam Topaz (Jul 02 2022 at 14:44):

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

Johan Commelin (Jul 02 2022 at 14:48):

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 (Jul 02 2022 at 14:48):

That works?

Johan Commelin (Jul 02 2022 at 14:48):

Wait, something very weird is happening

Adam Topaz (Jul 02 2022 at 14:49):

where is the 0 coming from?

Adam Topaz (Jul 02 2022 at 14:49):

oh the Z

Johan Commelin (Jul 02 2022 at 14:50):

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 (Jul 02 2022 at 14:50):

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

Joël Riou (Jul 02 2022 at 14:53):

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 (Jul 02 2022 at 14:53):

Ok, gotcha

Adam Topaz (Jul 02 2022 at 14:54):

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

Adam Topaz (Jul 02 2022 at 14:54):

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 (Jul 02 2022 at 14:55):

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 (Jul 02 2022 at 14:56):

That should follow from the AB5 file.

Adam Topaz (Jul 02 2022 at 14:57):

I suppose TC should just pick it up?

Adam Topaz (Jul 02 2022 at 14:57):

if not the isntance is called category_theory.homology_functor_preserves_filtered_colimits

Johan Commelin (Jul 02 2022 at 15:00):

I pushed something that breaks the sorry into pieces.

Johan Commelin (Jul 02 2022 at 15:01):

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

Johan Commelin (Jul 02 2022 at 15:07):

hmm, it aint working, we are missing some instances

Johan Commelin (Jul 02 2022 at 15:09):

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 (Jul 02 2022 at 15:13):

Oh that might actually be missing

Joël Riou (Jul 02 2022 at 15:38):

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.


Last updated: Dec 20 2023 at 11:08 UTC