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.HInfRes 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. In case n := 1, it is exact (see groupCohomology.H1InfRes_exact).

theorem groupCohomology.congr {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} {f₁ f₂ : G →* H} (h : f₁ = f₂) {φ : 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 k H} {B : Rep 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)).

Equations

• groupCohomology.cochainsMap f φ = { f := fun (i : ℕ) => ModuleCat.ofHom ((Rep.Hom.hom φ).compLeft (Fin i → G) ∘ₗ LinearMap.funLeft k ↑A fun (x : Fin i → G) => ⇑f ∘ x), comm' := ⋯ }

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

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

@[simp]

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

@[simp]

theorem groupCohomology.cochainsMap_id_f_hom_eq_compLeft {k G : Type u} [CommRing k] [Group G] {A B : Rep k G} (f : A ⟶ B) (i : ℕ) : ModuleCat.Hom.hom ((cochainsMap (MonoidHom.id G) f).f i) = (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 k K} {B : Rep k H} {C : Rep 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 k K} {B : Rep k H} {C : Rep 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.resMap g φ) ψ)) h = CategoryTheory.CategoryStruct.comp (cochainsMap f φ) (CategoryTheory.CategoryStruct.comp (cochainsMap g ψ) h)

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

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

@[simp]

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

theorem groupCohomology.cochainsMap_f_map_mono {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : 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 k G} (φ : A ⟶ B) [CategoryTheory.Mono φ] (i : ℕ) : CategoryTheory.Mono ((cochainsMap (MonoidHom.id G) φ).f i)

theorem groupCohomology.cochainsMap_f_map_epi {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : 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 k G} (φ : A ⟶ B) [CategoryTheory.Epi φ] (i : ℕ) : CategoryTheory.Epi ((cochainsMap (MonoidHom.id G) φ).f i)

@[reducible, inline]

noncomputable abbrev groupCohomology.cocyclesMap {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : 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)).

Equations

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

theorem groupCohomology.cochainsMap_congr {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} {f g : G →* H} {φ : Rep.res f A ⟶ B} {ψ : Rep.res g A ⟶ B} (hfg : f = g) (hφψ : (Rep.Hom.hom φ).toLinearMap = (Rep.Hom.hom ψ).toLinearMap) : cochainsMap f φ = cochainsMap g ψ

@[simp]

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

theorem groupCohomology.cocyclesMap_comp {k : Type u} [CommRing k] {G H K : Type u} [Group G] [Group H] [Group K] {A : Rep k K} {B : Rep k H} {C : Rep k G} (f : H →* K) (g : G →* H) (φ : 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 k K} {B : Rep k H} {C : Rep 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.resMap g φ) ψ) n) h = CategoryTheory.CategoryStruct.comp (cocyclesMap f φ n) (CategoryTheory.CategoryStruct.comp (cocyclesMap g ψ n) h)

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

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

@[reducible, inline]

noncomputable abbrev groupCohomology.map {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : 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)).

Equations

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

theorem groupCohomology.map_congr {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} {f g : G →* H} {φ : Rep.res f A ⟶ B} {ψ : Rep.res g A ⟶ B} (hfg : f = g) (hφψ : (Rep.Hom.hom φ).toLinearMap = (Rep.Hom.hom ψ).toLinearMap) (n : ℕ) : map f φ n = map g ψ n

theorem groupCohomology.π_map {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : 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 k H} {B : Rep 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 k H} {B : Rep 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 k G} (n : ℕ) : map (MonoidHom.id G) (CategoryTheory.CategoryStruct.id B) n = CategoryTheory.CategoryStruct.id (groupCohomology B n)

theorem groupCohomology.map_comp {k : Type u} [CommRing k] {G H K : Type u} [Group G] [Group H] [Group K] {A : Rep k K} {B : Rep k H} {C : Rep k G} (f : H →* K) (g : G →* H) (φ : 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 k K} {B : Rep k H} {C : Rep 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.resMap g φ) ψ) n) h = CategoryTheory.CategoryStruct.comp (map f φ n) (CategoryTheory.CategoryStruct.comp (map g ψ n) h)

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

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

theorem groupCohomology.map_eq_zero {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (n : ℕ) [NeZero n] (hf : f = 1) : map f φ n = 0

Let A be a representation of H, B be a representation of G, f : G →* H and φ : res f A ⟶ B. If f is the trivial morphism, the induced morphism is zero in group cohomology in nonzero degrees.

noncomputable def groupCohomology.mapIso {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (e : G ≃* H) (e' : ↑B ≃ₗ[k] ↑A) (he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e') (n : ℕ) : groupCohomology B n ≅ groupCohomology A n

The isomorphism between cohomology groups induced by a group isomorphism e : G ≃* H and a isomorphism between representations (restricted by e).

Equations

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

@[simp]

theorem groupCohomology.mapIso_hom {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (e : G ≃* H) (e' : ↑B ≃ₗ[k] ↑A) (he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e') (n : ℕ) : (mapIso e e' he n).hom = map (↑e.symm) (Rep.ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ }) n

@[simp]

theorem groupCohomology.mapIso_inv {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (e : G ≃* H) (e' : ↑B ≃ₗ[k] ↑A) (he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e') (n : ℕ) : (mapIso e e' he n).inv = map (↑e) (Rep.ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ }) n

@[reducible, inline]

noncomputable abbrev groupCohomology.cochainsMap₁ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : Rep.res f A ⟶ B) : ↧(H → ↑A) ⟶ ↧(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)).

Equations

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

@[reducible, inline]

noncomputable abbrev groupCohomology.cochainsMap₂ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : Rep.res f A ⟶ B) : ↧(H × H → ↑A) ⟶ ↧(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₂)).

Equations

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

@[reducible, inline]

noncomputable abbrev groupCohomology.cochainsMap₃ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : Rep.res f A ⟶ B) : ↧(H × H × H → ↑A) ⟶ ↧(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₃)).

Equations

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

@[simp]

theorem groupCohomology.cochainsMap_f_0_comp_cochainsIso₀ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : 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 k H} {B : Rep k G} (f : G →* H) (φ : Rep.res f A ⟶ B) {Z : ModuleCat k} (h : ↧↑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 k H} {B : Rep k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : (Fin 0 → H) → ↑A) : (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 k H} {B : Rep 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 k H} {B : Rep k G} (f : G →* H) (φ : Rep.res f A ⟶ B) {Z : ModuleCat k} (h : ↧(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 k H} {B : Rep k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : (Fin 1 → H) → ↑A) : (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 k H} {B : Rep 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 k H} {B : Rep k G} (f : G →* H) (φ : Rep.res f A ⟶ B) {Z : ModuleCat k} (h : ↧(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 k H} {B : Rep k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : (Fin 2 → H) → ↑A) : (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 k H} {B : Rep 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 k H} {B : Rep k G} (f : G →* H) (φ : Rep.res f A ⟶ B) {Z : ModuleCat k} (h : ↧(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 k H} {B : Rep k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : (Fin 3 → H) → ↑A) : (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 k H} {B : Rep 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 k H} {B : Rep 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 k H} {B : Rep 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 k G} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp (map (MonoidHom.id G) f 0) (H0Iso B).hom = CategoryTheory.CategoryStruct.comp (H0Iso A).hom ((Rep.invariantsFunctor k G).map f)

@[simp]

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

@[simp]

theorem groupCohomology.map_id_comp_H0Iso_hom_apply {k G : Type u} [CommRing k] [Group G] {A B : Rep k G} (f : A ⟶ B) (x : ↑(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 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 k H} {B : Rep 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 k H} {B : Rep 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 k H} {B : Rep 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 k H} {B : Rep 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).

Equations

• groupCohomology.mapShortComplexH1 f φ = { τ₁ := Rep.Hom.toModuleCatHom φ, τ₂ := groupCohomology.cochainsMap₁ f φ, τ₃ := groupCohomology.cochainsMap₂ f φ, comm₁₂ := ⋯, comm₂₃ := ⋯ }

@[simp]

theorem groupCohomology.mapShortComplexH1_τ₁ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : 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 k H} {B : Rep 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 k H} {B : Rep 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 k H} {B : Rep k G} (f : G →* H) : mapShortComplexH1 f 0 = 0

@[simp]

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

theorem groupCohomology.mapShortComplexH1_comp {k : Type u} [CommRing k] {G H K : Type u} [Group G] [Group H] [Group K] {A : Rep k K} {B : Rep k H} {C : Rep k G} (f : H →* K) (g : G →* H) (φ : 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 k K} {B : Rep k H} {C : Rep 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.resMap g φ) ψ)) h = CategoryTheory.CategoryStruct.comp (mapShortComplexH1 f φ) (CategoryTheory.CategoryStruct.comp (mapShortComplexH1 g ψ) h)

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

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

@[reducible, inline]

noncomputable abbrev groupCohomology.mapCocycles₁ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : Rep.res f A ⟶ B) : ↧↥(cocycles₁ A) ⟶ ↧↥(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).

Equations

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

theorem groupCohomology.mapCocycles₁_comp_i {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : 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 k H} {B : Rep 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 k H} {B : Rep 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 k H} {B : Rep k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : ↑↧↥(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 k H} {B : Rep 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 k H} {B : Rep k G} (f : G →* H) (φ : Rep.res f A ⟶ B) {Z : ModuleCat k} (h : ↧↥(cocycles₁ B) ⟶ Z) : CategoryTheory.CategoryStruct.comp (cocyclesMap f φ 1) (CategoryTheory.CategoryStruct.comp (isoCocycles₁ B).hom h) = CategoryTheory.CategoryStruct.comp (isoCocycles₁ A).hom (CategoryTheory.CategoryStruct.comp (mapCocycles₁ f φ) h)

@[simp]

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

@[simp]

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

@[implicit_reducible]

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

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

Equations

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

@[simp]

theorem groupCohomology.HInfRes_f {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] (n : ℕ) [NeZero n] : (HInfRes A S n).f = map (QuotientGroup.mk' S) (Rep.ofHom (A.ρ.quotientToInvariants_lift S)) n

@[simp]

theorem groupCohomology.HInfRes_X₃ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] (n : ℕ) [NeZero n] : (HInfRes A S n).X₃ = groupCohomology (Rep.res S.subtype A) n

@[simp]

theorem groupCohomology.HInfRes_X₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] (n : ℕ) [NeZero n] : (HInfRes A S n).X₁ = groupCohomology (A.quotientToInvariants S) n

@[simp]

theorem groupCohomology.HInfRes_g {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] (n : ℕ) [NeZero n] : (HInfRes A S n).g = map S.subtype (CategoryTheory.CategoryStruct.id (Rep.res S.subtype A)) n

@[simp]

theorem groupCohomology.HInfRes_X₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] (n : ℕ) [NeZero n] : (HInfRes A S n).X₂ = groupCohomology A n

@[reducible, inline]

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

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

Equations

• groupCohomology.H1InfRes A S = groupCohomology.HInfRes A S 1

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

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

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

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

noncomputable def groupCohomology.mapShortComplexH2 {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : 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).

Equations

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

@[simp]

theorem groupCohomology.mapShortComplexH2_τ₂ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : 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 k H} {B : Rep 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 k H} {B : Rep 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 k H} {B : Rep k G} (f : G →* H) : mapShortComplexH2 f 0 = 0

@[simp]

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

theorem groupCohomology.mapShortComplexH2_comp {k : Type u} [CommRing k] {G H K : Type u} [Group G] [Group H] [Group K] {A : Rep k K} {B : Rep k H} {C : Rep k G} (f : H →* K) (g : G →* H) (φ : 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 k K} {B : Rep k H} {C : Rep 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.resMap g φ) ψ)) h = CategoryTheory.CategoryStruct.comp (mapShortComplexH2 f φ) (CategoryTheory.CategoryStruct.comp (mapShortComplexH2 g ψ) h)

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

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

@[reducible, inline]

noncomputable abbrev groupCohomology.mapCocycles₂ {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : Rep.res f A ⟶ B) : ↧↥(cocycles₂ A) ⟶ ↧↥(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).

Equations

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

theorem groupCohomology.mapCocycles₂_comp_i {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : 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 k H} {B : Rep 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 k H} {B : Rep 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 k H} {B : Rep k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : ↑↧↥(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 k H} {B : Rep 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 k H} {B : Rep k G} (f : G →* H) (φ : Rep.res f A ⟶ B) {Z : ModuleCat k} (h : ↧↥(cocycles₂ B) ⟶ Z) : CategoryTheory.CategoryStruct.comp (cocyclesMap f φ 2) (CategoryTheory.CategoryStruct.comp (isoCocycles₂ B).hom h) = CategoryTheory.CategoryStruct.comp (isoCocycles₂ A).hom (CategoryTheory.CategoryStruct.comp (mapCocycles₂ f φ) h)

@[simp]

theorem groupCohomology.cocyclesMap_comp_isoCocycles₂_hom_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : 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 k H} {B : Rep 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 k H} {B : Rep 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 k H} {B : Rep 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 k G) (CochainComplex (ModuleCat k) ℕ)

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

Equations

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

@[simp]

theorem groupCohomology.cochainsFunctor_obj_d (k G : Type u) [CommRing k] [Group G] (A : Rep k G) (i j : ℕ) : ((cochainsFunctor k G).obj A).d i j = CochainComplex.of.d (fun (n : ℕ) => ↧((Fin n → G) → ↑A)) (fun (n : ℕ) => inhomogeneousCochains.d A n) i j

@[simp]

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

@[simp]

theorem groupCohomology.cochainsFunctor_obj_X_carrier (k G : Type u) [CommRing k] [Group G] (A : Rep k G) (n : ℕ) : ↑(((cochainsFunctor k G).obj A).X n) = ((Fin n → G) → ↑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 k G) (ModuleCat k)

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

Equations

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

@[simp]

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

@[simp]

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

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

noncomputable def groupCohomology.resNatTrans (k : Type u) {G H : Type u} [CommRing k] [Group G] [Group H] (f : G →* H) (n : ℕ) : functor k H n ⟶ (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)).

Equations

• groupCohomology.resNatTrans k f n = { app := fun (X : Rep k H) => groupCohomology.map f (CategoryTheory.CategoryStruct.id (Rep.res f X)) n, naturality := ⋯ }

@[simp]

theorem groupCohomology.resNatTrans_app (k : Type u) {G H : Type u} [CommRing k] [Group G] [Group H] (f : G →* H) (n : ℕ) (X : Rep k H) : (resNatTrans k f n).app X = map f (CategoryTheory.CategoryStruct.id (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).

Equations

• groupCohomology.infNatTrans k S n = { app := fun (A : Rep k G) => groupCohomology.map (QuotientGroup.mk' S) (Rep.ofHom (A.ρ.quotientToInvariants_lift S)) n, naturality := ⋯ }

@[simp]

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