Zulip Chat Archive

Stream: maths

Topic: categories


view this post on Zulip Reid Barton (Sep 05 2018 at 14:43):

This new functor arrow doesn't seem to have an abbreviation in emacs.
'to input: type "C-x 8 RET 2964" or "C-x 8 RET RIGHTWARDS HARPOON WITH BARB UP ABOVE RIGHTWARDS HARPOON WITH BARB DOWN"'

view this post on Zulip Reid Barton (Sep 05 2018 at 21:16):

Scott, I see in the latest version of limits, is_limit and so on have become classes. I'm not sure how workable that will be because there are so many different ways to obtain new (co)limits from old ones. Right now I'm proving that restriction along a cofinal functor preserves colimit cones, but also consider that a left adjoint preserves colimits, and pushout squares glue together, and the other stuff I proved in my colimit_lemmas.lean file. I think this is too much to ask of the class system, and I worry that making the is_* types classes will make it more difficult to apply all these facts about (co)limits.

view this post on Zulip Reid Barton (Sep 05 2018 at 21:43):

We still don't have is_singleton do we?

variables (C : Type u) [𝒞 : category.{u v} C]
include 𝒞

def is_connected : Type u := is_singleton (quot (λ (a b : C), nonempty (a  b)))

view this post on Zulip Reid Barton (Sep 05 2018 at 21:43):

Lean taught me that this is the True Definition.

view this post on Zulip Kenny Lau (Sep 05 2018 at 21:44):

so the empty graph isn't connected?

view this post on Zulip Reid Barton (Sep 05 2018 at 21:46):

You missed a discussion on this topic in Orsay.

view this post on Zulip Reid Barton (Sep 05 2018 at 21:46):

https://ncatlab.org/nlab/show/connected+category

view this post on Zulip Johannes Hölzl (Sep 05 2018 at 21:48):

Shouldn't is_singleton be a Prop?

view this post on Zulip Reid Barton (Sep 05 2018 at 21:51):

That is an interesting question. If I make it constructive, then I can prove the result about cofinal functors preserving colimits constructively as well. It's actually a bit subtle--you need to get your hands on an inhabitant of C, but if you define connectedness in terms of the existence of zigzags, then you don't need the zigzags constructively, because they are only used to prove equalities.

view this post on Zulip Reid Barton (Sep 05 2018 at 21:52):

Currently, I simply have def is_singleton (α : Type*) := α ≃ unit.
This plus the above definition gives the correct amount of constructiveness.

view this post on Zulip Reid Barton (Sep 05 2018 at 21:54):

is_colimit is not a Prop (it is a subsingleton though), because it includes the data of how to construct the map given by the universal property. In order to build that map in my setting, I need to know that certain categories are connected in the above constructive sense.

view this post on Zulip Reid Barton (Sep 05 2018 at 21:55):

I'm still not sure whether these distinctions between Prop and subsingletons are worth making in the context of category theory.

view this post on Zulip Reid Barton (Sep 05 2018 at 21:56):

For context, I proved basically the implication 1 => 3 at https://ncatlab.org/nlab/show/final+functor#properties.

view this post on Zulip Reid Barton (Sep 05 2018 at 21:56):

There it is stated as "a map ... is an isomorphism", which is also a proposition classically which has constructive content.

view this post on Zulip Reid Barton (Sep 05 2018 at 21:59):

It's kind of fun to see how all these constructive aspects relate to one another, but I'm not sure how useful it is and there are some associated minor annoyances.

view this post on Zulip Reid Barton (Sep 05 2018 at 21:59):

So: I don't know. :)

view this post on Zulip Reid Barton (Sep 05 2018 at 22:03):

Probably either the name or the definition is wrong though.

view this post on Zulip Kevin Buzzard (Sep 05 2018 at 22:03):

yeah, that's definitely path-connected ;-)

view this post on Zulip Reid Barton (Sep 05 2018 at 22:34):

Haha :) The distinction doesn't exist to a homotopy theorist.
I remember being very confused when I couldn't prove that an arbitrary product of discrete topological spaces is discrete. Then I realized it was only true up to weak homotopy equivalence...

view this post on Zulip Scott Morrison (Sep 06 2018 at 03:09):

I think it's relatively painless to turn is_limit and friends back into structures (not classes). I guess what I desired was that the fact that is_limit c is a subsingleton should imply that it's okay that there are different ways to construct it. But I understand that Lean is not actually that clever, and we will run into problems where two typeclass instances look different, even though a subsingleton instance is available.

