Potential Refactor

Stream: condensed mathematics

[Adam Topaz]

What do you think about changing our definition of Condensed.{u} Ab.{u+1} to Condensed.{u} (Module.{u+1} \Z).

The benefit is that mathlib has the monoidal structure for Module but not for Ab, and I don't feel like copying a bunch of code and being annoyed due to going back and forth between $\mathbb{Z}$-linear maps and add_monoid_homs.

The drawback is that it will require generalizing some universe parameters in mathlib, since the monoidal structure right now is only defined for Module.{u} R where R : Type u is a ring, and similarly for colimits of modules.

I'll at least start by trying to generalize these universe parameters (it shouldn't be too difficult, I hope...).

[Adam Topaz]

Ah, okay, the first snag is the monoidal unit would have to involve ulifts.

[Adam Topaz]

Okay, I'm starting to think that it would be less painful to just stick with Ab, and copy some code from mathlib about the fact that Module R is monoidal.

[Adam Topaz]

Adam Topaz said:

Ah, okay, the first snag is the monoidal unit would have to involve ulifts.

I'm now convinced that we should just stick with Ab. The required universe changes in mathlib would take up more work than it's worth right now IMO.

It's unfortunate that we can't just easily go back and forth between Ab.{u} and Module.{u} \Z. Is there something we can do about that?

[Johan Commelin]

I guess we would need a universe polymorphic ℤ (ahhrgg :scream_cat:)

[Johan Commelin]

My intuition says the we should indeed stick with Ab for now.

[Johan Commelin]

We will need "condensed ℤ[T⁻¹]-modules". But once again, I'm not sure if Condensed (Module (polynomial ℤ)) is the best way to implement that. Another option would be Condensed (endomorphism Ab), where endomorphism C is the category of pairs (X, f) with X : C and f : X ⟶ X.

[Filippo A. E. Nuccio]

One question that comes to my mind is that if we should not keep track that on "most" objects of interest to us (although not all test-objects), $T^{-1}$ is an isomorphism.

[Filippo A. E. Nuccio]

If we work in Condensed (endomorpmism Ab) this means that some arrows actually land in a subcategory and many lemmas (for instance Prop 6.8 saying that the "basic" condensed sets are profinite, which is crucial) use that $T$ is invertible.

[Johan Commelin]

We have normed_with_aut which kept track of that in the first half of the project

[Filippo A. E. Nuccio]

Sure, I was thinking on how to set-up this categorically.

[Johan Commelin]

But for Mbar, it is not an isomorphism. Same with ℤ[T⁻¹] itself. And those two objects will also play an important role.

[Filippo A. E. Nuccio]

Yes, I agree. Indeed, I don't suggest we work with Condensed (isomorphism Ab), I simply wonder if there is a way to keep track on the category side of the subcategory where this is invertible, in a way that is not too painful.

[Filippo A. E. Nuccio]

It could also not be necessary, of course.

[Filippo A. E. Nuccio]

I will think about it, at any rate.

[Kevin Buzzard]

Of course we could just drop universes ;-)

Amelia and Maria both wanted these in projects they've been doing (Amelia for group cohomology and Z[G]-modules, Maria for valuations into with_zero (multiplicative int)) so in my opinion this is an issue which we need to start thinking about. The issue is that int has some huge API and the moment you ulift it to pint you lose a chunk of it. Maybe automation can save us here?

But presumably independent of that we want the monoidal structure on Ab anyway. Can we get it from an equivalence to module Z or again is this something which is asking too much right now?

[Johan Commelin]

@Kevin Buzzard No, we can't drop universes. See the top post, where Adam writes

What do you think about changing our definition of Condensed.{u} Ab.{u+1} to Condensed.{u} (Module.{u+1} \Z).

That .{u+1} is causing the trouble. Because ℤ is not an object of Module.{0+1} ℤ. Only ulift ℤ is.

[Kevin Buzzard]

You always said this day would happen

[Kevin Buzzard]

I'm a bit surprised though. Surely the type of Z-modules is Type 1?

[Johan Commelin]

Which ℤ-modules?

[Johan Commelin]

You can have ℤ-modules with carriers in Type. But there's another category with carriers in Type 1, etc...

[Reid Barton]

