Localization of categories

Stream: maths

[Adam Topaz]

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]

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]

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]

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]

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]

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]

I don't think we even have delta functors

[Kevin Buzzard]

This stuff is all now just becoming possible

[Adam Topaz]

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

[Adam Topaz]

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

[Kevin Buzzard]

There is an irritating design decision here

[Kevin Buzzard]

Do you want them to be semi infinite or infinite?

[Adam Topaz]

Oh I see.

[Kevin Buzzard]

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

[Kevin Buzzard]

I learnt this trick from @Floris van Doorn

[Adam Topaz]

succ being the differential in this case?

[Kevin Buzzard]

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

[Kevin Buzzard]

I'm thinking of the type as an index type

[Adam Topaz]

Ah ok.

[Kevin Buzzard]

Eg nat or int

[Johan Commelin]

Complexes are already there

[Kevin Buzzard]

Oh great

[Kevin Buzzard]

What about short exact sequences of complexes?

[Johan Commelin]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Are you serious about infinity cats?

[Kevin Buzzard]

What do they have to do with it?

[Adam Topaz]

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

[Adam Topaz]

docs#chain_complex

[Kevin Buzzard]

Did you see the CGDA thread @Adam Topaz ?

[Adam Topaz]

No.

[Kevin Buzzard]

Things start to get a bit hairy after a while

[Johan Commelin]

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

[Adam Topaz]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Scott Morrison]

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

[Adam Topaz]

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

[Adam Topaz]

of chain complexes

[Adam Topaz]

I guess you could work in the homotopy category?

[Adam Topaz]

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

[Adam Topaz]

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

[Scott Morrison]

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]

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!

[Scott Morrison]

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]

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.