view this post on Zulip Scott Morrison (Sep 06 2018 at 03:10):

I do wonder if it could be a plausible addition to the typeclass mechanism: whenever we find that we using two instances that don't agree, first check for an instance of subsingleton before complaining about it.

view this post on Zulip Scott Morrison (Sep 06 2018 at 09:24):

So, @Reid Barton, I guess I don't really understand what the problem is with having is_limit being a typeclass. Certainly there is a problem with having too many instances (because we'll get colliding instances), but nothing particularly forces us to mark constructions as instances.

view this post on Zulip Scott Morrison (Sep 06 2018 at 09:25):

Having "really canonical" ones, like the one that has_limits provides, seems quite helpful.

view this post on Zulip Scott Morrison (Sep 06 2018 at 09:26):

As you point out, we'll certainly want to use non-instance instances of is_limit and friends, so I agree a good change could be to change it back to a structure and just add the class attribute afterwards, so the syntax is as usual for structures.

view this post on Zulip Scott Morrison (Sep 06 2018 at 09:26):

I'm also open to being convinced it just shouldn't be a class at all.

view this post on Zulip Reid Barton (Sep 06 2018 at 09:30):

I think the structure + attribute [class] option will probably address my concerns. I do see the use of instance lookup for common cases.

view this post on Zulip Reid Barton (Sep 06 2018 at 09:37):

The problem with just a class is that it's useful to handle these is_limit values manually, as you say, and maybe I am just bad at dealing with classes, but I find there's more friction there. For example maybe you have a cone which is only propositionally equal to one which you have a lemma about. Then it's easier to convert the lemma application and fix up the resulting subgoals.

view this post on Zulip Reid Barton (Sep 06 2018 at 09:38):

I tried making my is_colimit_of_is_cofinal into an instance and it did work in the simple use case later... provided I made is_cofinal an instance too. It's infectious!

view this post on Zulip Reid Barton (Sep 06 2018 at 09:39):

Made is_cofinal a class, I mean.

view this post on Zulip Johan Commelin (Sep 06 2018 at 09:39):

That's automation, man!

view this post on Zulip Reid Barton (Sep 06 2018 at 10:00):

For example maybe you have a cone which is only propositionally equal to one which you have a lemma about.

I guess the point here is that being a limit cone is a property of a diagram, and diagrams have morphisms in them, and it's really common to have non-syntactic or even non-definitional equalities between morphisms (we call them commutative diagrams). Whereas for the class group, for instance, it's much less common to have non-syntactic equalities between groups.

view this post on Zulip Scott Morrison (Sep 06 2018 at 10:13):

Okay: for now I will try out having them as structure with class added after the fact. If that doesn't go well, complain and we can just go back to bare structures. I think you're making more use of limits than I am, so I'm happy to follow your direction.

view this post on Zulip Scott Morrison (Sep 06 2018 at 10:15):

Also on the topic of categories, I'd be curious @Reid Barton and @Johan Commelin if you have any thought about my concerns re: @Johannes Hölzl's nice framework for building concrete categories from typeclasses.

view this post on Zulip Scott Morrison (Sep 06 2018 at 10:15):

https://github.com/leanprover/mathlib/pull/316#issuecomment-419039990

view this post on Zulip Scott Morrison (Sep 06 2018 at 10:15):

My main concern is that it boxes us in to using lots of sigma types and subtypes, where my instinct had been to define lots of custom structures. :-)

view this post on Zulip Johan Commelin (Sep 06 2018 at 10:16):

hmmm... ring_homs don't form an additive group... but never mind

view this post on Zulip Johan Commelin (Sep 06 2018 at 10:20):

@Scott Morrison One of the reasons I was asking about definitions by meta code yesterday was for this sort of thing. If we make concrete_category meta, then it could make all those bundled defintions for us, couldn't it?

view this post on Zulip Johan Commelin (Sep 06 2018 at 10:20):

But I'm still too much of an amateur to know what the pros and cons are of these approaches.

view this post on Zulip Johan Commelin (Sep 06 2018 at 10:21):

My gut feeling is that if Johannes writes something, I won't be able to improve it. (Maybe next year :smiley:)

view this post on Zulip Reid Barton (Sep 06 2018 at 10:23):

oh I hadn't seen those comments yet, thanks.

