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.{u_2, u, u} k H} {B : Rep.{u_2, u, u} k G} {f₁ f₂ : G →* H} (h : f₁ = f₂) {φ : Rep.res f₁ A ⟶ B} {T : Type u_1} (F : (f : G →* H) → (Rep.res f 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.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f 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_hom {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (i : ℕ) : ModuleCat.Hom.hom ((cochainsMap f φ).f i) = (Rep.Hom.hom φ).compLeft (Fin i → G) ∘ₗ LinearMap.funLeft k ↑A fun (x : Fin i → G) => ⇑f ∘ x

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

@[simp]

theorem groupCohomology.cochainsMap_id {k H : Type u} [CommRing k] [Group H] {A : Rep.{u, u, u} 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.{u, u, u} k G} (f : A ⟶ B) (i : ℕ) : ModuleCat.Hom.hom ((cochainsMap (MonoidHom.id G) f).f i) = (Rep.Hom.hom f).compLeft (Fin i → G)

theorem groupCohomology.cochainsMap_comp {k : Type u} [CommRing k] {G H K : Type u} [Group G] [Group H] [Group K] {A : Rep.{u, u, u} k K} {B : Rep.{u, u, u} k H} {C : Rep.{u, u, u} k G} (f : H →* K) (g : G →* H) (φ : Rep.res f A ⟶ B) (ψ : Rep.res g B ⟶ C) : cochainsMap (f.comp g) (CategoryTheory.CategoryStruct.comp ((Rep.resFunctor 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.{u, u, u} k K} {B : Rep.{u, u, u} k H} {C : Rep.{u, u, u} k G} (f : H →* K) (g : G →* H) (φ : Rep.res f A ⟶ B) (ψ : Rep.res g B ⟶ C) {Z : CochainComplex (ModuleCat k) ℕ} (h : inhomogeneousCochains C ⟶ Z) : CategoryTheory.CategoryStruct.comp (cochainsMap (f.comp g) (CategoryTheory.CategoryStruct.comp (Rep.ofHom { toLinearMap := ↑(Rep.Hom.hom φ), isIntertwining' := ⋯ }) ψ)) 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.{u, u, u} 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.{u, u, u} 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.{u, u, u} k H} {B : Rep.{u, u, u} 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.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f 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.{u, u, u} 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.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f 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.{u, u, u} 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.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f 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.{u, u, u} 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.{u, u, u} k K} {B : Rep.{u, u, u} k H} {C : Rep.{u, u, u} k G} (f : H →* K) (g : G →* H) (φ : Rep.res f A ⟶ B) (ψ : Rep.res g B ⟶ C) (n : ℕ) : cocyclesMap (f.comp g) (CategoryTheory.CategoryStruct.comp ((Rep.resFunctor 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.{u, u, u} k K} {B : Rep.{u, u, u} k H} {C : Rep.{u, u, u} k G} (f : H →* K) (g : G →* H) (φ : Rep.res f A ⟶ B) (ψ : Rep.res g B ⟶ C) (n : ℕ) {Z : ModuleCat k} (h : cocycles C n ⟶ Z) : CategoryTheory.CategoryStruct.comp (cocyclesMap (f.comp g) (CategoryTheory.CategoryStruct.comp (Rep.ofHom { toLinearMap := ↑(Rep.Hom.hom φ), isIntertwining' := ⋯ }) ψ) 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.{u, u, u} 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.{u, u, u} 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.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f 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.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f 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.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f 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.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (n : ℕ) (x : ↑(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.{u, u, u} 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.{u, u, u} k K} {B : Rep.{u, u, u} k H} {C : Rep.{u, u, u} k G} (f : H →* K) (g : G →* H) (φ : Rep.res f A ⟶ B) (ψ : Rep.res g B ⟶ C) (n : ℕ) : map (f.comp g) (CategoryTheory.CategoryStruct.comp ((Rep.resFunctor 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.{u, u, u} k K} {B : Rep.{u, u, u} k H} {C : Rep.{u, u, u} k G} (f : H →* K) (g : G →* H) (φ : Rep.res f A ⟶ B) (ψ : Rep.res g B ⟶ C) (n : ℕ) {Z : ModuleCat k} (h : groupCohomology C n ⟶ Z) : CategoryTheory.CategoryStruct.comp (map (f.comp g) (CategoryTheory.CategoryStruct.comp (Rep.ofHom { toLinearMap := ↑(Rep.Hom.hom φ), isIntertwining' := ⋯ }) ψ) 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.{u, u, u} 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.{u, u, u} 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.{u_1, u, u} k H} {B : Rep.{u_1, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) : ModuleCat.of k (H → ↑A) ⟶ ModuleCat.of k (G → ↑B)

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.{u_1, u, u} k H} {B : Rep.{u_1, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) : ModuleCat.of k (H × H → ↑A) ⟶ ModuleCat.of k (G × G → ↑B)

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.{u_1, u, u} k H} {B : Rep.{u_1, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) : ModuleCat.of k (H × H × H → ↑A) ⟶ ModuleCat.of k (G × G × G → ↑B)

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.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 0) (cochainsIso₀ B).hom = CategoryTheory.CategoryStruct.comp (cochainsIso₀ A).hom (Rep.Hom.toModuleCatHom φ)

@[simp]

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

@[simp]

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

@[simp]

theorem groupCohomology.cochainsMap_f_1_comp_cochainsIso₁ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f 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.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) {Z : ModuleCat k} (h : ModuleCat.of k (G → ↑B) ⟶ 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.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : ↑((inhomogeneousCochains A).X 1)) : (CategoryTheory.ConcreteCategory.hom (cochainsIso₁ B).hom) ((CategoryTheory.ConcreteCategory.hom ((cochainsMap f φ).f 1)) x) = ((Rep.Hom.hom φ).compLeft G) ((LinearMap.funLeft k ↑A ⇑f) ((CategoryTheory.ConcreteCategory.hom (cochainsIso₁ A).hom) x))

@[simp]

theorem groupCohomology.cochainsMap_f_2_comp_cochainsIso₂ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f 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.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) {Z : ModuleCat k} (h : ModuleCat.of k (G × G → ↑B) ⟶ 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.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : ↑((inhomogeneousCochains A).X 2)) : (CategoryTheory.ConcreteCategory.hom (cochainsIso₂ B).hom) ((CategoryTheory.ConcreteCategory.hom ((cochainsMap f φ).f 2)) x) = ((Rep.Hom.hom φ).compLeft (G × G)) ((LinearMap.funLeft k (↑A) (Prod.map ⇑f ⇑f)) ((CategoryTheory.ConcreteCategory.hom (cochainsIso₂ A).hom) x))

@[simp]

theorem groupCohomology.cochainsMap_f_3_comp_cochainsIso₃ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f 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.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) {Z : ModuleCat k} (h : ModuleCat.of k (G × G × G → ↑B) ⟶ 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.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : ↑((inhomogeneousCochains A).X 3)) : (CategoryTheory.ConcreteCategory.hom (cochainsIso₃ B).hom) ((CategoryTheory.ConcreteCategory.hom ((cochainsMap f φ).f 3)) x) = ((Rep.Hom.hom φ).compLeft (G × G × G)) ((LinearMap.funLeft k (↑A) (Prod.map (⇑f) (Prod.map ⇑f ⇑f))) ((CategoryTheory.ConcreteCategory.hom (cochainsIso₃ A).hom) x))

@[simp]

theorem groupCohomology.map_H0Iso_hom_f {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f 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 (Rep.Hom.toModuleCatHom φ))

@[simp]

theorem groupCohomology.map_H0Iso_hom_f_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f 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 (Rep.Hom.toModuleCatHom φ) h))

@[simp]

theorem groupCohomology.map_H0Iso_hom_f_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : ↑(groupCohomology A 0)) : (CategoryTheory.ConcreteCategory.hom (shortComplexH0 B).f) ((CategoryTheory.ConcreteCategory.hom (H0Iso B).hom) ((CategoryTheory.ConcreteCategory.hom (map f φ 0)) x)) = (Rep.Hom.hom φ).toLinearMap ((CategoryTheory.ConcreteCategory.hom (shortComplexH0 A).f) ((CategoryTheory.ConcreteCategory.hom (H0Iso A).hom) x))

@[simp]

theorem groupCohomology.map_id_comp_H0Iso_hom {k G : Type u} [CommRing k] [Group G] {A B : Rep.{u, u, u} 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.{u, u, u} 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.{u, u, u} k G} (f : A ⟶ B) (x : ↑(groupCohomology A 0)) : (CategoryTheory.ConcreteCategory.hom (H0Iso B).hom) ((CategoryTheory.ConcreteCategory.hom (map (MonoidHom.id G) f 0)) x) = (LinearMap.codRestrict B.ρ.invariants ((Rep.Hom.hom f).toLinearMap ∘ₗ A.ρ.invariants.subtype) ⋯) ((CategoryTheory.ConcreteCategory.hom (H0Iso A).hom) x)

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

theorem groupCohomology.cocyclesMap_cocyclesIso₀_hom_f {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f 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 (Rep.Hom.toModuleCatHom φ))

theorem groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f 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 (Rep.Hom.toModuleCatHom φ) h))

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

noncomputable def groupCohomology.mapShortComplexH1 {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{max u u_1, u, u} k H} {B : Rep.{max u u_1, u, u} k G} (f : G →* H) (φ : Rep.res f 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.{max u u_1, u, u} k H} {B : Rep.{max u u_1, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) : (mapShortComplexH1 f φ).τ₁ = Rep.Hom.toModuleCatHom φ

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem groupCohomology.mapShortComplexH1_id {k H : Type u} [CommRing k] [Group H] {A : Rep.{max u u_1, u, u} 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.{max u u_1, u, u} k K} {B : Rep.{max u u_1, u, u} k H} {C : Rep.{max u u_1, u, u} k G} (f : H →* K) (g : G →* H) (φ : Rep.res f A ⟶ B) (ψ : Rep.res g B ⟶ C) : mapShortComplexH1 (f.comp g) (CategoryTheory.CategoryStruct.comp ((Rep.resFunctor 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.{max u u_1, u, u} k K} {B : Rep.{max u u_1, u, u} k H} {C : Rep.{max u u_1, u, u} k G} (f : H →* K) (g : G →* H) (φ : Rep.res f A ⟶ B) (ψ : Rep.res g B ⟶ C) {Z : CategoryTheory.ShortComplex (ModuleCat k)} (h : shortComplexH1 C ⟶ Z) : CategoryTheory.CategoryStruct.comp (mapShortComplexH1 (f.comp g) (CategoryTheory.CategoryStruct.comp (Rep.ofHom { toLinearMap := ↑(Rep.Hom.hom φ), isIntertwining' := ⋯ }) ψ)) 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.{max u u_1, u, u} 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.{max u u_1, u, u} 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.{max u u_1, u, u} k H} {B : Rep.{max u u_1, u, u} k G} (f : G →* H) (φ : Rep.res f 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).

theorem groupCohomology.mapCocycles₁_comp_i {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{max u u_1, u, u} k H} {B : Rep.{max u u_1, u, u} k G} (f : G →* H) (φ : Rep.res f 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.{max u u_1, u, u} k H} {B : Rep.{max u u_1, u, u} k G} (f : G →* H) (φ : Rep.res f 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.{max u u_1, u, u} k H} {B : Rep.{max u u_1, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : ↥(cocycles₁ A)) : (ModuleCat.Hom.hom (shortComplexH1 B).g).ker.subtype ((CategoryTheory.ConcreteCategory.hom (mapCocycles₁ f φ)) x) = ((Rep.Hom.hom φ).compLeft G) ((LinearMap.funLeft k ↑A ⇑f) ((ModuleCat.Hom.hom (shortComplexH1 A).g).ker.subtype x))

@[simp]

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

@[simp]

theorem groupCohomology.cocyclesMap_comp_isoCocycles₁_hom {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f 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.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f 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.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : ↑(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)

@[simp]

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

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

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

Alias of groupCohomology.map_id.

@[simp]

theorem groupCohomology.H1π_comp_map {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f 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.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f 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.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : ↥(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)

@[simp]

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

noncomputable def groupCohomology.H1InfRes {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} 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.{u, u, u} k G) (S : Subgroup G) [S.Normal] : (H1InfRes A S).X₂ = groupCohomology A 1

@[simp]

theorem groupCohomology.H1InfRes_f {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [S.Normal] : (H1InfRes A S).f = map (QuotientGroup.mk' S) (Rep.ofHom (A.ρ.quotientToInvariants_lift S)) 1

@[simp]

theorem groupCohomology.H1InfRes_X₁ {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} 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.{u, u, u} k G) (S : Subgroup G) [S.Normal] : (H1InfRes A S).X₃ = groupCohomology (Rep.res S.subtype A) 1

@[simp]

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

instance groupCohomology.instMonoModuleCatFH1InfRes {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} 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.{u, u, u} 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.{u_1, u, u} k H} {B : Rep.{u_1, u, u} k G} (f : G →* H) (φ : Rep.res f 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.{u_1, u, u} k H} {B : Rep.{u_1, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) : (mapShortComplexH2 f φ).τ₃ = cochainsMap₃ f φ

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem groupCohomology.mapShortComplexH2_id {k H : Type u} [CommRing k] [Group H] {A : Rep.{u_1, u, u} 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.{u_1, u, u} k K} {B : Rep.{u_1, u, u} k H} {C : Rep.{u_1, u, u} k G} (f : H →* K) (g : G →* H) (φ : Rep.res f A ⟶ B) (ψ : Rep.res g B ⟶ C) : mapShortComplexH2 (f.comp g) (CategoryTheory.CategoryStruct.comp ((Rep.resFunctor 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.{u_1, u, u} k K} {B : Rep.{u_1, u, u} k H} {C : Rep.{u_1, u, u} k G} (f : H →* K) (g : G →* H) (φ : Rep.res f A ⟶ B) (ψ : Rep.res g B ⟶ C) {Z : CategoryTheory.ShortComplex (ModuleCat k)} (h : shortComplexH2 C ⟶ Z) : CategoryTheory.CategoryStruct.comp (mapShortComplexH2 (f.comp g) (CategoryTheory.CategoryStruct.comp (Rep.ofHom { toLinearMap := ↑(Rep.Hom.hom φ), isIntertwining' := ⋯ }) ψ)) 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.{u_1, u, u} 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.{u_1, u, u} 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.{u_1, u, u} k H} {B : Rep.{u_1, u, u} k G} (f : G →* H) (φ : Rep.res f 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).

theorem groupCohomology.mapCocycles₂_comp_i {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u_1, u, u} k H} {B : Rep.{u_1, u, u} k G} (f : G →* H) (φ : Rep.res f 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.{u_1, u, u} k H} {B : Rep.{u_1, u, u} k G} (f : G →* H) (φ : Rep.res f 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.{u_1, u, u} k H} {B : Rep.{u_1, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : ↥(cocycles₂ A)) : (ModuleCat.Hom.hom (shortComplexH2 B).g).ker.subtype ((CategoryTheory.ConcreteCategory.hom (mapCocycles₂ f φ)) x) = ((Rep.Hom.hom φ).compLeft (G × G)) ((LinearMap.funLeft k (↑A) (Prod.map ⇑f ⇑f)) ((ModuleCat.Hom.hom (shortComplexH2 A).g).ker.subtype x))

@[simp]

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

@[simp]

theorem groupCohomology.cocyclesMap_comp_isoCocycles₂_hom {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f 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.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f 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.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : ↑(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)

@[simp]

theorem groupCohomology.H2π_comp_map {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f 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.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f 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.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : ↥(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)

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

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

@[simp]

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

@[simp]

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

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.{u, u, u} 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.{u, u, u} 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.{u, u, u} 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 ⟶ (Rep.resFunctor 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.{u, u, u} k H) : (resNatTrans k f n).app X = map f (CategoryTheory.CategoryStruct.id (Rep.res f 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.{u, u, u} k G) : (infNatTrans k S n).app A = map (QuotientGroup.mk' S) (Rep.ofHom (A.ρ.quotientToInvariants_lift S)) n