In this "pyknotic" setup, you choose an inaccessible cardinal $\kappa$ as the "cutoff" for the size of the profinite spaces you want to allow. You want $\kappa$ to be an ordinary small cardinal relative to the values of the sheaves you consider so that you can do ordinary topos theory, so you need sheaves valued in a universe of sets that itself contains a smaller universe.
In Lean, you take $\kappa$ to be given by the cardinal Type (so that the profinite spaces you allow are those whose underlying set is a Type) and then you consider sheaves valued in Type 1. But ℤ itself is not a Type 1 and here is the problem.

[Reid Barton]

Or you take Type u for the profinite spaces and Type (u+1) for the values of the sheaves, but it doesn't help.

[Johan Commelin]

Johan Commelin said:

You can have ℤ-modules with carriers in Type. But there's another category with carriers in Type 1, etc...

Of course, if you are only interested in suitably finitely generated modules, then these categories are equivalent. But for arbitrary modules, they aren't.

[Johan Commelin]

I pushed a stub on endomorphism C to for_mathlib/endomorphisms.lean. The big sorry is

instance [abelian C] : abelian (endomorphism C)

[Johan Commelin]

Hmmm, one annoying thing about endomorphism is that we have to develop lots of stuff for it again. That it's abelian is only the beginning. We would need the monoidal structure, Hom-tensor adjunction, free objects, etc... And all of that also for the condensed version.

[Johan Commelin]

@Adam Topaz Do I understand correctly that this is almost all done for Condensed (Module R) already?

• It is abelian
• The free-forget adjunction is done (right?)
• monoidal structure is there in the uncondensed case, but needs to be sheafified.
• Hom-tensor adjunction is done in the uncondensed case, I think.

[Johan Commelin]

So maybe I should reconsider my intuition about Ab and endomorphism Ab.

[Johan Commelin]

Writing a constructor for Condensed (Module (polynomial ℤ)) given a Condensed (Module ℤ) + endomorphism shouldn't be hard.

[Johan Commelin]

Same for a Condensed Ab + endomorphism

[Adam Topaz]

The answers are yes, yes, yes, and almost docs#tensor_product.lift.equiv

[Johan Commelin]

Hmmz, mathlib doesn't yet know that Module R has colimits.

[Johan Commelin]

Or wait, maybe I just have the wrong imports

[Adam Topaz]

It does, but there are universe issues there as well

[Adam Topaz]

Those should be easier to fix

[Adam Topaz]

If we decide to go for this change, we should fix mathlib first, I think.

[Adam Topaz]

I hope the free forget adjunction for modules is sufficiently universe polymorphic.

[Johan Commelin]

Yeah, I'm now thinking that it will make sense to attempt this refactor.

[Johan Commelin]

It is the morally correct thing to do. And probably also the economically correct thing to do.

[Adam Topaz]

I think I agree... I didn't consider the Z[X] issue yesterday, and that pushes it over the edge.

[Adam Topaz]

PS... I added for_mathlib/internal_hom.lean yesterday. I was surprised we didn't have something like that in mathlib yet.

[Johan Commelin]

#11802 generalizes universes for colimits in Module R -- let's see if CI likes it.

[Reid Barton]

This might be dumb and/or already considered, but have you thought about instead of polynomial ℤ, using mv_polynomial punit ℤ?

[Adam Topaz]

We could also use mv_polynomial pempty Z

[Johan Commelin]

Hah, that would be a nifty hack!

[Adam Topaz]

https://github.com/leanprover-community/mathlib/blob/7f3590b4184c03b0ddccc7b5ff7d0a8c88d9f2ac/src/algebra/category/Module/adjunctions.lean#L47

:sad:

[Adam Topaz]

The universes there need to be fixed as well.

[Adam Topaz]

Adam Topaz said:

The universes there need to be fixed as well.

It looks like this file depends on the monoidal structure, so we should fix algebra/Module/monoidal first

[Adam Topaz]

I pushed some WIP for the universe generalization of the monoidal structure in branch#universe_monoidal_module
Please feel free to push to this branch!

[Adam Topaz]

