tensor products commute with direct limits

Stream: Is there code for X?

[Matej Penciak]

This may be another product of me being bad at searching for things, but does mathlib know that ⊗ M commutes with direct limits?

Also a small update, but I was able to finish the construction of the equivalence of a module with the direct limit of its finitely generated submodules! (hence why I'm looking for the above lemma haha)

[Johan Commelin]

@Matej Penciak The answer is "yes and no". Mathlib knows that the in the category Module R, the functor ⊗ M is a left adjoint, and hence preserves all colimits. With a bit of luck, there is also a lemma that says that the hands-on direct limit (which I'm assuming you have used) is an example of a colimit in the sense of the category theory library. Combining these facts should give your desired statement.
But this means that you will probably need a bit of glue to repackage your statements in the language of category_theory.

[Notification Bot]

2 messages were moved here from #new members > namespaces, and more by Johan Commelin.

[Johan Commelin]

@Matej Penciak I have moved your message to a new thread in a different stream. I think this location is more appropriate.

[Matej Penciak]

Johan Commelin said:

Matej Penciak I have moved your message to a new thread in a different stream. I think this location is more appropriate.

Gotcha! Thanks

[Matej Penciak]

Johan Commelin said:

Matej Penciak The answer is "yes and no". Mathlib knows that the in the category Module R, the functor ⊗ M is a left adjoint, and hence preserves all colimits. With a bit of luck, there is also a lemma that says that the hands-on direct limit (which I'm assuming you have used) is an example of a colimit in the sense of the category theory library. Combining these facts should give your desired statement.
But this means that you will probably need a bit of glue to repackage your statements in the language of category_theory.

I think I'll want to use the Module R language for different parts of the proof anyway, so I think I'll try to clean up what I have and try to provide some of that glue next. Thanks for your help!

[Scott Morrison]

There's a monoidal_closed instance for Module R, and this shows tensoring with an object preserves all colimits.

[Scott Morrison]

I've been using this just yesterday.

[Scott Morrison]

Let me know if you need help identifying all the moving parts!

[Junyan Xu]

Caution: in Module R any two modules lie in the same universe, so if you want to prove the fully universe polymorphic version of the result, you'll face universe issue when applying results in Module R.

[Johan Commelin]

That's a fair point. On the other hand, I don't think it makes sense to duplicate major parts of the category_theory library just to remain maximally universe polymorphic.

[Adam Topaz]

There aren't many colimits where the modules are in different universes anyway...

[Junyan Xu]

docs#module.direct_limit requires all modules lie in the same universe but possibly different from the ring's universe (of course, you can't define a function in Lean with values lie in different universes); it's docs#tensor_product that allows the two module (and the ring) to be in different universes. We don't seem to have a is_direct_limit predicate, so it seems the easiest way state the result in the OP is to use is_colimit/preserves_colimit (otherwise you need to say an isomorphism to the direct limit commuting with natural maps).

It's interesting to observe that docs#module.direct_limit doesn't include any commutativity conditions and there's docs#directed_system imposing the conditions, which isn't needed by many declarations in that file, but is used in flatstuff and certainly is needed for docs#Module.direct_limit_is_colimit.

[Junyan Xu]

Johan Commelin said:

That's a fair point. On the other hand, I don't think it makes sense to duplicate major parts of the category_theory library just to remain maximally universe polymorphic.

I think it's not duplication but refactoring that's required to achieve full universe polymorphism in this case. If M : Type u then M ⊗ is a functor from Module.{v} R to Module.{max u v} R which mathlib doesn't have, of which docs#category_theory.monoidal_category.tensor_left is a special case (u=v). We can show Hom is the right adjoint to this functor, which would specialize to the monoidal category case. Anyway, it's not a small effort and may be not worth it.

[Junyan Xu]

However, currently flatness is already defined allowing R and M be in different universes, so tensor product between modules in different universe (M with ideals of R) is present in the very definition! So you have to deal with it if you want to keep the generality.

[Johan Commelin]

But the Hom functor will have different universes, right? In the universe polymorphic setup, they aren't adjoint functors, I think.

[Johan Commelin]

I think it's easier to have a ulift functor, and show that it preserves limits and colimits.

[Johan Commelin]

But I think it's also perfectly fine to put everything in the same universe for now.

[Junyan Xu]

But the Hom functor will have different universes, right? In the universe polymorphic setup, they aren't adjoint functors, I think.

Hmm you're right, Hom(N,P) for N : Type v and P : Type (max u v) would lie in Type (max u v) instead of Type u, so the right adjoint may not exist.

[Kevin Buzzard]

There are criteria for flatness which involve testing against tensoring with ideals, and you could imagine that these criteria become false if the module is in a larger universe than the ring because there are "not enough ideals" somehow. I can't imagine applications where the ring and module aren't in the same universe (especially now ulift works)

[Junyan Xu]

Actually I'm not sure whether the tensoring functor preserves colimits if the universe v of the indexing type ι of docs#module.direct_limit is smaller than the universes w of the module. In general, does the lifting functor from Module.{u} to Module.{max u v} preserves "large" (i.e. the indexing category J is in higher universe than u) (co)limits? I guess the answer is yes, because if the (co)limit is too large to fit in Module.{u} then the (co)limit would simply not exist in Module.{u}, because you can construct cones with larger and larger cone point? Or you may consider the category Type, for which this becomes a set-theoretic question. I'd be interested to see a counterexample in either case.

[Junyan Xu]

Anyway, preserves_limits is defined to be docs#category_theory.limits.preserves_limits_of_size with J (both objects and morphisms) in the universe of the hom type of the domain of the functor, though, and it should suffice for the current application, since the type of f.g. submodules of a module lies in the same universe as the module.

[Johan Commelin]

The explicit construction of (co)limits in Type u doesn't really seem to care about universes, right?

[Junyan Xu]

I didn't check but I think that predates #10243

[Johan Commelin]

Yes, but the construction is compatible with ulift, right? Or was that not your question?

[Junyan Xu]

before #10243 you can't talk about limits with J is in not same universe as the morphisms, or functors between categories in different universes preserving limits. And certain (co)limits certainly shouldn't exist in the same universe, e.g. the disjoint union of #(Type u) many unit in Type u. The general construction would work but the result would like Type (u+1).

[Johan Commelin]

Right, so certain (co)limits don't exist for universe reasons. But apart from those obstructions, all (co)limits exists, and are compatible with making the universe of the ambient category larger by composing with ulift.

[Junyan Xu]

But I can't seem to rule out that the limit may exist in Type u but isn't isomorphic to the limit in Type (u+1), like a limit in RingedSpace isn't necessarily the same as that in LocallyRingedSpace...

[Junyan Xu]

Hmm, since Type has generator unit and cogenerator bool in any universe, I think I have proofs that indeed ulift_functor preserves arbitrary large limits and colimits. The comparison morphism from the limit in the lower universe to the limit in the higher universe would also be useful (and dually for colimits). Module also has a generator so limits would be preserved, but what about cogenerator? Maybe we can somehow utilize the concrete category structure on Module ...

[Adam Topaz]

For filtered colimits, you should be able to reduce to Type*.

[Mario Carneiro]

Junyan Xu said:

But I can't seem to rule out that the limit may exist in Type u but isn't isomorphic to the limit in Type (u+1), like a limit in RingedSpace isn't necessarily the same as that in LocallyRingedSpace...

I don't know any of the category theory context so someone should catch me up, but this sounds wrong. It should be possible to prove that limits and colimits taken in Type (u+1) are isomorphic to the analogous limit in Type u if it exists

[Junyan Xu]

Yes I just came up with proofs, but I don't think these are obvious from these categorical definitions docs#category_theory.limits.is_limit and docs#category_theory.limits.preserves_limits_of_size ...

[Adam Topaz]

You can see from the "explicit" definitions of limits and colimits in Type* that the ulift functor preserves (maybe even creates?) limits and colimit.

[Junyan Xu]

The explicit definition may give you something in a higher universe; when it's in the same universe then it's the categorical limit, and ulift would preserve the limit. What I was concerned with is when the construction gives a result in a higher universe, and at the same time there accidentally exists a limit in the original universe.

Will be back in 1.5 hours and try to formalize the proofs.

[Mario Carneiro]

If there is "accidentally" a limit in the original universe, then you can ulift it into the higher universe and it will still be a limit; you can then compare it with the categorical limit to derive isomorphism

[Junyan Xu]

For the constructed limits (and constructed tensor products etc.) we usually immediately prove that it satisfies the universal property in any universe, but for the accidental limit, we only know its universal property in its universe. Indeed there's a comparison morphism after lifting but it requires proof to show it's an isomorphism. The comparison morphism being isomorphism is equivalent to ulift_functor preserving limit, which means exactly that "ulift it into the higher universe and it will still be a limit", and which I am trying to prove.

[Junyan Xu]

There are lots of full subcategory inclusions (~ fully faithful functors) that don't preserve (co)limits, so I'd argue that Type u ⥤ Type (u+1) is the exception rather than the rule.

We do know docs#category_theory.limits.fully_faithful_reflects_limits and the same for colimits, so (co)limits in the larger category that lie in the smaller category are automatically (co)limits in the smaller category.

[Mario Carneiro]

There are lots of full subcategory inclusions (~ fully faithful functors) that don't preserve (co)limits, so I'd argue that Type u ⥤ Type (u+1) is the exception rather than the rule.

This should be true for Type and for any category where the objects have an "internal" definition, including Module and most other categories I can think of. Do you have an example where things go wrong?

[Mario Carneiro]

The reason ulift_functor preserves limits is not because of abstract nonsense but by unpacking the definition of the morphisms and how they interact with ulift specifically. I would expect that the abstract nonsense does not give you enough to prove the theorem, because as you say there are other kinds of fully faithful functors that don't preserve limits

[Junyan Xu]

I didn't quite propose to use abstract nonsense to prove it; unit being a generator means that Hom(unit, -) is faithful, which means that two functions are distinguished by their values on points; bool being a cogenerator means that Hom(-, bool) is faithful, which means that two functions are distinguished by considering preimages of subsets of the codomain. The key in this argument is that unit and bool already lie in the lowest universe.

I don't know what "internal" means, but here is an example showing the inclusion from abelian groups to groups where things go wrong (doesn't preserve colimits).

[Junyan Xu]

Here is a proof that ulift_functor preserves limits. I realized the colimit case is trickier than I thought; not every g : (Y -> bool) -> (X -> bool) comes from some f : X -> Y (Hom(-,bool) is faithful but not full, unlike Hom(unit,-) which is even an equivalence of categories), and I'm yet to write down a condition g should satisfy in order to recover f ...

import category_theory.limits.preserves.basic
open category_theory category_theory.limits opposite
universes u v w w'
variables {J : Type w} [category.{w'} J] {F : J ⥤ Type u} (c : cone F)

def cone_of_element {c : cone (F ⋙ ulift_functor.{v u})} (x : c.X) : cone F :=
{ X := punit, π :=
  { app := λ j _, (c.π.app j x).down,
    naturality' := λ i j f, by { ext, simp [← c.w f] } } }

lemma preserves_limits : preserves_limits_of_size.{w' w} ulift_functor.{v u} :=
{ preserves_limits_of_shape := λ J _, by exactI { preserves_limit := λ D, { preserves := λ c h,
  { lift := λ lc, λ x, ⟨h.lift (cone_of_element x) punit.star⟩,
    fac' := λ lc j, by { ext, apply congr_fun (h.fac _ j) },
    uniq' := λ lc f hf, by { ext, apply congr_fun (h.uniq _ (λ _, (f x).down) _),
      intro j, ext ⟨⟩, have := congr_fun (hf j) x, exact congr_arg ulift.down this } } } } }

[Junyan Xu]

Hmm, the condition should be that of boolean algebra hom, I guess.

[Yaël Dillies]

Boolean algebra homs? This is just docs#bounded_lattice_hom

[Junyan Xu]

I now have a complete proof that ulift_functor preserves all colimits as well. I believe it contains all ingredients to construct the contravariant equivalence between Type and the category of complete atomic Boolean algebras, but I use a direct approach that need not mention these concepts.

The same argument should work for limits in Group and AddCommGroup (because the generator Z already lies in the lowest universe), but for Module it would only apply if the lower universe contains the ring R, which also serves as a generator in the higher universe. In these arguments I do not assume the (co)limit exists in the higher universe so I do not have access to the comparison morphism. If you take advantage of that maybe you can prove more.

For colimits it's a different story: ulifting groups doesn't actually preserve colimits! One can embed any infinite group G canonically into a simple group of cardinality $2^{|G|}$, and we may transfinitely iterate this construction to obtain a direct system of groups indexed by ordinals in the universe, whose colimit G+ is again a simple group, whose cardinality is too large to lie in the universe, but does live in the next higher universe. In the lower universe, the colimit exists and is the trivial group, because for any cocone over the direct system, there exists a homomorphism from G+ to the cone point, which can't be an isomorphism onto the image due to cardinality reason, so must be trivial as G+ is simple. Therefore, ulifting to the next higher universe doesn't preserve colimits in Group. @Mario Carneiro

It's also interesting to learn that certain free objects (small coproducts of free objects on one generator) don't exist in the same universe but only in the next higher one, like the free complete lattice on three generators, or the free complete Boolean algebra on countably many generators, but these don't provide examples because the colimits don't exist in the lower universe.

There seems to exist other ways things can "go wrong": there are algebraic statements independent of ZFC, like the Whitehead problem. It looks plausible to me that there exists a model of Lean's type theory where Type 0 "is" the constructible universe, so all Whitehead groups there are free, while Type 1 "satisfies" Martin's axiom, and non-free Whitehead groups exists there. However, I haven't been able to connect such statements to limits.

[Kevin Buzzard]

Fascinating! Well done!

[Bhavik Mehta]

Asking for a nontrivial exact endofunctor on Set is a pretty reasonable statement, and it's equivalent to the existence of a measurable cardinal, which certainly isn't implied by ZFC: https://ncatlab.org/nlab/show/measurable+cardinal#in_category_theory, maybe this is the sort of connection to limits you might be looking for?

[Mario Carneiro]

@Junyan Xu That construction requires you to take a colimit over a large index set though. Hopefully the theorem should at least be true for small colimits of groups

[Mario Carneiro]

Junyan Xu said:

There seems to exist other ways things can "go wrong": there are algebraic statements independent of ZFC, like the Whitehead problem. It looks plausible to me that there exists a model of Lean's type theory where Type 0 "is" the constructible universe, so all Whitehead groups there are free, while Type 1 "satisfies" Martin's axiom, and non-free Whitehead groups exists there. However, I haven't been able to connect such statements to limits.

I don't believe it is possible for Martin's axiom or CH to be true in a higher universe and false in a lower one, because it is a statement about sets of bounded cardinality. Any "internal" property (i.e. not something like projectiveness that talks about the other types in the given universe) about small sets in a large universe can be reflected back down to the small universe.

[Mario Carneiro]

In your example, if Type 0 is the constructible universe, then all Whitehead groups of cardinality $\aleph_1$ are free, but then any Whitehead group in Type 1 is provably "small" because aleph 1 is a small cardinal, and hence is isomorphic to a group in Type 0; and group isomorphism preserves the Whitehead property, so all Whitehead groups of cardinality $\aleph_1$ in any universe are free.

[Mario Carneiro]

Another example of this kind of reasoning is that Con(ZFC + 6 inaccessibles) is a property of nat in Type 0 but it is provable in lean because we can construct a model of ZFC + 6 inaccessibles in Type 7

[Yaël Dillies]

@Junyan Xu @Junyan Xu definitely have a look at #11677

[Yi Hu]

Hello. I am new. I'd like to get an idea about the feasibility of formalizing a 159-page paper and approximate timescales. Thanks!

[Heather Macbeth]

Hi @Yi Hu, welcome! It depends very much on the paper, can you say more about it? But frankly, formalization is a long way from the research frontier in most fields of math, and you would have to build in the time to get to that research frontier as well as the time for formalizing the paper itself.

[Yi Hu]

The paper is here https://arxiv.org/abs/2203.03842
The main components are about a family of polynomials and their proper transforms after (hugely numerous) simple blowups.

[Heather Macbeth]

We're a long way from this, unfortunately. Although we do aspire to get there (in 5 years? 10?), and it would be great to have you join the effort :-).

Just looking at the first sentence, I'm not even sure that mathlib has the definition of a rational map between schemes.

[Heather Macbeth]

If you could extract a (very complicated) result purely about commutative algebra or polynomials which you wanted checked, that might be more within reach.

[Notification Bot]

5 messages were moved from this topic to #new members > Introductions: Yi Hu by Johan Commelin.