Factorization algebras

Stream: Is there code for X?

[Jackson Walters]

Are factorization algebras in Lean?

I heard that Perfectoid spaces made it in, and some fairly tricky proofs were successfully formalized at Scholze's behest. It seems like it should be possible to include factorization and pre-factorization algebras (co-sheafy) and vertex algebras (complex analytic and power series). During my thesis, we spent a lot of time unpacking and parsing a theorem of Costello-Gwilliam regarding conditions necessary to extract a vertex algebra from a prefactorization algebras satisfying certain technical conditions. To my surprise, it appears Daniel Bruegmann has organized this procedure quite nicely in a preprint (5/18/21, https://arxiv.org/pdf/2012.12214.pdf).

This backwards compatibility seems like a good goal.

[Johan Commelin]

Hi! I don't think I've heard about factorization algebras before. So they are probably not formalized in Lean.

[Johan Commelin]

Note that all the perfectoid and liquid stuff is in separate libraries that are not very well suited to build upon. We are trying to move stuff into the main library mathlib. But mathlib doesn't have any perfectoid or liquid maths at the moment.

[Jackson Walters]

Hello! These are objects used to formalize aspects of perturbative QFTs first written down by Kevin Costello and Owen Gwilliam in the teens. A book has now been published (https://people.math.umass.edu/~gwilliam/vol1may8.pdf).

[Johan Commelin]

Speaking broadly, what would be the dependencies? Some people have been doing physics related formalization work in Lean. But I don't think QFTs have been done.

[Jackson Walters]

Factorization algebras are quite distinct from perfectoid spaces. They appear in areas at the intersection of geometry, topology, and physics, broadly speaking. The dependencies would be at least include monoidal categories and topological vector spaces. Common examples are typically something like a co-sheaf assigning, like, the Chevalley-Eilenberg complex to open sets. I'm certainly not an expert, and it's been a bit since I was immersed in this, but know someone in the community and thought I should throw it out here.

[Adam Topaz]

We have docs#category_theory.monoidal_category and related constructions

[Johan Commelin]

We also have topological vector space.

[Johan Commelin]

We also have (Grothendieck) topologies. So it seems most ingredients would be there.

[Adam Topaz]

Looking briefly at the link above, it seems to me that a good starting point is to formalize the definition of an operad.

[Jackson Walters]

Assuming the relevant homological algebra and dg vector space language (derived geometry) is there, along with multicategories (a benign generalization of categories), it appears doable to at least define them.

[Kevin Buzzard]

I'm sure the community will be very keen to help if you want to make a little project formalising the definition of an operad in Lean. Here are the instructions on how to create a new Lean project on your computer, and the Zulip helpline is open 24/7. If you get it working you can learn about the PR process and getting it into mathlib. PS Kevin Costello was a former colleague of mine at Imperial.

[Kevin Buzzard]

@Oliver Nash @Eric Wieser the section on operads in the pdf link above, p232 onwards, might interest you. It's not often you see someone talking about associative algebras and Lie algebras at the same time.

[Jackson Walters]

Very cool, that sounds doable. I'll consider it as I move through the natural numbers game tutorial. Me and the faithful assistant here just proved associativity, which was oddly thrilling. Thanks for the pointers, it does sound fun to try to get it working. That's awesome. I knew one of Kevin's students, Brian Williams, a bit, and attended one or two conferences with Costello and co. A prof. at BU, Takashi Kimura, is well versed in operad theory and physics. Universal enveloping algebras are pretty rad.

[Scott Morrison]

I'd love to stuff in this direction in Lean. Long ago I wrote a paper "blob homology" which is in some sense an alternative to factorization algebras --- both more general (more interesting stuff can live on boundaries) and less general (stronger assumptions about duality / rotational invariance). So of course I've kept in mind the past few years how far off that all is... So far my answer has been "very". :-) But it's good to work towards.

[Kevin Buzzard]

Looking back at my conversation with Scholze in Dec 2020, he asked how far off proving things about Ext groups of condensed abelian groups in Lean was, and I said "very". This doesn't mean it's impossible though! It just means that you have to do some work :-) Having ambitious and hard goals is an essential part of moving any theory forward.

[Oliver Nash]

Kevin Buzzard said:

Oliver Nash Eric Wieser the section on operads in the pdf link above, p232 onwards, might interest you. It's not often you see someone talking about associative algebras and Lie algebras at the same time.

Thanks, yes it is interesting though I was a little sad to see this on page 240:
"It might surprise the reader that we neveruse their representation theory or almost any aspects emphasized in textbooks onLie theory. " :cry: