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.

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

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

Equations

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

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

theorem groupCohomology.cochainsMap_f_hom {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (i : ℕ) : ModuleCat.Hom.hom ((cochainsMap f φ).f i) = (ModuleCat.Hom.hom φ.hom).compLeft (Fin i → G) ∘ₗ LinearMap.funLeft k ↑A.V fun (x : Fin i → G) => ⇑f ∘ x

@[simp]

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

@[simp]

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

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

theorem groupCohomology.cochainsMap_id_comp {k G : Type u} [CommRing k] [Group G] {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) (φ : (Action.res (ModuleCat k) f).obj 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) (φ : (Action.res (ModuleCat k) f).obj 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) (φ : (Action.res (ModuleCat k) f).obj 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.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) (φ : (Action.res (ModuleCat k) f).obj 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_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)

@[reducible, inline]

abbrev groupCohomology.fOne {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : (H → ↑A.V) →ₗ[k] G → ↑B.V

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

Equations

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

@[reducible, inline]

abbrev groupCohomology.fTwo {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : (H × H → ↑A.V) →ₗ[k] G × G → ↑B.V

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

Equations

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

@[reducible, inline]

abbrev groupCohomology.fThree {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : (H × H × H → ↑A.V) →ₗ[k] G × G × G → ↑B.V

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

Equations

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

theorem groupCohomology.cochainsMap_f_0_comp_zeroCochainsLequiv {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 0) (zeroCochainsLequiv B).toModuleIso.hom = CategoryTheory.CategoryStruct.comp (zeroCochainsLequiv A).toModuleIso.hom φ.hom

theorem groupCohomology.cochainsMap_f_0_comp_zeroCochainsLequiv_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) {Z : ModuleCat k} (h : ModuleCat.of k ↑B.V ⟶ Z) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 0) (CategoryTheory.CategoryStruct.comp (zeroCochainsLequiv B).toModuleIso.hom h) = CategoryTheory.CategoryStruct.comp (zeroCochainsLequiv A).toModuleIso.hom (CategoryTheory.CategoryStruct.comp φ.hom h)

theorem groupCohomology.cochainsMap_f_1_comp_oneCochainsLequiv {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 1) (oneCochainsLequiv B).toModuleIso.hom = CategoryTheory.CategoryStruct.comp (oneCochainsLequiv A).toModuleIso.hom (ModuleCat.ofHom (fOne f φ))

theorem groupCohomology.cochainsMap_f_1_comp_oneCochainsLequiv_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) {Z : ModuleCat k} (h : ModuleCat.of k (G → ↑B.V) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 1) (CategoryTheory.CategoryStruct.comp (oneCochainsLequiv B).toModuleIso.hom h) = CategoryTheory.CategoryStruct.comp (oneCochainsLequiv A).toModuleIso.hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (fOne f φ)) h)

theorem groupCohomology.cochainsMap_f_2_comp_twoCochainsLequiv {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 2) (twoCochainsLequiv B).toModuleIso.hom = CategoryTheory.CategoryStruct.comp (twoCochainsLequiv A).toModuleIso.hom (ModuleCat.ofHom (fTwo f φ))

theorem groupCohomology.cochainsMap_f_2_comp_twoCochainsLequiv_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) {Z : ModuleCat k} (h : ModuleCat.of k (G × G → ↑B.V) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 2) (CategoryTheory.CategoryStruct.comp (twoCochainsLequiv B).toModuleIso.hom h) = CategoryTheory.CategoryStruct.comp (twoCochainsLequiv A).toModuleIso.hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (fTwo f φ)) h)

theorem groupCohomology.cochainsMap_f_3_comp_threeCochainsLequiv {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 3) (threeCochainsLequiv B).toModuleIso.hom = CategoryTheory.CategoryStruct.comp (threeCochainsLequiv A).toModuleIso.hom (ModuleCat.ofHom (fThree f φ))

theorem groupCohomology.cochainsMap_f_3_comp_threeCochainsLequiv_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) {Z : ModuleCat k} (h : ModuleCat.of k (G × G × G → ↑B.V) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((cochainsMap f φ).f 3) (CategoryTheory.CategoryStruct.comp (threeCochainsLequiv B).toModuleIso.hom h) = CategoryTheory.CategoryStruct.comp (threeCochainsLequiv A).toModuleIso.hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (fThree f φ)) h)

