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) [DecidableEq G] [DecidableEq H] : 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)).

Equations

• One or more equations did not get rendered due to their size.

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) [DecidableEq G] [DecidableEq H] (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) [DecidableEq G] [DecidableEq H] (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} [DecidableEq 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] [DecidableEq 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] [DecidableEq 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] [DecidableEq G] [Group H] [DecidableEq H] [Group K] [DecidableEq 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] [DecidableEq G] [Group H] [DecidableEq H] [Group K] [DecidableEq 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] [DecidableEq 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] [DecidableEq 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) [DecidableEq G] [DecidableEq 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) [DecidableEq G] [DecidableEq H] (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] [DecidableEq 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) [DecidableEq G] [DecidableEq H] (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] [DecidableEq 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) [DecidableEq G] [DecidableEq H] (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)).

Equations

• groupCohomology.cocyclesMap f φ n = HomologicalComplex.cyclesMap (groupCohomology.cochainsMap f φ) n

@[simp]

theorem groupCohomology.cocyclesMap_id {k G : Type u} [CommRing k] [Group G] {B : Rep k G} (n : ℕ) [DecidableEq G] : 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] [DecidableEq G] [Group H] [DecidableEq H] [Group K] [DecidableEq 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] [DecidableEq G] [Group H] [DecidableEq H] [Group K] [DecidableEq 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] [DecidableEq 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] [DecidableEq 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) [DecidableEq G] [DecidableEq H] (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)).

Equations

• groupCohomology.map f φ n = HomologicalComplex.homologyMap (groupCohomology.cochainsMap f φ) n

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) [DecidableEq G] [DecidableEq H] (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) [DecidableEq G] [DecidableEq H] (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) [DecidableEq G] [DecidableEq H] (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 : ℕ) [DecidableEq G] : 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] [DecidableEq G] [Group H] [DecidableEq H] [Group K] [DecidableEq 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] [DecidableEq G] [Group H] [DecidableEq H] [Group K] [DecidableEq 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] [DecidableEq 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] [DecidableEq 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.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)

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)).

Equations

• groupCohomology.fOne f φ = ModuleCat.ofHom ((ModuleCat.Hom.hom φ.hom).compLeft G ∘ₗ LinearMap.funLeft k ↑A.V ⇑f)

@[reducible, inline]

noncomputable abbrev 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)

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₂)).

Equations

• groupCohomology.fTwo f φ = ModuleCat.ofHom ((ModuleCat.Hom.hom φ.hom).compLeft (G × G) ∘ₗ LinearMap.funLeft k (↑A.V) (Prod.map ⇑f ⇑f))

@[reducible, inline]

noncomputable abbrev 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)

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₃)).

Equations

• groupCohomology.fThree f φ = ModuleCat.ofHom ((ModuleCat.Hom.hom φ.hom).compLeft (G × G × G) ∘ₗ LinearMap.funLeft k (↑A.V) (Prod.map (⇑f) (Prod.map ⇑f ⇑f)))

@[simp]

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) [DecidableEq G] [DecidableEq H] : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 0) (zeroCochainsIso B).hom = CategoryTheory.CategoryStruct.comp (zeroCochainsIso A).hom φ.hom

@[simp]

theorem groupCohomology.cochainsMap_f_0_comp_zeroCochainsIso_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) [DecidableEq G] [DecidableEq H] {Z : ModuleCat k} (h : B.V ⟶ Z) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 0) (CategoryTheory.CategoryStruct.comp (zeroCochainsIso B).hom h) = CategoryTheory.CategoryStruct.comp (zeroCochainsIso A).hom (CategoryTheory.CategoryStruct.comp φ.hom h)

@[simp]

