cast "h : n = m" on groupCohmology

Stream: Is there code for X?

[Edison Xie]

Do we want to have this definition? I had problem it when my degree is equal but not definitionally equal (e.g p + 1 and 1 + p)

import Mathlib

universe u

variable {R G : Type u} [CommRing R] [Group G] (A : Rep R G)

open CategoryTheory in
noncomputable def groupCohomology.cast {n m} (h : n = m) :
    groupCohomology A n ≅ groupCohomology A m := h ▸ Iso.refl _

[Joël Riou]

I am not sure we want this. Could you give more context?

[Kevin Buzzard]

The context seems to be: "how do I get an element of $H^{p+1}(G,M)$ when I have an element of $H^{1+p}(G,M)$" I guess?

[Joël Riou]

Then, the question is, how on earth did you get an element in $H^{1+p}$?!
(For example, for the composition of Ext-groups, I did not define a map $Ext^a \times Ext^b \to Ext^{a+b}$ but a map to $Ext^a \times Ext^b \to Ext^c$ whenever a + b = c.)

[Edison Xie]

Screenshot 2026-01-31 at 19.14.21.png

the context here is I'm trying to state the two commutative diagrams ((ii) is where the main issue is) about cup product and chasing the upper half of the diagram gives me p + q + 1 where chasing the other half gives me p + 1 + q

[Joël Riou]

Then, I would strongly recommend following a similar design for the cup product as for docs#CategoryTheory.Abelian.Ext.comp (this is also consistent with the way the API for shifts on categories of complexes is designed, or the API for the total complex of a bicomplex, etc.). Arguably, the target group of the connecting homomorphism could be in degree not just n + 1 but any m such that n + 1 = m (see also docs#DerivedCategory.HomologySequence.δ).

[Edison Xie]

that's a great advice, thanks!