BD lemma: last line

Stream: condensed mathematics

[Johan Commelin]

The last line of the proof of https://leanprover-community.github.io/liquid/sect0008.html#Qprime-prop is

In general, one can pick a two-term free resolution of $A$ and use the long exact sequence.

I am now wondering what the smoothest way is to do this in Lean.
The context is the following: Let $A$ be an abelian group and $0 → F₁ → F₀ → A → 0$ a free resolution. Let $M$ be a condensed abelian group (which we can assume to be torsion-free). We want to show that $\text{Ext}^i(M ⊗ A, N)$ vanishes, and we know already that $\text{Ext}^i(M ⊗ F_j, N)$ vanishes for free $F_j$.

I think the easiest way to continue is to show that $0 → M ⊗ F₁ → M ⊗ F₀ → M ⊗ A → 0$ is short exact, using the fact that $M$ is torsion-free. What I really want to avoid is any theoretical properties of Tor, because we don't have anything about it. What is the cheapest (in terms of ingredients) way to prove (on paper) that a torsion-free abelian group is flat?
Note that we don't even need to show that M ⊗ _ is exact: a direct proof that it sends injective maps between free abelian groups to injective maps is all we need.

[Kevin Buzzard]

Torsion-free is a filtered colimit of f.g. free, does that help?

[Johan Commelin]

I guess it does

[Filippo A. E. Nuccio]

OK, so moving from Kevin's suggestion, this is a strategy I came up with, trying to check what is already in mathlib:
1) Following Kevin's idea, I reduce to the case where both M, F1 and F2 are finitely generated free abelian groups. Yet, two things are not clear to me here:
1a) Is Kevin's claim already in mathlib (on in themathlib folder)?
1b) Same question for "filtered colimit of injections is injective" (aka left-exactness, but I do not know how and if this is implemented)
2) So now I have to prove that if $\varphi\colon F_1 \hookrightarrow F_2$ is an injection of finitely generated free abelian groups and $M$ is also f. g. free, then $\varphi\otimes 1\colon F_1\otimes M \rightarrow F_2\otimes M$ is injective. For this, I would use the

lemma foo (f : M →ₗ[R] N) (v : ι → M) (hv : basis ι R M)
 (hι : fintype ι)
 : function.injective f ↔ linear_independent R (f ∘ v) :=

saying that a linear map is injective iff it sends a basis to a linearly independent set.
3) So I have three bases $\{f_i\}, \{f'_j\}$ and $\{m_k\}$ of $F_1,F_2,M$ respectively; I can use docs#module.free.tensor to know that $\{f_i\otimes m_k\}$ is a basis of $F_1\otimes M$ and I apply $\varphi\otimes 1$ to each member. I need to show that the result is a linearly independent set.
4) For this, I would like to adapt some of the results we have for determinants (like the first part of docs#linear_independent) to show that if a determinant is non-zero, then the set is linearly independent
5) Finally, I would adapt some results from docs#matrix.kronecker to the effect that the matrix representing $\varphi\otimes 1$ wrt $\{f_i\otimes m_k\}$ and $\{f_j'\otimes m_k\}$ is the Kronecker product of the identity and of the matrix representing $\varphi$ and hence its determinant is non-zero by the assumption on $\varphi$.

Does it sound a sufficiently down-to-earth plan? I can start working on this soon.

[Johan Commelin]

I think you don't even need to do reduction steps for F₁ and F₂.
If you have a SES 0 → A → B → C → 0 and you tensor it with M, where M is a filtered colimit of fg free groups, then you reduce to checking that

• your 1b
• the SES remains injective after tensoring with fg free groups

[Johan Commelin]

But tensoring with fg free groups is just taking a suitable direct sum of the objects in the SES, and it should be easy to prove that this remains exact by induction.

[Adam Topaz]

I'm not so sure about that last point -- you really need the torsion-freeness assumption for that!

[Johan Commelin]

Which point? If you have a SES and you tensor it with ℤ^k then it remains a SES.

[Adam Topaz]

yeah

[Johan Commelin]