theorem groupCohomology.cochainsMap_f_0_comp_zeroCochainsIso_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) [DecidableEq G] [DecidableEq H] (x : CategoryTheory.ToType ((inhomogeneousCochains A).X 0)) : (CategoryTheory.ConcreteCategory.hom (zeroCochainsIso B).hom) ((CategoryTheory.ConcreteCategory.hom ((cochainsMap f φ).f 0)) x) = (CategoryTheory.ConcreteCategory.hom φ.hom) ((CategoryTheory.ConcreteCategory.hom (zeroCochainsIso A).hom) x)

@[deprecated groupCohomology.cochainsMap_f_0_comp_zeroCochainsIso (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) [DecidableEq G] [DecidableEq H] : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 0) (zeroCochainsIso B).hom = CategoryTheory.CategoryStruct.comp (zeroCochainsIso A).hom φ.hom

Alias of groupCohomology.cochainsMap_f_0_comp_zeroCochainsIso.

@[simp]

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) [DecidableEq G] [DecidableEq H] : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 1) (oneCochainsIso B).hom = CategoryTheory.CategoryStruct.comp (oneCochainsIso A).hom (fOne f φ)

@[simp]

theorem groupCohomology.cochainsMap_f_1_comp_oneCochainsIso_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) [DecidableEq G] [DecidableEq H] {Z : ModuleCat k} (h : ModuleCat.of k (G → ↑B.V) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 1) (CategoryTheory.CategoryStruct.comp (oneCochainsIso B).hom h) = CategoryTheory.CategoryStruct.comp (oneCochainsIso A).hom (CategoryTheory.CategoryStruct.comp (fOne f φ) h)

@[simp]

theorem groupCohomology.cochainsMap_f_1_comp_oneCochainsIso_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) [DecidableEq G] [DecidableEq H] (x : CategoryTheory.ToType ((inhomogeneousCochains A).X 1)) : (CategoryTheory.ConcreteCategory.hom (oneCochainsIso 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 (oneCochainsIso A).hom) x))

@[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) [DecidableEq G] [DecidableEq H] : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 1) (oneCochainsIso B).hom = CategoryTheory.CategoryStruct.comp (oneCochainsIso A).hom (fOne f φ)

Alias of groupCohomology.cochainsMap_f_1_comp_oneCochainsIso.

@[simp]

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) [DecidableEq G] [DecidableEq H] : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 2) (twoCochainsIso B).hom = CategoryTheory.CategoryStruct.comp (twoCochainsIso A).hom (fTwo f φ)

@[simp]

theorem groupCohomology.cochainsMap_f_2_comp_twoCochainsIso_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) [DecidableEq G] [DecidableEq H] {Z : ModuleCat k} (h : ModuleCat.of k (G × G → ↑B.V) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 2) (CategoryTheory.CategoryStruct.comp (twoCochainsIso B).hom h) = CategoryTheory.CategoryStruct.comp (twoCochainsIso A).hom (CategoryTheory.CategoryStruct.comp (fTwo f φ) h)

@[simp]

theorem groupCohomology.cochainsMap_f_2_comp_twoCochainsIso_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) [DecidableEq G] [DecidableEq H] (x : CategoryTheory.ToType ((inhomogeneousCochains A).X 2)) : (CategoryTheory.ConcreteCategory.hom (twoCochainsIso 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 (twoCochainsIso A).hom) x))

@[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) [DecidableEq G] [DecidableEq H] : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 2) (twoCochainsIso B).hom = CategoryTheory.CategoryStruct.comp (twoCochainsIso A).hom (fTwo f φ)

Alias of groupCohomology.cochainsMap_f_2_comp_twoCochainsIso.

@[simp]

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) [DecidableEq G] [DecidableEq H] : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 3) (threeCochainsIso B).hom = CategoryTheory.CategoryStruct.comp (threeCochainsIso A).hom (fThree f φ)

@[simp]

theorem groupCohomology.cochainsMap_f_3_comp_threeCochainsIso_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) [DecidableEq G] [DecidableEq H] {Z : ModuleCat k} (h : ModuleCat.of k (G × G × G → ↑B.V) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 3) (CategoryTheory.CategoryStruct.comp (threeCochainsIso B).hom h) = CategoryTheory.CategoryStruct.comp (threeCochainsIso A).hom (CategoryTheory.CategoryStruct.comp (fThree f φ) h)