@[reducible, inline]

abbrev groupCohomology.H0Map {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : H0 A ⟶ H0 B

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

Equations

• groupCohomology.H0Map f φ = ModuleCat.ofHom (LinearMap.codRestrict B.ρ.invariants (ModuleCat.Hom.hom φ.hom ∘ₗ A.ρ.invariants.subtype) ⋯)

@[simp]

theorem groupCohomology.H0Map_id {k H : Type u} [CommRing k] [Group H] {A : Rep k H} : H0Map (MonoidHom.id H) (CategoryTheory.CategoryStruct.id A) = CategoryTheory.CategoryStruct.id (H0 A)

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

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

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

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

theorem groupCohomology.H0Map_id_eq_invariantsFunctor_map {k G : Type u} [CommRing k] [Group G] {A B : Rep k G} (f : A ⟶ B) : H0Map (MonoidHom.id G) f = (Rep.invariantsFunctor k G).map f

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

@[simp]

theorem groupCohomology.cocyclesMap_comp_isoZeroCocycles_hom {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp (cocyclesMap f φ 0) (isoZeroCocycles B).hom = CategoryTheory.CategoryStruct.comp (isoZeroCocycles A).hom (H0Map f φ)

@[simp]

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

@[simp]

theorem groupCohomology.cocyclesMap_comp_isoZeroCocycles_hom_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (x : CategoryTheory.ToType (cocycles A 0)) : (CategoryTheory.ConcreteCategory.hom (isoZeroCocycles B).hom) ((CategoryTheory.ConcreteCategory.hom (cocyclesMap f φ 0)) x) = (LinearMap.codRestrict B.ρ.invariants (ModuleCat.Hom.hom φ.hom ∘ₗ A.ρ.invariants.subtype) ⋯) ((CategoryTheory.ConcreteCategory.hom (isoZeroCocycles A).hom) x)

@[simp]

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

@[simp]

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

@[simp]

theorem groupCohomology.map_comp_isoH0_hom_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (x : CategoryTheory.ToType (groupCohomology A 0)) : (CategoryTheory.ConcreteCategory.hom (isoH0 B).hom) ((CategoryTheory.ConcreteCategory.hom (map f φ 0)) x) = (LinearMap.codRestrict B.ρ.invariants (ModuleCat.Hom.hom φ.hom ∘ₗ A.ρ.invariants.subtype) ⋯) ((CategoryTheory.ConcreteCategory.hom (isoH0 A).hom) x)

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

@[reducible, inline]

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

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

Equations

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

@[simp]

theorem groupCohomology.mapOneCocycles_comp_subtype {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp (mapOneCocycles f φ) (ModuleCat.ofHom (oneCocycles B).subtype) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (oneCocycles A).subtype) (ModuleCat.ofHom (fOne f φ))

@[simp]

theorem groupCohomology.mapOneCocycles_comp_subtype_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) {Z : ModuleCat k} (h : ModuleCat.of k (G → ↑B.V) ⟶ Z) : CategoryTheory.CategoryStruct.comp (mapOneCocycles f φ) (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (oneCocycles B).subtype) h) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (oneCocycles A).subtype) (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (fOne f φ)) h)

@[simp]

theorem groupCohomology.mapOneCocycles_comp_subtype_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (x : CategoryTheory.ToType (ModuleCat.of k ↥(oneCocycles A))) : ⇑((CategoryTheory.ConcreteCategory.hom (mapOneCocycles f φ)) x) = ((ModuleCat.Hom.hom φ.hom).compLeft G) ((LinearMap.funLeft k ↑A.V ⇑f) ⇑x)

@[simp]

theorem groupCohomology.cocyclesMap_comp_isoOneCocycles_hom {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp (cocyclesMap f φ 1) (isoOneCocycles B).hom = CategoryTheory.CategoryStruct.comp (isoOneCocycles A).hom (mapOneCocycles f φ)

@[simp]

theorem groupCohomology.cocyclesMap_comp_isoOneCocycles_hom_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) {Z : ModuleCat k} (h : ModuleCat.of k ↥(oneCocycles B) ⟶ Z) : CategoryTheory.CategoryStruct.comp (cocyclesMap f φ 1) (CategoryTheory.CategoryStruct.comp (isoOneCocycles B).hom h) = CategoryTheory.CategoryStruct.comp (isoOneCocycles A).hom (CategoryTheory.CategoryStruct.comp (mapOneCocycles f φ) h)

