Functoriality of group homology

Given a commutative ring k, a group homomorphism f : G →* H, a k-linear G-representation A, a k-linear H-representation B, and a representation morphism A ⟶ Res(f)(B), we get a chain map inhomogeneousChains A ⟶ inhomogeneousChains B and hence maps on homology Hₙ(G, A) ⟶ Hₙ(H, B).

We also provide extra API for these maps in degrees 0, 1, 2.

Main definitions

• groupHomology.chainsMap f φ is the map inhomogeneousChains A ⟶ inhomogeneousChains B induced by a group homomorphism f : G →* H and a representation morphism φ : A ⟶ Res(f)(B).
• groupHomology.map f φ n is the map Hₙ(G, A) ⟶ Hₙ(H, B) induced by a group homomorphism f : G →* H and a representation morphism φ : A ⟶ Res(f)(B).

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

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

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

theorem groupHomology.chainsMap_f_hom {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ (Action.res (ModuleCat k) f).obj B) (i : ℕ) : ModuleCat.Hom.hom ((chainsMap f φ).f i) = Finsupp.mapRange.linearMap (ModuleCat.Hom.hom φ.hom) ∘ₗ Finsupp.lmapDomain (↑A.V) k fun (x : Fin i → G) => ⇑f ∘ x

theorem groupHomology.chainsMap_f {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ (Action.res (ModuleCat k) f).obj B) (i : ℕ) : (chainsMap f φ).f i = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Finsupp.lmapDomain (↑A.V) k fun (x : Fin i → G) => ⇑f ∘ x)) (ModuleCat.ofHom (Finsupp.mapRange.linearMap (ModuleCat.Hom.hom φ.hom)))

@[simp]

theorem groupHomology.lsingle_comp_chainsMap_f {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ (Action.res (ModuleCat k) f).obj B) (n : ℕ) (x : Fin n → G) : CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Finsupp.lsingle x)) ((chainsMap f φ).f n) = CategoryTheory.CategoryStruct.comp φ.hom (ModuleCat.ofHom (Finsupp.lsingle (⇑f ∘ x)))

@[simp]

theorem groupHomology.lsingle_comp_chainsMap_f_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ (Action.res (ModuleCat k) f).obj B) (n : ℕ) (x : Fin n → G) {Z : ModuleCat k} (h : (inhomogeneousChains B).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Finsupp.lsingle x)) (CategoryTheory.CategoryStruct.comp ((chainsMap f φ).f n) h) = CategoryTheory.CategoryStruct.comp φ.hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Finsupp.lsingle (⇑f ∘ x))) h)

theorem groupHomology.chainsMap_f_single {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ (Action.res (ModuleCat k) f).obj B) (n : ℕ) (x : Fin n → G) (a : ↑A.V) : (CategoryTheory.ConcreteCategory.hom ((chainsMap f φ).f n)) (Finsupp.single x a) = Finsupp.single (⇑f ∘ x) ((CategoryTheory.ConcreteCategory.hom φ.hom) a)

@[simp]

theorem groupHomology.chainsMap_id {k G : Type u} [CommRing k] [Group G] {A : Rep k G} : chainsMap (MonoidHom.id G) (CategoryTheory.CategoryStruct.id A) = CategoryTheory.CategoryStruct.id (inhomogeneousChains A)

@[simp]

theorem groupHomology.chainsMap_id_f_hom_eq_mapRange {k G : Type u} [CommRing k] [Group G] {A B : Rep k G} (i : ℕ) (φ : A ⟶ B) : ModuleCat.Hom.hom ((chainsMap (MonoidHom.id G) φ).f i) = Finsupp.mapRange.linearMap (ModuleCat.Hom.hom φ.hom)

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

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

@[simp]

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

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

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

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

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

@[reducible, inline]

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

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

@[simp]