@[simp]

theorem groupCohomology.cochainsMap_f_3_comp_threeCochainsIso_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) [DecidableEq G] [DecidableEq H] (x : CategoryTheory.ToType ((inhomogeneousCochains A).X 3)) : (CategoryTheory.ConcreteCategory.hom (threeCochainsIso 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 (threeCochainsIso A).hom) x))

@[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) [DecidableEq G] [DecidableEq H] : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 3) (threeCochainsIso B).hom = CategoryTheory.CategoryStruct.comp (threeCochainsIso A).hom (fThree f φ)

Alias of groupCohomology.cochainsMap_f_3_comp_threeCochainsIso.

@[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) [DecidableEq G] [DecidableEq H] (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ᴳ.

Equations

• @groupCohomology.H0Map = @groupCohomology.map

@[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 : ℕ) [DecidableEq G] : 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] [DecidableEq G] [Group H] [DecidableEq H] [Group K] [DecidableEq 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] [DecidableEq 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) [DecidableEq G] [DecidableEq H] : 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) [DecidableEq G] [DecidableEq H] {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) [DecidableEq G] [DecidableEq H] (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) [DecidableEq G] [DecidableEq H] : 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] [DecidableEq 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] [DecidableEq 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] [DecidableEq 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] [DecidableEq 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] [DecidableEq 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] [DecidableEq 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_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) [DecidableEq G] [DecidableEq H] : CategoryTheory.CategoryStruct.comp (cocyclesMap f φ 0) (CategoryTheory.CategoryStruct.comp (zeroCocyclesIso B).hom (shortComplexH0 B).f) = CategoryTheory.CategoryStruct.comp (zeroCocyclesIso A).hom (CategoryTheory.CategoryStruct.comp (shortComplexH0 A).f φ.hom)

theorem groupCohomology.cocyclesMap_zeroIsoCocycles_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) [DecidableEq G] [DecidableEq H] {Z : ModuleCat k} (h : (shortComplexH0 B).X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (cocyclesMap f φ 0) (CategoryTheory.CategoryStruct.comp (zeroCocyclesIso B).hom (CategoryTheory.CategoryStruct.comp (shortComplexH0 B).f h)) = CategoryTheory.CategoryStruct.comp (zeroCocyclesIso A).hom (CategoryTheory.CategoryStruct.comp (shortComplexH0 A).f (CategoryTheory.CategoryStruct.comp φ.hom h))

theorem groupCohomology.cocyclesMap_zeroIsoCocycles_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) [DecidableEq G] [DecidableEq H] (x : CategoryTheory.ToType (cocycles A 0)) : (CategoryTheory.CategoryStruct.comp (iCocycles B 0) (zeroCochainsIso B).hom) ((CategoryTheory.ConcreteCategory.hom (cocyclesMap f φ 0)) x) = (CategoryTheory.CategoryStruct.comp (iCocycles A 0) (CategoryTheory.CategoryStruct.comp (zeroCochainsIso A).hom φ.hom)) x

@[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) [DecidableEq G] [DecidableEq H] : CategoryTheory.CategoryStruct.comp (cocyclesMap f φ 0) (CategoryTheory.CategoryStruct.comp (zeroCocyclesIso B).hom (shortComplexH0 B).f) = CategoryTheory.CategoryStruct.comp (zeroCocyclesIso A).hom (CategoryTheory.CategoryStruct.comp (shortComplexH0 A).f φ.hom)

Alias of groupCohomology.cocyclesMap_zeroIsoCocycles_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 --dZero--> Fun(H, A) --dOne--> Fun(H × H, A) to B --dZero--> Fun(G, B) --dOne--> Fun(G × G, B).

Equations

