Ext

Stream: condensed mathematics

[Johan Commelin]

Do we already know in which way we want to talk about Ext?

1. The version that is currently in mathlib, using left_derived
2. The version in LTE using homological functors.

• Can we show that they are isomorphic?
• Can we compute $\text{Ext}^1(ℤ/2ℤ, ℤ/2ℤ)$ with either of these definitions?
• Do we have the LES for Ext for either of these two versions? (I mean syntactically mentioning Ext. Not just left_derived. There are some passages to opposite categories that need to be crossed.)

[Adam Topaz]

As far as I know, the first answer is no, we can't yet relate the two notions. I think it should be straightforward(ish) to compute the Ext1 you mention with the homological functor approach. You take the usual projective resolution of Z/2 as a Z-indexed complex. Next, I'm fairly sure we have the lemmas to show that this is K-projective. Maybe @Andrew Yang can confirm? And finally, it comes down to computing some Hom between complexes.

The homological approach has the LES specifically for Ext in both variables. For the left_derived approach, we would need some more API for taking op of an exact_seq, but that shouldn't be too hard?

[Andrew Yang]

We know that a bounded above complex of projective objects is K-projective.

[Adam Topaz]

Oh, one missing thing on the LES for ext with the homological approach is to show that Ext i A[-1] B is Ext (i+1) A B, which should just be some general thing about hom between shifts (I hope I got the indexing right!). There are also a handful of sorry's in this work that should be closed at some point ;)

[Adam Topaz]

Johan and I discussed a bit this morning, and we agree that the nicest (and almost the quickest?) way to convince ourselves that our Ext is correct is to prove that it's a universal delta functor.
I made a PR with the basic definitions and a sketch here:
https://github.com/leanprover-community/lean-liquid/pull/96

[Adam Topaz]

I proved that effaceable delta functors are universal.
https://github.com/leanprover-community/lean-liquid/pull/97

The fact that Ext is universal should now be easy!

[Adam Topaz]

This is now done

instance (B : A) : delta_functor.universal (Ext_δ_functor A B) :=
delta_functor.universal_of_effacable _

https://github.com/leanprover-community/lean-liquid/pull/105

[Adam Topaz]

Is this convincing enough?

[Adam Topaz]

(This is saying that Ext^i(-,B) is universal, where Ext^i is really defined using Ext' i which is Ext i applied to objects of the bounded homotopy category obtained by applying the single 0 functor.)

[Johan Commelin]

Cool!

[Johan Commelin]

I think that we can certainly use this to write a convincing examples/Ext.lean.

[Adam Topaz]

Yeah, let's get those two PRs merged (the one above, and your start of the examples/Ext) then we can finish off the example file for Ext.

[Johan Commelin]

It can include the nice defeqs of Ext_δ_functor, an example of a 5-term LES, the computation of Ext^1(ℤ/nℤ, ℤ/nℤ) and the isomorphism between Ext^0 and Hom.

[Johan Commelin]

Together, those seem to me like a good "extensional" spec of Ext.

[Adam Topaz]

We don't have universality in the second variable, unfortunately.

[Adam Topaz]

(and we probably wont for a while!)

[Johan Commelin]

Sure, it's not a complete spec, but it's good enough, I think.

[Johan Commelin]

Adam Topaz said:

This is now done

instance (B : A) : delta_functor.universal (Ext_δ_functor A B) :=
delta_functor.universal_of_effacable _

https://github.com/leanprover-community/lean-liquid/pull/105

I left two mini comments.

[Johan Commelin]

Both PRs are merged

[Adam Topaz]

Some more work on the ext example file
https://github.com/leanprover-community/lean-liquid/pull/107

Note in particular:

/-- Any natural transformation `Hom(-,B) ⟶ F 0` to the zeroth-component of some
delta functor `F` extends in a unique way to a morphism of delta functors
`Ext_δ_functor A B ⟶ F`.
Note that `Ext' 0 (X,B)` is not defeq to `Hom(X,B)`, so we must compose with the isomorphism
`Ext'_zero_flip_iso` that was mentioned in the previous example.
-/
theorem Ext_δ_functor_is_universal_for_Hom (B : A) (F : Aᵒᵖ ⥤δ Ab.{v})
  (e0 : preadditive_yoneda.obj B ⟶ F 0) :
  ∃! (e : Ext_δ_functor A B ⟶ F),
  e0 = (Ext'_zero_flip_iso _ _).inv ≫ (e : Ext_δ_functor A B ⟶ F) 0 := ...

[Adam Topaz]

I guess I should now ask if there is anyone who is NOT convinced that this is the right Ext, and to explain what it would take for them to be convinced.

[Reid Barton]

Is there some elementary reformulation of "Ext^i(A, B) = 0 for all i >= 1"? e.g. Ext^1(A, B) = 0 means that every extension of A by B is trivial

[Adam Topaz]

We have this example :)

/-- An explicit computation: `Ext^1(ℤ/n,ℤ/n) = ℤ/n`. -/
example (n : ℕ) (hn : n ≠ 0) :
  ((Ext' 1).obj (op $ of $ zmod n)).obj (of $ zmod n) ≅ of (zmod n) :=

[Adam Topaz]

and a proof that Ext i (P,B) = 0 whenever P is projective ( this is not in the examples file yet, although it would be very easy to add).

[Adam Topaz]

Actually, it wouldn't be too hard to prove that $Ext^i(P,B) = 0$ for all $i > 0$ and all B implies $P$ is projective.

[Adam Topaz]

Adam Topaz said:

Actually, it wouldn't be too hard to prove that $Ext^i(P,B) = 0$ for all $i > 0$ and all B implies $P$ is projective.

Well, maybe it's not so easy, because it seems that we never set up the API for the LES in the second variable (although we have some general thing that Ext i(X,-) is a homological functor)

[Johan Commelin]

The PR is merged.

[Adam Topaz]

Thanks!

[Adam Topaz]

Are there other properties of Ext you think we should add? We could add the characterization of projectives in terms of Ext, but that would take some more work (we don't have a convenient LES in the second variable)

[Johan Commelin]

The main thing missing from https://github.com/leanprover-community/lean-liquid/tree/master/src/examples is some examples for $\mathcal{M}_{p'}(S)$. But we'll get there in the next few days.

[Johan Commelin]

We could add an explicit example of a 5-or-6-term LES of Ext-groups. Just to show what it looks like in Lean. I don't think it would add to the "convincing evidence" but it does have "showcase" value, I think.