universe levels in preserves statements

Stream: maths

[Jakob von Raumer]

@Markus Himmel and me have found many ove the universe level restrictions in category_theory.limits.preserves to be too strong in that they require both categories to live in the same universe. I started to work on a generalization at preserves-universes but for many of the more specific type classes, e.g. preserves_binary_products, the fix needs to pin the universe level of the diagram category. In general it seems more consistent with other parts of mathlib to have things like the walking_pairin Type instead of being universe polymorphic. Edge cases like preserves_finite_limits are harder to decide on. Any comments on these changes, esp @Scott Morrison ? I seem to have fixed most files, but there's still some work to do...

[Johan Commelin]

@Jakob von Raumer I guess you know the back story, that the indexing diagram used to be a small category at the same universe level as that of the morphisms of category in which you take limits. This was decoupled a while ago. So I agree that it's now a good idea for walking_pair and friends to simply live in Type.
For things like preserves_finite_limits, I think we should at least support a universe polymorphic version. It could be called preserves_finite_limits_of_size for example.

[Adam Topaz]

I'm concerned that these more relaxed universe parameters will mean the
preserves instances will almost never fire automatically. We are already running into some issues in LTE where we have to provide universes explicitly to has_limit (or similar) instances. Is that better than dealing with ulift once in a while? I don't know...

[Jakob von Raumer]

Johan Commelin said:

For things like preserves_finite_limits, I think we should at least support a universe polymorphic version. It could be called preserves_finite_limits_of_size for example.

Yes, that's what it's like on the branch now. There's a sparate lemma preserves_smallest_finite_limits_of_preserves_limitsreflecting it down to Type which we can locally make an instance.

[Jakob von Raumer]

Adam Topaz said:

I'm concerned that these more relaxed universe parameters will mean the
preserves instances will almost never fire automatically. We are already running into some issues in LTE where we have to provide universes explicitly to has_limit (or similar) instances. Is that better than dealing with ulift once in a while? I don't know...

Since I'm almost through refactoring mathlib, I can say that it does require a few explicit universes but then it removes some others (partially because now the index categories have fixed universes).

[Jakob von Raumer]

Going from an index level > 0 to 0 in order to have e.g. binary products is not completely painless, but in most places we will have has_finite_limits which maybe should default to 0 (as opposed to a has_finite_limits_of_size)

[Jakob von Raumer]

@Andrew Yang One point I'm stuck at is Lan_preserves_finite_limits_of_flat in category_theory.functor.flat, can you help me? I'm on branch preserves-universes

[Andrew Yang]

I think there should not be a need for has_finite_limits_of_size. Since we have fin_category.equiv_as_type and has_limits_of_shape_of_equivalence, has_finite_limits should suffice.

I believe Lan_preserves_finite_limits_of_flat should work if the two are merged and we have the instances

instance has_limits_of_shape_of_has_finite_limits [has_finite_limits C] {J : Type*}
  [small_category J] [fin_category J] :
  has_limits_of_shape J C := sorry

instance preserves_limits_of_shape_of_preserves_finite_limits (F : C ⥤ D)
  [preserves_finite_limits F] {J : Type*}
  [small_category J] [fin_category J] :
  preserves_limits_of_shape J F := sorry

[Jakob von Raumer]

Thanks! I'll have a look at it tomorrow :)

[Jakob von Raumer]

Andrew Yang said:

I think there should not be a need for has_finite_limits_of_size. Since we have fin_category.equiv_as_type and has_limits_of_shape_of_equivalence, has_finite_limits should suffice.

It's a tough decision. I think I'll keep it for now, and we can consider removing it in a second refactor step.

[Jakob von Raumer]

Maybe I can get some help from the community with this: On the preserves-universes I'm currently trying to relax all sorts of universe constraints, which in turn suggests changing constant index categories like walking_parallel_pair and the like to not be universe polymorphic but instead live in Type. This causes a problem with over B categories, though: In those we only derive connected limits in the universe v of the morphisms instead of in universe 0. One should think that this is not a problem, but the issue is that connectedness is not preserved by ulift (since the space of discrete categories we use to test the functor's being constant grows), so we can't derive that over B has e.g. pullbacks because we miss the instance is_connected (ulift_hom (ulift walking_cospan)), and it's not really easy to derive this instance in a general way. Any ideas on how to solve this? @Scott Morrison ?

[Jakob von Raumer]

(this is the file)

[Reid Barton]

The definition of is_connected should really just be that if you quotient the objects by nonempty (A --> B), you get a singleton. I'm not sure why we have this complicated definition instead.

[Reid Barton]

Certainly connectedness really is preserved by any kind of universe lifting.

[Jakob von Raumer]

With the current complicated definition, is it really?

[Reid Barton]

Yes, because it is equivalent to the simple definition

[Reid Barton]

If it isn't, then it's wrong!

[Adam Topaz]