• groupCohomology.mapShortComplexH1 f φ = { τ₁ := φ.hom, τ₂ := groupCohomology.fOne f φ, τ₃ := groupCohomology.fTwo f φ, comm₁₂ := ⋯, comm₂₃ := ⋯ }

@[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 φ).τ₃ = fTwo 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 φ).τ₂ = fOne 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.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 ↥(oneCocycles A) ⟶ ModuleCat.of k ↥(oneCocycles 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).

Equations

• One or more equations did not get rendered due to their size.

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 (mapOneCocycles f φ) (shortComplexH1 B).moduleCatLeftHomologyData.i = CategoryTheory.CategoryStruct.comp (shortComplexH1 A).moduleCatLeftHomologyData.i (fOne f φ)

theorem groupCohomology.mapOneCocycles_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 (mapOneCocycles f φ) (CategoryTheory.CategoryStruct.comp (shortComplexH1 B).moduleCatLeftHomologyData.i h) = CategoryTheory.CategoryStruct.comp (shortComplexH1 A).moduleCatLeftHomologyData.i (CategoryTheory.CategoryStruct.comp (fOne f φ) h)

theorem groupCohomology.mapOneCocycles_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 ↥(oneCocycles A))) : (LinearMap.ker (ModuleCat.Hom.hom (shortComplexH1 B).g)).subtype ((CategoryTheory.ConcreteCategory.hom (mapOneCocycles 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

@[simp]

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 ↥(oneCocycles A))) : ⇑((CategoryTheory.ConcreteCategory.hom (mapOneCocycles f φ)) x) = (CategoryTheory.ConcreteCategory.hom (fOne f φ)) ⇑x

@[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 (mapOneCocycles f φ) (shortComplexH1 B).moduleCatLeftHomologyData.i = CategoryTheory.CategoryStruct.comp (shortComplexH1 A).moduleCatLeftHomologyData.i (fOne f φ)

Alias of groupCohomology.mapOneCocycles_comp_i.

@[simp]

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) [DecidableEq G] [DecidableEq H] : CategoryTheory.CategoryStruct.comp (cocyclesMap f φ 1) (isoOneCocycles B).hom = CategoryTheory.CategoryStruct.comp (isoOneCocycles A).hom (mapOneCocycles f φ)

@[simp]

theorem groupCohomology.cocyclesMap_comp_isoOneCocycles_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) [DecidableEq G] [DecidableEq H] {Z : ModuleCat k} (h : ModuleCat.of k ↥(oneCocycles B) ⟶ Z) : CategoryTheory.CategoryStruct.comp (cocyclesMap f φ 1) (CategoryTheory.CategoryStruct.comp (isoOneCocycles B).hom h) = CategoryTheory.CategoryStruct.comp (isoOneCocycles A).hom (CategoryTheory.CategoryStruct.comp (mapOneCocycles f φ) h)

@[simp]

theorem groupCohomology.cocyclesMap_comp_isoOneCocycles_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) [DecidableEq G] [DecidableEq H] (x : CategoryTheory.ToType (cocycles A 1)) : (CategoryTheory.ConcreteCategory.hom (isoOneCocycles B).hom) ((CategoryTheory.ConcreteCategory.hom (cocyclesMap f φ 1)) x) = (CategoryTheory.ConcreteCategory.hom (mapOneCocycles f φ)) ((CategoryTheory.ConcreteCategory.hom (isoOneCocycles A).hom) x)

@[simp]

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) : mapOneCocycles 1 φ = 0

@[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) [DecidableEq G] [DecidableEq H] (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).

Equations

• @groupCohomology.H1Map = @groupCohomology.map

