Tensor Products

Stream: condensed mathematics

[Adam Topaz]

Quick update:
The file condensed/tensor is sorry-free. This defines the tensor product of a condensed abelian group with an abelian group, as a condensed abelian group, and shows that it can be evaluated pointwise when evaluated on extremallly disconnected sets.

[Adam Topaz]

I just pushed a skeleton for the isomorphism $H^i(Q'(\mathbb{Z})) \otimes M \cong H^i(Q'(M))$. It's in condensed/bd_lemma and still has various sorries to fill in (but all the data required for this isomoprhism should be there)

[Johan Commelin]

Cool! You made a bunch of progress while I was away!

[Johan Commelin]

@Filippo A. E. Nuccio pushed a proof of instance : no_zero_smul_divisors ℤ (Lbar r' S). That will be useful once we apply the BD lemma in our concrete situation.

[Adam Topaz]

Do we only need this for the case where S is finite?

[Filippo A. E. Nuccio]

AFAIK no, I was planning to work on proving that if this holds for finite S then it passes through profinite ones.

[Filippo A. E. Nuccio]

Do we already know (well: "is it true?", first of all; and then...) that for S : Profinite.{u}

preserves_limit (fintype_diagram S ⋙ Fintype_Lbar.{u u} r') (category_theory.forget.{u+1 u u}(ProFiltPseuNormGrpWithTinv₁.{u} r'))

? As composition of two functors, it boils down to knowing if both fintype_diagram and Fintype_Lbar do: @Adam Topaz , have you already implemented these? This should be more or less trivial for Fintype_Lbar, what about fintype_diagram?

[Adam Topaz]

I don't think this is true as stated because the limits of ProFilt... are these so-called bounded limits (take a look at pseudo_normed_group/bounded_limits)

[Filippo A. E. Nuccio]

Ah ok: but do you agree that the problem comes from fintype_diagram?

[Adam Topaz]

I'm not so sure... what are you trying to use this for?

[Filippo A. E. Nuccio]

I used it to prove that Lbar evaluated at a profinite set was torsion_free, and I finished the proof with that sorry, which you now tell me is false. I will try to dig tomorrow in bounded_limit to understand what can be adapted. Have to rush now!

[Filippo A. E. Nuccio]

Thanks!

[Adam Topaz]

I see... I think the way to go here is to use the bounded limits stuff to now that the underlying abelian group of a limit of these ProFilt...s embeds in the limit of the underlying abelian groups of the ProFilt...s, and use the fact that the limit of abelian groups embeds in the Cartesian product. That should let you reduce from from the profinite case to the finite case.

[Filippo A. E. Nuccio]

Great, thanks. I will try this tomorrow morning and will come back if I need help

[Filippo A. E. Nuccio]

@Adam Topaz So I went through the bounded_limit and I have pushed a first attempt at implementing this for PFPNG_with_Tinv in Lbar.torsion_free_flat.

[Filippo A. E. Nuccio]

My idea was to adapt most of your work done for PseuNormGrp₁.

[Filippo A. E. Nuccio]

Do you think you can have a look at the file? In particular, at the final proof of the instance on line 154. I think that

• the have lim_to_Ab corresponds to what you meant by " the limit of the underlying ab. grps"
• the have h_tf is the claim I am looking for but computed in Ab
• the have iso is the fact that the bounded gadget is indeed a limit and so two of them must be isomorphic.

[Filippo A. E. Nuccio]

How does it sound?

[Filippo A. E. Nuccio]

(of course, if you do not have time now, please do not worry!)

[Adam Topaz]

Oh, sorry I should have been more detailed... there is no need to duplicate the bounded limits work because we already know that the functor which drops the Tinv action preserves limits. So you first pass to pfpng1 with no Tinv, the. You can use the bounded limit api that's already there

[Filippo A. E. Nuccio]

Yes, I thought so, that's why I passed through your work and I have sorried the functor from PNPF_withTinv to pfpng1, just to have everything compile.

[Filippo A. E. Nuccio]

But I was indeed hoping that all the duplication would not be needed.

[Adam Topaz]

M quite sure we have that...

[Filippo A. E. Nuccio]

Adam Topaz said:

M quite sure we have that...

Sure, I was just lazy in looking for it. I was first checking with you if the strategy set up in the proof of the instance on l. 154 looked OK to you, if yes I will look more carefully.

[Adam Topaz]

I'm on mobile right now so it will be hard for me to check, but I'll look in the next couple of hours.

[Adam Topaz]

In fact we should know that the functor to pfpng1 even creates limits!

[Adam Topaz]

So you could do a grep for creates_limits and see what comes up

