Zulip Chat Archive
Stream: condensed mathematics
Topic: Lbar.ext
Kevin Buzzard (Apr 03 2022 at 13:08):
Is there a place in the blueprint where I can read about the mathematics happening in this file src/Lbar/ext.lean? I can jump from blueprint to lean but I don't know how to go the other way
Johan Commelin (Apr 04 2022 at 06:09):
Johan Commelin (Apr 04 2022 at 06:10):
But I included this file in the list of "easy" sorries by mistake.
Kevin Buzzard (Apr 04 2022 at 16:21):
Has there been a misunderstanding here? I am asking about the blueprint. I can jump from the blueprint to github but I don't know how to jump back.
Patrick Massot (Apr 04 2022 at 16:35):
You cannot jump back.
Patrick Massot (Apr 04 2022 at 16:35):
If you are frustrated about getting stuck on Github pages you can try to add your voice to https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Rendered.20source, hoping that Mario or Gabriel will pity us.
Johan Commelin (Jun 20 2022 at 09:49):
At the bottom of Lbar/ext.lean are 6 easy SELFCONTAINED sorries (all Props). There is one SELFCONTAINED above that, which is a bit less trivial.
Johan Commelin (Jun 20 2022 at 15:04):
There are now 11 SELFCONTAINED sorries in this file.
Johan Commelin (Jun 20 2022 at 15:04):
Now it's time to catch a train.
Kevin Buzzard (Jun 20 2022 at 15:39):
I'll take a look at this, I've had some time to do other admin now
Riccardo Brasca (Jun 20 2022 at 15:42):
I can also have a look, but they don't seem to me totally self contained, they depend on a lot of previous definitions and I was quickly lost. Am I missing something easy?
Johan Commelin (Jun 20 2022 at 17:15):
At least the 6 at the end should be really straightforward.
Johan Commelin (Jun 20 2022 at 17:16):
The others require fooling around with functors, but I think you only need to know that the functor is additive.
Riccardo Brasca (Jun 20 2022 at 17:26):
Ah yes,
begin
rintro (rfl | j),
all_goals { simp [ι'] }
end
proved 3 of them. Let me have a look at the others
Johan Commelin (Jun 20 2022 at 19:31):
I pushed a slight restructure of some of the earlier ones.
Johan Commelin (Jul 09 2022 at 13:14):
I'm attacking these sorries atm.
Johan Commelin (Jul 09 2022 at 17:51):
I've filled in almost all of the data.
Johan Commelin (Jul 09 2022 at 17:51):
But now I hit an annoying roadbump: LCC_iso_Cond_of_top_ab is not universe polymorphic.
Johan Commelin (Jul 09 2022 at 17:52):
And my laptop is complaining when I ask it to recompile large parts of the system.
Adam Topaz (Jul 09 2022 at 18:12):
Whats the statement?
Johan Commelin (Jul 09 2022 at 18:15):
Of what?
Johan Commelin (Jul 09 2022 at 18:15):
My laptop is about as fast as a spherical cow...
Johan Commelin (Jul 09 2022 at 18:16):
I guess it is jet-lagged...
Adam Topaz (Jul 09 2022 at 18:18):
LCC_iso...: LCC seems to be missing a composition with Ab.ulift
Johan Commelin (Jul 09 2022 at 18:19):
Right, but making it universe polymorphic requires touching a bunch of basic files. Which turns my laptop into a toaster.
Adam Topaz (Jul 09 2022 at 18:19):
Well, look at
def of_top_ab : Condensed.{u} Ab.{u+1} :=
{ val := of_top_ab.presheaf A ⋙ Ab.ulift.{u+1},
Johan Commelin (Jul 09 2022 at 18:20):
Here's another piece of data that I haven't filled in yet:
def preadditive_yoneda_obj_obj_CondensedSet_to_Condensed_Ab
(M : Condensed.{u} Ab.{u+1}) (X : Profinite) :
(preadditive_yoneda.obj M).obj (op $ CondensedSet_to_Condensed_Ab.obj (Profinite_to_Condensed.obj X)) ≅
M.val.obj (op X) :=
sorry
Do we have this (additive!) isomorphism already?
Adam Topaz (Jul 09 2022 at 18:20):
so LCC is okay, but when it gets converted into a condensed abelian group, we should compose with Ab.ulift
Adam Topaz (Jul 09 2022 at 18:20):
I think that other iso is somewhere....
Adam Topaz (Jul 09 2022 at 18:21):
I used something similar in the free pfpng stuff IIRC
Johan Commelin (Jul 09 2022 at 18:21):
But you can't just update that statement, because it's defined using stuff that isn't universe polymorphic.
Adam Topaz (Jul 09 2022 at 18:27):
I'm pushing this:
def Condensed_LCC : Condensed.{u} Ab.{u+1} :=
{ val := LCC.{u} V ⋙ Ab.ulift.{u+1},
cond := begin
let e := LCC_iso_Cond_of_top_ab V,
let e' := iso_whisker_right e Ab.ulift.{u+1},
apply presheaf.is_sheaf_of_iso proetale_topology.{u} e',
exact (Condensed.of_top_ab _).2,
end }
Adam Topaz (Jul 09 2022 at 18:28):
And this
def Condensed_LCC_iso_of_top_ab :
Condensed_LCC V ≅ Condensed.of_top_ab V :=
Sheaf.iso.mk _ _ $ iso_whisker_right (LCC_iso_Cond_of_top_ab _) _
Johan Commelin (Jul 09 2022 at 18:31):
ooh, that's a nice hack!
Johan Commelin (Jul 09 2022 at 18:33):
aah, you added it to that basic file :rofl: :rofl:
Adam Topaz (Jul 09 2022 at 18:33):
is that a problem?
Johan Commelin (Jul 09 2022 at 18:33):
now I need to wait until CI gives me oleans
Adam Topaz (Jul 09 2022 at 18:33):
oh, sorry!
Johan Commelin (Jul 09 2022 at 18:34):
never mind, I'll just answer a couple of emails
Joël Riou (Jul 09 2022 at 20:35):
I have basically filled the data for the Breen-Deligne homology iso for eg and presheaves of abelian groups. It might be easier for you @Adam Topaz or @Johan Commelin to pass to condensed abelian groups in condensed/bd_lemma.lean. There is basically only one naturality sorry in breen_deligne/apply_Pow.lean. While working on this, I introduced nat_iso.map_homological_complex at the same time as @Johan Commelin! I have moved this definition to a separate file for_mathlib/nat_iso_map_homological_complex.
Johan Commelin (Jul 09 2022 at 21:23):
The joys of universes:
Ab.ulift.{u+1}.obj
((forget₂ SemiNormedGroup Ab).obj
(SemiNormedGroup.Completion.obj ((SemiNormedGroup.LocallyConstan.obj V).obj (op X.as)))) ≅
(forget₂ SemiNormedGroup Ab).obj
(SemiNormedGroup.Completion.obj
((SemiNormedGroup.LocallyConstant.obj (SemiNormedGroup.ulift.obj V)).obj (op X.as)))
Johan Commelin (Jul 10 2022 at 18:00):
The last bit of data has been filled in. All the sorries in Lbar/ext are now Proppy.
Last updated: Dec 20 2023 at 11:08 UTC