theorem groupHomology.cyclesMap_id {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (n : ℕ) : cyclesMap (MonoidHom.id G) (CategoryTheory.CategoryStruct.id A) n = CategoryTheory.CategoryStruct.id (cycles A n)

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

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

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

@[reducible, inline]

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

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

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

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

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

@[simp]

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

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

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem groupHomology.chainsMap_f_0_comp_chainsIso₀_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ (Action.res (ModuleCat k) f).obj B) (x : CategoryTheory.ToType ((inhomogeneousChains A).X 0)) : (CategoryTheory.ConcreteCategory.hom (chainsIso₀ B).hom) ((CategoryTheory.ConcreteCategory.hom ((chainsMap f φ).f 0)) x) = (CategoryTheory.CategoryStruct.comp (chainsIso₀ A).hom φ.hom) x

@[simp]

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

@[simp]

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

@[simp]

theorem groupHomology.chainsMap_f_1_comp_chainsIso₁_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ (Action.res (ModuleCat k) f).obj B) (x : CategoryTheory.ToType ((inhomogeneousChains A).X 1)) : (CategoryTheory.ConcreteCategory.hom (chainsIso₁ B).hom) ((CategoryTheory.ConcreteCategory.hom ((chainsMap f φ).f 1)) x) = Finsupp.mapRange ⇑(ModuleCat.Hom.hom φ.hom) ⋯ (Finsupp.mapDomain (⇑f) ((CategoryTheory.ConcreteCategory.hom (chainsIso₁ A).hom) x))

@[simp]

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

@[simp]

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

@[simp]

theorem groupHomology.chainsMap_f_2_comp_chainsIso₂_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ (Action.res (ModuleCat k) f).obj B) (x : CategoryTheory.ToType ((inhomogeneousChains A).X 2)) : (CategoryTheory.ConcreteCategory.hom (chainsIso₂ B).hom) ((CategoryTheory.ConcreteCategory.hom ((chainsMap f φ).f 2)) x) = Finsupp.mapRange ⇑(ModuleCat.Hom.hom φ.hom) ⋯ (Finsupp.mapDomain (Prod.map ⇑f ⇑f) ((CategoryTheory.ConcreteCategory.hom (chainsIso₂ A).hom) x))

@[simp]

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

@[simp]

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

@[simp]

theorem groupHomology.chainsMap_f_3_comp_chainsIso₃_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ (Action.res (ModuleCat k) f).obj B) (x : CategoryTheory.ToType ((inhomogeneousChains A).X 3)) : (CategoryTheory.ConcreteCategory.hom (chainsIso₃ B).hom) ((CategoryTheory.ConcreteCategory.hom ((chainsMap f φ).f 3)) x) = Finsupp.mapRange ⇑(ModuleCat.Hom.hom φ.hom) ⋯ (Finsupp.mapDomain (Prod.map (⇑f) (Prod.map ⇑f ⇑f)) ((CategoryTheory.ConcreteCategory.hom (chainsIso₃ A).hom) x))

@[simp]

theorem groupHomology.cyclesMap_comp_cyclesIso₀_hom {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ (Action.res (ModuleCat k) f).obj B) : CategoryTheory.CategoryStruct.comp (cyclesMap f φ 0) (cyclesIso₀ B).hom = CategoryTheory.CategoryStruct.comp (cyclesIso₀ A).hom φ.hom

@[simp]

theorem groupHomology.cyclesMap_comp_cyclesIso₀_hom_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ (Action.res (ModuleCat k) f).obj B) {Z : ModuleCat k} (h : B.V ⟶ Z) : CategoryTheory.CategoryStruct.comp (cyclesMap f φ 0) (CategoryTheory.CategoryStruct.comp (cyclesIso₀ B).hom h) = CategoryTheory.CategoryStruct.comp (cyclesIso₀ A).hom (CategoryTheory.CategoryStruct.comp φ.hom h)

@[simp]

