Functoriality of group cohomology

Given a commutative ring k, a group homomorphism f : G →* H, a k-linear H-representation A, a k-linear G-representation B, and a representation morphism Res(f)(A) ⟶ B, we get a cochain map inhomogeneousCochains A ⟶ inhomogeneousCochains B and hence maps on cohomology Hⁿ(H, A) ⟶ Hⁿ(G, B). We also provide extra API for these maps in degrees 0, 1, 2.

Main definitions

• groupCohomology.cochainsMap f φ is the map inhomogeneousCochains A ⟶ inhomogeneousCochains B induced by a group homomorphism f : G →* H and a representation morphism φ : Res(f)(A) ⟶ B.
• groupCohomology.map f φ n is the map Hⁿ(H, A) ⟶ Hⁿ(G, B) induced by a group homomorphism f : G →* H and a representation morphism φ : Res(f)(A) ⟶ B.
• groupCohomology.H1InfRes A S is the short complex H¹(G ⧸ S, A^S) ⟶ H¹(G, A) ⟶ H¹(S, A) for a normal subgroup S ≤ G and a G-representation A.

theorem groupCohomology.congr {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} {f₁ f₂ : G →* H} (h : f₁ = f₂) {φ : (Action.res (ModuleCat k) f₁).obj A ⟶ B} {T : Type u_1} (F : (f : G →* H) → ((Action.res (ModuleCat k) f).obj A ⟶ B) → T) : F f₁ φ = F f₂ (h ▸ φ)

