IsKFiltered.{k} ?

Stream: maths

[Robert Maxton]

Mario Carneiro said:

(This is unlike the situation for Type u, which you cannot prove is the same cardinality as those three types because Type u is not a quotient, e.g. there could be a very large number of empty types in it and the axioms don't rule this possibility out.)

... Huh.

So, I think I'm in a scenario where I would like to be able to talk about k-filtered categories, where k is here not a cardinality but rather just a universe level. (This is mainly for convenience, as all of our existing category HasFooOfSize is also written for universe levels.) I got most of the way through proving that k-filtered categories are in fact a well-defined thing that have cocones for k-sized diagrams and generally behave as you'd expect them to as if k was a regular cardinal $\kappa$, though I hadn't quite gotten to proving the key "k-filtered colimits commute with k-small limits" theorem before noticing that docs#CategoryTheory.IsCardinalFiltered existed and giving it up under the assumption that it already existed.

And then I started trying to use it, couldn't find an existing proof that #(Type k) is regular, and ran across this post while trying to figure out if one should exist. So, it sounds like it'd be nontrivial to use IsCardinalFiltered in the case where κ = #(Type k), because #(Type k) isn't something we can pin down to begin with?

[Robert Maxton]

That being the case, would IsKFiltered.{k} be worth separately implementing after all? Assuming that the last proof goes through, but I would imagine it should since whatever size Type k is it's the same size in the filtering condition and the limit...

[Robert Maxton]

(Alternatively, someone can toss me a proof of #(Type k).IsRegular and the point becomes moot, but sadly my education in theory of cardinals is completely nonextant :p )

[Mario Carneiro]

I think this needs some #xy. Where is #(Type k) arising? You can certainly make use of a universe level to measure sizes, but the correct way to turn that into a cardinal is to use #Cardinal.{k} rather than #(Type k).

[Mario Carneiro]

#(Type k) is not necessarily a regular cardinal

[Mario Carneiro]

the only thing one can prove about it is that it's a cardinal and it's larger than #Cardinal.{k} which is a strong inaccessible

[Mario Carneiro]

it may well be cofinality omega

[Mario Carneiro]

it's easy to produce non-regular cardinals above an inaccessible $\kappa$, just take $\aleph_{\kappa+\omega}$

[Robert Maxton]

Wonderful. :wry:

#xy : I'm (hopefully) finishing up my implementation of colimits in Quiv.{v, u} where $v \neq u$. Quiv.{v, u} is no longer an entire presheaf category, it's now a full subcategory, so definitionally it's missing some of its colimits. I'm trying to pin down exactly which colimits it's missing; after flailing at trying to make filtered colimits work I'm now pretty sure that I need u-filtered colimits, because among other reasons I have a handwavey argument that says that Quiv.{v, u} can still be implemented as a limit over a diagram of size u (by 'hard-coding' the type of the vertices)

[Robert Maxton]

(Also because if I have u-filteredness then I can say that any collection of vertices of size u are identified in the colimit iff they were already identified somewhere in the base of the cocone, and since everything in the base of the cocone is v, u-small by assumption then the colimit also has to be v, u small)

[Mario Carneiro]

The question is, at what point does a # meet a Type u. When you talk about "u-small" with regard to Type u it's not about cardinality, it's about various type families coming from the appropriate universes

[Robert Maxton]

Right. The point where # meets Type u is the point where I want to use existing API, specifically IsCardinalFiltered, instead of inventing my own and duplicating a bunch of code. If that's not possible then of course I can just redo everything with universe levels from the start.

[Mario Carneiro]

How exactly are you using IsCardinalFiltered?

[Mario Carneiro]

you should certainly be able to use it

[Mario Carneiro]

I think you are just instantiating it incorrectly

[Mario Carneiro]

I think you just need to pass in Cardinal.univ to that function

[Robert Maxton]

open Cardinal in
/--A `k`-filtered category is one which `IsCardinalFiltered C #(Type k)`-/
abbrev IsKFiltered.{k} (C : Type u) [Category.{v} C] :=
  IsCardinalFiltered C #(Type k)

/--For a `k`-filtered colimit, any `k`-sized collection of vertices in the colimit
are identified iff they are already identified in some quiver in the base of the cone.-/
lemma kFilteredColimit_iInj.{k} [UnivLE.{w, v}] {J : Type w} [Category.{w} J]
    [IsKFiltered.{k} J] {ι : Type k}
    (F : J ⥤ WalkingQuiver ⥤ Type v) (c : ColimitCocone F) (q₀ : WalkingQuiver)
    {j : ι → J} (X : (i : ι) →  F.obj i |>.obj q₀) :
    (∀ (i₁ i₂ : ι), (c.1.ι.app (j i₁)).app q₀ (X i₁) = (c.1.ι.app (j i₂)).app q₀ (X i₂)) ↔
      ∃ (k : J) (f : (i : ι) → (j i) ⟶ k), ∀ (i₁ i₂ : ι),
        (F.map (f i₁)).app q₀ (X i₁) = (F.map (f i₂)).app q₀ (X i₂) := by sorry

[Robert Maxton]

If I just pass Cardinal.univ.{k} instead, will that get me the ability to take maxima in J of collections of size k?

[Mario Carneiro]

yes

[Robert Maxton]

mk
I'll go with that then, thanks

[Mario Carneiro]

I think there is still some subtlety here though, because the HasCardinalLT (Arrow A) κ assumption is measuring the size of a category of arrows, and so I can imagine that if A is Type u then this will also implicate #(Type u) in some fashion

[Mario Carneiro]

You don't need to change the definition, but in such a case you would want to show that the category has a small skeleton (or something along those lines), even if it has a lot of redundant objects that push up the raw size of the category

[Robert Maxton]

hm
nods
Alright, lemme start elaborating this and see where it goes