## Stream: maths

### Topic: Localization of categories

#### 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?

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

#### 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

#### 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

#### 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

#### 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

#### Kevin Buzzard (Aug 21 2020 at 15:04):

I don't think we even have delta functors

#### Kevin Buzzard (Aug 21 2020 at 15:04):

This stuff is all now just becoming possible

#### Adam Topaz (Aug 21 2020 at 15:05):

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

#### Adam Topaz (Aug 21 2020 at 15:05):

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

#### Kevin Buzzard (Aug 21 2020 at 15:05):

There is an irritating design decision here

#### Kevin Buzzard (Aug 21 2020 at 15:05):

Do you want them to be semi infinite or infinite?

Oh I see.

#### 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

#### Kevin Buzzard (Aug 21 2020 at 15:06):

I learnt this trick from @Floris van Doorn

#### Adam Topaz (Aug 21 2020 at 15:07):

succ being the differential in this case?

#### Kevin Buzzard (Aug 21 2020 at 15:08):

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

#### Kevin Buzzard (Aug 21 2020 at 15:08):

I'm thinking of the type as an index type

Ah ok.

Eg nat or int

Oh great

#### Kevin Buzzard (Aug 21 2020 at 15:08):

What about short exact sequences of complexes?

#### Johan Commelin (Aug 21 2020 at 15:09):

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

#### Kevin Buzzard (Aug 21 2020 at 15:09):

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

#### Kevin Buzzard (Aug 21 2020 at 15:09):

Are you serious about infinity cats?

#### Kevin Buzzard (Aug 21 2020 at 15:09):

What do they have to do with it?

#### Adam Topaz (Aug 21 2020 at 15:09):

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

#### Adam Topaz (Aug 21 2020 at 15:11):

docs#chain_complex

No.

#### Kevin Buzzard (Aug 21 2020 at 15:11):

Things start to get a bit hairy after a while

#### Johan Commelin (Aug 21 2020 at 15:14):

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

#### 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?

#### Johan Commelin (Aug 21 2020 at 15:14):

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

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

#### 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 )

#### Kevin Buzzard (Aug 21 2020 at 15:26):

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

#### 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

#### Scott Morrison (Aug 21 2020 at 23:01):

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

#### 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. :-)

#### Adam Topaz (Aug 21 2020 at 23:02):

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

#### Adam Topaz (Aug 21 2020 at 23:02):

of chain complexes

#### Adam Topaz (Aug 21 2020 at 23:07):

I guess you could work in the homotopy category?

#### Adam Topaz (Aug 21 2020 at 23:10):

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

#### Adam Topaz (Aug 21 2020 at 23:21):

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

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

#### Scott Morrison (Aug 22 2020 at 00:17):

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!

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

#### 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