(I have to teach soon, so I can't work on this more right now.)

[Adam Topaz]

(oops! I wrote punit instead of pempty, let me fix)

[Reid Barton]

FWIW I think mv_polynomial punit is, to some extent, not even really a hack if you think about this $T^{-1}$ as a specific thing which is nominally different from other generators of polynomial rings. You could define

inductive cond_gen
| Tinv

And then at that point you could put cond_gen in universe u+1 on the general principle that we only care about one universe at a time.

[Reid Barton]

Adam Topaz said:

I pushed some WIP for the universe generalization of the monoidal structure in branch#universe_monoidal_module
Please feel free to push to this branch!

What's the statement you're going for? An adjunction between Type (max u v) and Module.{max (u v)} R?

[Johan Commelin]

True. But mv_polynomial pempty ℤ is very much a hack to place ℤ in Type u.

[Adam Topaz]

Reid Barton said:

Adam Topaz said:

I pushed some WIP for the universe generalization of the monoidal structure in branch#universe_monoidal_module
Please feel free to push to this branch!

What's the statement you're going for? An adjunction between Type (max u v) and Module.{max (u v)} R?

In that branch, just the monoidal structure on Module.{max v u} R where R : Type u is a comm_ring R..

[Adam Topaz]

Once that's done, we can fix the universes similarly in algebra/category/Module/adjunctions.

[Adam Topaz]

The current monoidal structure on Module R only works for Module.{u} R with R : Type u because the tensor unit is defined to be Module.of R R.

[Adam Topaz]

Feel free to replace tensor_unit with Module.of R (ulift R), if you think that would be better!

[Johan Commelin]

Johan Commelin said:

#11802 generalizes universes for colimits in Module R -- let's see if CI likes it.

The build passed. Linter raised a universe issue, which I fixed. So this should be good now.

[Adam Topaz]

Adam Topaz said:

Feel free to replace tensor_unit with Module.of R (ulift R), if you think that would be better!

You would have to register a module instance for ulift R in this case.

[Adam Topaz]

Alright, I really do have to go teach now (class starts in 3 mins)

[Yaël Dillies]

And they say they aren't addicted

[Adam Topaz]

I can't seem to find the universal property of mv_polynomial (as the free commutative algebra on a type). Am I just blind?

[Adam Topaz]

I suppose we are meant to use docs#mv_polynomial.aeval and docs#mv_polynomial.aeval_unique ?

[Johan Commelin]

Yes, I think so

[Adam Topaz]

#11807

[Adam Topaz]

The only drawback I see is that now things have become noncomputable, due to the use of mv_polynomial

[Reid Barton]

So I would also expect that these definitions would become hard to use because one of the universe parameters (I guess v) only appears in Module.{max v u} R in the arguments

[Adam Topaz]

I hope that in practice we either have u = v or u = 0, so maybe it will be okay? But yeah, if we want something for the most general universe parameters it may require manually adding universes.

[Reid Barton]

does LTE use these? does it build against your PR?

[Adam Topaz]

I haven't tried.

[Adam Topaz]

But we don't really use Module at all yet, so I think it's fine (for LTE at least)

[Reid Barton]

I think there is some linter which tries to guess whether this will be an issue, so we can see what it says.

[Adam Topaz]

Yeah, that's the same linter that caught Johan's PR at first

[Reid Barton]

If there are no users yet, then a priori it's hard to know whether you're actually making things better than if you just had to use Module (ulift R) (and maybe you are making things worse in the happy case of rings and modules in the same universe).

[Reid Barton]

My gut feeling is that working with things like Module.{v u} R is not worth it in the long run

[Adam Topaz]

The ideal situation would be if it were possible to write R : Type u [comm_ring R], u \leq v and Module.{v} R.

[Reid Barton]

I mean once the tensor unit is not R anyways, seems like you might as well work with modules over it instead

[Reid Barton]

Yeah, it would be nice if we could have a coherent story about how we'd like universes to work.

[Reid Barton]

Though in this case, the tensor unit would still not be R if u < v (it would fix some other things though).

[Adam Topaz]

I guess cumulative universes would fix that.

[Adam Topaz]

Does ulift \Z have a ring instance registered in mathlib?

[Adam Topaz]

Ah, it does in algebra.ring.ulift. Maybe we should go with that approach? @Johan Commelin what do you think?

[Adam Topaz]

PS. #11807 already broke -- it looks like the monoidal structure of Module.{u} R with R : Type u was not found.

[Adam Topaz]

Well... the colimits thing is also not ideal. With the new change:

import algebra.category.Module.colimits

open category_theory.limits
universes u v

example : has_colimits (Module.{37} ℤ) := infer_instance
example : has_colimits (Module.{u} ℤ) := infer_instance
example (R : Type v) [comm_ring R] : has_colimits (Module.{max u v} R) := infer_instance
example (R : Type v) [comm_ring R] : has_colimits (Module.{max v u} R) := infer_instance -- fails
example (R : Type v) [comm_ring R] : has_colimits (Module.{v} R) := infer_instance -- fails

[Reid Barton]

What about

example (R : Type v) [comm_ring R] : has_colimits (Module.{u} R) := infer_instance

[Adam Topaz]

That would require changing the construction altogether.

[Reid Barton]

aha!

[Adam Topaz]

The current construction is an inductive-quotient construction

[Reid Barton]

But it is actu... gotcha.

[Reid Barton]

It is actually true though right?

[Adam Topaz]

I think so, yes.

[Adam Topaz]

Well, with the correctly sized index category.

[Reid Barton]

I think a marginally better-known example of this phenomenon is the "topos" of G-sets for G a large group

[Reid Barton]

Any small collection of such sets could be viewed as having an action by some small quotient of G

[Reid Barton]

But the whole category is not generated by a set of objects (if G has a proper class of set-sized quotients). Quite similar to condensed sets really.

[Reid Barton]

So I think Module.{v u} R is cocomplete, but (generally) not locally presentable

[Reid Barton]

Anyways, assuming you don't want to do the other construction...

[Reid Barton]

Since has_colimits is a Prop, it might be okay to have both the old and new instances?

[Reid Barton]

But in general, this kind of thing is why I think Module.{v u} is a bad idea--more precisely, it would be better to invest the time into making it easier to deal with ulift

[Adam Topaz]

Reid Barton said:

Since has_colimits is a Prop, it might be okay to have both the old and new instances?

I think we can just add these instances manually.

[Adam Topaz]

This works

import algebra.category.Module.colimits

open category_theory.limits
universes u v

instance foo1 (R : Type v) [comm_ring R] : has_colimits (Module.{max v u} R) :=
Module.colimits.has_colimits_Module.{v u}

instance foo2 (R : Type v) [comm_ring R] : has_colimits (Module.{v} R) :=
Module.colimits.has_colimits_Module.{v v}

example : has_colimits (Module.{37} ℤ) := infer_instance
example : has_colimits (Module.{u} ℤ) := infer_instance
example (R : Type v) [comm_ring R] : has_colimits (Module.{max u v} R) := infer_instance
example (R : Type v) [comm_ring R] : has_colimits (Module.{max v u} R) := infer_instance
example (R : Type v) [comm_ring R] : has_colimits (Module.{v} R) := infer_instance

[Adam Topaz]

#11812

[Adam Topaz]

I hope this will pass the strict background check by the typeclass police.

[Johan Commelin]

@Adam Topaz Which PRs should I be reviewing now?

[Adam Topaz]

#11807 is broken -- ignore it (I tagged as maybe later)

#11812 should be good to go

[Adam Topaz]

I think Reid convinced me to go with Module (ulift \Z). What do you think?

[Johan Commelin]

#11812

[Johan Commelin]

Adam Topaz said:

I think Reid convinced me to go with Module (ulift \Z). What do you think?

So that u = v everywhere in sight? I guess that makes sense. I don't have a preference between ulift ℤ and mv_polynomial pempty ℤ. Since we need to go back and forth between modules over ℤ and ℤ[T⁻¹], maybe the mv_polynomial version is a bit smoother than ulift?

[Adam Topaz]

I think over the next few days, I'll try to just change the stuff we have for Condensed Ab to Condensed (Module A)

[Adam Topaz]

We can decide on the ulift vs polynomial issue later.

[Johan Commelin]

Yeah, that makes sense

[Adam Topaz]

If we go with ulift Z, we could just use polynomial (ulift Z) and call it good

[Johan Commelin]

But in that refactor, you can assume A to be in the correct universe, which is a relief.

[Adam Topaz]

Fortunately, the stuff I did for the ExtrSheaf equivalence uses arbitrary categories which have finite biproducts, so that should be effortless to generalize.

[Johan Commelin]

Big shoutout to abstraction and generalization!

[Adam Topaz]

oops! #11837

Also the following is done (for any R : Type (u+1) with [ring R], where CondensedMod R := Condensed.{u} (Module.{u+1} R))

instance CondensedMod_has_enough_projective : enough_projectives (CondensedMod R) :=

[Adam Topaz]

I also introduced the notation $R[S]$ for a ring $R$ and S : Profinite, see e.g. https://github.com/leanprover-community/lean-liquid/blob/3725961d6024d9bb5f7ee81e62197574b7d8ab47/src/condensed/projective_resolution_module.lean#L134

[Johan Commelin]

Just for the record: with the new roadmap it's clear that we can continue using Condensed Ab. There's no more need to work with modules over ulifted rings, etc...