That's just because ℤ^k is free, hence flat.

[Adam Topaz]

Oh sorry, tensor WITH Z^k, okay yeah that's easy

[Johan Commelin]

The torsion-free-ness is used completely in showing that M is a filtered colimit of fg free groups.

[Adam Topaz]

yeah I agree sorry I should have read more carefully

[Adam Topaz]

that should indeed just be a simple induction on k

[Johan Commelin]

I think I would try to stay in the realm of category theory as long as possible. You should be able to avoid kronecker products completely.

[Adam Topaz]

Do we know that tf implies filtered colimit of f.g. free?

[Johan Commelin]

Nope, I guess not.

[Filippo A. E. Nuccio]

Yes, I guess you are right, we do not need to pick basis for $F_1$ and $F_2$. I will then first of all try to prove that tf implies filtered colimit of f.g. free, and then prove the lemma by induction on $k=\mathrm{rk}M$.

[Filippo A. E. Nuccio]

Another idea that came to my mind is the following: I fix two free $\mathbb{Z}$-modules $F_1,F_2$ with an injection $\varphi\colon F_1\hookrightarrow F_2$ and a torsion-free $M$. If we can show that $F_1\otimes M \otimes \mathbb{Q}\rightarrow F_2\otimes M\otimes\mathbb{Q}$ is injective, then also $F_1\otimes M\rightarrow F_2\otimes M$ is injective, because so is $F_1\otimes M\hookrightarrow F_1\otimes M\otimes\mathbb{Q}$ by the torsion-freeness assumption. In order to show that $F_1\otimes M \otimes \mathbb{Q}\rightarrow F_2\otimes M\otimes\mathbb{Q}$ is injective, we can write the arrow as

$$(F_1\otimes \mathbb{Q})\otimes_{\mathbb{Q}}(M \otimes \mathbb{Q})\rightarrow (F_2\otimes \mathbb{Q})\otimes_{\mathbb{Q}}(M\otimes\mathbb{Q})$$

and therefore the key point becomes to show that (not-necessarily finite dimensional) vector spaces are flat. One proof of this fact goes through proving that they are a cofiltered limit of their finite dimensional subspaces, but then we are basically back at Kevin's suggestion. Is there an easier way to show this flatness of vector spaces directly? According to this thread on MO, it only holds under AC...

[Johan Commelin]

I think this requires API about base change of the ring of scalars that we don't have yet.

[Filippo A. E. Nuccio]

At which point? We have that the tensor product is associative and commutative and that the tensor prod of two free is free.

[Filippo A. E. Nuccio]

If it is about tensoring over $\mathbb{Q}$ instead of over $\mathbb{Z}$ once everything is a v.s., isn't it worth building this API?

[Filippo A. E. Nuccio]

I also understand that you want to go straight to the point, but if there was an easier way avoiding the fact that colimits are left exact and that a torsion-free is a filtered colimit of f.g. free, I though it might be at any rate a good trial.

[Johan Commelin]

I think it's certainly worth building that API at some point. But I think exhibiting a tf ab group as cofiltered limit of fg free ones shouldn't be too hard, and is also worth building.

[Filippo A. E. Nuccio]

OK, I guess you have a clearer picture. I will follow that line. And what about left-exactness of colimits, is it already there (in LTE, perhaps)?

[Adam Topaz]

You could use the fact that filtered colimits commute with finite limits (e.g. kernels) which is in mathlib, or just do it by hand since you're working with abelian groups, using the mathlib api for filtered colimits in concrete categories (category_theory/limits/concrete)

[Adam Topaz]

Well, the quickest way is probably to just do things in a totally hands on way with sums of basic tensors. Take an element of the tensor product, write it as a sum of basic tensors to find a f.g. free submodule whose tensor product contains those elements, and use that to reduce to the free case.

[Filippo A. E. Nuccio]

Yes, I agree this should be the quickest way. Thanks!

[Filippo A. E. Nuccio]

(deleted)

[Filippo A. E. Nuccio]

(deleted)

[Filippo A. E. Nuccio]

(deleted)