All these ulift constructiions should provide some equivalence of caategories, and connectedness is preserves under equivalences (the complicateed definition makes it not so bad to prove that!)

[Adam Topaz]

see docs#category_theory.is_connected_of_equivalent

[Adam Topaz]

And I think we have docs#category_theory.is_connected_of_zigzag

[Reid Barton]

Adam Topaz said:

see docs#category_theory.is_connected_of_equivalent

This one only covers categories with objects in the same universe

[Adam Topaz]

That seems wrong...

[Reid Barton]

It's the easy case for this definition because you are eliminating into the same discrete categories

[Reid Barton]

If you have different object universes then you run into what Jakob mentioned, and usually the easiest way to prove something like this is to prove equivalence to the "predicative" definition

[Jakob von Raumer]

Seems about right. I think the equivalence to the existence of zigzags is such a predicative definition which could be used. I'll try to go that route and see how much hassle it is to deal with lifts of zigzags :grimacing:

[Reid Barton]

You don't necessarily even need to deal with zigzags, you can just take a quot

[Jakob von Raumer]

With zigzags the advantage would be that the equivalence to the currrent is_connected is already there

[Jakob von Raumer]

Ah, I think induct_on_objects might be enough to prove it, still a bit messy though

[Jakob von Raumer]

example [is_connected J] [hn : nonempty J] : is_connected (ulift_hom.{v₂} (ulift.{u₂} J)) :=
begin
  haveI : nonempty (ulift_hom.{v₂} (ulift.{u₂} J)), { simpa [ulift_hom] },
  let j₀ : J := classical.choice hn,
  fapply is_connected.of_induct,
  { exact ⟨j₀⟩ },
  { intros p hj₀ h j, cases j with j,
    let p' : set J := ((λ (j : J), p {down := j}) : set J),
    have hj₀' : j₀ ∈ p', { simp only [p'], exact hj₀ },
    apply induct_on_objects (λ (j : J), p {down := j}) hj₀',
    intros j₁ j₂ f, apply h,
    exact (ulift_hom_ulift_category.equiv J).functor.map f }
end

[Kevin Buzzard]

Nice!

[Bhavik Mehta]

Reid Barton said:

The definition of is_connected should really just be that if you quotient the objects by nonempty (A --> B), you get a singleton. I'm not sure why we have this complicated definition instead.

My hope was that I could pick any one definition in which the universe choices were obvious then show that the others are equivalent, it would be good enough (which is eg why I didn't pick of_constant_of_preserves_morphisms as the definition), and then the quotient definition vs the functor definition differ only in whether you care more about a slightly more complex definition, or more things needed to define before the main definition, and I picked arbitrarily. I have no objection to switching the definition!

[Jakob von Raumer]

In the end it doesn't matter that much, if we have all the right equivalences...

[Jakob von Raumer]

Status report (to help myself remember, too :sweat_smile: ): Made some progress, now category_theory.graded_object.lean cannot derive an instance mono (colimit.ι (discrete.functor (λ (i : β), Y i)) {as := i}) where before it had

[class_instances] caching instance for @mono ((λ (_x : β), C) i) _inst_1 (Y i)
  ((@colim (discrete (ulift β)) (category_theory.discrete_category (ulift β)) C _inst_1 _).obj
     (@discrete.functor C _inst_1 (ulift β) (λ (i : ulift β), Y i.down)))
  (@colimit.ι (discrete (ulift β)) (category_theory.discrete_category (ulift β)) C _inst_1
     (@discrete.functor C _inst_1 (ulift β) (λ (i : ulift β), Y i.down))
     _
     (@discrete.mk (ulift β) (@ulift.up β i)))
@split_mono.mono ((λ (_x : β), C) i) _inst_1 (Y i)
  ((@colim (discrete (ulift β)) (category_theory.discrete_category (ulift β)) C _inst_1 (_inst_2 (ulift β))).obj
     (@discrete.functor C _inst_1 (ulift β) (λ (i : ulift β), Y i.down)))
  (@colimit.ι (discrete (ulift β)) (category_theory.discrete_category (ulift β)) C _inst_1
     (@discrete.functor C _inst_1 (ulift β) (λ (i : ulift β), Y i.down))
     (@limits.has_colimit_of_has_colimits_of_shape C _inst_1 (discrete (ulift β))
        (category_theory.discrete_category (ulift β))
        (_inst_2 (ulift β))
        (@discrete.functor C _inst_1 (ulift β) (λ (i : ulift β), Y i.down)))
     (@discrete.mk (ulift β) (@ulift.up β i)))
  (@limits.split_mono_sigma_ι ((λ (_x : β), C) i) _inst_1 (ulift β) _inst_3 (λ (i : ulift β), Y i.down)
     (@limits.has_colimit_of_has_colimits_of_shape C _inst_1 (discrete (ulift β))
        (category_theory.discrete_category (ulift β))
        (_inst_2 (ulift β))
        (@discrete.functor C _inst_1 (ulift β) (λ (i : ulift β), Y i.down)))
     (@ulift.up β i))

and I'm still stuck at one universe conflict at category_theory.sites.sheaf.lean.

[Jakob von Raumer]

@Andrew Yang Can you have a look at locally_ringed_space/has_colimits.lean on the branch? Without a universe polymorphic walking_parallel_pair, the argument about the locally ringed space having colimits doesn't really work the same any more, because we cannot seem to generalise presheafed_space/has_colimits.lean to support index categories on any other universe level than the one of the morphisms of C...

[Jakob von Raumer]

With the PR being at 1,080 additions and 758 deletions, there's still any help welcome! @Scott Morrison @Johan Commelin

[Andrew Yang]

I have not yet looked into the problem, but doesn't has_finite_limits_of_has_limits_of_size (or some more universe-general version of it) solve the problem?

[Andrew Yang]

Also I would strongly suggest you to do the refactor a small portion at a time. That seems like a large diff to keep up with. Maybe one shape at a time if it is possible.

[Jakob von Raumer]

Not really possible, because the generalisation of preserves_limits is the big chunk that breaks everything.

[Jakob von Raumer]

Andrew Yang said:

I have not yet looked into the problem, but doesn't has_finite_limits_of_has_limits_of_size (or some more universe-general version of it) solve the problem?

No, the lies more in some auxiliary constructions from which has_coequalizers is derived. Since we don't want walking_parallel_pair to be universe polymorphic anymore, it seems this is one of the places where we do have to insert ulifts

[Andrew Yang]

Is there a core statement that you want to generalize, and all the other changes are just to prevent it from breaking?

[Jakob von Raumer]

I want preserves_limits, preserves_products, etc, and co to be compatible with functors between categories of different universe levels.

[Jakob von Raumer]

I do feel like I'm at least 80% to 90% through the critical files, it's mostly been straightforward fixes. The only critcal areas were sheaves and biproducts

[Andrew Yang]

Could you not generalize the universe for each of the definitions one at a time?
Note that the original PR #10736 that changed preserves_limits to preserves_limits_of_shape only has a diff of +208, -157.

[Jakob von Raumer]

I never fixed anything I didn't need to. The issue is that once one changes one limit over a fixed, finite index category like coequalizers, all of the others need to be changed, too.

[Jakob von Raumer]

Fixing the universe level for, say, walking_pair would be one first PR, but it does require all the fixes that make it so tedious right now.

[Andrew Yang]

Is there a reason that you couldn't leave presheafed_space.lean alone?
Since the file should not depend on any particular shapes, it shouldn't break when the other files upstream provides strictly stronger statements?

[Jakob von Raumer]

presheafed_space.lean itself is fine. it's presheafed_space/has_colimits.lean which does depend on a particular shape in that references coequalizers.

[Jakob von Raumer]

The file upstream is not strictly stronger because to have a maximally universe polymorphic preserves_coequalizers statement, we need to fix walking_parallel_pairs universe level and not pin it on the one of the category it's used for. This in turn causes (mostly trivial) need for fixes down the tree.

[Andrew Yang]

I pushed a attempt that seems to make both presheafed_space/has_colimits.lean and locally_ringed_space/has_colimits.lean both compile.

[Jakob von Raumer]

Cool, thanks a lot!!!

[Jakob von Raumer]

I think that's it, only lint errors remaining! :)

[Jakob von Raumer]

PR'ed: #15067

[Jakob von Raumer]

So if anyone volunteers to review this, I'm happy to make it a proper interactive video call review :grinning_face_with_smiling_eyes:

[Johan Commelin]

So everything about finite (co)limits now happens with index categories in Type, right?

[Johan Commelin]

And in the occasional moment where we have a finite type in a higher universe, we just have to forcefully bump it down.

[Jakob von Raumer]

Exactly. This can always be done with the equivalence to finset.

[Andrew Yang]

Will we ever need a PresheafedSpace valued in C : Type u with [category.{v} C] where the topological space is not in Top.{v}? The downside of this that we would always need to write PresheafedSpace.{v}.

[Jakob von Raumer]

/cc @Scott Morrison

[Jakob von Raumer]

I mean it does look like a place where in the light of topos theory etc the size matters and the universes diverges...

[Johan Commelin]

Andrew Yang said:

Will we ever need a PresheafedSpace valued in C : Type u with [category.{v} C] where the topological space is not in Top.{v}? The downside of this that we would always need to write PresheafedSpace.{v}.

In mathematical practice: most likely not. But sometimes Lean forces a situation on you where it might be natural to have differing universes.

[Johan Commelin]

I wouldn't bother generalizing it atm.

[Markus Himmel]

Jakob already generalized it, so the question is whether to un-generalize it

[Johan Commelin]

I think I wouldn't bother with that either :lol: