Ext commutes with coproducts

Stream: condensed mathematics

[Adam Topaz]

Hi all,

I've been working on the fact that $Ext(-,Y)$ sends coproducts to products.
The statement is here:
https://github.com/leanprover-community/lean-liquid/blob/734501a160b2c70d7783ef0eab9d2efda97ca696/src/for_mathlib/derived/ext_coproducts.lean#L379

There are a few sorries left for this:

1. A coproduct of quasi isos is a quasi iso:
   https://github.com/leanprover-community/lean-liquid/blob/734501a160b2c70d7783ef0eab9d2efda97ca696/src/for_mathlib/derived/ext_coproducts.lean#L238

2. Existence of projective replacements with a uniform bound in a family of complexes, given that the members of the family have a uniform upper bound (this should be more-or-less just repackaging what's already been done about projective replacements):
   https://github.com/leanprover-community/lean-liquid/blob/734501a160b2c70d7783ef0eab9d2efda97ca696/src/for_mathlib/derived/lemmas.lean#L509

[Adam Topaz]

We will also need some naturality properties of this isomorphism, but those shouldn't be too difficult.

[Adam Topaz]

(the result about quasi-isos might need some additional assumptions on the abelian category)

[Adam Topaz]

The only two sorries left for this (ext commutes with coproducts) are here:
https://github.com/leanprover-community/lean-liquid/blob/9cef18ca127f1c740f7da2fcfc9b120f0b07cf3e/src/for_mathlib/ab4.lean#L102

[Adam Topaz]

Okay, it's down to one sorry:
https://github.com/leanprover-community/lean-liquid/blob/c94305820be33c01342fa53b41406f7a61648eb8/src/for_mathlib/ab4.lean#L107

This is just some statement about regular homology (I already added the necessary glue to pass to the homotopy category).
It should be doable in case anyone is bored (Kevin?)

[Kevin Buzzard]

I've got my hands full with showing that if |(X-2)g(X)|<=c then |g(X)|<=c' right now, so am no longer bored.

[Adam Topaz]

Quick update:

noncomputable
def Ext_coproduct_iso
  [AB4 A]
  {α : Type v}
  (X : α → bounded_homotopy_category A)
  [uniformly_bounded X]
  (i : ℤ) (Y) :
  ((Ext i).obj (op (sigma_obj X))).obj Y ≅
  pi_obj (λ a : α, ((Ext i).obj (op (X a))).obj Y) := ...

is sorry-free.

Unfortunately, the [uniformly_bounded X] assumption makes it hard to state a correct version in terms of Ext commuting with certain (co)limits, so we may have to prove the naturality conditions separately, although they should not be difficult.

[Adam Topaz]

Alright, I added the following naturality sttatements as well:

lemma Ext_coproduct_iso_naturality
  [AB4 A]
  {α : Type v}
  (X₁ X₂ : α → bounded_homotopy_category A)
  [uniformly_bounded X₁]
  [uniformly_bounded X₂]
  (g : X₁ ⟶ X₂)
  (i : ℤ) (Y) :
  ((Ext i).map (sigma.desc (λ b, g b ≫ sigma.ι X₂ b) : ∐ X₁ ⟶ ∐ X₂).op).app Y ≫
  (Ext_coproduct_iso _ _ _).hom =
  (Ext_coproduct_iso _ _ _).hom ≫
  pi.lift (λ b, pi.π _ b ≫ ((Ext i).map (g b).op).app Y) := ...

lemma Ext_coproduct_iso_naturality'
  [AB4 A]
  {α : Type v}
  (X : α → bounded_homotopy_category A)
  [uniformly_bounded X]
  (i : ℤ) (Y₁ Y₂) (f : Y₁ ⟶ Y₂) :
  ((Ext i).obj (op (sigma_obj X))).map f ≫
  (Ext_coproduct_iso _ _ _).hom =
  (Ext_coproduct_iso _ _ _).hom ≫
  pi.lift (λ a, pi.π _ a ≫ ((Ext i).obj _).map f) := ...

[Johan Commelin]

That's really great! We're getting close to ticking off two more ovals.

[Johan Commelin]

Hmm... we might also need the fact that chain_complex.to_bounded_homotopy_category preserves coproducts.

[Johan Commelin]

We can prove that we have a termwise short exact sequence $\bigoplus \to \bigoplus \to \text{foo}$ at the level of complexes, and then we want to apply Ext(_, V) to that, and get a LES, and pull the coproducts out of the Ext.

[Adam Topaz]

@Johan Commelin that should be trivial to prove

[Adam Topaz]

Write it as a composition of going via the homotopy cat, and I think i proved both functors preserve coproducts

[Adam Topaz]

I can add it in a few mins

[Johan Commelin]

Aha, so you have this uniformly-bounded type class also for the homotopy cat?

[Johan Commelin]

I just pushed some stuff. There are plenty sorries :see_no_evil: The glue to get to first_target is at least as painful as I was expecting it to be. Really everything has to be functorial... which makes it annoying to even write down statements.

[Adam Topaz]

@Johan Commelin where can I find chain_complex.to_bounded_homotopy_category again?

[Johan Commelin]

derived/example.lean

[Adam Topaz]

I was wrong in my comment above, but it should still be easy to prove

[Johan Commelin]

We should really clean up that file

[Adam Topaz]

Agreed.

[Adam Topaz]

If anyone wants to get annoyed with completely trivial things that are hard in lean, here are a few sorries for you:

noncomputable
instance homological_complex_embed_preserves_coproducts {α : Type v}
  {M N : Type} (c₁ : complex_shape M) (c₂ : complex_shape N) (e : c₁.embedding c₂) :
  preserves_colimits_of_shape (discrete α)
  (homological_complex.embed e : homological_complex A _ ⥤ _) :=
preserves_coproducts_aux
(homological_complex.embed e : homological_complex A _ ⥤ _)
(λ (X : α → homological_complex A c₁), homological_complex.hom.iso_of_components
sorry sorry) -- Ugh... this is so annoying!
sorry

They can be found here:
https://github.com/leanprover-community/lean-liquid/blob/c60d928c4fab0c3e9f87a8da50415515dca3b0bc/src/for_mathlib/derived/ext_coproducts.lean#L282

[Kevin Buzzard]

I've just removed the sorry from invpoly/ses.lean so on the tube home I'll get annoyed with this.

[Kevin Buzzard]

ooh, is the first goal full of option.recs and doesn't fit on one screen? Maybe I won't even have time to get annoyed with it, I might spend the journey trying to figure out what the question is.

[Adam Topaz]

The option.rec stuff probably needs to be modified slightly.

[Kevin Buzzard]

  { simp_rw [h₁, h₂],
    dsimp,
    simp,
    sorry -- still annoying

seems to change the first sorry into a statement of the form "d commutes with a map comprised of the composition of about 4 canonical isomorphisms"

[Adam Topaz]

Oh nice! It should be doable now!

[Adam Topaz]

take a look at the lemma called embed.d_eq_of_some_of_some` (or some variant)

[Adam Topaz]

I'm working on that sorry now

[Adam Topaz]

Okay, that sorry is killed.... but

-- still annoying

remains

[Kevin Buzzard]

Oh lol I thought the hard part was pushing the d through the isomorphisms :-)

[Adam Topaz]

Alright, the remaining sorry is done as well!

[Adam Topaz]

It's (very) far from the cleanest proof...

[Kevin Buzzard]

I would send a :tada: but I'm getting an exciting new error "failed to add reaction" on Android

[Adam Topaz]

I think in android congratulations is broken but tada works? :shrug:

[Adam Topaz]

:congratulations:

[Johan Commelin]

Kevin Buzzard said:

I've just removed the sorry from invpoly/ses.lean so on the tube home I'll get annoyed with this.

Unfortunately there is no oval for this in the graph. But I'm certainly glad that this is done!

[Kevin Buzzard]

Changing the subject a bit then: do you now have a clear overview of all the remaining sorrys, eg are you convinced that they're all fillable without any refactors, is there any sorryed data, are there people working on every sorry, are there things which can be farmed out (you've done a very good job of farming out sorries to me, you directed me to problems that were within my skillset to solve etc).

[Johan Commelin]

Yesterday I added a bunch of sorrys that are data. :see_no_evil: They are "canonical" isomorphisms between certain functors.
I can not promise that we don't need any further refactors. The glue between the first and the second part of the project is not very pleasant.

[Johan Commelin]

Of course, hindsight is 20-20. But if I could start again, there are two things that I would do differently in the first part:

• Given M : ProFiltPNGWithTinv and BD : breen_deligne.data + suitable constants, define FPSystem : chain_complex (Free int Profinite) nat. That's a fundamental kind of object, where a lot of the computations happen. After that, apply the V-hat functor and take T^{-1}-invariants.
  • Currently, all the computations happen after apply V-hat(_)^{T-1} functor, making many proofs complicated and messy.
  • It would be one contribution to make the glue easier (although I have now defined FPSystem and glued it to the first part, so from the pov of the second part, we can now basically assume that FPSystem was used in the first part.
• Minor technical issue: Use Free int in the definition of Breen-Deligne data, instead of free_abelian_group. It would mesh better with the point above. Also free_abelian_group lacks API, even though it occasionally has a nice defeq. But in the end, finsupp is just better.
  • Eg. given a term x : free_abelian_group X, it is very annoying to talk about the support of x. But with finitely supported functions to int this is trivial.