Zulip Chat Archive

Stream: new members

Topic: Directed/filtered categories


view this post on Zulip Calle Sönne (Jun 13 2019 at 19:17):

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

view this post on Zulip Johan Commelin (Jun 13 2019 at 19:18):

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

view this post on Zulip Scott Morrison (Jun 13 2019 at 23:12):

I think this would be a great project!

view this post on Zulip Reid Barton (Jun 16 2019 at 01:12):

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

view this post on Zulip Calle Sönne (Jun 18 2019 at 15:18):

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

view this post on Zulip Reid Barton (Jun 18 2019 at 15:36):

@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.

view this post on Zulip Reid Barton (Jun 18 2019 at 15:37):

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.

view this post on Zulip Reid Barton (Jun 18 2019 at 15:37):

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

view this post on Zulip Calle Sönne (Jun 18 2019 at 16:24):

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

view this post on Zulip Calle Sönne (Jun 18 2019 at 16:26):

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".

view this post on Zulip Reid Barton (Jun 18 2019 at 16:28):

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.

view this post on Zulip Chris Hughes (Jun 18 2019 at 16:31):

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.

view this post on Zulip Reid Barton (Jun 18 2019 at 16:34):

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.

view this post on Zulip Calle Sönne (Jun 18 2019 at 16:35):

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?

view this post on Zulip Chris Hughes (Jun 18 2019 at 16:37):

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.

view this post on Zulip Kevin Buzzard (Jun 18 2019 at 16:40):

@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.

view this post on Zulip Calle Sönne (Jun 18 2019 at 16:47):

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

view this post on Zulip Chris Hughes (Jun 18 2019 at 16:51):

Yes.

view this post on Zulip Ken Lee (Jun 18 2019 at 17:11):

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

view this post on Zulip Reid Barton (Jun 18 2019 at 17:16):

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

view this post on Zulip Scott Morrison (Jun 18 2019 at 21:55):

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.

view this post on Zulip Scott Morrison (Jun 18 2019 at 21:55):

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

view this post on Zulip Scott Morrison (Jun 18 2019 at 21:56):

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.

view this post on Zulip Scott Morrison (Jun 18 2019 at 21:56):

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.

view this post on Zulip Scott Morrison (Jun 18 2019 at 21:57):

(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.)

view this post on Zulip Scott Morrison (Jun 18 2019 at 21:58):

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.


Last updated: May 10 2021 at 00:31 UTC