view this post on Zulip Reid Barton (Sep 06 2018 at 10:33):

I also had the same, vague concern about your point 1. I hadn't thought of your point 2, will have to think about that one some more.
I think the example you gave of homeomorphisms isn't that compelling, because you could also build (Top, homeos) as the category- (or groupoid-)of-isomorphisms-in the concrete-category Top. Maybe we can come up with a more interesting example?

view this post on Zulip Reid Barton (Sep 06 2018 at 10:50):

I commented about point 1 on the issue.

view this post on Zulip Kevin Buzzard (Sep 06 2018 at 10:58):

I guess what I desired was that the fact that is_limit c is a subsingleton should imply that it's okay that there are different ways to construct it. But I understand that Lean is not actually that clever, and we will run into problems where two typeclass instances look different, even though a subsingleton instance is available.

Chris Hughes had typeclass problems with fintype even though it's a subsingleton -- he would occasionally get two instances kicking around and then rewrites would start to fail. He even talked at some point about writing a tactic which might solve his problems, but somehow tactic-writing is not our fort\'e in London, nobody can do it yet, and he just ended up with too many questions which nobody could answer.

Even more interesting -- is_linear_map is a Prop but Johannes made it a structure not a class. I talked to him about this a bit in Orsay. My impression was that he couldn't see the point of adding it to the type class inference system, because the instance that you want to trigger -- composition of two linear maps is a linear map -- tends not to trigger, because in functional languages people compose functions by writing them next to each other rather than using function.comp. We now have a hybrid system where is_group_hom is a class and is_linear_map is not.

view this post on Zulip Scott Morrison (Sep 06 2018 at 11:02):

hmmm... ring_homs don't form an additive group... but never mind

Ooops. :flushed: I'll remove the evidence of that one. :-) There are plenty of less-wrong examples, of course.

view this post on Zulip Scott Morrison (Sep 06 2018 at 11:05):

The question about is_linear_map being problematic, because people write their functions using lambdas, could be solved by educating everyone to not use lambdas when you're hoping to use typeclass inference, I guess. It's not totally unreasonable. :-)

view this post on Zulip Reid Barton (Sep 06 2018 at 11:07):

And here I have been wondering how hard it would be to get something like lambda syntax for functors...

view this post on Zulip Kevin Buzzard (Sep 06 2018 at 11:11):

I actually engaged with Scott's category theory library for the first time yesterday, thanks to @Ned Summers peppering me with questions, and I must say it was a bit scary having to do all the morphism composition using some morphism composition operator...

view this post on Zulip Reid Barton (Sep 06 2018 at 11:11):

I tried writing down just the expression "colim_{j in J} lim_{i in I} F(i, j)" and it turned into something ugly like colimit ((curry.map F).comp lim)

view this post on Zulip Reid Barton (Sep 06 2018 at 11:13):

Kevin, that's why most of my files contain the magic words local notation f ` ∘ `:80 g:80 := g ≫ f :)

view this post on Zulip Scott Morrison (Sep 06 2018 at 11:23):

@Kevin Buzzard, were you referring to having to write some composition operator, rather than a lambda, or to the fact that the composition operator is "backwards"?

view this post on Zulip Scott Morrison (Sep 06 2018 at 11:25):

