Zulip Chat Archive
Stream: condensed mathematics
Topic: SES of thm 6.9
Filippo A. E. Nuccio (Jan 20 2022 at 07:51):
I am getting closer to finishing the proof of Theorem 6.9 for finite S. Is there already a place where it is used in some form (I guess, either inserted in some homological machinery to extract a LES or in some limit machinery to deduce the SES for profinite S)? I would like to make sure that my final statement will match the required formulation.
Johan Commelin (Jan 20 2022 at 08:03):
No, I don't think it's used yet. So we can adapt the application to what ever final form you come up with (-;
Filippo A. E. Nuccio (Jan 20 2022 at 08:05):
Ok, good to know. I guess at any rate it will be needed in a correct categorial form; do we know that CompHausFilteredblah (the category containing both real and Laurent measures) is abelian?
Johan Commelin (Jan 20 2022 at 08:05):
No, it's not abelian, if I recall correctly.
Johan Commelin (Jan 20 2022 at 08:06):
And for silly reasons: if you take the identity map M → M but you rescale the filtration on one of the two Ms, then the id might still be a hom, but clearly not an iso.
Johan Commelin (Jan 20 2022 at 08:06):
You can only scale in the correct direction of course. Because the filtration has to be preserved.
Filippo A. E. Nuccio (Jan 20 2022 at 08:07):
Sure, the usual problem somewhat.
Johan Commelin (Jan 20 2022 at 08:07):
So really, we'll have to push the sequence to Cond(Ab) and start reasoning there.
Filippo A. E. Nuccio (Jan 20 2022 at 08:08):
OK; so we need to take the limit to get to profinite S. But can we say at least it is a sequence (is the category exact)?
Filippo A. E. Nuccio (Jan 20 2022 at 08:10):
Perhaps the best would be if I look more carefully at what the state of the art of the other files is, to see how much category language I can use to express its exactness...
Adam Topaz (Jan 20 2022 at 15:05):
The category CompHausFilt_1 may actually be abelian (or close to it).... I'm not sure.
Well.... it's probably not abelian (I think colimits would pose an issue), but certainly limits are well behaved in there.
Maybe it's abelian... I should stop guessing until after I have some coffee.
Filippo A. E. Nuccio (Jan 20 2022 at 15:33):
Well, to be honest my question about it being abelian was too much. For the time being I care about being able to write exact sequences (does having zero objects suffice?) and taking limits to pass to profinite sets.
Filippo A. E. Nuccio (Jan 20 2022 at 15:34):
I am very close to a "brutal" version of exactness (I can check that the RHS is surjective and the LHS is injective and that if something goes to 0 under the right map it is in the image of the first) and I am wondering how to translate it in fancy terms that we can give to a colimit functor to produce the nice SES in Cond Ab.
Filippo A. E. Nuccio (Jan 20 2022 at 15:35):
If you have a file you want to point me at, so that I can check for myself, that's also fine.
Adam Topaz (Jan 20 2022 at 15:38):
To take a limit, you would need to work in CompHausFilt_1. The category without the 1 does not have limits (for essentially the reason that Johan mentioned above).
Filippo A. E. Nuccio (Jan 20 2022 at 15:41):
OK, so I need to show that my two morphisms are CompHausFilt_1-morphisms. But has CompHausFilt_1 kernels, zero and cokernels so that I can state my ES is a SES (and do mono/epi coincide with set-theoretic injections/surjections)?
Filippo A. E. Nuccio (Jan 20 2022 at 15:41):
Also, is this what you need to move forward?
Johan Commelin (Jan 20 2022 at 15:44):
Yes, that sounds good to me. But certainly, having the "brutal" version is going to be needed no matter what.
Johan Commelin (Jan 20 2022 at 15:45):
Once that's in, we sit down and figure out how to get the version in Cond(Ab) and for profinite S.
Johan Commelin (Jan 20 2022 at 15:45):
But this should really just be a matter of "glue"
Filippo A. E. Nuccio (Jan 20 2022 at 15:48):
OK, good. I will then come back here to sit down together once the brutal version is completed in order to decide what to do. :living_room:
Last updated: Dec 20 2023 at 11:08 UTC