[Filippo A. E. Nuccio]

No problem, sure! Let me simply emphasize that I was quite sure (having seen the amazing! work you did for the bounded limits in the pfpng1 setting) that we already had excellent technology. So I was not trying to redo anything, and I also do not need much input from you. When you have time, please just have a look if what I did seems completely insane or reasonable, and in the second case I will go on on my own. After all, things are starting to become much clearer with these limits...

[Adam Topaz]

@Filippo A. E. Nuccio I pushed a commented-out skeleton for the argument I had in mind, as part of the same proof you pointed me to.
I also filled in the missing functor as it was just a composition of two we already had, and I used previous work to observe that it preserves limits (which is required for the skeleton I sketched). I hope this helps!

In terms of what you had written, it would work in principle, of course, but the key step where you embed the bounded limit cone point into the limit of abelian groups was missing (well, hidden in the sorry labeled h_tf).

[Johan Commelin]

I pushed a (sorried) condensed version of the statement that Lbar is torsion free.

[Johan Commelin]

@Filippo A. E. Nuccio Would it be possible to abstract over Fintype_Lbar?

[Johan Commelin]

I think

lemma extend_torsion_free (A : Fintype.{u} ⥤ CompHausFiltPseuNormGrp₁)
  (hA : ∀ X, no_zero_smul_divisors ℤ (A.obj X)) (S : Profinite) :
  no_zero_smul_divisors ℤ ((Profinite.extend A).obj S) :=
sorry

should be provable, and maybe easier because you don't have to worry about Lbar.

[Johan Commelin]

I have a proof of