theorem groupHomology.cyclesMap_comp_cyclesIso₀_hom_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ (Action.res (ModuleCat k) f).obj B) (x : CategoryTheory.ToType (cycles A 0)) : (CategoryTheory.ConcreteCategory.hom (cyclesIso₀ B).hom) ((CategoryTheory.ConcreteCategory.hom (cyclesMap f φ 0)) x) = (CategoryTheory.CategoryStruct.comp (cyclesIso₀ A).hom φ.hom) x

@[simp]

theorem groupHomology.cyclesIso₀_inv_comp_cyclesMap {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ (Action.res (ModuleCat k) f).obj B) : CategoryTheory.CategoryStruct.comp (cyclesIso₀ A).inv (cyclesMap f φ 0) = CategoryTheory.CategoryStruct.comp φ.hom (cyclesIso₀ B).inv

@[simp]

theorem groupHomology.cyclesIso₀_inv_comp_cyclesMap_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ (Action.res (ModuleCat k) f).obj B) {Z : ModuleCat k} (h : cycles B 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (cyclesIso₀ A).inv (CategoryTheory.CategoryStruct.comp (cyclesMap f φ 0) h) = CategoryTheory.CategoryStruct.comp φ.hom (CategoryTheory.CategoryStruct.comp (cyclesIso₀ B).inv h)

@[simp]

theorem groupHomology.cyclesIso₀_inv_comp_cyclesMap_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ (Action.res (ModuleCat k) f).obj B) (x : CategoryTheory.ToType A.V) : (CategoryTheory.ConcreteCategory.hom (cyclesMap f φ 0)) ((CategoryTheory.ConcreteCategory.hom (cyclesIso₀ A).inv) x) = (CategoryTheory.ConcreteCategory.hom (cyclesIso₀ B).inv) ((CategoryTheory.ConcreteCategory.hom φ.hom) x)

@[simp]

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

@[simp]

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

@[simp]

theorem groupHomology.H0π_comp_map_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ (Action.res (ModuleCat k) f).obj B) (x : CategoryTheory.ToType A.V) : (CategoryTheory.ConcreteCategory.hom (map f φ 0)) ((CategoryTheory.ConcreteCategory.hom (H0π A)) x) = (CategoryTheory.ConcreteCategory.hom (H0π B)) ((CategoryTheory.ConcreteCategory.hom φ.hom) x)

@[simp]

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

@[simp]

theorem groupHomology.map_id_comp_H0Iso_hom_assoc {k G : Type u} [CommRing k] [Group G] {A B : Rep k G} (f : A ⟶ B) {Z : ModuleCat k} (h : (Rep.coinvariantsFunctor k G).obj B ⟶ 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.coinvariantsFunctor k G).map f) h)

@[simp]

theorem groupHomology.map_id_comp_H0Iso_hom_apply {k G : Type u} [CommRing k] [Group G] {A B : Rep k G} (f : A ⟶ B) (x : CategoryTheory.ToType (groupHomology A 0)) : (CategoryTheory.ConcreteCategory.hom (H0Iso B).hom) ((CategoryTheory.ConcreteCategory.hom (map (MonoidHom.id G) f 0)) x) = (Representation.Coinvariants.map A.ρ B.ρ (ModuleCat.Hom.hom f.hom) ⋯) ((CategoryTheory.ConcreteCategory.hom (H0Iso A).hom) x)

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem groupHomology.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) ψ)

@[reducible, inline]

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

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

theorem groupHomology.mapCycles₁_hom {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ (Action.res (ModuleCat k) f).obj B) : ModuleCat.Hom.hom (mapCycles₁ f φ) = (ModuleCat.Hom.hom (chainsMap₁ f φ)).restrict ⋯

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

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

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

@[simp]

theorem groupHomology.coe_mapCycles₁ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ (Action.res (ModuleCat k) f).obj B) (x : ↑(ModuleCat.of k ↥(cycles₁ A))) : ↑((CategoryTheory.ConcreteCategory.hom (mapCycles₁ f φ)) x) = (CategoryTheory.ConcreteCategory.hom (chainsMap₁ f φ)) ↑x

