Shapiro's lemma

Stream: Is there code for X?

[Judith Ludwig]

I'm trying to get an overview of what's been formalized in the context of group cohomology. I am under the impression that Shapiro's lemma has not yet been formalized. Is this correct?

[Johan Commelin]

I'm quite sure it's not. Let's ping @Amelia Livingston and @Richard Hill to double check.

[Richard Hill]

I don't think Shapiro's lemma is in Mathlib and I personally haven't formalized it, but @Amelia Livingston would know better than me.

[Kevin Buzzard]

Do we even have induced representations? Which version of representation theory do you need it for? What is the formal statement?

[Judith Ludwig]

Thanks everyone for their reply!
No need for anything specific at this point, just wanted to understand what has been done / or is currently being done.

[Filippo A. E. Nuccio]

Probably we also need to ping @Joël Riou

[Joël Riou]

I have not yet formalized the adjunction between derived categories induced by exact adjoint functors (which would imply an "adjunction" formula for Ext).