@[simp]

theorem groupCohomology.cocyclesMap_comp_isoOneCocycles_hom_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (x : CategoryTheory.ToType (cocycles A 1)) : (CategoryTheory.ConcreteCategory.hom (isoOneCocycles B).hom) ((CategoryTheory.ConcreteCategory.hom (cocyclesMap f φ 1)) x) = (CategoryTheory.ConcreteCategory.hom (mapOneCocycles f φ)) ((CategoryTheory.ConcreteCategory.hom (isoOneCocycles A).hom) x)

@[reducible, inline]

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

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

Equations

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

@[simp]

theorem groupCohomology.H1Map_id {k H : Type u} [CommRing k] [Group H] {A : Rep k H} : H1Map (MonoidHom.id H) (CategoryTheory.CategoryStruct.id A) = CategoryTheory.CategoryStruct.id (H1 A)

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

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

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

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

@[simp]

theorem groupCohomology.H1π_comp_H1Map {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp (H1π A) (H1Map f φ) = CategoryTheory.CategoryStruct.comp (mapOneCocycles f φ) (H1π B)

@[simp]

theorem groupCohomology.H1π_comp_H1Map_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) {Z : ModuleCat k} (h : H1 B ⟶ Z) : CategoryTheory.CategoryStruct.comp (H1π A) (CategoryTheory.CategoryStruct.comp (H1Map f φ) h) = CategoryTheory.CategoryStruct.comp (mapOneCocycles f φ) (CategoryTheory.CategoryStruct.comp (H1π B) h)

@[simp]

theorem groupCohomology.H1π_comp_H1Map_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (x : CategoryTheory.ToType (ModuleCat.of k ↥(oneCocycles A))) : (CategoryTheory.ConcreteCategory.hom (H1Map f φ)) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((CategoryTheory.ConcreteCategory.hom (mapOneCocycles f φ)) x)

@[simp]

theorem groupCohomology.map_comp_isoH1_hom {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp (map f φ 1) (isoH1 B).hom = CategoryTheory.CategoryStruct.comp (isoH1 A).hom (H1Map f φ)

@[simp]

theorem groupCohomology.map_comp_isoH1_hom_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) {Z : ModuleCat k} (h : H1 B ⟶ Z) : CategoryTheory.CategoryStruct.comp (map f φ 1) (CategoryTheory.CategoryStruct.comp (isoH1 B).hom h) = CategoryTheory.CategoryStruct.comp (isoH1 A).hom (CategoryTheory.CategoryStruct.comp (H1Map f φ) h)

@[simp]

theorem groupCohomology.map_comp_isoH1_hom_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (x : CategoryTheory.ToType (groupCohomology A 1)) : (CategoryTheory.ConcreteCategory.hom (isoH1 B).hom) ((CategoryTheory.ConcreteCategory.hom (map f φ 1)) x) = (CategoryTheory.ConcreteCategory.hom (H1Map f φ)) ((CategoryTheory.ConcreteCategory.hom (isoH1 A).hom) x)

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

@[reducible, inline]

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

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

Equations

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

@[simp]

theorem groupCohomology.mapTwoCocycles_comp_subtype {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp (mapTwoCocycles f φ) (ModuleCat.ofHom (twoCocycles B).subtype) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (twoCocycles A).subtype) (ModuleCat.ofHom (fTwo f φ))

@[simp]

theorem groupCohomology.mapTwoCocycles_comp_subtype_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) {Z : ModuleCat k} (h : ModuleCat.of k (G × G → ↑B.V) ⟶ Z) : CategoryTheory.CategoryStruct.comp (mapTwoCocycles f φ) (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (twoCocycles B).subtype) h) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (twoCocycles A).subtype) (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (fTwo f φ)) h)

@[simp]

theorem groupCohomology.mapTwoCocycles_comp_subtype_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (x : CategoryTheory.ToType (ModuleCat.of k ↥(twoCocycles A))) : ⇑((CategoryTheory.ConcreteCategory.hom (mapTwoCocycles f φ)) x) = ((ModuleCat.Hom.hom φ.hom).compLeft (G × G)) ((LinearMap.funLeft k (↑A.V) (Prod.map ⇑f ⇑f)) ⇑x)

@[simp]