@[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 : ℕ) [DecidableEq G] : 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] [DecidableEq G] [Group H] [DecidableEq H] [Group K] [DecidableEq 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] [DecidableEq 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) [DecidableEq G] [DecidableEq H] : CategoryTheory.CategoryStruct.comp (H1π A) (map f φ 1) = CategoryTheory.CategoryStruct.comp (mapOneCocycles 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) [DecidableEq G] [DecidableEq H] {Z : ModuleCat k} (h : groupCohomology B 1 ⟶ Z) : CategoryTheory.CategoryStruct.comp (H1π A) (CategoryTheory.CategoryStruct.comp (map f φ 1) h) = CategoryTheory.CategoryStruct.comp (mapOneCocycles 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) [DecidableEq G] [DecidableEq H] (x : CategoryTheory.ToType (ModuleCat.of k ↥(oneCocycles A))) : (CategoryTheory.ConcreteCategory.hom (map f φ 1)) ((CategoryTheory.ConcreteCategory.hom (H1π A)) x) = (CategoryTheory.ConcreteCategory.hom (H1π B)) ((CategoryTheory.ConcreteCategory.hom (mapOneCocycles 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) [DecidableEq G] [DecidableEq H] : CategoryTheory.CategoryStruct.comp (H1π A) (map f φ 1) = CategoryTheory.CategoryStruct.comp (mapOneCocycles f φ) (H1π B)

Alias of groupCohomology.H1π_comp_map.

@[simp]

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

@[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} [DecidableEq G] [DecidableEq H] (φ : (Action.res (ModuleCat k) 1).obj A ⟶ B) : map 1 φ 1 = 0

Alias of groupCohomology.map_1_one.

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

theorem groupCohomology.H1InfRes_f {k G : Type u} [CommRing k] [Group G] [DecidableEq G] (A : Rep k G) (S : Subgroup G) [S.Normal] [DecidableEq (G ⧸ S)] : (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] [DecidableEq G] (A : Rep k G) (S : Subgroup G) [S.Normal] [DecidableEq (G ⧸ S)] : (H1InfRes A S).X₁ = groupCohomology (A.quotientToInvariants S) 1

@[simp]

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

instance groupCohomology.instMonoModuleCatFH1InfRes {k G : Type u} [CommRing k] [Group G] [DecidableEq G] (A : Rep k G) (S : Subgroup G) [S.Normal] [DecidableEq (G ⧸ S)] : 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] [DecidableEq G] (A : Rep k G) (S : Subgroup G) [S.Normal] [DecidableEq (G ⧸ S)] : (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) --dOne--> Fun(H × H, A) --dTwo--> Fun(H × H × H, A) to Fun(G, B) --dOne--> Fun(G × G, B) --dTwo--> Fun(G × G × G, B).

Equations

• groupCohomology.mapShortComplexH2 f φ = { τ₁ := groupCohomology.fOne f φ, τ₂ := groupCohomology.fTwo f φ, τ₃ := groupCohomology.fThree f φ, comm₁₂ := ⋯, comm₂₃ := ⋯ }

@[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 φ).τ₁ = fOne 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 φ).τ₂ = fTwo 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 φ).τ₃ = fThree 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.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 ↥(twoCocycles A) ⟶ ModuleCat.of k ↥(twoCocycles 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).

Equations

• One or more equations did not get rendered due to their size.

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 (mapTwoCocycles f φ) (shortComplexH2 B).moduleCatLeftHomologyData.i = CategoryTheory.CategoryStruct.comp (shortComplexH2 A).moduleCatLeftHomologyData.i (fTwo f φ)

theorem groupCohomology.mapTwoCocycles_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 (mapTwoCocycles f φ) (CategoryTheory.CategoryStruct.comp (shortComplexH2 B).moduleCatLeftHomologyData.i h) = CategoryTheory.CategoryStruct.comp (shortComplexH2 A).moduleCatLeftHomologyData.i (CategoryTheory.CategoryStruct.comp (fTwo f φ) h)