(I've been thinking a lot recently about monoidal categories enriched in a braided category, and here it really matters that you write composition "correctly", because every time you move symbols past each other you have to keep track of a braiding.)

view this post on Zulip Kevin Buzzard (Sep 06 2018 at 11:29):

I can handle "backwards", it was the shock of having to do it at all.

view this post on Zulip Scott Morrison (Sep 06 2018 at 11:39):

@Reid Barton, unfortunately I'm having trouble with the structure + attribute [class] approach: I can't ever get it to infer the is_limit instances, making it pretty useless.

view this post on Zulip Scott Morrison (Sep 06 2018 at 11:40):

I guess I will go back to just structures.

view this post on Zulip Kevin Buzzard (Sep 06 2018 at 12:11):

If it's any help, I think this (structure + attribute [class]) is how topological spaces are set up.

view this post on Zulip Ned Summers (Sep 06 2018 at 17:12):

Hey guys,

I've got a situation where I have two objects of a category X and Y, and a theorem that says X = Y. Obviously there then is a f : X ⟶ Y corresponding to the identity morphism on X (or the identity morphism on Y). I was wondering if writing/using this has been dealt with so far in the mathlib category theory content?

(this is in the context of lean asking for something of type Y ⟶ Y. I have one of type X ⟶ X in mind but lean is not happy if I give it that here (except using cast or eq.rec and these have already caused a lot of trouble). Kevin and I figured it might be easier to instead compose on either side of this choice these morphisms X ⟶ Y and Y ⟶ X corresponding to those identities. Any ideas about that also welcomed!)
Thanks!

view this post on Zulip Reid Barton (Sep 06 2018 at 17:17):

Yes, there is something for exactly this situation. See eq_to_iso in category_theory.isomorphism.

view this post on Zulip Reid Barton (Sep 06 2018 at 17:18):

And there are a couple simp lemmas there which are supposed to make proving things about composition with these morphisms easier than proving things about eq.rec.

view this post on Zulip Reid Barton (Sep 06 2018 at 19:18):

@Scott Morrison, do you have some conversions between equiv and iso in Set somewhere?

view this post on Zulip Scott Morrison (Sep 06 2018 at 23:01):

No, I don't have that conversion, but it should be added!

view this post on Zulip Scott Morrison (Sep 06 2018 at 23:01):

"equiv is iso to iso"? :-)

view this post on Zulip Kenny Lau (Sep 07 2018 at 01:51):

@Scott Morrison Do we have Yoneda? :D

view this post on Zulip Scott Morrison (Sep 07 2018 at 01:57):

Sure, it's in <https://github.com/semorrison/lean-category-theory/blob/master/src/category_theory/yoneda.lean>. It's slowly getting towards the head of the queue for PR'ing into mathlib...

view this post on Zulip Reid Barton (Sep 09 2018 at 22:33):

Mario, do you have an opinion on whether "the category C is connected" and "the functor F is cofinal" should be props or subsingletons?

view this post on Zulip Reid Barton (Sep 09 2018 at 22:35):

I have a version using subsingletons and it means you can prove cofinal functors preserve colimits constructively (e.g., produce an inverse to the induced map) which is kind of cool, but now I feel it's probably not worth the hassle

view this post on Zulip Mario Carneiro (Sep 09 2018 at 22:40):

https://ncatlab.org/nlab/show/final+functor

A functor F:C→DF : C \to D is final (often called cofinal)

WHYY

view this post on Zulip Mario Carneiro (Sep 09 2018 at 22:40):

Dually, a functor is initial (sometimes called co-cofinal)

wtf

view this post on Zulip Mario Carneiro (Sep 09 2018 at 22:41):

I think I'm co-confused

view this post on Zulip Mario Carneiro (Sep 09 2018 at 22:48):

To me, "connected" sounds like a Prop, I'm not sure how to state it naturally as a subsingleton without using trunc

view this post on Zulip Mario Carneiro (Sep 09 2018 at 22:49):

The definition of cofinal appears to use "nonempty and connected", which sounds like an "is_singleton" statement, which I can see usefully as a type. Is there a natural choice of inhabitant in this case?

view this post on Zulip Mario Carneiro (Sep 09 2018 at 22:50):

I think that being able to construct inverses to given maps is one of the more relevant uses of doing category theory constructively

view this post on Zulip Reid Barton (Sep 10 2018 at 02:25):

Yeah the terminology is unfortunate. The "co-" is not the dualizing "co-", but the "together" one, like the categories have the same behavior as you go towards the "end". In practice people only care about (co)final functors and not the other side I think.

view this post on Zulip Reid Barton (Sep 10 2018 at 02:27):

Is there a natural choice of inhabitant in this case?

There isn't automatically one in general but typically when you prove a functor is cofinal there will be an obvious way to choose an inhabitant.

view this post on Zulip Reid Barton (Sep 10 2018 at 02:33):

Oh yes, by connected I mean to include nonempty. That's the only part which is data

view this post on Zulip Reid Barton (Sep 10 2018 at 02:36):

The connected components are quot (λ (a b : C), nonempty (a ⟶ b)) (for some reason I don't remember ever seeing this very simple and Lean-friendly definition), and then you need to say this type has exactly one inhabitant, which can be constructively or not.

view this post on Zulip Reid Barton (Sep 10 2018 at 02:40):

I guess I'll continue to try with the constructive definition if you don't have a strong opinion. The pros and cons of both approaches are pretty minor


Last updated: May 09 2021 at 10:11 UTC