theorem groupCohomology.cocyclesMap_comp_isoTwoCocycles_hom {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp (cocyclesMap f φ 2) (isoTwoCocycles B).hom = CategoryTheory.CategoryStruct.comp (isoTwoCocycles A).hom (mapTwoCocycles f φ)

@[simp]

theorem groupCohomology.cocyclesMap_comp_isoTwoCocycles_hom_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) {Z : ModuleCat k} (h : ModuleCat.of k ↥(twoCocycles B) ⟶ Z) : CategoryTheory.CategoryStruct.comp (cocyclesMap f φ 2) (CategoryTheory.CategoryStruct.comp (isoTwoCocycles B).hom h) = CategoryTheory.CategoryStruct.comp (isoTwoCocycles A).hom (CategoryTheory.CategoryStruct.comp (mapTwoCocycles f φ) h)

@[simp]

theorem groupCohomology.cocyclesMap_comp_isoTwoCocycles_hom_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (x : CategoryTheory.ToType (cocycles A 2)) : (CategoryTheory.ConcreteCategory.hom (isoTwoCocycles B).hom) ((CategoryTheory.ConcreteCategory.hom (cocyclesMap f φ 2)) x) = (CategoryTheory.ConcreteCategory.hom (mapTwoCocycles f φ)) ((CategoryTheory.ConcreteCategory.hom (isoTwoCocycles A).hom) x)

@[reducible, inline]

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

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

Equations

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

@[simp]

theorem groupCohomology.H2Map_id {k H : Type u} [CommRing k] [Group H] {A : Rep k H} : H2Map (MonoidHom.id H) (CategoryTheory.CategoryStruct.id A) = CategoryTheory.CategoryStruct.id (H2 A)

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

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

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

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

@[simp]

theorem groupCohomology.H2π_comp_H2Map {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp (H2π A) (H2Map f φ) = CategoryTheory.CategoryStruct.comp (mapTwoCocycles f φ) (H2π B)

@[simp]

theorem groupCohomology.H2π_comp_H2Map_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) {Z : ModuleCat k} (h : H2 B ⟶ Z) : CategoryTheory.CategoryStruct.comp (H2π A) (CategoryTheory.CategoryStruct.comp (H2Map f φ) h) = CategoryTheory.CategoryStruct.comp (mapTwoCocycles f φ) (CategoryTheory.CategoryStruct.comp (H2π B) h)

@[simp]

theorem groupCohomology.H2π_comp_H2Map_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (x : CategoryTheory.ToType (ModuleCat.of k ↥(twoCocycles A))) : (CategoryTheory.ConcreteCategory.hom (H2Map f φ)) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((CategoryTheory.ConcreteCategory.hom (mapTwoCocycles f φ)) x)

@[simp]

theorem groupCohomology.map_comp_isoH2_hom {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) : CategoryTheory.CategoryStruct.comp (map f φ 2) (isoH2 B).hom = CategoryTheory.CategoryStruct.comp (isoH2 A).hom (H2Map f φ)

@[simp]

theorem groupCohomology.map_comp_isoH2_hom_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) {Z : ModuleCat k} (h : H2 B ⟶ Z) : CategoryTheory.CategoryStruct.comp (map f φ 2) (CategoryTheory.CategoryStruct.comp (isoH2 B).hom h) = CategoryTheory.CategoryStruct.comp (isoH2 A).hom (CategoryTheory.CategoryStruct.comp (H2Map f φ) h)

@[simp]

theorem groupCohomology.map_comp_isoH2_hom_apply {k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep k H} {B : Rep k G} (f : G →* H) (φ : (Action.res (ModuleCat k) f).obj A ⟶ B) (x : CategoryTheory.ToType (groupCohomology A 2)) : (CategoryTheory.ConcreteCategory.hom (isoH2 B).hom) ((CategoryTheory.ConcreteCategory.hom (map f φ 2)) x) = (CategoryTheory.ConcreteCategory.hom (H2Map f φ)) ((CategoryTheory.ConcreteCategory.hom (isoH2 A).hom) 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_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 (k G : Type u) [CommRing k] [Group G] (A : Rep k G) : (cochainsFunctor k G).obj A = inhomogeneousCochains A

instance groupCohomology.instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor {k G : Type u} [CommRing k] [Group G] : (cochainsFunctor k G).PreservesZeroMorphisms

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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