@[simp]

theorem groupHomology.cyclesMap_comp_isoCycles₁_hom {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ (Action.res (ModuleCat k) f).obj B) : CategoryTheory.CategoryStruct.comp (cyclesMap f φ 1) (isoCycles₁ B).hom = CategoryTheory.CategoryStruct.comp (isoCycles₁ A).hom (mapCycles₁ f φ)

@[simp]

theorem groupHomology.cyclesMap_comp_isoCycles₁_hom_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ (Action.res (ModuleCat k) f).obj B) {Z : ModuleCat k} (h : ModuleCat.of k ↥(cycles₁ B) ⟶ Z) : CategoryTheory.CategoryStruct.comp (cyclesMap f φ 1) (CategoryTheory.CategoryStruct.comp (isoCycles₁ B).hom h) = CategoryTheory.CategoryStruct.comp (isoCycles₁ A).hom (CategoryTheory.CategoryStruct.comp (mapCycles₁ f φ) h)

@[simp]

theorem groupHomology.cyclesMap_comp_isoCycles₁_hom_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ (Action.res (ModuleCat k) f).obj B) (x : CategoryTheory.ToType (cycles A 1)) : (CategoryTheory.ConcreteCategory.hom (isoCycles₁ B).hom) ((CategoryTheory.ConcreteCategory.hom (cyclesMap f φ 1)) x) = (CategoryTheory.ConcreteCategory.hom (mapCycles₁ f φ)) ((CategoryTheory.ConcreteCategory.hom (isoCycles₁ A).hom) x)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance groupHomology.mapCycles₁_quotientGroupMk'_epi {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] : CategoryTheory.Epi (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)

noncomputable def groupHomology.H1CoresCoinfOfTrivial {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] : CategoryTheory.ShortComplex (ModuleCat k)

Given a G-representation A on which a normal subgroup S ≤ G acts trivially, this is the short complex H₁(S, A) ⟶ H₁(G, A) ⟶ H₁(G ⧸ S, A).

@[simp]

theorem groupHomology.H1CoresCoinfOfTrivial_X₃ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] : (H1CoresCoinfOfTrivial A S).X₃ = H1 (A.ofQuotient S)

@[simp]

theorem groupHomology.H1CoresCoinfOfTrivial_X₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] : (H1CoresCoinfOfTrivial A S).X₁ = H1 ((Action.res (ModuleCat k) S.subtype).obj A)

@[simp]

theorem groupHomology.H1CoresCoinfOfTrivial_g {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] : (H1CoresCoinfOfTrivial A S).g = map (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv 1

@[simp]

theorem groupHomology.H1CoresCoinfOfTrivial_X₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] : (H1CoresCoinfOfTrivial A S).X₂ = H1 A

@[simp]

theorem groupHomology.H1CoresCoinfOfTrivial_f {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] : (H1CoresCoinfOfTrivial A S).f = map S.subtype (CategoryTheory.CategoryStruct.id ((Action.res (ModuleCat k) S.subtype).obj A)) 1

instance groupHomology.map_1_quotientGroupMk'_epi {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] : CategoryTheory.Epi (map (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv 1)

instance groupHomology.H1CoresCoinfOfTrivial_g_epi {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] : CategoryTheory.Epi (H1CoresCoinfOfTrivial A S).g

Given a G-representation A on which a normal subgroup S ≤ G acts trivially, the induced map H₁(G, A) ⟶ H₁(G ⧸ S, A) is an epimorphism.

theorem groupHomology.H1CoresCoinfOfTrivial_exact {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] : (H1CoresCoinfOfTrivial A S).Exact

Given a G-representation A on which a normal subgroup S ≤ G acts trivially, the short complex H₁(S, A) ⟶ H₁(G, A) ⟶ H₁(G ⧸ S, A) is exact.

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem groupHomology.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) ψ)

