Zulip Chat Archive

Stream: maths

Topic: Localization of categories


view this post on Zulip Adam Topaz (Aug 21 2020 at 14:56):

I've been playing around more with these inductive-quotient constructions, and I've sketched out the localization of a category here:
https://github.com/leanprover-community/mathlib/blob/cat_localization/src/category_theory/localization.lean

I'm sure others have thought about doing this, e.g. in relation to derived categories. I didn't find anything in mathlib, so I wonder whether there is another branch that makes a similar construction?

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 14:58):

Categories have been a work in progress for many many years. We only got things like abelian categories very recently and so it's only now that we can start to do what in number theory one would think of as "the basics".

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 15:00):

If you look at how many lines of code there is in the category theory and algebra/category files you can see how much work Scott has done on this stuff, but it has been a huge ongoing project and in some sense is currently largely unrelated to the rest of mathlib

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 15:01):

This has been one of the criticisms of the development -- "what is the point of it?". But Scott has persevered for years and now it's looking increasingly likely that we're going to be using it to do schemes

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 15:02):

But IIRC a year ago he was still formalising things like limits, equalisers etc. He's been mostly working alone whilst simultaneously developing tactics

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 15:03):

Now is the time for us to find out whether his theory is usable and I think it will be, but I also think it's a great time to start making stuff like derived functors etc

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 15:04):

I don't think we even have delta functors

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 15:04):

This stuff is all now just becoming possible

view this post on Zulip Adam Topaz (Aug 21 2020 at 15:05):

Since abelian categories now exist, what about the category of complexes?

view this post on Zulip Adam Topaz (Aug 21 2020 at 15:05):

Someone is working on that, if I recall correctly...

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 15:05):

There is an irritating design decision here

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 15:05):

Do you want them to be semi infinite or infinite?

view this post on Zulip Adam Topaz (Aug 21 2020 at 15:06):

Oh I see.

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 15:06):

I think that perhaps the correct setting for this is to have some kind of type with a succ function

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 15:06):

I learnt this trick from @Floris van Doorn

view this post on Zulip Adam Topaz (Aug 21 2020 at 15:07):

succ being the differential in this case?

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 15:08):

And a complex is a functor from this diagram to Ab,

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 15:08):

I'm thinking of the type as an index type

view this post on Zulip Adam Topaz (Aug 21 2020 at 15:08):

Ah ok.

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 15:08):

Eg nat or int

view this post on Zulip Johan Commelin (Aug 21 2020 at 15:08):

Complexes are already there

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 15:08):

Oh great

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 15:08):

What about short exact sequences of complexes?

view this post on Zulip Johan Commelin (Aug 21 2020 at 15:09):

So we only need to turn it into an infty-cat

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 15:09):

Are they indexed by nat, int or a more general thing?

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 15:09):

Are you serious about infinity cats?

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 15:09):

What do they have to do with it?

view this post on Zulip Adam Topaz (Aug 21 2020 at 15:09):

I mean, complexes are just simplicial abelian groups right? :triangular_ruler:

view this post on Zulip Adam Topaz (Aug 21 2020 at 15:11):

docs#chain_complex

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 15:11):

Did you see the CGDA thread @Adam Topaz ?

view this post on Zulip Adam Topaz (Aug 21 2020 at 15:11):

No.

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 15:11):

Things start to get a bit hairy after a while

view this post on Zulip Johan Commelin (Aug 21 2020 at 15:14):

It's not clear to me whether I'm serious about infty-cats

view this post on Zulip Adam Topaz (Aug 21 2020 at 15:14):

Johan Commelin said:

It's not clear to me whether I'm serious about infty-cats

Certainly we would want to consider the internal hom, right?

view this post on Zulip Johan Commelin (Aug 21 2020 at 15:14):

I'm scared by all the coherence issues that homological algebra will bring upon us

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 15:19):

I can't link to the CDGA thread because I'm on mobile but if you search for "I thought the discussion related to definitional associativity of addition and so on might benefit from a concrete example" you'll find it.

view this post on Zulip Adam Topaz (Aug 21 2020 at 15:19):

I found it (in case it helps: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/CDGAs/near/167848869 )

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 15:26):

In short, somehow considering the direct sum of the objects seems to be an essential trick

view this post on Zulip Kevin Buzzard (Aug 21 2020 at 15:26):

Implementation issues start getting serious at this point and until we've tried a few ways we won't know what works best in dependent type theory

view this post on Zulip Scott Morrison (Aug 21 2020 at 23:01):

Another approach to CDGAs now would be as an internal commutative monoid.

view this post on Zulip Scott Morrison (Aug 21 2020 at 23:02):

I suspect this would provide excellent insulation from DTT hell. Whether they're usable is a separate question. :-)

view this post on Zulip Adam Topaz (Aug 21 2020 at 23:02):

Right, but the associative condition / commutative condition are only true up to homotopy

view this post on Zulip Adam Topaz (Aug 21 2020 at 23:02):

of chain complexes

view this post on Zulip Adam Topaz (Aug 21 2020 at 23:07):

I guess you could work in the homotopy category?

view this post on Zulip Adam Topaz (Aug 21 2020 at 23:10):

Oh never mind, it's just a monoid object in complexes

view this post on Zulip Adam Topaz (Aug 21 2020 at 23:21):

I guess these so-called A_infinity algebras are monoids up to homotopy?

view this post on Zulip Scott Morrison (Aug 22 2020 at 00:15):

Kevin Buzzard said:

This has been one of the criticisms of the development -- "what is the point of it?". But Scott has persevered for years and now it's looking increasingly likely that we're going to be using it to do schemes

@Bhavik Mehta, @Markus Himmel and @Johan Commelin have all made very substantial contributions, and there are others as well. Homological algebra and sheaves, both built on top of this library, have finally started to arrive.

view this post on Zulip Scott Morrison (Aug 22 2020 at 00:17):

Adam Topaz said:

I've been playing around more with these inductive-quotient constructions, and I've sketched out the localization of a category here:
https://github.com/leanprover-community/mathlib/blob/cat_localization/src/category_theory/localization.lean

I'm sure others have thought about doing this, e.g. in relation to derived categories. I didn't find anything in mathlib, so I wonder whether there is another branch that makes a similar construction?

I do remember seeing someone's branch a while back, but I think it did less than you've already got here. This looks good!

view this post on Zulip Scott Morrison (Aug 22 2020 at 00:18):

Kevin Buzzard said:

What about short exact sequences of complexes?

There isn't a bundled ShortExactSequence structure, but Markus PR'd the definition of exactness a week or so ago, so it's completely possible to state the theorem about long exact sequences now.

view this post on Zulip Adam Topaz (Aug 22 2020 at 01:47):

Okay! I'll try to clean it up a bit and open a PR soon. I think it's worthwhile to prove, e.g., that lift is functorial in F. But the statement is a bit complicated, since the source category is the full subcategory of functors which map S to isomorphisms.


Last updated: May 11 2021 at 16:22 UTC