Sarah El Boustany

Stream: new members

[Sarah El Boustany]

Hi everyone!
I am currently doing a PhD in Galway on Hochschild cohomology and some of my work is going to involve formalization. I am still very much a beginner, but I am looking forward to contributing to Lean!

[Ruben Van de Velde]

Welcome!

[Kevin Buzzard]

Step 1 would be to formalize the definition of Hochschild cohomology! We have group cohomology plus evidence that it works, so I should think that this is a possible and interesting project.

[Sarah El Boustany]

I started looking into group cohomology as that is a very important aspect of the project that I'm a part of (COGENT project). Are there any other things that I should look into so that I can know what I would be building off of?

[Joël Riou]

We have reasonable good API for modules over commutative rings, tensor products, etc, but the situation may not be as good/developed in the case of non commutative algebras and bimodules, which appear in Hochschild (co)homology. Depending on the specific results you want to formalize, you may have to contribute foundational definitions/design for (bi)modules over non-commutative rings.

[Sarah El Boustany]

Oh, that's good to know!

[Ruben Van de Velde]

Which would be welcome, as I understand it, fwiw