homology of Q'

Stream: condensed mathematics

[Johan Commelin]

In https://leanprover-community.github.io/liquid/sect0008.html#Qprime-Cond we have the statement

$$H_i(Q'(M)) ≅ H_i(Q'(ℤ)) ⊗ M$$

for torsion-free condensed abelian groups $M$. The way you prove this is by writing $M$ as a filtered colimit of fg free objects, and then noting that $H_i$ and $Q'$ both commute with filtered colimits and direct sums. $Q'$ commutes with direct sums when viewed as a functor to the homotopy category because of the homotopy condition in BD packages.

I don't see any obstructions to formalizing this. But I have a maths question: what we really need is the fact that this is also natural in $M$. More precisely: if $f \colon M → M$ is an endomorphism, and we push it through the functors on the left, why do we end up with $\text{id} ⊗ f$ on the right?

[Johan Commelin]

It's the only reasonable candidate, but I couldn't figure out a precise proof easily.

[Peter Scholze]

About the proof: You first prove the result on presheaves -- $H_i(Q'(M(S)))\cong H_i(Q'(\mathbb Z))\otimes M(S)$ for extremally disconnected $S$ -- and for this you write $M(S)$ in the way described in Johan's message. ($M$ itself is very much not a filtered colimit of fg free objects in general.)

[Johan Commelin]

Aah, good point. Yes, my verbal summary of the strategy was a bit too fast.

[Peter Scholze]

To get functoriality: Maybe it's easier if you first describe the map, at least on elementary tensors? It sends $v\otimes m\in H_i(Q'(\mathbb Z))\otimes M(S)$ to the image of $v$ under the map $H_i(Q'(\mathbb Z))\to H_i(Q'(M(S)))$ induced by the map $\mathbb Z\to M(S)$ sending $1$ to $m$.

[Adam Topaz]

@Johan Commelin do we have an established way to talk about torsion-free (condensed) abelian groups?

[Johan Commelin]

Nope, I don't think there is anything about torsion free. Although mathlib does have something about torsion, but I'm not sure that's too relevant.

[Adam Topaz]

I added some work in progress toward this lemma in for_mathlib/AddcommGroup near the bottom.
A few sorries there are very easy... any help would be much appreciated!

[Adam Topaz]

Adam Topaz said:

Johan Commelin do we have an established way to talk about torsion-free (condensed) abelian groups?

For future reference, I used docs#no_zero_smul_divisors because that's what's used in docs#module.free_of_finite_type_torsion_free

[Adam Topaz]

This is now sorry-free in for_mathlib/AddCommGroup

lemma is_iso_of_preserves_of_is_tensor_unit {𝓐 : Type u'} [category.{u} 𝓐] [preadditive 𝓐]
  (F G : AddCommGroup ⥤ 𝓐)
  [F.additive]
  [G.additive]
  [limits.preserves_filtered_colimits F]
  [limits.preserves_filtered_colimits G]
  (η : F ⟶ G)
  (U : AddCommGroup)
  (hU : U.is_tensor_unit)
  [hη : is_iso (η.app U)]
  (A : AddCommGroup.{u})
  [no_zero_smul_divisors ℤ A] :
  is_iso (η.app A) := ...

where

def is_tensor_unit (A : AddCommGroup.{u}) : Prop :=
∃ a : A, ∀ (B : AddCommGroup.{u}), function.bijective
  (λ f : A ⟶ B, (f : A → B) a)

This way we don't need to make a choice about what tensor unit we choose.