@[reducible, inline]

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

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

theorem groupHomology.mapCycles₂_hom {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ (Action.res (ModuleCat k) f).obj B) : ModuleCat.Hom.hom (mapCycles₂ f φ) = (ModuleCat.Hom.hom (chainsMap₂ f φ)).restrict ⋯

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

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

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

@[simp]

theorem groupHomology.coe_mapCycles₂ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ (Action.res (ModuleCat k) f).obj B) (x : ↑(ModuleCat.of k ↥(cycles₂ A))) : ↑((CategoryTheory.ConcreteCategory.hom (mapCycles₂ f φ)) x) = (CategoryTheory.ConcreteCategory.hom (chainsMap₂ f φ)) ↑x

@[simp]

theorem groupHomology.cyclesMap_comp_isoCycles₂_hom {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ (Action.res (ModuleCat k) f).obj B) : CategoryTheory.CategoryStruct.comp (cyclesMap f φ 2) (isoCycles₂ B).hom = CategoryTheory.CategoryStruct.comp (isoCycles₂ A).hom (mapCycles₂ f φ)

@[simp]

theorem groupHomology.cyclesMap_comp_isoCycles₂_hom_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ (Action.res (ModuleCat k) f).obj B) {Z : ModuleCat k} (h : ModuleCat.of k ↥(cycles₂ B) ⟶ Z) : CategoryTheory.CategoryStruct.comp (cyclesMap f φ 2) (CategoryTheory.CategoryStruct.comp (isoCycles₂ B).hom h) = CategoryTheory.CategoryStruct.comp (isoCycles₂ A).hom (CategoryTheory.CategoryStruct.comp (mapCycles₂ f φ) h)

@[simp]

theorem groupHomology.cyclesMap_comp_isoCycles₂_hom_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k G} {B : Rep k H} (f : G →* H) (φ : A ⟶ (Action.res (ModuleCat k) f).obj B) (x : CategoryTheory.ToType (cycles A 2)) : (CategoryTheory.ConcreteCategory.hom (isoCycles₂ B).hom) ((CategoryTheory.ConcreteCategory.hom (cyclesMap f φ 2)) x) = (CategoryTheory.ConcreteCategory.hom (mapCycles₂ f φ)) ((CategoryTheory.ConcreteCategory.hom (isoCycles₂ A).hom) x)

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def groupHomology.chainsFunctor (k G : Type u) [CommRing k] [Group G] : CategoryTheory.Functor (Rep k G) (ChainComplex (ModuleCat k) ℕ)

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

@[simp]

theorem groupHomology.chainsFunctor_obj (k G : Type u) [CommRing k] [Group G] (A : Rep k G) : (chainsFunctor k G).obj A = inhomogeneousChains A

@[simp]

theorem groupHomology.chainsFunctor_map (k G : Type u) [CommRing k] [Group G] {X✝ Y✝ : Rep k G} (f : X✝ ⟶ Y✝) : (chainsFunctor k G).map f = chainsMap (MonoidHom.id G) f

instance groupHomology.instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor (k G : Type u) [CommRing k] [Group G] : (chainsFunctor k G).PreservesZeroMorphisms

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

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

@[simp]

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

@[simp]

theorem groupHomology.functor_map (k G : Type u) [CommRing k] [Group G] (n : ℕ) {A B : Rep k G} (φ : A ⟶ B) : (functor k G n).map φ = map (MonoidHom.id G) φ n

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

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

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

@[simp]

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

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

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

@[simp]

theorem groupHomology.coinfNatTrans_app (k : Type u) {G : Type u} [CommRing k] [Group G] (S : Subgroup G) [S.Normal] (n : ℕ) (A : Rep k G) : (coinfNatTrans k S n).app A = map (QuotientGroup.mk' S) (A.mkQ (Representation.Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)) ⋯) n