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

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

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

Equations

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

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

Equations

• groupHomology.cyclesMap f φ n = HomologicalComplex.cyclesMap (groupHomology.chainsMap f φ) n

@[simp]

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

Equations

• groupHomology.map f φ n = HomologicalComplex.homologyMap (groupHomology.chainsMap f φ) n

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