Commit 2025-05-29 17:22 afd03ad4

feat(RepresentationTheory/GroupCohomology/Functoriality): the degree 1 part of the inflation-restriction exact sequence (#22653) Given a G-representation A and a normal subgroup S of G, this PR defines the inflation-restriction short complex H¹(G ⧸ S, A^S) ⟶ H¹(G, A) ⟶ H¹(S, A) induced by the natural inclusions S → G, A^S → A and projection G → G / S. We proves it's exact, and that the lefthand map is a monomorphism.