noncomputable def groupCohomology.cochainsMap {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : inhomogeneousCochains A ⟶ inhomogeneousCochains B

Given a group homomorphism f : G →* H and a representation morphism φ : Res(f)(A) ⟶ B, this is the chain map sending x : Hⁿ → A to (g : Gⁿ) ↦ φ (x (f ∘ g)).

theorem groupCohomology.cochainsMap_f {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (i : ℕ) : (cochainsMap f φ).f i = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (LinearMap.funLeft k ↑A.V fun (x : Fin i → G) => ⇑f ∘ x)) (ModuleCat.ofHom ((ModuleCat.Hom.hom φ.hom).compLeft (Fin i → G)))

theorem groupCohomology.cochainsMap_f_hom {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (i : ℕ) : ModuleCat.Hom.hom ((cochainsMap f φ).f i) = (ModuleCat.Hom.hom φ.hom).compLeft (Fin i → G) ∘ₗ LinearMap.funLeft k ↑A.V fun (x : Fin i → G) => ⇑f ∘ x

@[simp]

theorem groupCohomology.cochainsMap_id {k H : Type u} [CommRing k] [Group H] {A : Rep k H} : cochainsMap (MonoidHom.id H) (CategoryTheory.CategoryStruct.id A) = CategoryTheory.CategoryStruct.id (inhomogeneousCochains A)

@[simp]

theorem groupCohomology.cochainsMap_id_f_hom_eq_compLeft {k G : Type u} [CommRing k] [Group G] {A B : Rep k G} (f : A ⟶ B) (i : ℕ) : ModuleCat.Hom.hom ((cochainsMap (MonoidHom.id G) f).f i) = (ModuleCat.Hom.hom f.hom).compLeft (Fin i → G)

@[deprecated groupCohomology.cochainsMap_id_f_hom_eq_compLeft (since := "2025-06-11")]

theorem groupCohomology.cochainsMap_id_f_eq_compLeft {k G : Type u} [CommRing k] [Group G] {A B : Rep k G} (f : A ⟶ B) (i : ℕ) : ModuleCat.Hom.hom ((cochainsMap (MonoidHom.id G) f).f i) = (ModuleCat.Hom.hom f.hom).compLeft (Fin i → G)

Alias of groupCohomology.cochainsMap_id_f_hom_eq_compLeft.

theorem groupCohomology.cochainsMap_comp {k : Type u} [CommRing k] {G H K : Type u} [Group G] [Group H] [Group K] {A : Rep k K} {B : Rep k H} {C : Rep k G} (f : H →* K) (g : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (ψ : (Action.res (ModuleCat k) g).obj B ⟶ C) : cochainsMap (f.comp g) (CategoryTheory.CategoryStruct.comp ((Action.res (ModuleCat k) g).map φ) ψ) = CategoryTheory.CategoryStruct.comp (cochainsMap f φ) (cochainsMap g ψ)

theorem groupCohomology.cochainsMap_comp_assoc {k : Type u} [CommRing k] {G H K : Type u} [Group G] [Group H] [Group K] {A : Rep k K} {B : Rep k H} {C : Rep k G} (f : H →* K) (g : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (ψ : (Action.res (ModuleCat k) g).obj B ⟶ C) {Z : CochainComplex (ModuleCat k) ℕ} (h : inhomogeneousCochains C ⟶ Z) : CategoryTheory.CategoryStruct.comp (cochainsMap (f.comp g) (CategoryTheory.CategoryStruct.comp ((Action.res (ModuleCat k) g).map φ) ψ)) h = CategoryTheory.CategoryStruct.comp (cochainsMap f φ) (CategoryTheory.CategoryStruct.comp (cochainsMap g ψ) h)

theorem groupCohomology.cochainsMap_id_comp {k G : Type u} [CommRing k] [Group G] {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C) : cochainsMap (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ) = CategoryTheory.CategoryStruct.comp (cochainsMap (MonoidHom.id G) φ) (cochainsMap (MonoidHom.id G) ψ)

theorem groupCohomology.cochainsMap_id_comp_assoc {k G : Type u} [CommRing k] [Group G] {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C) {Z : CochainComplex (ModuleCat k) ℕ} (h : inhomogeneousCochains C ⟶ Z) : CategoryTheory.CategoryStruct.comp (cochainsMap (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ)) h = CategoryTheory.CategoryStruct.comp (cochainsMap (MonoidHom.id G) φ) (CategoryTheory.CategoryStruct.comp (cochainsMap (MonoidHom.id G) ψ) h)

@[simp]

theorem groupCohomology.cochainsMap_zero {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) : cochainsMap f 0 = 0

theorem groupCohomology.cochainsMap_f_map_mono {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (hf : Function.Surjective ⇑f) [CategoryTheory.Mono φ] (i : ℕ) : CategoryTheory.Mono ((cochainsMap f φ).f i)

instance groupCohomology.cochainsMap_id_f_map_mono {k G : Type u} [CommRing k] [Group G] {A B : Rep k G} (φ : A ⟶ B) [CategoryTheory.Mono φ] (i : ℕ) : CategoryTheory.Mono ((cochainsMap (MonoidHom.id G) φ).f i)

theorem groupCohomology.cochainsMap_f_map_epi {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (hf : Function.Injective ⇑f) [CategoryTheory.Epi φ] (i : ℕ) : CategoryTheory.Epi ((cochainsMap f φ).f i)

instance groupCohomology.cochainsMap_id_f_map_epi {k G : Type u} [CommRing k] [Group G] {A B : Rep k G} (φ : A ⟶ B) [CategoryTheory.Epi φ] (i : ℕ) : CategoryTheory.Epi ((cochainsMap (MonoidHom.id G) φ).f i)

@[reducible, inline]

noncomputable abbrev groupCohomology.cocyclesMap {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (n : ℕ) : cocycles A n ⟶ cocycles B n

Given a group homomorphism f : G →* H and a representation morphism φ : Res(f)(A) ⟶ B, this is the induced map Zⁿ(H, A) ⟶ Zⁿ(G, B) sending x : Hⁿ → A to (g : Gⁿ) ↦ φ (x (f ∘ g)).

@[simp]

theorem groupCohomology.cocyclesMap_id {k G : Type u} [CommRing k] [Group G] {B : Rep k G} (n : ℕ) : cocyclesMap (MonoidHom.id G) (CategoryTheory.CategoryStruct.id B) n = CategoryTheory.CategoryStruct.id (cocycles B n)

theorem groupCohomology.cocyclesMap_comp {k : Type u} [CommRing k] {G H K : Type u} [Group G] [Group H] [Group K] {A : Rep k K} {B : Rep k H} {C : Rep k G} (f : H →* K) (g : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (ψ : (Action.res (ModuleCat k) g).obj B ⟶ C) (n : ℕ) : cocyclesMap (f.comp g) (CategoryTheory.CategoryStruct.comp ((Action.res (ModuleCat k) g).map φ) ψ) n = CategoryTheory.CategoryStruct.comp (cocyclesMap f φ n) (cocyclesMap g ψ n)

theorem groupCohomology.cocyclesMap_comp_assoc {k : Type u} [CommRing k] {G H K : Type u} [Group G] [Group H] [Group K] {A : Rep k K} {B : Rep k H} {C : Rep k G} (f : H →* K) (g : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (ψ : (Action.res (ModuleCat k) g).obj B ⟶ C) (n : ℕ) {Z : ModuleCat k} (h : cocycles C n ⟶ Z) : CategoryTheory.CategoryStruct.comp (cocyclesMap (f.comp g) (CategoryTheory.CategoryStruct.comp ((Action.res (ModuleCat k) g).map φ) ψ) n) h = CategoryTheory.CategoryStruct.comp (cocyclesMap f φ n) (CategoryTheory.CategoryStruct.comp (cocyclesMap g ψ n) h)

theorem groupCohomology.cocyclesMap_id_comp {k G : Type u} [CommRing k] [Group G] {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C) (n : ℕ) : cocyclesMap (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ) n = CategoryTheory.CategoryStruct.comp (cocyclesMap (MonoidHom.id G) φ n) (cocyclesMap (MonoidHom.id G) ψ n)

theorem groupCohomology.cocyclesMap_id_comp_assoc {k G : Type u} [CommRing k] [Group G] {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C) (n : ℕ) {Z : ModuleCat k} (h : cocycles C n ⟶ Z) : CategoryTheory.CategoryStruct.comp (cocyclesMap (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ) n) h = CategoryTheory.CategoryStruct.comp (cocyclesMap (MonoidHom.id G) φ n) (CategoryTheory.CategoryStruct.comp (cocyclesMap (MonoidHom.id G) ψ n) h)

@[reducible, inline]

noncomputable abbrev groupCohomology.map {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (n : ℕ) : groupCohomology A n ⟶ groupCohomology B n

Given a group homomorphism f : G →* H and a representation morphism φ : Res(f)(A) ⟶ B, this is the induced map Hⁿ(H, A) ⟶ Hⁿ(G, B) sending x : Hⁿ → A to (g : Gⁿ) ↦ φ (x (f ∘ g)).

theorem groupCohomology.π_map {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (n : ℕ) : CategoryTheory.CategoryStruct.comp (π A n) (map f φ n) = CategoryTheory.CategoryStruct.comp (cocyclesMap f φ n) (π B n)

theorem groupCohomology.π_map_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (n : ℕ) {Z : ModuleCat k} (h : groupCohomology B n ⟶ Z) : CategoryTheory.CategoryStruct.comp (π A n) (CategoryTheory.CategoryStruct.comp (map f φ n) h) = CategoryTheory.CategoryStruct.comp (cocyclesMap f φ n) (CategoryTheory.CategoryStruct.comp (π B n) h)

theorem groupCohomology.π_map_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (n : ℕ) (x : CategoryTheory.ToType (cocycles A n)) : (CategoryTheory.ConcreteCategory.hom (map f φ n)) ((CategoryTheory.ConcreteCategory.hom (π A n)) x) = (CategoryTheory.ConcreteCategory.hom (π B n)) ((CategoryTheory.ConcreteCategory.hom (cocyclesMap f φ n)) x)

@[simp]

theorem groupCohomology.map_id {k G : Type u} [CommRing k] [Group G] {B : Rep k G} (n : ℕ) : map (MonoidHom.id G) (CategoryTheory.CategoryStruct.id B) n = CategoryTheory.CategoryStruct.id (groupCohomology B n)

theorem groupCohomology.map_comp {k : Type u} [CommRing k] {G H K : Type u} [Group G] [Group H] [Group K] {A : Rep k K} {B : Rep k H} {C : Rep k G} (f : H →* K) (g : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (ψ : (Action.res (ModuleCat k) g).obj B ⟶ C) (n : ℕ) : map (f.comp g) (CategoryTheory.CategoryStruct.comp ((Action.res (ModuleCat k) g).map φ) ψ) n = CategoryTheory.CategoryStruct.comp (map f φ n) (map g ψ n)

theorem groupCohomology.map_comp_assoc {k : Type u} [CommRing k] {G H K : Type u} [Group G] [Group H] [Group K] {A : Rep k K} {B : Rep k H} {C : Rep k G} (f : H →* K) (g : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (ψ : (Action.res (ModuleCat k) g).obj B ⟶ C) (n : ℕ) {Z : ModuleCat k} (h : groupCohomology C n ⟶ Z) : CategoryTheory.CategoryStruct.comp (map (f.comp g) (CategoryTheory.CategoryStruct.comp ((Action.res (ModuleCat k) g).map φ) ψ) n) h = CategoryTheory.CategoryStruct.comp (map f φ n) (CategoryTheory.CategoryStruct.comp (map g ψ n) h)

theorem groupCohomology.map_id_comp {k G : Type u} [CommRing k] [Group G] {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C) (n : ℕ) : map (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ) n = CategoryTheory.CategoryStruct.comp (map (MonoidHom.id G) φ n) (map (MonoidHom.id G) ψ n)

theorem groupCohomology.map_id_comp_assoc {k G : Type u} [CommRing k] [Group G] {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C) (n : ℕ) {Z : ModuleCat k} (h : groupCohomology C n ⟶ Z) : CategoryTheory.CategoryStruct.comp (map (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ) n) h = CategoryTheory.CategoryStruct.comp (map (MonoidHom.id G) φ n) (CategoryTheory.CategoryStruct.comp (map (MonoidHom.id G) ψ n) h)

@[reducible, inline]

noncomputable abbrev groupCohomology.cochainsMap₁ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : ModuleCat.of k (H → ↑A.V) ⟶ ModuleCat.of k (G → ↑B.V)

Given a group homomorphism f : G →* H and a representation morphism φ : Res(f)(A) ⟶ B, this is the induced map sending x : H → A to (g : G) ↦ φ (x (f g)).

@[deprecated groupCohomology.cochainsMap₁ (since := "2025-07-12")]

def groupCohomology.f₁ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : ModuleCat.of k (H → ↑A.V) ⟶ ModuleCat.of k (G → ↑B.V)

Alias of groupCohomology.cochainsMap₁.

---

Given a group homomorphism f : G →* H and a representation morphism φ : Res(f)(A) ⟶ B, this is the induced map sending x : H → A to (g : G) ↦ φ (x (f g)).

@[deprecated groupCohomology.f₁ (since := "2025-06-25")]

def groupCohomology.fOne {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : ModuleCat.of k (H → ↑A.V) ⟶ ModuleCat.of k (G → ↑B.V)

Alias of groupCohomology.cochainsMap₁.

---

Alias of groupCohomology.cochainsMap₁.

---

Given a group homomorphism f : G →* H and a representation morphism φ : Res(f)(A) ⟶ B, this is the induced map sending x : H → A to (g : G) ↦ φ (x (f g)).

@[reducible, inline]

noncomputable abbrev groupCohomology.cochainsMap₂ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : ModuleCat.of k (H × H → ↑A.V) ⟶ ModuleCat.of k (G × G → ↑B.V)

Given a group homomorphism f : G →* H and a representation morphism φ : Res(f)(A) ⟶ B, this is the induced map sending x : H × H → A to (g₁, g₂ : G × G) ↦ φ (x (f g₁, f g₂)).

@[deprecated groupCohomology.cochainsMap₂ (since := "2025-07-12")]

def groupCohomology.f₂ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : ModuleCat.of k (H × H → ↑A.V) ⟶ ModuleCat.of k (G × G → ↑B.V)

Alias of groupCohomology.cochainsMap₂.

---

Given a group homomorphism f : G →* H and a representation morphism φ : Res(f)(A) ⟶ B, this is the induced map sending x : H × H → A to (g₁, g₂ : G × G) ↦ φ (x (f g₁, f g₂)).

@[deprecated groupCohomology.f₂ (since := "2025-06-25")]

def groupCohomology.fTwo {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : ModuleCat.of k (H × H → ↑A.V) ⟶ ModuleCat.of k (G × G → ↑B.V)

Alias of groupCohomology.cochainsMap₂.

---

Alias of groupCohomology.cochainsMap₂.

---

Given a group homomorphism f : G →* H and a representation morphism φ : Res(f)(A) ⟶ B, this is the induced map sending x : H × H → A to (g₁, g₂ : G × G) ↦ φ (x (f g₁, f g₂)).

@[reducible, inline]

noncomputable abbrev groupCohomology.cochainsMap₃ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : ModuleCat.of k (H × H × H → ↑A.V) ⟶ ModuleCat.of k (G × G × G → ↑B.V)

Given a group homomorphism f : G →* H and a representation morphism φ : Res(f)(A) ⟶ B, this is the induced map sending x : H × H × H → A to (g₁, g₂, g₃ : G × G × G) ↦ φ (x (f g₁, f g₂, f g₃)).

@[deprecated groupCohomology.cochainsMap₃ (since := "2025-07-12")]

def groupCohomology.f₃ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : ModuleCat.of k (H × H × H → ↑A.V) ⟶ ModuleCat.of k (G × G × G → ↑B.V)

Alias of groupCohomology.cochainsMap₃.

---

Given a group homomorphism f : G →* H and a representation morphism φ : Res(f)(A) ⟶ B, this is the induced map sending x : H × H × H → A to (g₁, g₂, g₃ : G × G × G) ↦ φ (x (f g₁, f g₂, f g₃)).

@[deprecated groupCohomology.f₃ (since := "2025-06-25")]

def groupCohomology.fThree {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : ModuleCat.of k (H × H × H → ↑A.V) ⟶ ModuleCat.of k (G × G × G → ↑B.V)

Alias of groupCohomology.cochainsMap₃.

---

Alias of groupCohomology.cochainsMap₃.

---

Given a group homomorphism f : G →* H and a representation morphism φ : Res(f)(A) ⟶ B, this is the induced map sending x : H × H × H → A to (g₁, g₂, g₃ : G × G × G) ↦ φ (x (f g₁, f g₂, f g₃)).

@[simp]

theorem groupCohomology.cochainsMap_f_0_comp_cochainsIso₀ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 0) (cochainsIso₀ B).hom = CategoryTheory.CategoryStruct.comp (cochainsIso₀ A).hom φ.hom

@[simp]

theorem groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) {Z : ModuleCat k} (h : B.V ⟶ Z) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 0) (CategoryTheory.CategoryStruct.comp (cochainsIso₀ B).hom h) = CategoryTheory.CategoryStruct.comp (cochainsIso₀ A).hom (CategoryTheory.CategoryStruct.comp φ.hom h)

@[simp]

theorem groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (x : CategoryTheory.ToType ((inhomogeneousCochains A).X 0)) : (CategoryTheory.ConcreteCategory.hom (cochainsIso₀ B).hom) ((CategoryTheory.ConcreteCategory.hom ((cochainsMap f φ).f 0)) x) = (CategoryTheory.ConcreteCategory.hom φ.hom) ((CategoryTheory.ConcreteCategory.hom (cochainsIso₀ A).hom) x)

@[deprecated groupCohomology.cochainsMap_f_0_comp_cochainsIso₀ (since := "2025-06-25")]

theorem groupCohomology.cochainsMap_f_0_comp_zeroCochainsIso {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 0) (cochainsIso₀ B).hom = CategoryTheory.CategoryStruct.comp (cochainsIso₀ A).hom φ.hom

Alias of groupCohomology.cochainsMap_f_0_comp_cochainsIso₀.

@[deprecated groupCohomology.cochainsMap_f_0_comp_cochainsIso₀ (since := "2025-05-09")]

theorem groupCohomology.cochainsMap_f_0_comp_zeroCochainsLequiv {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 0) (cochainsIso₀ B).hom = CategoryTheory.CategoryStruct.comp (cochainsIso₀ A).hom φ.hom

Alias of groupCohomology.cochainsMap_f_0_comp_cochainsIso₀.

@[simp]

theorem groupCohomology.cochainsMap_f_1_comp_cochainsIso₁ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 1) (cochainsIso₁ B).hom = CategoryTheory.CategoryStruct.comp (cochainsIso₁ A).hom (cochainsMap₁ f φ)

@[simp]

theorem groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) {Z : ModuleCat k} (h : ModuleCat.of k (G → ↑B.V) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 1) (CategoryTheory.CategoryStruct.comp (cochainsIso₁ B).hom h) = CategoryTheory.CategoryStruct.comp (cochainsIso₁ A).hom (CategoryTheory.CategoryStruct.comp (cochainsMap₁ f φ) h)

@[simp]

theorem groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (x : CategoryTheory.ToType ((inhomogeneousCochains A).X 1)) : (CategoryTheory.ConcreteCategory.hom (cochainsIso₁ B).hom) ((CategoryTheory.ConcreteCategory.hom ((cochainsMap f φ).f 1)) x) = ((ModuleCat.Hom.hom φ.hom).compLeft G) ((LinearMap.funLeft k ↑A.V ⇑f) ((CategoryTheory.ConcreteCategory.hom (cochainsIso₁ A).hom) x))

@[deprecated groupCohomology.cochainsMap_f_1_comp_cochainsIso₁ (since := "2025-06-25")]

theorem groupCohomology.cochainsMap_f_1_comp_oneCochainsIso {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 1) (cochainsIso₁ B).hom = CategoryTheory.CategoryStruct.comp (cochainsIso₁ A).hom (cochainsMap₁ f φ)

Alias of groupCohomology.cochainsMap_f_1_comp_cochainsIso₁.

@[deprecated groupCohomology.cochainsMap_f_1_comp_oneCochainsIso (since := "2025-05-09")]

theorem groupCohomology.cochainsMap_f_1_comp_oneCochainsLequiv {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 1) (cochainsIso₁ B).hom = CategoryTheory.CategoryStruct.comp (cochainsIso₁ A).hom (cochainsMap₁ f φ)

Alias of groupCohomology.cochainsMap_f_1_comp_cochainsIso₁.

---

Alias of groupCohomology.cochainsMap_f_1_comp_cochainsIso₁.

@[simp]

theorem groupCohomology.cochainsMap_f_2_comp_cochainsIso₂ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 2) (cochainsIso₂ B).hom = CategoryTheory.CategoryStruct.comp (cochainsIso₂ A).hom (cochainsMap₂ f φ)

@[simp]

theorem groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) {Z : ModuleCat k} (h : ModuleCat.of k (G × G → ↑B.V) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 2) (CategoryTheory.CategoryStruct.comp (cochainsIso₂ B).hom h) = CategoryTheory.CategoryStruct.comp (cochainsIso₂ A).hom (CategoryTheory.CategoryStruct.comp (cochainsMap₂ f φ) h)

@[simp]

theorem groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (x : CategoryTheory.ToType ((inhomogeneousCochains A).X 2)) : (CategoryTheory.ConcreteCategory.hom (cochainsIso₂ B).hom) ((CategoryTheory.ConcreteCategory.hom ((cochainsMap f φ).f 2)) x) = ((ModuleCat.Hom.hom φ.hom).compLeft (G × G)) ((LinearMap.funLeft k (↑A.V) (Prod.map ⇑f ⇑f)) ((CategoryTheory.ConcreteCategory.hom (cochainsIso₂ A).hom) x))

@[deprecated groupCohomology.cochainsMap_f_2_comp_cochainsIso₂ (since := "2025-06-25")]

theorem groupCohomology.cochainsMap_f_2_comp_twoCochainsIso {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 2) (cochainsIso₂ B).hom = CategoryTheory.CategoryStruct.comp (cochainsIso₂ A).hom (cochainsMap₂ f φ)

Alias of groupCohomology.cochainsMap_f_2_comp_cochainsIso₂.

@[deprecated groupCohomology.cochainsMap_f_2_comp_twoCochainsIso (since := "2025-05-09")]

theorem groupCohomology.cochainsMap_f_2_comp_twoCochainsLequiv {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 2) (cochainsIso₂ B).hom = CategoryTheory.CategoryStruct.comp (cochainsIso₂ A).hom (cochainsMap₂ f φ)

Alias of groupCohomology.cochainsMap_f_2_comp_cochainsIso₂.

---

Alias of groupCohomology.cochainsMap_f_2_comp_cochainsIso₂.

@[simp]

theorem groupCohomology.cochainsMap_f_3_comp_cochainsIso₃ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 3) (cochainsIso₃ B).hom = CategoryTheory.CategoryStruct.comp (cochainsIso₃ A).hom (cochainsMap₃ f φ)

@[simp]

theorem groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) {Z : ModuleCat k} (h : ModuleCat.of k (G × G × G → ↑B.V) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 3) (CategoryTheory.CategoryStruct.comp (cochainsIso₃ B).hom h) = CategoryTheory.CategoryStruct.comp (cochainsIso₃ A).hom (CategoryTheory.CategoryStruct.comp (cochainsMap₃ f φ) h)

@[simp]

theorem groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (x : CategoryTheory.ToType ((inhomogeneousCochains A).X 3)) : (CategoryTheory.ConcreteCategory.hom (cochainsIso₃ B).hom) ((CategoryTheory.ConcreteCategory.hom ((cochainsMap f φ).f 3)) x) = ((ModuleCat.Hom.hom φ.hom).compLeft (G × G × G)) ((LinearMap.funLeft k (↑A.V) (Prod.map (⇑f) (Prod.map ⇑f ⇑f))) ((CategoryTheory.ConcreteCategory.hom (cochainsIso₃ A).hom) x))

@[deprecated groupCohomology.cochainsMap_f_3_comp_cochainsIso₃ (since := "2025-06-25")]

theorem groupCohomology.cochainsMap_f_3_comp_threeCochainsIso {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 3) (cochainsIso₃ B).hom = CategoryTheory.CategoryStruct.comp (cochainsIso₃ A).hom (cochainsMap₃ f φ)

Alias of groupCohomology.cochainsMap_f_3_comp_cochainsIso₃.

@[deprecated groupCohomology.cochainsMap_f_3_comp_threeCochainsIso (since := "2025-05-09")]

theorem groupCohomology.cochainsMap_f_3_comp_threeCochainsLequiv {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 3) (cochainsIso₃ B).hom = CategoryTheory.CategoryStruct.comp (cochainsIso₃ A).hom (cochainsMap₃ f φ)

Alias of groupCohomology.cochainsMap_f_3_comp_cochainsIso₃.

---

Alias of groupCohomology.cochainsMap_f_3_comp_cochainsIso₃.

@[deprecated groupCohomology.map (since := "2025-06-09")]

def groupCohomology.H0Map {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (n : ℕ) : groupCohomology A n ⟶ groupCohomology B n

Given a group homomorphism f : G →* H and a representation morphism φ : Res(f)(A) ⟶ B, this is induced map Aᴴ ⟶ Bᴳ.

@[deprecated groupCohomology.map_id (since := "2025-06-09")]

theorem groupCohomology.H0Map_id {k G : Type u} [CommRing k] [Group G] {B : Rep k G} (n : ℕ) : map (MonoidHom.id G) (CategoryTheory.CategoryStruct.id B) n = CategoryTheory.CategoryStruct.id (groupCohomology B n)

Alias of groupCohomology.map_id.

@[deprecated groupCohomology.map_comp (since := "2025-06-09")]

theorem groupCohomology.H0Map_comp {k : Type u} [CommRing k] {G H K : Type u} [Group G] [Group H] [Group K] {A : Rep k K} {B : Rep k H} {C : Rep k G} (f : H →* K) (g : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (ψ : (Action.res (ModuleCat k) g).obj B ⟶ C) (n : ℕ) : map (f.comp g) (CategoryTheory.CategoryStruct.comp ((Action.res (ModuleCat k) g).map φ) ψ) n = CategoryTheory.CategoryStruct.comp (map f φ n) (map g ψ n)

Alias of groupCohomology.map_comp.

@[deprecated groupCohomology.map_id_comp (since := "2025-06-09")]

theorem groupCohomology.H0Map_id_comp {k G : Type u} [CommRing k] [Group G] {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C) (n : ℕ) : map (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ) n = CategoryTheory.CategoryStruct.comp (map (MonoidHom.id G) φ n) (map (MonoidHom.id G) ψ n)

Alias of groupCohomology.map_id_comp.

@[simp]

theorem groupCohomology.map_H0Iso_hom_f {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp (map f φ 0) (CategoryTheory.CategoryStruct.comp (H0Iso B).hom (shortComplexH0 B).f) = CategoryTheory.CategoryStruct.comp (H0Iso A).hom (CategoryTheory.CategoryStruct.comp (shortComplexH0 A).f φ.hom)

@[simp]

theorem groupCohomology.map_H0Iso_hom_f_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) {Z : ModuleCat k} (h : (shortComplexH0 B).X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (map f φ 0) (CategoryTheory.CategoryStruct.comp (H0Iso B).hom (CategoryTheory.CategoryStruct.comp (shortComplexH0 B).f h)) = CategoryTheory.CategoryStruct.comp (H0Iso A).hom (CategoryTheory.CategoryStruct.comp (shortComplexH0 A).f (CategoryTheory.CategoryStruct.comp φ.hom h))

@[simp]

theorem groupCohomology.map_H0Iso_hom_f_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (x : CategoryTheory.ToType (groupCohomology A 0)) : (CategoryTheory.ConcreteCategory.hom (shortComplexH0 B).f) ((CategoryTheory.ConcreteCategory.hom (H0Iso B).hom) ((CategoryTheory.ConcreteCategory.hom (map f φ 0)) x)) = (CategoryTheory.CategoryStruct.comp (H0Iso A).hom (CategoryTheory.CategoryStruct.comp (shortComplexH0 A).f φ.hom)) x

@[deprecated groupCohomology.map_H0Iso_hom_f (since := "2025-06-09")]

theorem groupCohomology.H0Map_comp_f {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp (map f φ 0) (CategoryTheory.CategoryStruct.comp (H0Iso B).hom (shortComplexH0 B).f) = CategoryTheory.CategoryStruct.comp (H0Iso A).hom (CategoryTheory.CategoryStruct.comp (shortComplexH0 A).f φ.hom)

Alias of groupCohomology.map_H0Iso_hom_f.

@[simp]

theorem groupCohomology.map_id_comp_H0Iso_hom {k G : Type u} [CommRing k] [Group G] {A B : Rep k G} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp (map (MonoidHom.id G) f 0) (H0Iso B).hom = CategoryTheory.CategoryStruct.comp (H0Iso A).hom ((Rep.invariantsFunctor k G).map f)

@[simp]

theorem groupCohomology.map_id_comp_H0Iso_hom_assoc {k G : Type u} [CommRing k] [Group G] {A B : Rep k G} (f : A ⟶ B) {Z : ModuleCat k} (h : ModuleCat.of k ↥B.ρ.invariants ⟶ Z) : CategoryTheory.CategoryStruct.comp (map (MonoidHom.id G) f 0) (CategoryTheory.CategoryStruct.comp (H0Iso B).hom h) = CategoryTheory.CategoryStruct.comp (H0Iso A).hom (CategoryTheory.CategoryStruct.comp ((Rep.invariantsFunctor k G).map f) h)

@[simp]

theorem groupCohomology.map_id_comp_H0Iso_hom_apply {k G : Type u} [CommRing k] [Group G] {A B : Rep k G} (f : A ⟶ B) (x : CategoryTheory.ToType (groupCohomology A 0)) : (CategoryTheory.ConcreteCategory.hom (H0Iso B).hom) ((CategoryTheory.ConcreteCategory.hom (map (MonoidHom.id G) f 0)) x) = (CategoryTheory.CategoryStruct.comp (H0Iso A).hom ((Rep.invariantsFunctor k G).map f)) x

@[deprecated groupCohomology.map_id_comp_H0Iso_hom (since := "2025-06-09")]

theorem groupCohomology.H0Map_id_eq_invariantsFunctor_map {k G : Type u} [CommRing k] [Group G] {A B : Rep k G} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp (map (MonoidHom.id G) f 0) (H0Iso B).hom = CategoryTheory.CategoryStruct.comp (H0Iso A).hom ((Rep.invariantsFunctor k G).map f)

Alias of groupCohomology.map_id_comp_H0Iso_hom.

instance groupCohomology.mono_map_0_of_mono {k G : Type u} [CommRing k] [Group G] {A B : Rep k G} (f : A ⟶ B) [CategoryTheory.Mono f] : CategoryTheory.Mono (map (MonoidHom.id G) f 0)

@[deprecated groupCohomology.mono_map_0_of_mono (since := "2025-06-09")]

theorem groupCohomology.mono_H0Map_of_mono {k G : Type u} [CommRing k] [Group G] {A B : Rep k G} (f : A ⟶ B) [CategoryTheory.Mono f] : CategoryTheory.Mono (map (MonoidHom.id G) f 0)

Alias of groupCohomology.mono_map_0_of_mono.

theorem groupCohomology.cocyclesMap_cocyclesIso₀_hom_f {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp (cocyclesMap f φ 0) (CategoryTheory.CategoryStruct.comp (cocyclesIso₀ B).hom (shortComplexH0 B).f) = CategoryTheory.CategoryStruct.comp (cocyclesIso₀ A).hom (CategoryTheory.CategoryStruct.comp (shortComplexH0 A).f φ.hom)

theorem groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) {Z : ModuleCat k} (h : (shortComplexH0 B).X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (cocyclesMap f φ 0) (CategoryTheory.CategoryStruct.comp (cocyclesIso₀ B).hom (CategoryTheory.CategoryStruct.comp (shortComplexH0 B).f h)) = CategoryTheory.CategoryStruct.comp (cocyclesIso₀ A).hom (CategoryTheory.CategoryStruct.comp (shortComplexH0 A).f (CategoryTheory.CategoryStruct.comp φ.hom h))

theorem groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (x : CategoryTheory.ToType (cocycles A 0)) : (CategoryTheory.CategoryStruct.comp (iCocycles B 0) (cochainsIso₀ B).hom) ((CategoryTheory.ConcreteCategory.hom (cocyclesMap f φ 0)) x) = (CategoryTheory.CategoryStruct.comp (iCocycles A 0) (CategoryTheory.CategoryStruct.comp (cochainsIso₀ A).hom φ.hom)) x

@[deprecated groupCohomology.cocyclesMap_cocyclesIso₀_hom_f (since := "2025-07-02")]

theorem groupCohomology.cocyclesMap_zeroIsoCocycles_hom_f {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp (cocyclesMap f φ 0) (CategoryTheory.CategoryStruct.comp (cocyclesIso₀ B).hom (shortComplexH0 B).f) = CategoryTheory.CategoryStruct.comp (cocyclesIso₀ A).hom (CategoryTheory.CategoryStruct.comp (shortComplexH0 A).f φ.hom)

Alias of groupCohomology.cocyclesMap_cocyclesIso₀_hom_f.

@[deprecated groupCohomology.cocyclesMap_zeroIsoCocycles_hom_f (since := "2025-06-12")]

theorem groupCohomology.cocyclesMap_comp_isoZeroCocycles_hom {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp (cocyclesMap f φ 0) (CategoryTheory.CategoryStruct.comp (cocyclesIso₀ B).hom (shortComplexH0 B).f) = CategoryTheory.CategoryStruct.comp (cocyclesIso₀ A).hom (CategoryTheory.CategoryStruct.comp (shortComplexH0 A).f φ.hom)

Alias of groupCohomology.cocyclesMap_cocyclesIso₀_hom_f.

---

Alias of groupCohomology.cocyclesMap_cocyclesIso₀_hom_f.

noncomputable def groupCohomology.mapShortComplexH1 {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : shortComplexH1 A ⟶ shortComplexH1 B

Given a group homomorphism f : G →* H and a representation morphism φ : Res(f)(A) ⟶ B, this is the induced map from the short complex A --d₀₁--> Fun(H, A) --d₁₂--> Fun(H × H, A) to B --d₀₁--> Fun(G, B) --d₁₂--> Fun(G × G, B).

@[simp]

theorem groupCohomology.mapShortComplexH1_τ₂ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : (mapShortComplexH1 f φ).τ₂ = cochainsMap₁ f φ

@[simp]

theorem groupCohomology.mapShortComplexH1_τ₁ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : (mapShortComplexH1 f φ).τ₁ = φ.hom

@[simp]

theorem groupCohomology.mapShortComplexH1_τ₃ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : (mapShortComplexH1 f φ).τ₃ = cochainsMap₂ f φ

@[simp]

theorem groupCohomology.mapShortComplexH1_zero {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) : mapShortComplexH1 f 0 = 0

@[simp]

theorem groupCohomology.mapShortComplexH1_id {k H : Type u} [CommRing k] [Group H] {A : Rep k H} : mapShortComplexH1 (MonoidHom.id H) (CategoryTheory.CategoryStruct.id A) = CategoryTheory.CategoryStruct.id (shortComplexH1 A)

theorem groupCohomology.mapShortComplexH1_comp {k : Type u} [CommRing k] {G H K : Type u} [Group G] [Group H] [Group K] {A : Rep k K} {B : Rep k H} {C : Rep k G} (f : H →* K) (g : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (ψ : (Action.res (ModuleCat k) g).obj B ⟶ C) : mapShortComplexH1 (f.comp g) (CategoryTheory.CategoryStruct.comp ((Action.res (ModuleCat k) g).map φ) ψ) = CategoryTheory.CategoryStruct.comp (mapShortComplexH1 f φ) (mapShortComplexH1 g ψ)

theorem groupCohomology.mapShortComplexH1_comp_assoc {k : Type u} [CommRing k] {G H K : Type u} [Group G] [Group H] [Group K] {A : Rep k K} {B : Rep k H} {C : Rep k G} (f : H →* K) (g : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (ψ : (Action.res (ModuleCat k) g).obj B ⟶ C) {Z : CategoryTheory.ShortComplex (ModuleCat k)} (h : shortComplexH1 C ⟶ Z) : CategoryTheory.CategoryStruct.comp (mapShortComplexH1 (f.comp g) (CategoryTheory.CategoryStruct.comp ((Action.res (ModuleCat k) g).map φ) ψ)) h = CategoryTheory.CategoryStruct.comp (mapShortComplexH1 f φ) (CategoryTheory.CategoryStruct.comp (mapShortComplexH1 g ψ) h)

theorem groupCohomology.mapShortComplexH1_id_comp {k G : Type u} [CommRing k] [Group G] {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C) : mapShortComplexH1 (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ) = CategoryTheory.CategoryStruct.comp (mapShortComplexH1 (MonoidHom.id G) φ) (mapShortComplexH1 (MonoidHom.id G) ψ)

theorem groupCohomology.mapShortComplexH1_id_comp_assoc {k G : Type u} [CommRing k] [Group G] {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C) {Z : CategoryTheory.ShortComplex (ModuleCat k)} (h : shortComplexH1 C ⟶ Z) : CategoryTheory.CategoryStruct.comp (mapShortComplexH1 (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ)) h = CategoryTheory.CategoryStruct.comp (mapShortComplexH1 (MonoidHom.id G) φ) (CategoryTheory.CategoryStruct.comp (mapShortComplexH1 (MonoidHom.id G) ψ) h)

@[reducible, inline]

noncomputable abbrev groupCohomology.mapCocycles₁ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : ModuleCat.of k ↥(cocycles₁ A) ⟶ ModuleCat.of k ↥(cocycles₁ B)

Given a group homomorphism f : G →* H and a representation morphism φ : Res(f)(A) ⟶ B, this is induced map Z¹(H, A) ⟶ Z¹(G, B).

@[deprecated groupCohomology.mapCocycles₁ (since := "2025-06-25")]

def groupCohomology.mapOneCocycles {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : ModuleCat.of k ↥(cocycles₁ A) ⟶ ModuleCat.of k ↥(cocycles₁ B)

Alias of groupCohomology.mapCocycles₁.

---

Given a group homomorphism f : G →* H and a representation morphism φ : Res(f)(A) ⟶ B, this is induced map Z¹(H, A) ⟶ Z¹(G, B).

theorem groupCohomology.mapCocycles₁_comp_i {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp (mapCocycles₁ f φ) (shortComplexH1 B).moduleCatLeftHomologyData.i = CategoryTheory.CategoryStruct.comp (shortComplexH1 A).moduleCatLeftHomologyData.i (cochainsMap₁ f φ)

theorem groupCohomology.mapCocycles₁_comp_i_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) {Z : ModuleCat k} (h : (shortComplexH1 B).X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (mapCocycles₁ f φ) (CategoryTheory.CategoryStruct.comp (shortComplexH1 B).moduleCatLeftHomologyData.i h) = CategoryTheory.CategoryStruct.comp (shortComplexH1 A).moduleCatLeftHomologyData.i (CategoryTheory.CategoryStruct.comp (cochainsMap₁ f φ) h)

theorem groupCohomology.mapCocycles₁_comp_i_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (x : CategoryTheory.ToType (ModuleCat.of k ↥(cocycles₁ A))) : (LinearMap.ker (ModuleCat.Hom.hom (shortComplexH1 B).g)).subtype ((CategoryTheory.ConcreteCategory.hom (mapCocycles₁ f φ)) x) = (CategoryTheory.CategoryStruct.comp (shortComplexH1 A).moduleCatLeftHomologyData.i (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (LinearMap.funLeft k ↑A.V ⇑f)) (ModuleCat.ofHom ((ModuleCat.Hom.hom φ.hom).compLeft G)))) x

@[deprecated groupCohomology.mapCocycles₁_comp_i (since := "2025-06-25")]

theorem groupCohomology.mapOneCocycles_comp_i {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp (mapCocycles₁ f φ) (shortComplexH1 B).moduleCatLeftHomologyData.i = CategoryTheory.CategoryStruct.comp (shortComplexH1 A).moduleCatLeftHomologyData.i (cochainsMap₁ f φ)

Alias of groupCohomology.mapCocycles₁_comp_i.

@[simp]

theorem groupCohomology.coe_mapCocycles₁ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (x : ↑(ModuleCat.of k ↥(cocycles₁ A))) : ⇑((CategoryTheory.ConcreteCategory.hom (mapCocycles₁ f φ)) x) = (CategoryTheory.ConcreteCategory.hom (cochainsMap₁ f φ)) ⇑x

@[deprecated groupCohomology.coe_mapCocycles₁ (since := "2025-06-25")]

theorem groupCohomology.coe_mapOneCocycles {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (x : ↑(ModuleCat.of k ↥(cocycles₁ A))) : ⇑((CategoryTheory.ConcreteCategory.hom (mapCocycles₁ f φ)) x) = (CategoryTheory.ConcreteCategory.hom (cochainsMap₁ f φ)) ⇑x

Alias of groupCohomology.coe_mapCocycles₁.

@[deprecated groupCohomology.mapOneCocycles_comp_i (since := "2025-05-09")]

theorem groupCohomology.mapOneCocycles_comp_subtype {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp (mapCocycles₁ f φ) (shortComplexH1 B).moduleCatLeftHomologyData.i = CategoryTheory.CategoryStruct.comp (shortComplexH1 A).moduleCatLeftHomologyData.i (cochainsMap₁ f φ)

Alias of groupCohomology.mapCocycles₁_comp_i.

---

Alias of groupCohomology.mapCocycles₁_comp_i.

@[simp]

theorem groupCohomology.cocyclesMap_comp_isoCocycles₁_hom {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp (cocyclesMap f φ 1) (isoCocycles₁ B).hom = CategoryTheory.CategoryStruct.comp (isoCocycles₁ A).hom (mapCocycles₁ f φ)

@[simp]

theorem groupCohomology.cocyclesMap_comp_isoCocycles₁_hom_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) {Z : ModuleCat k} (h : ModuleCat.of k ↥(cocycles₁ B) ⟶ Z) : CategoryTheory.CategoryStruct.comp (cocyclesMap f φ 1) (CategoryTheory.CategoryStruct.comp (isoCocycles₁ B).hom h) = CategoryTheory.CategoryStruct.comp (isoCocycles₁ A).hom (CategoryTheory.CategoryStruct.comp (mapCocycles₁ f φ) h)

@[simp]

theorem groupCohomology.cocyclesMap_comp_isoCocycles₁_hom_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (x : CategoryTheory.ToType (cocycles A 1)) : (CategoryTheory.ConcreteCategory.hom (isoCocycles₁ B).hom) ((CategoryTheory.ConcreteCategory.hom (cocyclesMap f φ 1)) x) = (CategoryTheory.ConcreteCategory.hom (mapCocycles₁ f φ)) ((CategoryTheory.ConcreteCategory.hom (isoCocycles₁ A).hom) x)

@[deprecated groupCohomology.cocyclesMap_comp_isoCocycles₁_hom (since := "2025-06-25")]

theorem groupCohomology.cocyclesMap_comp_isoOneCocycles_hom {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp (cocyclesMap f φ 1) (isoCocycles₁ B).hom = CategoryTheory.CategoryStruct.comp (isoCocycles₁ A).hom (mapCocycles₁ f φ)

Alias of groupCohomology.cocyclesMap_comp_isoCocycles₁_hom.

@[simp]

theorem groupCohomology.mapCocycles₁_one {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (φ : (Action.res (ModuleCat k) 1).obj A ⟶ B) : mapCocycles₁ 1 φ = 0

@[deprecated groupCohomology.mapCocycles₁_one (since := "2025-06-25")]

theorem groupCohomology.mapOneCocycles_one {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (φ : (Action.res (ModuleCat k) 1).obj A ⟶ B) : mapCocycles₁ 1 φ = 0

Alias of groupCohomology.mapCocycles₁_one.

@[deprecated groupCohomology.map (since := "2025-06-09")]

def groupCohomology.H1Map {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (n : ℕ) : groupCohomology A n ⟶ groupCohomology B n

Given a group homomorphism f : G →* H and a representation morphism φ : Res(f)(A) ⟶ B, this is induced map H¹(H, A) ⟶ H¹(G, B).

@[deprecated groupCohomology.map_id (since := "2025-6-09")]

theorem groupCohomology.H1Map_id {k G : Type u} [CommRing k] [Group G] {B : Rep k G} (n : ℕ) : map (MonoidHom.id G) (CategoryTheory.CategoryStruct.id B) n = CategoryTheory.CategoryStruct.id (groupCohomology B n)

Alias of groupCohomology.map_id.

@[deprecated groupCohomology.map_comp (since := "2025-06-09")]

theorem groupCohomology.H1Map_comp {k : Type u} [CommRing k] {G H K : Type u} [Group G] [Group H] [Group K] {A : Rep k K} {B : Rep k H} {C : Rep k G} (f : H →* K) (g : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (ψ : (Action.res (ModuleCat k) g).obj B ⟶ C) (n : ℕ) : map (f.comp g) (CategoryTheory.CategoryStruct.comp ((Action.res (ModuleCat k) g).map φ) ψ) n = CategoryTheory.CategoryStruct.comp (map f φ n) (map g ψ n)

Alias of groupCohomology.map_comp.

@[deprecated groupCohomology.map_id_comp (since := "2025-06-09")]

theorem groupCohomology.H1Map_id_comp {k G : Type u} [CommRing k] [Group G] {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C) (n : ℕ) : map (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ) n = CategoryTheory.CategoryStruct.comp (map (MonoidHom.id G) φ n) (map (MonoidHom.id G) ψ n)

Alias of groupCohomology.map_id_comp.

@[simp]

theorem groupCohomology.H1π_comp_map {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp (H1π A) (map f φ 1) = CategoryTheory.CategoryStruct.comp (mapCocycles₁ f φ) (H1π B)

@[simp]

theorem groupCohomology.H1π_comp_map_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) {Z : ModuleCat k} (h : groupCohomology B 1 ⟶ Z) : CategoryTheory.CategoryStruct.comp (H1π A) (CategoryTheory.CategoryStruct.comp (map f φ 1) h) = CategoryTheory.CategoryStruct.comp (mapCocycles₁ f φ) (CategoryTheory.CategoryStruct.comp (H1π B) h)

@[simp]

theorem groupCohomology.H1π_comp_map_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (x : CategoryTheory.ToType (ModuleCat.of k ↥(cocycles₁ A))) : (CategoryTheory.ConcreteCategory.hom (map f φ 1)) ((CategoryTheory.ConcreteCategory.hom (H1π A)) x) = (CategoryTheory.ConcreteCategory.hom (H1π B)) ((CategoryTheory.ConcreteCategory.hom (mapCocycles₁ f φ)) x)

@[deprecated groupCohomology.H1π_comp_map (since := "2025-06-12")]

theorem groupCohomology.H1π_comp_H1Map {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp (H1π A) (map f φ 1) = CategoryTheory.CategoryStruct.comp (mapCocycles₁ f φ) (H1π B)

Alias of groupCohomology.H1π_comp_map.

@[simp]

theorem groupCohomology.map₁_one {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (φ : (Action.res (ModuleCat k) 1).obj A ⟶ B) : map 1 φ 1 = 0

@[deprecated groupCohomology.map₁_one (since := "2025-07-31")]

theorem groupCohomology.map_1_one {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (φ : (Action.res (ModuleCat k) 1).obj A ⟶ B) : map 1 φ 1 = 0

Alias of groupCohomology.map₁_one.

@[deprecated groupCohomology.map_1_one (since := "2025-06-09")]

theorem groupCohomology.H1Map_one {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (φ : (Action.res (ModuleCat k) 1).obj A ⟶ B) : map 1 φ 1 = 0

Alias of groupCohomology.map₁_one.

---

Alias of groupCohomology.map₁_one.

noncomputable def groupCohomology.H1InfRes {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] : CategoryTheory.ShortComplex (ModuleCat k)

The short complex H¹(G ⧸ S, A^S) ⟶ H¹(G, A) ⟶ H¹(S, A).

@[simp]

theorem groupCohomology.H1InfRes_X₃ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] : (H1InfRes A S).X₃ = groupCohomology ((Action.res (ModuleCat k) S.subtype).obj A) 1

@[simp]

theorem groupCohomology.H1InfRes_g {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] : (H1InfRes A S).g = map S.subtype (CategoryTheory.CategoryStruct.id ((Action.res (ModuleCat k) S.subtype).obj A)) 1

@[simp]

theorem groupCohomology.H1InfRes_f {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] : (H1InfRes A S).f = map (QuotientGroup.mk' S) (A.subtype (Representation.invariants (MonoidHom.comp A.ρ S.subtype)) ⋯) 1

@[simp]

theorem groupCohomology.H1InfRes_X₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] : (H1InfRes A S).X₁ = groupCohomology (A.quotientToInvariants S) 1

@[simp]

theorem groupCohomology.H1InfRes_X₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] : (H1InfRes A S).X₂ = groupCohomology A 1

instance groupCohomology.instMonoModuleCatFH1InfRes {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] : CategoryTheory.Mono (H1InfRes A S).f

The inflation map H¹(G ⧸ S, A^S) ⟶ H¹(G, A) is a monomorphism.

theorem groupCohomology.H1InfRes_exact {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] : (H1InfRes A S).Exact

Given a G-representation A and a normal subgroup S ≤ G, the short complex H¹(G ⧸ S, A^S) ⟶ H¹(G, A) ⟶ H¹(S, A) is exact.

noncomputable def groupCohomology.mapShortComplexH2 {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : shortComplexH2 A ⟶ shortComplexH2 B

Given a group homomorphism f : G →* H and a representation morphism φ : Res(f)(A) ⟶ B, this is the induced map from the short complex Fun(H, A) --d₁₂--> Fun(H × H, A) --d₂₃--> Fun(H × H × H, A) to Fun(G, B) --d₁₂--> Fun(G × G, B) --d₂₃--> Fun(G × G × G, B).

@[simp]

theorem groupCohomology.mapShortComplexH2_τ₂ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : (mapShortComplexH2 f φ).τ₂ = cochainsMap₂ f φ

@[simp]

theorem groupCohomology.mapShortComplexH2_τ₁ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : (mapShortComplexH2 f φ).τ₁ = cochainsMap₁ f φ

@[simp]

theorem groupCohomology.mapShortComplexH2_τ₃ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : (mapShortComplexH2 f φ).τ₃ = cochainsMap₃ f φ

@[simp]

theorem groupCohomology.mapShortComplexH2_zero {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) : mapShortComplexH2 f 0 = 0

@[simp]

theorem groupCohomology.mapShortComplexH2_id {k H : Type u} [CommRing k] [Group H] {A : Rep k H} : mapShortComplexH2 (MonoidHom.id H) (CategoryTheory.CategoryStruct.id A) = CategoryTheory.CategoryStruct.id (shortComplexH2 A)

theorem groupCohomology.mapShortComplexH2_comp {k : Type u} [CommRing k] {G H K : Type u} [Group G] [Group H] [Group K] {A : Rep k K} {B : Rep k H} {C : Rep k G} (f : H →* K) (g : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (ψ : (Action.res (ModuleCat k) g).obj B ⟶ C) : mapShortComplexH2 (f.comp g) (CategoryTheory.CategoryStruct.comp ((Action.res (ModuleCat k) g).map φ) ψ) = CategoryTheory.CategoryStruct.comp (mapShortComplexH2 f φ) (mapShortComplexH2 g ψ)

theorem groupCohomology.mapShortComplexH2_comp_assoc {k : Type u} [CommRing k] {G H K : Type u} [Group G] [Group H] [Group K] {A : Rep k K} {B : Rep k H} {C : Rep k G} (f : H →* K) (g : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (ψ : (Action.res (ModuleCat k) g).obj B ⟶ C) {Z : CategoryTheory.ShortComplex (ModuleCat k)} (h : shortComplexH2 C ⟶ Z) : CategoryTheory.CategoryStruct.comp (mapShortComplexH2 (f.comp g) (CategoryTheory.CategoryStruct.comp ((Action.res (ModuleCat k) g).map φ) ψ)) h = CategoryTheory.CategoryStruct.comp (mapShortComplexH2 f φ) (CategoryTheory.CategoryStruct.comp (mapShortComplexH2 g ψ) h)

theorem groupCohomology.mapShortComplexH2_id_comp {k G : Type u} [CommRing k] [Group G] {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C) : mapShortComplexH2 (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ) = CategoryTheory.CategoryStruct.comp (mapShortComplexH2 (MonoidHom.id G) φ) (mapShortComplexH2 (MonoidHom.id G) ψ)

theorem groupCohomology.mapShortComplexH2_id_comp_assoc {k G : Type u} [CommRing k] [Group G] {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C) {Z : CategoryTheory.ShortComplex (ModuleCat k)} (h : shortComplexH2 C ⟶ Z) : CategoryTheory.CategoryStruct.comp (mapShortComplexH2 (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ)) h = CategoryTheory.CategoryStruct.comp (mapShortComplexH2 (MonoidHom.id G) φ) (CategoryTheory.CategoryStruct.comp (mapShortComplexH2 (MonoidHom.id G) ψ) h)

@[reducible, inline]

noncomputable abbrev groupCohomology.mapCocycles₂ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : ModuleCat.of k ↥(cocycles₂ A) ⟶ ModuleCat.of k ↥(cocycles₂ B)

Given a group homomorphism f : G →* H and a representation morphism φ : Res(f)(A) ⟶ B, this is induced map Z²(H, A) ⟶ Z²(G, B).

@[deprecated groupCohomology.mapCocycles₂ (since := "2025-06-25")]

def groupCohomology.mapTwoCocycles {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : ModuleCat.of k ↥(cocycles₂ A) ⟶ ModuleCat.of k ↥(cocycles₂ B)

Alias of groupCohomology.mapCocycles₂.

---

Given a group homomorphism f : G →* H and a representation morphism φ : Res(f)(A) ⟶ B, this is induced map Z²(H, A) ⟶ Z²(G, B).

theorem groupCohomology.mapCocycles₂_comp_i {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp (mapCocycles₂ f φ) (shortComplexH2 B).moduleCatLeftHomologyData.i = CategoryTheory.CategoryStruct.comp (shortComplexH2 A).moduleCatLeftHomologyData.i (cochainsMap₂ f φ)

theorem groupCohomology.mapCocycles₂_comp_i_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) {Z : ModuleCat k} (h : (shortComplexH2 B).X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (mapCocycles₂ f φ) (CategoryTheory.CategoryStruct.comp (shortComplexH2 B).moduleCatLeftHomologyData.i h) = CategoryTheory.CategoryStruct.comp (shortComplexH2 A).moduleCatLeftHomologyData.i (CategoryTheory.CategoryStruct.comp (cochainsMap₂ f φ) h)

theorem groupCohomology.mapCocycles₂_comp_i_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (x : CategoryTheory.ToType (ModuleCat.of k ↥(cocycles₂ A))) : (LinearMap.ker (ModuleCat.Hom.hom (shortComplexH2 B).g)).subtype ((CategoryTheory.ConcreteCategory.hom (mapCocycles₂ f φ)) x) = (CategoryTheory.CategoryStruct.comp (shortComplexH2 A).moduleCatLeftHomologyData.i (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (LinearMap.funLeft k (↑A.V) (Prod.map ⇑f ⇑f))) (ModuleCat.ofHom ((ModuleCat.Hom.hom φ.hom).compLeft (G × G))))) x

@[deprecated groupCohomology.mapCocycles₂_comp_i (since := "2025-06-25")]

theorem groupCohomology.mapTwoCocycles_comp_i {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp (mapCocycles₂ f φ) (shortComplexH2 B).moduleCatLeftHomologyData.i = CategoryTheory.CategoryStruct.comp (shortComplexH2 A).moduleCatLeftHomologyData.i (cochainsMap₂ f φ)

Alias of groupCohomology.mapCocycles₂_comp_i.

@[simp]

theorem groupCohomology.coe_mapCocycles₂ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (x : ↑(ModuleCat.of k ↥(cocycles₂ A))) : ⇑((CategoryTheory.ConcreteCategory.hom (mapCocycles₂ f φ)) x) = (CategoryTheory.ConcreteCategory.hom (cochainsMap₂ f φ)) ⇑x

@[deprecated groupCohomology.coe_mapCocycles₂ (since := "2025-06-25")]

theorem groupCohomology.coe_mapTwoCocycles {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (x : ↑(ModuleCat.of k ↥(cocycles₂ A))) : ⇑((CategoryTheory.ConcreteCategory.hom (mapCocycles₂ f φ)) x) = (CategoryTheory.ConcreteCategory.hom (cochainsMap₂ f φ)) ⇑x

Alias of groupCohomology.coe_mapCocycles₂.

@[deprecated groupCohomology.mapTwoCocycles_comp_i (since := "2025-05-09")]

theorem groupCohomology.mapTwoCocycles_comp_subtype {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp (mapCocycles₂ f φ) (shortComplexH2 B).moduleCatLeftHomologyData.i = CategoryTheory.CategoryStruct.comp (shortComplexH2 A).moduleCatLeftHomologyData.i (cochainsMap₂ f φ)

Alias of groupCohomology.mapCocycles₂_comp_i.

---

Alias of groupCohomology.mapCocycles₂_comp_i.

@[simp]

theorem groupCohomology.cocyclesMap_comp_isoCocycles₂_hom {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp (cocyclesMap f φ 2) (isoCocycles₂ B).hom = CategoryTheory.CategoryStruct.comp (isoCocycles₂ A).hom (mapCocycles₂ f φ)

@[simp]

theorem groupCohomology.cocyclesMap_comp_isoCocycles₂_hom_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) {Z : ModuleCat k} (h : ModuleCat.of k ↥(cocycles₂ B) ⟶ Z) : CategoryTheory.CategoryStruct.comp (cocyclesMap f φ 2) (CategoryTheory.CategoryStruct.comp (isoCocycles₂ B).hom h) = CategoryTheory.CategoryStruct.comp (isoCocycles₂ A).hom (CategoryTheory.CategoryStruct.comp (mapCocycles₂ f φ) h)

@[simp]

theorem groupCohomology.cocyclesMap_comp_isoCocycles₂_hom_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (x : CategoryTheory.ToType (cocycles A 2)) : (CategoryTheory.ConcreteCategory.hom (isoCocycles₂ B).hom) ((CategoryTheory.ConcreteCategory.hom (cocyclesMap f φ 2)) x) = (CategoryTheory.ConcreteCategory.hom (mapCocycles₂ f φ)) ((CategoryTheory.ConcreteCategory.hom (isoCocycles₂ A).hom) x)

@[deprecated groupCohomology.cocyclesMap_comp_isoCocycles₂_hom (since := "2025-06-25")]

theorem groupCohomology.cocyclesMap_comp_isoTwoCocycles_hom {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp (cocyclesMap f φ 2) (isoCocycles₂ B).hom = CategoryTheory.CategoryStruct.comp (isoCocycles₂ A).hom (mapCocycles₂ f φ)

Alias of groupCohomology.cocyclesMap_comp_isoCocycles₂_hom.

@[deprecated groupCohomology.map (since := "2025-06-09")]

def groupCohomology.H2Map {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (n : ℕ) : groupCohomology A n ⟶ groupCohomology B n

Given a group homomorphism f : G →* H and a representation morphism φ : Res(f)(A) ⟶ B, this is induced map H²(H, A) ⟶ H²(G, B).

@[deprecated groupCohomology.map_id (since := "2025-06-09")]

theorem groupCohomology.H2Map_id {k G : Type u} [CommRing k] [Group G] {B : Rep k G} (n : ℕ) : map (MonoidHom.id G) (CategoryTheory.CategoryStruct.id B) n = CategoryTheory.CategoryStruct.id (groupCohomology B n)

Alias of groupCohomology.map_id.

@[deprecated groupCohomology.map_comp (since := "2025-06-09")]

theorem groupCohomology.H2Map_comp {k : Type u} [CommRing k] {G H K : Type u} [Group G] [Group H] [Group K] {A : Rep k K} {B : Rep k H} {C : Rep k G} (f : H →* K) (g : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (ψ : (Action.res (ModuleCat k) g).obj B ⟶ C) (n : ℕ) : map (f.comp g) (CategoryTheory.CategoryStruct.comp ((Action.res (ModuleCat k) g).map φ) ψ) n = CategoryTheory.CategoryStruct.comp (map f φ n) (map g ψ n)

Alias of groupCohomology.map_comp.

@[deprecated groupCohomology.map_id_comp (since := "2025-06-09")]

theorem groupCohomology.H2Map_id_comp {k G : Type u} [CommRing k] [Group G] {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C) (n : ℕ) : map (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ) n = CategoryTheory.CategoryStruct.comp (map (MonoidHom.id G) φ n) (map (MonoidHom.id G) ψ n)

Alias of groupCohomology.map_id_comp.

@[simp]

theorem groupCohomology.H2π_comp_map {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp (H2π A) (map f φ 2) = CategoryTheory.CategoryStruct.comp (mapCocycles₂ f φ) (H2π B)

@[simp]

theorem groupCohomology.H2π_comp_map_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) {Z : ModuleCat k} (h : groupCohomology B 2 ⟶ Z) : CategoryTheory.CategoryStruct.comp (H2π A) (CategoryTheory.CategoryStruct.comp (map f φ 2) h) = CategoryTheory.CategoryStruct.comp (mapCocycles₂ f φ) (CategoryTheory.CategoryStruct.comp (H2π B) h)

@[simp]

theorem groupCohomology.H2π_comp_map_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (x : CategoryTheory.ToType (ModuleCat.of k ↥(cocycles₂ A))) : (CategoryTheory.ConcreteCategory.hom (map f φ 2)) ((CategoryTheory.ConcreteCategory.hom (H2π A)) x) = (CategoryTheory.ConcreteCategory.hom (H2π B)) ((CategoryTheory.ConcreteCategory.hom (mapCocycles₂ f φ)) x)

@[deprecated groupCohomology.H2π_comp_map (since := "2025-06-12")]

theorem groupCohomology.H2π_comp_H2Map {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp (H2π A) (map f φ 2) = CategoryTheory.CategoryStruct.comp (mapCocycles₂ f φ) (H2π B)

Alias of groupCohomology.H2π_comp_map.

noncomputable def groupCohomology.cochainsFunctor (k G : Type u) [CommRing k] [Group G] : CategoryTheory.Functor (Rep k G) (CochainComplex (ModuleCat k) ℕ)

The functor sending a representation to its complex of inhomogeneous cochains.

@[simp]

theorem groupCohomology.cochainsFunctor_obj (k G : Type u) [CommRing k] [Group G] (A : Rep k G) : (cochainsFunctor k G).obj A = inhomogeneousCochains A

@[simp]

theorem groupCohomology.cochainsFunctor_map (k G : Type u) [CommRing k] [Group G] {X✝ Y✝ : Rep k G} (f : X✝ ⟶ Y✝) : (cochainsFunctor k G).map f = cochainsMap (MonoidHom.id G) f

instance groupCohomology.instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor (k G : Type u) [CommRing k] [Group G] : (cochainsFunctor k G).PreservesZeroMorphisms

instance groupCohomology.instAdditiveRepCochainComplexModuleCatNatCochainsFunctor (k G : Type u) [CommRing k] [Group G] : (cochainsFunctor k G).Additive

noncomputable def groupCohomology.functor (k G : Type u) [CommRing k] [Group G] (n : ℕ) : CategoryTheory.Functor (Rep k G) (ModuleCat k)

The functor sending a G-representation A to Hⁿ(G, A).

@[simp]

theorem groupCohomology.functor_obj (k G : Type u) [CommRing k] [Group G] (n : ℕ) (A : Rep k G) : (functor k G n).obj A = groupCohomology A n

@[simp]

theorem groupCohomology.functor_map (k G : Type u) [CommRing k] [Group G] (n : ℕ) {X✝ Y✝ : Rep k G} (φ : X✝ ⟶ Y✝) : (functor k G n).map φ = map (MonoidHom.id G) φ n

instance groupCohomology.instPreservesZeroMorphismsRepModuleCatFunctor (k G : Type u) [CommRing k] [Group G] (n : ℕ) : (functor k G n).PreservesZeroMorphisms

noncomputable def groupCohomology.resNatTrans (k : Type u) {G H : Type u} [CommRing k] [Group G] [Group H] (f : G →* H) (n : ℕ) : functor k H n ⟶ (Action.res (ModuleCat k) f).comp (functor k G n)

Given a group homomorphism f : G →* H, this is a natural transformation between the functors sending A : Rep k H to Hⁿ(H, A) and to Hⁿ(G, Res(f)(A)).

@[simp]

theorem groupCohomology.resNatTrans_app (k : Type u) {G H : Type u} [CommRing k] [Group G] [Group H] (f : G →* H) (n : ℕ) (X : Rep k H) : (resNatTrans k f n).app X = map f (CategoryTheory.CategoryStruct.id ((Action.res (ModuleCat k) f).obj X)) n

noncomputable def groupCohomology.infNatTrans (k : Type u) {G : Type u} [CommRing k] [Group G] (S : Subgroup G) [S.Normal] (n : ℕ) : (Rep.quotientToInvariantsFunctor k S).comp (functor k (G ⧸ S) n) ⟶ functor k G n

Given a normal subgroup S ≤ G, this is a natural transformation between the functors sending A : Rep k G to Hⁿ(G ⧸ S, A^S) and to Hⁿ(G, A).

@[simp]

theorem groupCohomology.infNatTrans_app (k : Type u) {G : Type u} [CommRing k] [Group G] (S : Subgroup G) [S.Normal] (n : ℕ) (A : Rep k G) : (infNatTrans k S n).app A = map (QuotientGroup.mk' S) (A.subtype (Representation.invariants (MonoidHom.comp A.ρ S.subtype)) ⋯) n