Directed/filtered categories

Stream: new members

[Calle Sönne]

Is directed/filtered categories in mathlib? Cant seem to find it in the category theory folder

[Johan Commelin]

Nope, not yet. I think @Reid Barton has some stuff in his homotopy theory repo

[Scott Morrison]

I think this would be a great project!

[Reid Barton]

@Calle Sönne what did you want to use them for?

[Calle Sönne]

Nothing much really, I was just curious as to how/if they were defined in lean

[Reid Barton]

@Calle Sönne One definition is at https://github.com/leanprover-community/mathlib/blob/filtered-colimits-2/src/category_theory/filtered.lean. That branch also has some facts about filtered colimits of sets starting at https://github.com/leanprover-community/mathlib/blob/filtered-colimits-2/src/category_theory/limits/types.lean#L100.

[Reid Barton]

The main question is whether the notion of being filtered should be a Prop (as I made it there), a subsingleton (to maintain constructivity, while still being faithful to the fact that being filtered is a property in math, not additional structure), or really encode a choice of cocones on each relevant thing, so that the same category could have multiple distinct filtered structures.

[Reid Barton]

Or perhaps more than one of these turns out to be useful

[Calle Sönne]

Thank you!

(cocone_objs : ∀ (X Y : C), ∃ Z (f : X ⟶ Z) (g : Y ⟶ Z), true)

@Ken Lee this is a nice way to do the "filtered" criterion

[Calle Sönne]

Me and @Ken Lee tried to define it ourselves, and ended up defining it as a category with additional structure (not sure if that is what you mean by subsingleton), what would be the main difference between that and prop? To me as a math student they seem to be the "same".

[Reid Barton]

To make it a subsingleton you would use trunc of a sigma type in place of an exists. Or make a structure which contains all the choices and take a trunc of the whole thing.

[Chris Hughes]

A good example of a subsingleton that isn't a prop is fintype

class fintype (α : Type*) :=
(elems : finset α)
(complete : ∀ x : α, x ∈ elems)

The difference is that with this definition I can compute using the finset in question. For example #eval fintype.elems bool returns {ff, tt}, which I couldn't do with a mere proof that such a finset existed.

[Reid Barton]

Right, and the advantage of a Prop is that you never have to worry about having two different (as in non-definitionally equal) values of the Prop, or something else depending on the proof of that Prop.

[Calle Sönne]

To make it a subsingleton you would use trunc of a sigma type in place of an exists. Or make a structure which contains all the choices and take a trunc of the whole thing.

What do you mean by trunc?

[Chris Hughes]

trunc is quotient by the always true relation. This is a computable version of nonempty. It maintains some computability since you can turn any constant computable function X -> Y into a function trunc X -> Y computably.

[Kevin Buzzard]

@Calle Sönne as you may well know, in Lean all proofs of P are the same. So if P : Prop and then h1 : P and h2 : P then we will have h1 = h2 (and the proof will be rfl). However there are other types which have exactly one term, and then it might be a theorem that two terms of that type are equal rather than being true by definition. And furthermore the terms might somehow store data, whereas a proof in Lean is checked by the kernel and then instantly forgotten about (Lean basically just puts a tick by the proposition to say "this has been proved"). A subsingleton is a type T for which you can prove that if a : T and b : T then a = b. Examples are propositions, but there are other examples too.

[Calle Sönne]

So fintype, as @Chris Hughes defined it, is a subsingleton since any two finite sets that contains exactly all terms of alpha are equal?

[Chris Hughes]

Yes.

[Ken Lee]

wow, the type of cocone_objs... feels like cheating :joy:

[Reid Barton]

This exists ... ..., true is a bit silly but I find it's often easier and clearer than alternatives

[Scott Morrison]

my feeling is that it's best to have filtered_structure, which unashamedly contains the data of a cone for each pair, etc, and then have a filtered typeclass which is just trunc filtered_structure.

[Scott Morrison]

I'm not so keen on the intermediate solution where each individual field of filtered is either an existential statement or truncd data.

[Scott Morrison]

It's really a question of where you want to put the proof obligations of showing your construction didn't depend on the filtered structure.

[Scott Morrison]

You either have to do it every time you use a cone or equaliser, or once after a multi-step construction that uses several cones/equalisers.

[Scott Morrison]

(The first alternative is what you get if each field of filtereed is an existential or trunc. The second alternative is what you get if you trunc the entire structure.)

[Scott Morrison]

My limited experience using filtered was that the second alternative was more pleasant to use --- and it's the sort of argument that feels like you should be able to automate away, so it's nice if it's all quarantined in one place.