instance (S : Profinite.{u}) (T : ExtrDisc.{u}) :
  no_zero_smul_divisors ℤ (((condensed.{u} r').obj S).val.obj (op T.val)) :=

that only depends on that sorry

[Johan Commelin]

In other words, the glue from the profinite extension to condensed abelian groups is done.

[Johan Commelin]

It's in src/Lbar/torsion_free_condensed.lean

[Adam Topaz]

Yeah that's a better generalization.

[Adam Topaz]

The skeleton I wrote should adapt easily to this

[Filippo A. E. Nuccio]

@Adam Topaz @Johan Commelin Thanks Adam! I will look at both the files on Monday. I think that abstracting over Fintype_Lbar will not be an issue at all, I will write here if I find any problem.

[Adam Topaz]

@Joël Riou I see that you're working on the tensor product colimit sorry -- I think the simple way to do this is to use the fact that evaluation at ExtrDiscs jointly creates colimits of condensed abelian groups, which lets you reduce to the abelian group case (using some already existing isomorphisms). Your approach would work as well, of course.

[Adam Topaz]

if you prefer, you could also use the fact that the functor from ExtrSheaf to presheaves creates colimits (this is an existing instance)

[Adam Topaz]

I pushed the argument just now

[Adam Topaz]

(it can be used to show that tensor preserves all colimits, not just coproducts)

[Adam Topaz]

Well, there are two small sorries:

def tensor_functor_iso_flip :
  tensor_functor.flip ≅ tensor_functor :=
nat_iso.of_components (λ A,
  nat_iso.of_components (λ B, tensor_flip _ _) sorry) sorry

[Adam Topaz]

(that's for plain abelian groups)

[Adam Topaz]

okay, the file should be sorry-free now :)

[Joël Riou]

Sorry, I had not seen your message. I had reached the same reduction to abelian groups (by a slightly longer path). Thanks for pushing all this. (I learnt a few things in the process!)

[Adam Topaz]

the equivalence with sheaves on ExtrDisc is a really powerful trick

[Patrick Massot]

This is even true on paper, right?

[Patrick Massot]

I mean my understand is it's not a trick, it's a rather important part of the story.

[Adam Topaz]

Yeah of course, trick is not the right word, it's really a key part

[Adam Topaz]

I guess what surprises me a little is just how powerful/useful this equivalence is from the formalization perspective. I think we've used it in LTE even more than the paper proof (By which I mean the blueprint)

[Johan Commelin]

I got the impression that

lemma tensor_short_exact (A : (Condensed.{u} Ab.{u+1}))
  [∀ S : ExtrDisc.{u}, no_zero_smul_divisors ℤ (A.val.obj (op S.val))]
  {X Y Z : Ab} (f : X ⟶ Y) (g : Y ⟶ Z) (hfg : short_exact f g) :
  short_exact ((tensor_functor.obj A).map f) ((tensor_functor.obj A).map g) :=
sorry

is basically done. Is that true? If so, where?

[Adam Topaz]

Maybe it's not quite done. But if you use exact_iff_ExtrDisc along with the isomorphism (which we have) you get by evaluating the tensor product at an ExtrDisc with the plain tensor product of abelian groups, then you can reduce to the usual flatness of a tf-abelian group.

[Adam Topaz]

Maybe we should also have short_exact_iff_ExtrDisc?

[Johan Commelin]

I think we have it

[Johan Commelin]

But we should move it out of that QprimeFP file

[Johan Commelin]

I moved it to a new file condensed/short_exact.lean

[Johan Commelin]

Do we have the statement that exact f g → exact (F.map f) (F.map g) is F preserves finite limits and colimits?

[Adam Topaz]

yes it's somewhere

[Adam Topaz]

don't ask me where :hear_no_evil:

[Johan Commelin]

Aha, we have

def exact : Prop :=
∀ ⦃X Y Z : A⦄ (f : X ⟶ Y) (g : Y ⟶ Z), exact f g → exact (F.map f) (F.map g)

[Adam Topaz]

yeah but that's not very good

[Adam Topaz]

because we really want to use functors that preserve finite (co)limits

[Adam Topaz]

docs#category_theory.abelian.functor.preserves_exact_of_preserves_finite_limits_of_mono

[Adam Topaz]

oh that has a mono

[Adam Topaz]

blah!

[Adam Topaz]

I'm proving it. give me 5 mins

[Adam Topaz]

done at for_mathlib/preserves_exact

[Johan Commelin]

wow, that was fast!

[Adam Topaz]

I got some good coffee today ;)

[Johan Commelin]

Do we have

instance tensor_functor_preserves_finite_limits [no_zero_smul_divisors ℤ A] :
  limits.preserves_finite_limits (tensor_functor.obj A) :=
sorry

[Adam Topaz]

Is this something @Filippo A. E. Nuccio proved, perhaps?

[Joël Riou]

If it is not already there, preserves_finite_limits_of_exact in exact_functor.lean could help, but the critical statement would be that tensoring with a torsionfree abelian group preserves monos, which is usually obtained by reducing to finitely generated subgroups, which are free, but do we have these facts?

[Adam Topaz]

Yes we do. I'll dig up the relevant facts in a minute

[Adam Topaz]

Okay, so first, we have that tensoring preserves colimits in condensed/tensor in the AddcommGroup section.
In the file for_mathlib/AddCommGroup.lean we have AddCommGroup.is_colimit_cocone which expresses a tf-abelian group as a colimit of its f.g. subgroups, and AddCommGroup.exists_sigma_iso_of_index can be used to show that all such are coproducts of the tensor unit. Together those should give the result!

[Adam Topaz]

The "tensor unit" tunit is constructed in a bit of an ad-hoc way, but we have a general is_tensor_unit in the same file (which could use some more API)

[Filippo A. E. Nuccio]

I had started working on this, but then I got distracted by proving that the limit of tf things is tf. I can resume working on this, but @Joël Riou or @Adam Topaz please go ahead as you seem to have a clear picture of what needs to be done.

[Adam Topaz]

It may even be possible to use is_iso_of_preserves_of_is_tensor_unit directly!

[Joël Riou]

@Filippo A. E. Nuccio I will have no time to deal with this soon. Adam and you have a better understanding of what is already in LTE!

[Adam Topaz]

I'll see what I can do.

[Adam Topaz]

I proved

instance tensor_obj_map_preserves_mono [no_zero_smul_divisors ℤ A] :
  mono ((tensor_functor.obj A).map f) :=

at the bottom of for_mathlib/AddCommGroup/tensor. I haven't yet used this to show preservation of finite limits, and I have to stop for the day. If someone wants to pick it up from there, that would be great!

[Johan Commelin]

So we know it preserves monos and cokernels. Hence it preserves short exact sequences. But I guess we don't yet have a machine to go from there to preserving finite limits.

[Markus Himmel]

This is proved in #14026

[Johan Commelin]

Aah, since mathlib bumps is not what I want to think about right now, maybe we just copy-pasta it into LTE?

[Johan Commelin]

@Jakob von Raumer Is that ok with you?

[Johan Commelin]

I pushed the statement to src/for_mathlib/preserves_finite_limits.lean

[Jakob von Raumer]

Fine with me!

[Jakob von Raumer]

I had completely forgotten about that PR, it's WIP since we wanted to generalise it from abelian to preadditive categories first.

[Johan Commelin]

Any volunteers for this backport?

[Markus Himmel]

I'll do it today

[Johan Commelin]

Great! Thanks a lot

[Markus Himmel]

This is now done

[Johan Commelin]

Awesome