theorem groupCohomology.mapTwoCocycles_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 ↥(twoCocycles A))) : (LinearMap.ker (ModuleCat.Hom.hom (shortComplexH2 B).g)).subtype ((CategoryTheory.ConcreteCategory.hom (mapTwoCocycles 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

@[simp]

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 ↥(twoCocycles A))) : ⇑((CategoryTheory.ConcreteCategory.hom (mapTwoCocycles f φ)) x) = (CategoryTheory.ConcreteCategory.hom (fTwo f φ)) ⇑x

@[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 (mapTwoCocycles f φ) (shortComplexH2 B).moduleCatLeftHomologyData.i = CategoryTheory.CategoryStruct.comp (shortComplexH2 A).moduleCatLeftHomologyData.i (fTwo f φ)

Alias of groupCohomology.mapTwoCocycles_comp_i.

@[simp]

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) [DecidableEq G] [DecidableEq H] : CategoryTheory.CategoryStruct.comp (cocyclesMap f φ 2) (isoTwoCocycles B).hom = CategoryTheory.CategoryStruct.comp (isoTwoCocycles A).hom (mapTwoCocycles f φ)

@[simp]

theorem groupCohomology.cocyclesMap_comp_isoTwoCocycles_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) [DecidableEq G] [DecidableEq H] {Z : ModuleCat k} (h : ModuleCat.of k ↥(twoCocycles B) ⟶ Z) : CategoryTheory.CategoryStruct.comp (cocyclesMap f φ 2) (CategoryTheory.CategoryStruct.comp (isoTwoCocycles B).hom h) = CategoryTheory.CategoryStruct.comp (isoTwoCocycles A).hom (CategoryTheory.CategoryStruct.comp (mapTwoCocycles f φ) h)

@[simp]

theorem groupCohomology.cocyclesMap_comp_isoTwoCocycles_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) [DecidableEq G] [DecidableEq H] (x : CategoryTheory.ToType (cocycles A 2)) : (CategoryTheory.ConcreteCategory.hom (isoTwoCocycles B).hom) ((CategoryTheory.ConcreteCategory.hom (cocyclesMap f φ 2)) x) = (CategoryTheory.ConcreteCategory.hom (mapTwoCocycles f φ)) ((CategoryTheory.ConcreteCategory.hom (isoTwoCocycles A).hom) x)

@[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) [DecidableEq G] [DecidableEq H] (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).

Equations

• @groupCohomology.H2Map = @groupCohomology.map

@[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 : ℕ) [DecidableEq G] : 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] [DecidableEq G] [Group H] [DecidableEq H] [Group K] [DecidableEq 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] [DecidableEq 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) [DecidableEq G] [DecidableEq H] : CategoryTheory.CategoryStruct.comp (H2π A) (map f φ 2) = CategoryTheory.CategoryStruct.comp (mapTwoCocycles 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) [DecidableEq G] [DecidableEq H] {Z : ModuleCat k} (h : groupCohomology B 2 ⟶ Z) : CategoryTheory.CategoryStruct.comp (H2π A) (CategoryTheory.CategoryStruct.comp (map f φ 2) h) = CategoryTheory.CategoryStruct.comp (mapTwoCocycles 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) [DecidableEq G] [DecidableEq H] (x : CategoryTheory.ToType (ModuleCat.of k ↥(twoCocycles A))) : (CategoryTheory.ConcreteCategory.hom (map f φ 2)) ((CategoryTheory.ConcreteCategory.hom (H2π A)) x) = (CategoryTheory.ConcreteCategory.hom (H2π B)) ((CategoryTheory.ConcreteCategory.hom (mapTwoCocycles 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) [DecidableEq G] [DecidableEq H] : CategoryTheory.CategoryStruct.comp (H2π A) (map f φ 2) = CategoryTheory.CategoryStruct.comp (mapTwoCocycles f φ) (H2π B)

Alias of groupCohomology.H2π_comp_map.

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem groupCohomology.cochainsFunctor_obj (k G : Type u) [CommRing k] [Group G] [DecidableEq 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] [DecidableEq 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] [DecidableEq G] : (cochainsFunctor k G).PreservesZeroMorphisms

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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

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