preserves_finite_colimits_of_exact

Stream: condensed mathematics

[Joël Riou]

As Kevin suggested, I may give some help in the LTE. I just browsed into the repository to find some sorry that I could remove. I am able to finish the proof of preserves_finite_colimits_of_exact in for_mathlib/exact_functor.lean. What remained was that an exact functor between abelian categories preserves coequalizers, and as the work had already been done for cokernels, the proof was purely nonsensical (expressing a coequalizer as the cokernel of a difference of the two maps). I do not know what is the procedure to contribute to the LTE repository: how should I proceed?

[Johan Commelin]

Fantastic! Thanks a lot for helping. Here's an invite: https://github.com/leanprover-community/lean-liquid/invitations
Feel free to push to master directly. We follow a very loose policy, compared to mathlib.
The only rule is that master should compile without errors. This rule is broken approximately once a month. But it's usually fixed in a couple of hours, and then that's fine.

[Joël Riou]

Thanks! I have pushed this. I shall try to continue fixing some other sorries.

[Adam Topaz]

Thanks @Joël Riou ! That same file has several (smaller) sorries around homology that should be relatively easy.

[Joël Riou]

@Adam Topaz Indeed, I already removed two other small sorries for homology_iso. For homology_functor_iso, I would be tempted to change the definition and make this a quite straightforward application of homology_iso as something starting like :

def homology_functor_iso {M : Type*} (c : complex_shape M) (i : M) :
  homology_functor A c i ⋙ F ≅
  F.map_homological_complex _ ⋙ homology_functor B c i :=
nat_iso.of_components
(λ X,
begin
  refine homology_iso F (X.d_to i) (X.d_from i) (X.d_to_comp_d_from i) (by simp [← F.map_comp])
    ≪≫ homology.map_iso _ _ _ _ _,

It seems the only place where the definition of homology_functor_iso is used is in the unfinished proof of homology_functor_preserves_filtered_colimit in ab5.lean, so that changing the def would not seriously break anything. The sorry in that unfinished proof seems uneasy (it is an intricate equality of morphisms). A more basic approach for this would be to prove that the nat_trans.kernel_functor (resp. cokernel_functor) of a natural transformation between filtering colimit preserving functors also preserve filtering colimits. Then, expressing the homology as a combination of kernel and cokernel, the lemma would basically reduce to the fact that the evaluation functors homological_complex A c ⥤ A preserve filtered colimits, which you did already. It might be quite long, but each step would be small. However, it seems there are suboptimal universe assumptions in the definition of nat_trans.kernel_functor in mathlib. Then, the right thing would be to fix this in mathlib, which may imply syncing with the current version of mathlib. :skull_and_crossbones:

[Adam Topaz]

From past experience, it seems that homology is easier to work with if maps to/from are defined using homology.liftand homology.desc' (note the '), so I would prefer to keep the defs as they are. With you suggestion, the map would be a composition of two such morphisms, so it would still be reasonable to work with.

[Adam Topaz]

Oh actually using homology.map_iso would probably introduce some stuff that's not very pleasant...