computing Ext with acyclics

Stream: condensed mathematics

[Johan Commelin]

I basically have the following sorry-free

def Ext_compute_with_acyclic
  (C : cochain_complex 𝓐 ℤ) (B : 𝓐)
  [((quotient 𝓐 (complex_shape.up ℤ)).obj C).is_bounded_above]
  (hC : ∀ k, ∀ i > 0, is_zero (((Ext' i).obj (op $ C.X k)).obj B))
  (i : ℤ) :
  ((Ext i).obj (op $ of' C)).obj ((single _ 0).obj B) ≅
  (((preadditive_yoneda.obj B).right_op.map_homological_complex _).obj C).unop.homology (-i) :=

But I'm quite terrified of proving that this is natural in C. Especially because the typeclass condition on C forbids stating this as an isom of functors.

[Johan Commelin]

see for_mathlib/acyclic if you want to inspect this interactively.

[Adam Topaz]

Nice!

[Adam Topaz]

The preserving coproduct thing is almost done... the only sorry left for that is

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 _ ⥤ _) := sorry

[Adam Topaz]

(I.e. all the homotopy junk has been removed from the statementt)

[Adam Topaz]

I'll try to finish it off, but I don't have much more lean time today, so I don't know how far I'll get.

[Adam Topaz]

It's near the bottom of for_mathlib/derived/ext_coproducts, just in case