The low-degree cohomology of a k-linear G-representation

Let k be a commutative ring and G a group. This file contains specialised API for the cocycles and group cohomology of a k-linear G-representation A in degrees 0, 1 and 2.

In Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean, we define the nth group cohomology of A to be the cohomology of a complex inhomogeneousCochains A, whose objects are (Fin n → G) → A; this is unnecessarily unwieldy in low degree. Here, meanwhile, we define the one and two cocycles and coboundaries as submodules of Fun(G, A) and Fun(G × G, A), and provide maps to H1 and H2.

We also show that when the representation on A is trivial, H¹(G, A) ≃ Hom(G, A).

Given an additive or multiplicative abelian group A with an appropriate scalar action of G, we provide support for turning a function f : G → A satisfying the 1-cocycle identity into an element of the cocycles₁ of the representation on A (or Additive A) corresponding to the scalar action. We also do this for 1-coboundaries, 2-cocycles and 2-coboundaries. The multiplicative case, starting with the section IsMulCocycle, just mirrors the additive case; unfortunately @[to_additive] can't deal with scalar actions.

The file also contains an identification between the definitions in Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean, groupCohomology.cocycles A n, and the cocyclesₙ in this file, for n = 0, 1, 2.

Main definitions

• groupCohomology.H0Iso A: isomorphism between H⁰(G, A) and the invariants Aᴳ of the G-representation on A.
• groupCohomology.H1π A: epimorphism from the 1-cocycles (i.e. Z¹(G, A) := Ker(d¹ : Fun(G, A) → Fun(G², A)) to H¹(G, A).
• groupCohomology.H2π A: epimorphism from the 2-cocycles (i.e. Z²(G, A) := Ker(d² : Fun(G², A) → Fun(G³, A)) to H²(G, A).
• groupCohomology.H1IsoOfIsTrivial: the isomorphism H¹(G, A) ≅ Hom(G, A) when the representation on A is trivial.

TODO

• The relationship between H2 and group extensions
• Nonabelian group cohomology

def groupCohomology.cochainsIso₀ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (inhomogeneousCochains A).X 0 ≅ A.V

The 0th object in the complex of inhomogeneous cochains of A : Rep k G is isomorphic to A as a k-module.

Equations

• groupCohomology.cochainsIso₀ A = (LinearEquiv.funUnique (Fin 0 → G) k ↑A.V).toModuleIso

def groupCohomology.cochainsIso₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (inhomogeneousCochains A).X 1 ≅ ModuleCat.of k (G → ↑A.V)

The 1st object in the complex of inhomogeneous cochains of A : Rep k G is isomorphic to Fun(G, A) as a k-module.

Equations

• groupCohomology.cochainsIso₁ A = (LinearEquiv.funCongrLeft k (↑A.V) (Equiv.funUnique (Fin 1) G)).toModuleIso.symm

def groupCohomology.cochainsIso₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (inhomogeneousCochains A).X 2 ≅ ModuleCat.of k (G × G → ↑A.V)

The 2nd object in the complex of inhomogeneous cochains of A : Rep k G is isomorphic to Fun(G², A) as a k-module.

Equations

• groupCohomology.cochainsIso₂ A = (LinearEquiv.funCongrLeft k (↑A.V) (piFinTwoEquiv fun (x : Fin 2) => G)).toModuleIso.symm

def groupCohomology.cochainsIso₃ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (inhomogeneousCochains A).X 3 ≅ ModuleCat.of k (G × G × G → ↑A.V)

The 3rd object in the complex of inhomogeneous cochains of A : Rep k G is isomorphic to Fun(G³, A) as a k-module.

Equations

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

def groupCohomology.d₀₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : A.V ⟶ ModuleCat.of k (G → ↑A.V)

The 0th differential in the complex of inhomogeneous cochains of A : Rep k G, as a k-linear map A → Fun(G, A). It sends (a, g) ↦ ρ_A(g)(a) - a.

Equations

• groupCohomology.d₀₁ A = ModuleCat.ofHom { toFun := fun (m : ↑A.1) (g : G) => (A.ρ g) m - m, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem groupCohomology.d₀₁_hom_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (m : ↑A.1) (g : G) : (ModuleCat.Hom.hom (d₀₁ A)) m g = (A.ρ g) m - m

theorem groupCohomology.d₀₁_ker_eq_invariants {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (ModuleCat.Hom.hom (d₀₁ A)).ker = A.ρ.invariants

@[simp]

theorem groupCohomology.d₀₁_eq_zero {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] : d₀₁ A = 0

@[simp]

theorem groupCohomology.subtype_comp_d₀₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom A.ρ.invariants.subtype) (d₀₁ A) = 0

@[simp]

theorem groupCohomology.subtype_comp_d₀₁_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : ModuleCat.of k (G → ↑A.V) ⟶ Z) : CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom A.ρ.invariants.subtype) (CategoryTheory.CategoryStruct.comp (d₀₁ A) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem groupCohomology.subtype_comp_d₀₁_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : CategoryTheory.ToType (ModuleCat.of k ↥A.ρ.invariants)) : (CategoryTheory.ConcreteCategory.hom (d₀₁ A)) ↑x = 0

def groupCohomology.d₁₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : ModuleCat.of k (G → ↑A.V) ⟶ ModuleCat.of k (G × G → ↑A.V)

The 1st differential in the complex of inhomogeneous cochains of A : Rep k G, as a k-linear map Fun(G, A) → Fun(G × G, A). It sends (f, (g₁, g₂)) ↦ ρ_A(g₁)(f(g₂)) - f(g₁g₂) + f(g₁).

Equations

• groupCohomology.d₁₂ A = ModuleCat.ofHom { toFun := fun (f : G → ↑A.V) (g : G × G) => (A.ρ g.1) (f g.2) - f (g.1 * g.2) + f g.1, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem groupCohomology.d₁₂_hom_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (f : G → ↑A.V) (g : G × G) : (ModuleCat.Hom.hom (d₁₂ A)) f g = (A.ρ g.1) (f g.2) - f (g.1 * g.2) + f g.1

def groupCohomology.d₂₃ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : ModuleCat.of k (G × G → ↑A.V) ⟶ ModuleCat.of k (G × G × G → ↑A.V)

The 2nd differential in the complex of inhomogeneous cochains of A : Rep k G, as a k-linear map Fun(G × G, A) → Fun(G × G × G, A). It sends (f, (g₁, g₂, g₃)) ↦ ρ_A(g₁)(f(g₂, g₃)) - f(g₁g₂, g₃) + f(g₁, g₂g₃) - f(g₁, g₂).

Equations

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

@[simp]

theorem groupCohomology.d₂₃_hom_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (f : G × G → ↑A.V) (g : G × G × G) : (ModuleCat.Hom.hom (d₂₃ A)) f g = (A.ρ g.1) (f g.2) - f (g.1 * g.2.1, g.2.2) + f (g.1, g.2.1 * g.2.2) - f (g.1, g.2.1)

theorem groupCohomology.comp_d₀₁_eq {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (cochainsIso₀ A).hom (d₀₁ A) = CategoryTheory.CategoryStruct.comp ((inhomogeneousCochains A).d 0 1) (cochainsIso₁ A).hom

Let C(G, A) denote the complex of inhomogeneous cochains of A : Rep k G. This lemma says d₀₁ gives a simpler expression for the 0th differential: that is, the following square commutes:

  C⁰(G, A) --d 0 1--> C¹(G, A)
  |                     |
  |                     |
  |                     |
  v                     v
  A ------d₀₁-----> Fun(G, A)

where the vertical arrows are cochainsIso₀ and cochainsIso₁ respectively.

@[simp]

theorem groupCohomology.eq_d₀₁_comp_inv {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (cochainsIso₀ A).inv ((inhomogeneousCochains A).d 0 1) = CategoryTheory.CategoryStruct.comp (d₀₁ A) (cochainsIso₁ A).inv

@[simp]

theorem groupCohomology.eq_d₀₁_comp_inv_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : (inhomogeneousCochains A).X 1 ⟶ Z) : CategoryTheory.CategoryStruct.comp (cochainsIso₀ A).inv (CategoryTheory.CategoryStruct.comp ((inhomogeneousCochains A).d 0 1) h) = CategoryTheory.CategoryStruct.comp (d₀₁ A) (CategoryTheory.CategoryStruct.comp (cochainsIso₁ A).inv h)

@[simp]

theorem groupCohomology.eq_d₀₁_comp_inv_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : CategoryTheory.ToType A.V) : (CategoryTheory.ConcreteCategory.hom ((inhomogeneousCochains A).d 0 1)) ((CategoryTheory.ConcreteCategory.hom (cochainsIso₀ A).inv) x) = (CategoryTheory.ConcreteCategory.hom (cochainsIso₁ A).inv) ((CategoryTheory.ConcreteCategory.hom (d₀₁ A)) x)

theorem groupCohomology.comp_d₁₂_eq {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (cochainsIso₁ A).hom (d₁₂ A) = CategoryTheory.CategoryStruct.comp ((inhomogeneousCochains A).d 1 2) (cochainsIso₂ A).hom

Let C(G, A) denote the complex of inhomogeneous cochains of A : Rep k G. This lemma says d₁₂ gives a simpler expression for the 1st differential: that is, the following square commutes:

  C¹(G, A) ---d 1 2---> C²(G, A)
    |                      |
    |                      |
    |                      |
    v                      v
  Fun(G, A) --d₁₂--> Fun(G × G, A)

where the vertical arrows are cochainsIso₁ and cochainsIso₂ respectively.

@[simp]

theorem groupCohomology.eq_d₁₂_comp_inv {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (cochainsIso₁ A).inv ((inhomogeneousCochains A).d 1 2) = CategoryTheory.CategoryStruct.comp (d₁₂ A) (cochainsIso₂ A).inv

@[simp]

theorem groupCohomology.eq_d₁₂_comp_inv_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : (inhomogeneousCochains A).X 2 ⟶ Z) : CategoryTheory.CategoryStruct.comp (cochainsIso₁ A).inv (CategoryTheory.CategoryStruct.comp ((inhomogeneousCochains A).d 1 2) h) = CategoryTheory.CategoryStruct.comp (d₁₂ A) (CategoryTheory.CategoryStruct.comp (cochainsIso₂ A).inv h)

@[simp]

theorem groupCohomology.eq_d₁₂_comp_inv_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : CategoryTheory.ToType (ModuleCat.of k (G → ↑A.V))) : (CategoryTheory.ConcreteCategory.hom ((inhomogeneousCochains A).d 1 2)) ((CategoryTheory.ConcreteCategory.hom (cochainsIso₁ A).inv) x) = (CategoryTheory.ConcreteCategory.hom (cochainsIso₂ A).inv) ((CategoryTheory.ConcreteCategory.hom (d₁₂ A)) x)

theorem groupCohomology.comp_d₂₃_eq {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (cochainsIso₂ A).hom (d₂₃ A) = CategoryTheory.CategoryStruct.comp ((inhomogeneousCochains A).d 2 3) (cochainsIso₃ A).hom

Let C(G, A) denote the complex of inhomogeneous cochains of A : Rep k G. This lemma says d₂₃ gives a simpler expression for the 2nd differential: that is, the following square commutes:

      C²(G, A) ----d 2 3----> C³(G, A)
        |                         |
        |                         |
        |                         |
        v                         v
  Fun(G × G, A) --d₂₃--> Fun(G × G × G, A)

where the vertical arrows are cochainsIso₂ and cochainsIso₃ respectively.

@[simp]

theorem groupCohomology.eq_d₂₃_comp_inv {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (cochainsIso₂ A).inv ((inhomogeneousCochains A).d 2 3) = CategoryTheory.CategoryStruct.comp (d₂₃ A) (cochainsIso₃ A).inv

@[simp]

theorem groupCohomology.eq_d₂₃_comp_inv_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : (inhomogeneousCochains A).X 3 ⟶ Z) : CategoryTheory.CategoryStruct.comp (cochainsIso₂ A).inv (CategoryTheory.CategoryStruct.comp ((inhomogeneousCochains A).d 2 3) h) = CategoryTheory.CategoryStruct.comp (d₂₃ A) (CategoryTheory.CategoryStruct.comp (cochainsIso₃ A).inv h)

@[simp]

theorem groupCohomology.eq_d₂₃_comp_inv_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : CategoryTheory.ToType (ModuleCat.of k (G × G → ↑A.V))) : (CategoryTheory.ConcreteCategory.hom ((inhomogeneousCochains A).d 2 3)) ((CategoryTheory.ConcreteCategory.hom (cochainsIso₂ A).inv) x) = (CategoryTheory.ConcreteCategory.hom (cochainsIso₃ A).inv) ((CategoryTheory.ConcreteCategory.hom (d₂₃ A)) x)

@[simp]

theorem groupCohomology.d₀₁_comp_d₁₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (d₀₁ A) (d₁₂ A) = 0

@[simp]

theorem groupCohomology.d₀₁_comp_d₁₂_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : ModuleCat.of k (G × G → ↑A.V) ⟶ Z) : CategoryTheory.CategoryStruct.comp (d₀₁ A) (CategoryTheory.CategoryStruct.comp (d₁₂ A) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem groupCohomology.d₀₁_comp_d₁₂_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : CategoryTheory.ToType A.V) : (CategoryTheory.ConcreteCategory.hom (d₁₂ A)) ((CategoryTheory.ConcreteCategory.hom (d₀₁ A)) x) = 0

@[simp]

theorem groupCohomology.d₁₂_comp_d₂₃ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (d₁₂ A) (d₂₃ A) = 0

@[simp]

theorem groupCohomology.d₁₂_comp_d₂₃_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : ModuleCat.of k (G × G × G → ↑A.V) ⟶ Z) : CategoryTheory.CategoryStruct.comp (d₁₂ A) (CategoryTheory.CategoryStruct.comp (d₂₃ A) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem groupCohomology.d₁₂_comp_d₂₃_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : CategoryTheory.ToType (ModuleCat.of k (G → ↑A.V))) : (CategoryTheory.ConcreteCategory.hom (d₂₃ A)) ((CategoryTheory.ConcreteCategory.hom (d₁₂ A)) x) = 0

def groupCohomology.shortComplexH0 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.ShortComplex (ModuleCat k)

The (exact) short complex A.ρ.invariants ⟶ A ⟶ (G → A).

Equations

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

theorem groupCohomology.shortComplexH0_f {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (shortComplexH0 A).f = ModuleCat.ofHom A.ρ.invariants.subtype

theorem groupCohomology.shortComplexH0_g {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (shortComplexH0 A).g = d₀₁ A

def groupCohomology.shortComplexH1 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.ShortComplex (ModuleCat k)

The short complex A --d₀₁--> Fun(G, A) --d₁₂--> Fun(G × G, A).

Equations

• groupCohomology.shortComplexH1 A = { X₁ := A.V, X₂ := ModuleCat.of k (G → ↑A.V), X₃ := ModuleCat.of k (G × G → ↑A.V), f := groupCohomology.d₀₁ A, g := groupCohomology.d₁₂ A, zero := ⋯ }

theorem groupCohomology.shortComplexH1_g {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (shortComplexH1 A).g = d₁₂ A

theorem groupCohomology.shortComplexH1_f {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (shortComplexH1 A).f = d₀₁ A

def groupCohomology.shortComplexH2 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.ShortComplex (ModuleCat k)

The short complex Fun(G, A) --d₁₂--> Fun(G × G, A) --d₂₃--> Fun(G × G × G, A).

Equations

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

theorem groupCohomology.shortComplexH2_g {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (shortComplexH2 A).g = d₂₃ A

theorem groupCohomology.shortComplexH2_f {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (shortComplexH2 A).f = d₁₂ A

def groupCohomology.cocycles₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : Submodule k (G → ↑A.V)

The 1-cocycles Z¹(G, A) of A : Rep k G, defined as the kernel of the map Fun(G, A) → Fun(G × G, A) sending (f, (g₁, g₂)) ↦ ρ_A(g₁)(f(g₂)) - f(g₁g₂) + f(g₁).

Equations

• groupCohomology.cocycles₁ A = (ModuleCat.Hom.hom (groupCohomology.d₁₂ A)).ker

def groupCohomology.cocycles₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : Submodule k (G × G → ↑A.V)

The 2-cocycles Z²(G, A) of A : Rep k G, defined as the kernel of the map Fun(G × G, A) → Fun(G × G × G, A) sending (f, (g₁, g₂, g₃)) ↦ ρ_A(g₁)(f(g₂, g₃)) - f(g₁g₂, g₃) + f(g₁, g₂g₃) - f(g₁, g₂).

Equations

• groupCohomology.cocycles₂ A = (ModuleCat.Hom.hom (groupCohomology.d₂₃ A)).ker

instance groupCohomology.instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCocycles₁ {k G : Type u} [CommRing k] [Group G] {A : Rep k G} : FunLike (↥(cocycles₁ A)) G ↑A.V

Equations

• groupCohomology.instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCocycles₁ = { coe := Subtype.val, coe_injective' := ⋯ }

@[simp]

theorem groupCohomology.cocycles₁.coe_mk {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : G → ↑A.V) (hf : f ∈ cocycles₁ A) : ⇑⟨f, hf⟩ = f

@[simp]

theorem groupCohomology.cocycles₁.val_eq_coe {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : ↥(cocycles₁ A)) : ↑f = ⇑f

theorem groupCohomology.cocycles₁_ext {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f₁ f₂ : ↥(cocycles₁ A)} (h : ∀ (g : G), f₁ g = f₂ g) : f₁ = f₂

theorem groupCohomology.cocycles₁_ext_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f₁ f₂ : ↥(cocycles₁ A)} : f₁ = f₂ ↔ ∀ (g : G), f₁ g = f₂ g

theorem groupCohomology.mem_cocycles₁_def {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : G → ↑A.V) : f ∈ cocycles₁ A ↔ ∀ (g h : G), (A.ρ g) (f h) - f (g * h) + f g = 0

theorem groupCohomology.mem_cocycles₁_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : G → ↑A.V) : f ∈ cocycles₁ A ↔ ∀ (g h : G), f (g * h) = (A.ρ g) (f h) + f g

@[simp]

theorem groupCohomology.cocycles₁_map_one {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : ↥(cocycles₁ A)) : f 1 = 0

@[simp]

theorem groupCohomology.cocycles₁_map_inv {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : ↥(cocycles₁ A)) (g : G) : (A.ρ g) (f g⁻¹) = -f g

theorem groupCohomology.d₀₁_apply_mem_cocycles₁ {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x : ↑A.V) : (CategoryTheory.ConcreteCategory.hom (d₀₁ A)) x ∈ cocycles₁ A

@[simp]

theorem groupCohomology.cocycles₁.d₁₂_apply {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x : ↥(cocycles₁ A)) : (CategoryTheory.ConcreteCategory.hom (d₁₂ A)) ⇑x = 0

theorem groupCohomology.cocycles₁_map_mul_of_isTrivial {k G : Type u} [CommRing k] [Group G] {A : Rep k G} [A.IsTrivial] (f : ↥(cocycles₁ A)) (g h : G) : f (g * h) = f g + f h

theorem groupCohomology.mem_cocycles₁_of_addMonoidHom {k G : Type u} [CommRing k] [Group G] {A : Rep k G} [A.IsTrivial] (f : Additive G →+ ↑A.V) : ⇑f ∘ ⇑Additive.ofMul ∈ cocycles₁ A

def groupCohomology.cocycles₁IsoOfIsTrivial {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [hA : A.IsTrivial] : ModuleCat.of k ↥(cocycles₁ A) ≅ ModuleCat.of k (Additive G →+ ↑A.V)

When A : Rep k G is a trivial representation of G, Z¹(G, A) is isomorphic to the group homs G → A.

Equations

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

@[simp]

theorem groupCohomology.cocycles₁IsoOfIsTrivial_inv_hom_apply_coe {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [hA : A.IsTrivial] (a : Additive G →+ ↑A.V) (a✝ : Additive G) : ↑((ModuleCat.Hom.hom (cocycles₁IsoOfIsTrivial A).inv) a) a✝ = a a✝

@[simp]

theorem groupCohomology.cocycles₁IsoOfIsTrivial_hom_hom_apply_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [hA : A.IsTrivial] (f : ↥(cocycles₁ A)) (a✝ : Additive G) : ((ModuleCat.Hom.hom (cocycles₁IsoOfIsTrivial A).hom) f) a✝ = f (Additive.toMul a✝)

instance groupCohomology.instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCocycles₂ {k G : Type u} [CommRing k] [Group G] {A : Rep k G} : FunLike (↥(cocycles₂ A)) (G × G) ↑A.V

Equations

• groupCohomology.instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCocycles₂ = { coe := Subtype.val, coe_injective' := ⋯ }

@[simp]

theorem groupCohomology.cocycles₂.coe_mk {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : G × G → ↑A.V) (hf : f ∈ cocycles₂ A) : ⇑⟨f, hf⟩ = f

@[simp]

theorem groupCohomology.cocycles₂.val_eq_coe {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : ↥(cocycles₂ A)) : ↑f = ⇑f

theorem groupCohomology.cocycles₂_ext {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f₁ f₂ : ↥(cocycles₂ A)} (h : ∀ (g h : G), f₁ (g, h) = f₂ (g, h)) : f₁ = f₂

theorem groupCohomology.cocycles₂_ext_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f₁ f₂ : ↥(cocycles₂ A)} : f₁ = f₂ ↔ ∀ (g h : G), f₁ (g, h) = f₂ (g, h)

theorem groupCohomology.mem_cocycles₂_def {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : G × G → ↑A.V) : f ∈ cocycles₂ A ↔ ∀ (g h j : G), (A.ρ g) (f (h, j)) - f (g * h, j) + f (g, h * j) - f (g, h) = 0

theorem groupCohomology.mem_cocycles₂_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : G × G → ↑A.V) : f ∈ cocycles₂ A ↔ ∀ (g h j : G), f (g * h, j) + f (g, h) = (A.ρ g) (f (h, j)) + f (g, h * j)

theorem groupCohomology.cocycles₂_map_one_fst {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : ↥(cocycles₂ A)) (g : G) : f (1, g) = f (1, 1)

theorem groupCohomology.cocycles₂_map_one_snd {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : ↥(cocycles₂ A)) (g : G) : f (g, 1) = (A.ρ g) (f (1, 1))

theorem groupCohomology.cocycles₂_ρ_map_inv_sub_map_inv {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : ↥(cocycles₂ A)) (g : G) : (A.ρ g) (f (g⁻¹, g)) - f (g, g⁻¹) = f (1, 1) - f (g, 1)

theorem groupCohomology.d₁₂_apply_mem_cocycles₂ {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x : G → ↑A.V) : (CategoryTheory.ConcreteCategory.hom (d₁₂ A)) x ∈ cocycles₂ A

@[simp]

theorem groupCohomology.cocycles₂.d₂₃_apply {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x : ↥(cocycles₂ A)) : (CategoryTheory.ConcreteCategory.hom (d₂₃ A)) ⇑x = 0

def groupCohomology.coboundaries₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : Submodule k (G → ↑A.V)

The 1-coboundaries B¹(G, A) of A : Rep k G, defined as the image of the map A → Fun(G, A) sending (a, g) ↦ ρ_A(g)(a) - a.

Equations

• groupCohomology.coboundaries₁ A = (ModuleCat.Hom.hom (groupCohomology.d₀₁ A)).range

def groupCohomology.coboundaries₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : Submodule k (G × G → ↑A.V)

The 2-coboundaries B²(G, A) of A : Rep k G, defined as the image of the map Fun(G, A) → Fun(G × G, A) sending (f, (g₁, g₂)) ↦ ρ_A(g₁)(f(g₂)) - f(g₁g₂) + f(g₁).

Equations

• groupCohomology.coboundaries₂ A = (ModuleCat.Hom.hom (groupCohomology.d₁₂ A)).range

instance groupCohomology.instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCoboundaries₁ {k G : Type u} [CommRing k] [Group G] {A : Rep k G} : FunLike (↥(coboundaries₁ A)) G ↑A.V

Equations

• groupCohomology.instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCoboundaries₁ = { coe := Subtype.val, coe_injective' := ⋯ }

@[simp]

theorem groupCohomology.coboundaries₁.coe_mk {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : G → ↑A.V) (hf : f ∈ coboundaries₁ A) : ⇑⟨f, hf⟩ = f

@[simp]

theorem groupCohomology.coboundaries₁.val_eq_coe {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : ↥(coboundaries₁ A)) : ↑f = ⇑f

theorem groupCohomology.coboundaries₁_ext {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f₁ f₂ : ↥(coboundaries₁ A)} (h : ∀ (g : G), f₁ g = f₂ g) : f₁ = f₂

theorem groupCohomology.coboundaries₁_ext_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f₁ f₂ : ↥(coboundaries₁ A)} : f₁ = f₂ ↔ ∀ (g : G), f₁ g = f₂ g

theorem groupCohomology.coboundaries₁_le_cocycles₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : coboundaries₁ A ≤ cocycles₁ A

@[reducible, inline]

abbrev groupCohomology.coboundariesToCocycles₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : ↥(coboundaries₁ A) →ₗ[k] ↥(cocycles₁ A)

Natural inclusion B¹(G, A) →ₗ[k] Z¹(G, A).

Equations

• groupCohomology.coboundariesToCocycles₁ A = Submodule.inclusion ⋯

@[simp]

theorem groupCohomology.coboundariesToCocycles₁_apply {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x : ↥(coboundaries₁ A)) : ⇑((coboundariesToCocycles₁ A) x) = ↑x

theorem groupCohomology.coboundaries₁_eq_bot_of_isTrivial {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] : coboundaries₁ A = ⊥

instance groupCohomology.instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCoboundaries₂ {k G : Type u} [CommRing k] [Group G] {A : Rep k G} : FunLike (↥(coboundaries₂ A)) (G × G) ↑A.V

Equations

• groupCohomology.instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCoboundaries₂ = { coe := Subtype.val, coe_injective' := ⋯ }

@[simp]

theorem groupCohomology.coboundaries₂.coe_mk {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : G × G → ↑A.V) (hf : f ∈ coboundaries₂ A) : ⇑⟨f, hf⟩ = f

@[simp]

theorem groupCohomology.coboundaries₂.val_eq_coe {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : ↥(coboundaries₂ A)) : ↑f = ⇑f

theorem groupCohomology.coboundaries₂_ext {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f₁ f₂ : ↥(coboundaries₂ A)} (h : ∀ (g h : G), f₁ (g, h) = f₂ (g, h)) : f₁ = f₂

theorem groupCohomology.coboundaries₂_ext_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f₁ f₂ : ↥(coboundaries₂ A)} : f₁ = f₂ ↔ ∀ (g h : G), f₁ (g, h) = f₂ (g, h)

theorem groupCohomology.coboundaries₂_le_cocycles₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : coboundaries₂ A ≤ cocycles₂ A

@[reducible, inline]

abbrev groupCohomology.coboundariesToCocycles₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : ↥(coboundaries₂ A) →ₗ[k] ↥(cocycles₂ A)

Natural inclusion B²(G, A) →ₗ[k] Z²(G, A).

Equations

• groupCohomology.coboundariesToCocycles₂ A = Submodule.inclusion ⋯

@[simp]

theorem groupCohomology.coboundariesToCocycles₂_apply {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x : ↥(coboundaries₂ A)) : ⇑((coboundariesToCocycles₂ A) x) = ↑x

def groupCohomology.IsCocycle₁ {G : Type u_1} {A : Type u_2} [Mul G] [AddCommGroup A] [SMul G A] (f : G → A) : Prop

A function f : G → A satisfies the 1-cocycle condition if f(gh) = g • f(h) + f(g) for all g, h : G.

Equations

• groupCohomology.IsCocycle₁ f = ∀ (g h : G), f (g * h) = g • f h + f g

def groupCohomology.IsCocycle₂ {G : Type u_1} {A : Type u_2} [Mul G] [AddCommGroup A] [SMul G A] (f : G × G → A) : Prop

A function f : G × G → A satisfies the 2-cocycle condition if f(gh, j) + f(g, h) = g • f(h, j) + f(g, hj) for all g, h : G.

Equations

• groupCohomology.IsCocycle₂ f = ∀ (g h j : G), f (g * h, j) + f (g, h) = g • f (h, j) + f (g, h * j)

theorem groupCohomology.map_one_of_isCocycle₁ {G : Type u_1} {A : Type u_2} [Monoid G] [AddCommGroup A] [MulAction G A] {f : G → A} (hf : IsCocycle₁ f) : f 1 = 0

theorem groupCohomology.map_one_fst_of_isCocycle₂ {G : Type u_1} {A : Type u_2} [Monoid G] [AddCommGroup A] [MulAction G A] {f : G × G → A} (hf : IsCocycle₂ f) (g : G) : f (1, g) = f (1, 1)

theorem groupCohomology.map_one_snd_of_isCocycle₂ {G : Type u_1} {A : Type u_2} [Monoid G] [AddCommGroup A] [MulAction G A] {f : G × G → A} (hf : IsCocycle₂ f) (g : G) : f (g, 1) = g • f (1, 1)

theorem groupCohomology.map_inv_of_isCocycle₁ {G : Type u_1} {A : Type u_2} [Group G] [AddCommGroup A] [MulAction G A] {f : G → A} (hf : IsCocycle₁ f) (g : G) : g • f g⁻¹ = -f g

theorem groupCohomology.smul_map_inv_sub_map_inv_of_isCocycle₂ {G : Type u_1} {A : Type u_2} [Group G] [AddCommGroup A] [MulAction G A] {f : G × G → A} (hf : IsCocycle₂ f) (g : G) : g • f (g⁻¹, g) - f (g, g⁻¹) = f (1, 1) - f (g, 1)

def groupCohomology.IsCoboundary₁ {G : Type u_1} {A : Type u_2} [AddCommGroup A] [SMul G A] (f : G → A) : Prop

A function f : G → A satisfies the 1-coboundary condition if there's x : A such that g • x - x = f(g) for all g : G.

Equations

• groupCohomology.IsCoboundary₁ f = ∃ (x : A), ∀ (g : G), g • x - x = f g

def groupCohomology.IsCoboundary₂ {G : Type u_1} {A : Type u_2} [Mul G] [AddCommGroup A] [SMul G A] (f : G × G → A) : Prop

A function f : G × G → A satisfies the 2-coboundary condition if there's x : G → A such that g • x(h) - x(gh) + x(g) = f(g, h) for all g, h : G.

Equations

• groupCohomology.IsCoboundary₂ f = ∃ (x : G → A), ∀ (g h : G), g • x h - x (g * h) + x g = f (g, h)

def groupCohomology.cocyclesOfIsCocycle₁ {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] {f : G → A} (hf : IsCocycle₁ f) : ↥(cocycles₁ (Rep.ofDistribMulAction k G A))

Given a k-module A with a compatible DistribMulAction of G, and a function f : G → A satisfying the 1-cocycle condition, produces a 1-cocycle for the representation on A induced by the DistribMulAction.

Equations

• groupCohomology.cocyclesOfIsCocycle₁ hf = ⟨f, ⋯⟩

@[simp]

theorem groupCohomology.cocyclesOfIsCocycle₁_coe {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] {f : G → A} (hf : IsCocycle₁ f) (a✝ : G) : ↑(cocyclesOfIsCocycle₁ hf) a✝ = f a✝

theorem groupCohomology.isCocycle₁_of_mem_cocycles₁ {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (f : G → A) (hf : f ∈ cocycles₁ (Rep.ofDistribMulAction k G A)) : IsCocycle₁ f

@[deprecated groupCohomology.isCocycle₁_of_mem_cocycles₁ (since := "2025-07-02")]

theorem groupCohomology.isOneCocycle_of_mem_oneCocycles {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (f : G → A) (hf : f ∈ cocycles₁ (Rep.ofDistribMulAction k G A)) : IsCocycle₁ f

Alias of groupCohomology.isCocycle₁_of_mem_cocycles₁.

def groupCohomology.coboundariesOfIsCoboundary₁ {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] {f : G → A} (hf : IsCoboundary₁ f) : ↥(coboundaries₁ (Rep.ofDistribMulAction k G A))

Given a k-module A with a compatible DistribMulAction of G, and a function f : G → A satisfying the 1-coboundary condition, produces a 1-coboundary for the representation on A induced by the DistribMulAction.

Equations

• groupCohomology.coboundariesOfIsCoboundary₁ hf = ⟨f, ⋯⟩

@[simp]

theorem groupCohomology.coboundariesOfIsCoboundary₁_coe {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] {f : G → A} (hf : IsCoboundary₁ f) (a✝ : G) : ↑(coboundariesOfIsCoboundary₁ hf) a✝ = f a✝

theorem groupCohomology.isCoboundary₁_of_mem_coboundaries₁ {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (f : G → A) (hf : f ∈ coboundaries₁ (Rep.ofDistribMulAction k G A)) : IsCoboundary₁ f

@[deprecated groupCohomology.isCoboundary₁_of_mem_coboundaries₁ (since := "2025-07-02")]

theorem groupCohomology.isOneCoboundary_of_mem_oneCoboundaries {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (f : G → A) (hf : f ∈ coboundaries₁ (Rep.ofDistribMulAction k G A)) : IsCoboundary₁ f

Alias of groupCohomology.isCoboundary₁_of_mem_coboundaries₁.

def groupCohomology.cocyclesOfIsCocycle₂ {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] {f : G × G → A} (hf : IsCocycle₂ f) : ↥(cocycles₂ (Rep.ofDistribMulAction k G A))

Given a k-module A with a compatible DistribMulAction of G, and a function f : G × G → A satisfying the 2-cocycle condition, produces a 2-cocycle for the representation on A induced by the DistribMulAction.

Equations

• groupCohomology.cocyclesOfIsCocycle₂ hf = ⟨f, ⋯⟩

@[simp]

theorem groupCohomology.cocyclesOfIsCocycle₂_coe {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] {f : G × G → A} (hf : IsCocycle₂ f) (a✝ : G × G) : ↑(cocyclesOfIsCocycle₂ hf) a✝ = f a✝

theorem groupCohomology.isCocycle₂_of_mem_cocycles₂ {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (f : G × G → A) (hf : f ∈ cocycles₂ (Rep.ofDistribMulAction k G A)) : IsCocycle₂ f

@[deprecated groupCohomology.isCocycle₂_of_mem_cocycles₂ (since := "2025-07-02")]

theorem groupCohomology.isTwoCocycle_of_mem_twoCocycles {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (f : G × G → A) (hf : f ∈ cocycles₂ (Rep.ofDistribMulAction k G A)) : IsCocycle₂ f

Alias of groupCohomology.isCocycle₂_of_mem_cocycles₂.

def groupCohomology.coboundariesOfIsCoboundary₂ {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] {f : G × G → A} (hf : IsCoboundary₂ f) : ↥(coboundaries₂ (Rep.ofDistribMulAction k G A))

Given a k-module A with a compatible DistribMulAction of G, and a function f : G × G → A satisfying the 2-coboundary condition, produces a 2-coboundary for the representation on A induced by the DistribMulAction.

Equations

• groupCohomology.coboundariesOfIsCoboundary₂ hf = ⟨f, ⋯⟩

@[simp]

theorem groupCohomology.coboundariesOfIsCoboundary₂_coe {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] {f : G × G → A} (hf : IsCoboundary₂ f) (a✝ : G × G) : ↑(coboundariesOfIsCoboundary₂ hf) a✝ = f a✝

theorem groupCohomology.isCoboundary₂_of_mem_coboundaries₂ {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (f : G × G → A) (hf : f ∈ coboundaries₂ (Rep.ofDistribMulAction k G A)) : IsCoboundary₂ f

@[deprecated groupCohomology.isCoboundary₂_of_mem_coboundaries₂ (since := "2025-07-02")]

theorem groupCohomology.isTwoCoboundary_of_mem_twoCoboundaries {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (f : G × G → A) (hf : f ∈ coboundaries₂ (Rep.ofDistribMulAction k G A)) : IsCoboundary₂ f

Alias of groupCohomology.isCoboundary₂_of_mem_coboundaries₂.

The next few sections, until the section CocyclesIso, are a multiplicative copy of the previous few sections beginning with IsCocycle. Unfortunately @[to_additive] doesn't work with scalar actions.

def groupCohomology.IsMulCocycle₁ {G : Type u_1} {M : Type u_2} [Mul G] [CommGroup M] [SMul G M] (f : G → M) : Prop

A function f : G → M satisfies the multiplicative 1-cocycle condition if f(gh) = g • f(h) * f(g) for all g, h : G.

Equations

• groupCohomology.IsMulCocycle₁ f = ∀ (g h : G), f (g * h) = g • f h * f g

def groupCohomology.IsMulCocycle₂ {G : Type u_1} {M : Type u_2} [Mul G] [CommGroup M] [SMul G M] (f : G × G → M) : Prop

A function f : G × G → M satisfies the multiplicative 2-cocycle condition if f(gh, j) * f(g, h) = g • f(h, j) * f(g, hj) for all g, h : G.

Equations

• groupCohomology.IsMulCocycle₂ f = ∀ (g h j : G), f (g * h, j) * f (g, h) = g • f (h, j) * f (g, h * j)

theorem groupCohomology.map_one_of_isMulCocycle₁ {G : Type u_1} {M : Type u_2} [Monoid G] [CommGroup M] [MulAction G M] {f : G → M} (hf : IsMulCocycle₁ f) : f 1 = 1

theorem groupCohomology.map_one_fst_of_isMulCocycle₂ {G : Type u_1} {M : Type u_2} [Monoid G] [CommGroup M] [MulAction G M] {f : G × G → M} (hf : IsMulCocycle₂ f) (g : G) : f (1, g) = f (1, 1)

theorem groupCohomology.map_one_snd_of_isMulCocycle₂ {G : Type u_1} {M : Type u_2} [Monoid G] [CommGroup M] [MulAction G M] {f : G × G → M} (hf : IsMulCocycle₂ f) (g : G) : f (g, 1) = g • f (1, 1)

theorem groupCohomology.map_inv_of_isMulCocycle₁ {G : Type u_1} {M : Type u_2} [Group G] [CommGroup M] [MulAction G M] {f : G → M} (hf : IsMulCocycle₁ f) (g : G) : g • f g⁻¹ = (f g)⁻¹

theorem groupCohomology.smul_map_inv_div_map_inv_of_isMulCocycle₂ {G : Type u_1} {M : Type u_2} [Group G] [CommGroup M] [MulAction G M] {f : G × G → M} (hf : IsMulCocycle₂ f) (g : G) : g • f (g⁻¹, g) / f (g, g⁻¹) = f (1, 1) / f (g, 1)

@[deprecated groupCohomology.smul_map_inv_div_map_inv_of_isMulCocycle₂ (since := "2025-07-02")]

theorem groupCohomology.smul_map_inv_div_map_inv_of_isMulTwoCocycle {G : Type u_1} {M : Type u_2} [Group G] [CommGroup M] [MulAction G M] {f : G × G → M} (hf : IsMulCocycle₂ f) (g : G) : g • f (g⁻¹, g) / f (g, g⁻¹) = f (1, 1) / f (g, 1)

Alias of groupCohomology.smul_map_inv_div_map_inv_of_isMulCocycle₂.

def groupCohomology.IsMulCoboundary₁ {G : Type u_1} {M : Type u_2} [CommGroup M] [SMul G M] (f : G → M) : Prop

A function f : G → M satisfies the multiplicative 1-coboundary condition if there's x : M such that g • x / x = f(g) for all g : G.

Equations

• groupCohomology.IsMulCoboundary₁ f = ∃ (x : M), ∀ (g : G), g • x / x = f g

def groupCohomology.IsMulCoboundary₂ {G : Type u_1} {M : Type u_2} [Mul G] [CommGroup M] [SMul G M] (f : G × G → M) : Prop

A function f : G × G → M satisfies the 2-coboundary condition if there's x : G → M such that g • x(h) / x(gh) * x(g) = f(g, h) for all g, h : G.

Equations

• groupCohomology.IsMulCoboundary₂ f = ∃ (x : G → M), ∀ (g h : G), g • x h / x (g * h) * x g = f (g, h)

def groupCohomology.cocyclesOfIsMulCocycle₁ {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] {f : G → M} (hf : IsMulCocycle₁ f) : ↥(cocycles₁ (Rep.ofMulDistribMulAction G M))

Given an abelian group M with a MulDistribMulAction of G, and a function f : G → M satisfying the multiplicative 1-cocycle condition, produces a 1-cocycle for the representation on Additive M induced by the MulDistribMulAction.

Equations

• groupCohomology.cocyclesOfIsMulCocycle₁ hf = ⟨⇑Additive.ofMul ∘ f, ⋯⟩

@[simp]

theorem groupCohomology.cocyclesOfIsMulCocycle₁_coe {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] {f : G → M} (hf : IsMulCocycle₁ f) (a✝ : G) : ↑(cocyclesOfIsMulCocycle₁ hf) a✝ = (⇑Additive.ofMul ∘ f) a✝

theorem groupCohomology.isMulCocycle₁_of_mem_cocycles₁ {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] (f : G → M) (hf : f ∈ cocycles₁ (Rep.ofMulDistribMulAction G M)) : IsMulCocycle₁ (⇑Additive.toMul ∘ f)

@[deprecated groupCohomology.isMulCocycle₁_of_mem_cocycles₁ (since := "2025-07-02")]

theorem groupCohomology.isMulOneCocycle_of_mem_oneCocycles {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] (f : G → M) (hf : f ∈ cocycles₁ (Rep.ofMulDistribMulAction G M)) : IsMulCocycle₁ (⇑Additive.toMul ∘ f)

Alias of groupCohomology.isMulCocycle₁_of_mem_cocycles₁.

def groupCohomology.coboundariesOfIsMulCoboundary₁ {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] {f : G → M} (hf : IsMulCoboundary₁ f) : ↥(coboundaries₁ (Rep.ofMulDistribMulAction G M))

Given an abelian group M with a MulDistribMulAction of G, and a function f : G → M satisfying the multiplicative 1-coboundary condition, produces a 1-coboundary for the representation on Additive M induced by the MulDistribMulAction.

Equations

• groupCohomology.coboundariesOfIsMulCoboundary₁ hf = ⟨⇑Additive.ofMul ∘ f, ⋯⟩

@[simp]

theorem groupCohomology.coboundariesOfIsMulCoboundary₁_coe {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] {f : G → M} (hf : IsMulCoboundary₁ f) (a✝ : G) : ↑(coboundariesOfIsMulCoboundary₁ hf) a✝ = (⇑Additive.ofMul ∘ f) a✝

theorem groupCohomology.isMulCoboundary₁_of_mem_coboundaries₁ {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] (f : G → M) (hf : f ∈ coboundaries₁ (Rep.ofMulDistribMulAction G M)) : IsMulCoboundary₁ (⇑Additive.ofMul ∘ f)

@[deprecated groupCohomology.isMulCoboundary₁_of_mem_coboundaries₁ (since := "2025-07-02")]

theorem groupCohomology.isMulOneCoboundary_of_mem_oneCoboundaries {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] (f : G → M) (hf : f ∈ coboundaries₁ (Rep.ofMulDistribMulAction G M)) : IsMulCoboundary₁ (⇑Additive.ofMul ∘ f)

Alias of groupCohomology.isMulCoboundary₁_of_mem_coboundaries₁.

def groupCohomology.cocyclesOfIsMulCocycle₂ {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] {f : G × G → M} (hf : IsMulCocycle₂ f) : ↥(cocycles₂ (Rep.ofMulDistribMulAction G M))

Given an abelian group M with a MulDistribMulAction of G, and a function f : G × G → M satisfying the multiplicative 2-cocycle condition, produces a 2-cocycle for the representation on Additive M induced by the MulDistribMulAction.

Equations

• groupCohomology.cocyclesOfIsMulCocycle₂ hf = ⟨⇑Additive.ofMul ∘ f, ⋯⟩

@[simp]

theorem groupCohomology.cocyclesOfIsMulCocycle₂_coe {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] {f : G × G → M} (hf : IsMulCocycle₂ f) (a✝ : G × G) : ↑(cocyclesOfIsMulCocycle₂ hf) a✝ = (⇑Additive.ofMul ∘ f) a✝

theorem groupCohomology.isMulCocycle₂_of_mem_cocycles₂ {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] (f : G × G → M) (hf : f ∈ cocycles₂ (Rep.ofMulDistribMulAction G M)) : IsMulCocycle₂ (⇑Additive.toMul ∘ f)

@[deprecated groupCohomology.isMulCocycle₂_of_mem_cocycles₂ (since := "2025-07-02")]

theorem groupCohomology.isMulTwoCocycle_of_mem_twoCocycles {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] (f : G × G → M) (hf : f ∈ cocycles₂ (Rep.ofMulDistribMulAction G M)) : IsMulCocycle₂ (⇑Additive.toMul ∘ f)

Alias of groupCohomology.isMulCocycle₂_of_mem_cocycles₂.

def groupCohomology.coboundariesOfIsMulCoboundary₂ {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] {f : G × G → M} (hf : IsMulCoboundary₂ f) : ↥(coboundaries₂ (Rep.ofMulDistribMulAction G M))

Given an abelian group M with a MulDistribMulAction of G, and a function f : G × G → M satisfying the multiplicative 2-coboundary condition, produces a 2-coboundary for the representation on M induced by the MulDistribMulAction.

Equations

• groupCohomology.coboundariesOfIsMulCoboundary₂ hf = ⟨⇑Additive.ofMul ∘ f, ⋯⟩

theorem groupCohomology.isMulCoboundary₂_of_mem_coboundaries₂ {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] (f : G × G → M) (hf : f ∈ coboundaries₂ (Rep.ofMulDistribMulAction G M)) : IsMulCoboundary₂ (⇑Additive.toMul ∘ f)

@[deprecated groupCohomology.isMulCoboundary₂_of_mem_coboundaries₂ (since := "2025-07-02")]

theorem groupCohomology.isMulTwoCoboundary_of_mem_twoCoboundaries {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] (f : G × G → M) (hf : f ∈ coboundaries₂ (Rep.ofMulDistribMulAction G M)) : IsMulCoboundary₂ (⇑Additive.toMul ∘ f)

Alias of groupCohomology.isMulCoboundary₂_of_mem_coboundaries₂.

instance groupCohomology.instMonoModuleCatFShortComplexH0 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.Mono (shortComplexH0 A).f

theorem groupCohomology.shortComplexH0_exact {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (shortComplexH0 A).Exact

def groupCohomology.dArrowIso₀₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.Arrow.mk ((inhomogeneousCochains A).d 0 1) ≅ CategoryTheory.Arrow.mk (d₀₁ A)

The arrow A --d₀₁--> Fun(G, A) is isomorphic to the differential (inhomogeneousCochains A).d 0 1 of the complex of inhomogeneous cochains of A.

Equations

• groupCohomology.dArrowIso₀₁ A = CategoryTheory.Arrow.isoMk (groupCohomology.cochainsIso₀ A) (groupCohomology.cochainsIso₁ A) ⋯

@[simp]

theorem groupCohomology.dArrowIso₀₁_inv_left {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (dArrowIso₀₁ A).inv.left = (cochainsIso₀ A).inv

@[simp]

theorem groupCohomology.dArrowIso₀₁_hom_right {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (dArrowIso₀₁ A).hom.right = (cochainsIso₁ A).hom

@[simp]

theorem groupCohomology.dArrowIso₀₁_inv_right {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (dArrowIso₀₁ A).inv.right = (cochainsIso₁ A).inv

@[simp]

theorem groupCohomology.dArrowIso₀₁_hom_left {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (dArrowIso₀₁ A).hom.left = (cochainsIso₀ A).hom

def groupCohomology.cocyclesIso₀ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : cocycles A 0 ≅ ModuleCat.of k ↥A.ρ.invariants

The 0-cocycles of the complex of inhomogeneous cochains of A are isomorphic to A.ρ.invariants, which is a simpler type.

Equations

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

@[deprecated groupCohomology.cocyclesIso₀ (since := "2025-07-02")]

def groupCohomology.zeroCocyclesIso {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : cocycles A 0 ≅ ModuleCat.of k ↥A.ρ.invariants

Alias of groupCohomology.cocyclesIso₀.

---

The 0-cocycles of the complex of inhomogeneous cochains of A are isomorphic to A.ρ.invariants, which is a simpler type.

Equations

• @groupCohomology.zeroCocyclesIso = @groupCohomology.cocyclesIso₀

@[simp]

theorem groupCohomology.cocyclesIso₀_hom_comp_f {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (cocyclesIso₀ A).hom (shortComplexH0 A).f = CategoryTheory.CategoryStruct.comp (iCocycles A 0) (cochainsIso₀ A).hom

@[simp]

theorem groupCohomology.cocyclesIso₀_hom_comp_f_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : (shortComplexH0 A).X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (cocyclesIso₀ A).hom (CategoryTheory.CategoryStruct.comp (shortComplexH0 A).f h) = CategoryTheory.CategoryStruct.comp (iCocycles A 0) (CategoryTheory.CategoryStruct.comp (cochainsIso₀ A).hom h)

@[simp]

theorem groupCohomology.cocyclesIso₀_hom_comp_f_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : CategoryTheory.ToType (cocycles A 0)) : (CategoryTheory.ConcreteCategory.hom (shortComplexH0 A).f) ((CategoryTheory.ConcreteCategory.hom (cocyclesIso₀ A).hom) x) = (CategoryTheory.CategoryStruct.comp (iCocycles A 0) (cochainsIso₀ A).hom) x

@[deprecated groupCohomology.cocyclesIso₀_hom_comp_f (since := "2025-07-02")]

theorem groupCohomology.zeroCocyclesIso_hom_comp_f {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (cocyclesIso₀ A).hom (shortComplexH0 A).f = CategoryTheory.CategoryStruct.comp (iCocycles A 0) (cochainsIso₀ A).hom

Alias of groupCohomology.cocyclesIso₀_hom_comp_f.

@[simp]

theorem groupCohomology.cocyclesIso₀_inv_comp_iCocycles {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (cocyclesIso₀ A).inv (iCocycles A 0) = CategoryTheory.CategoryStruct.comp (shortComplexH0 A).f (cochainsIso₀ A).inv

@[simp]

theorem groupCohomology.cocyclesIso₀_inv_comp_iCocycles_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : (inhomogeneousCochains A).X 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (cocyclesIso₀ A).inv (CategoryTheory.CategoryStruct.comp (iCocycles A 0) h) = CategoryTheory.CategoryStruct.comp (shortComplexH0 A).f (CategoryTheory.CategoryStruct.comp (cochainsIso₀ A).inv h)

@[simp]

theorem groupCohomology.cocyclesIso₀_inv_comp_iCocycles_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : CategoryTheory.ToType (ModuleCat.of k ↥A.ρ.invariants)) : (CategoryTheory.ConcreteCategory.hom (iCocycles A 0)) ((CategoryTheory.ConcreteCategory.hom (cocyclesIso₀ A).inv) x) = (CategoryTheory.CategoryStruct.comp (shortComplexH0 A).f (cochainsIso₀ A).inv) x

@[deprecated groupCohomology.cocyclesIso₀_inv_comp_iCocycles (since := "2025-07-02")]

theorem groupCohomology.zeroCocyclesIso_inv_comp_iCocycles {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (cocyclesIso₀ A).inv (iCocycles A 0) = CategoryTheory.CategoryStruct.comp (shortComplexH0 A).f (cochainsIso₀ A).inv

Alias of groupCohomology.cocyclesIso₀_inv_comp_iCocycles.

theorem groupCohomology.cocyclesMk₀_eq {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x : ↥A.ρ.invariants) : cocyclesMk ((CategoryTheory.ConcreteCategory.hom (cochainsIso₀ A).inv) ↑x) ⋯ = (CategoryTheory.ConcreteCategory.hom (cocyclesIso₀ A).inv) x

@[deprecated groupCohomology.cocyclesMk₀_eq (since := "2025-07-02")]

theorem groupCohomology.cocyclesMk_0_eq {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x : ↥A.ρ.invariants) : cocyclesMk ((CategoryTheory.ConcreteCategory.hom (cochainsIso₀ A).inv) ↑x) ⋯ = (CategoryTheory.ConcreteCategory.hom (cocyclesIso₀ A).inv) x

Alias of groupCohomology.cocyclesMk₀_eq.

def groupCohomology.isoShortComplexH1 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : HomologicalComplex.sc (inhomogeneousCochains A) 1 ≅ shortComplexH1 A

The short complex A --d₀₁--> Fun(G, A) --d₁₂--> Fun(G × G, A) is isomorphic to the 1st short complex associated to the complex of inhomogeneous cochains of A.

Equations

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

@[simp]

theorem groupCohomology.isoShortComplexH1_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (isoShortComplexH1 A).hom = CategoryTheory.CategoryStruct.comp ((HomologicalComplex.natIsoSc' (ModuleCat k) (ComplexShape.up ℕ) 0 1 2 isoShortComplexH1._proof_1 isoShortComplexH1._proof_2).hom.app (inhomogeneousCochains A)) (CategoryTheory.ShortComplex.isoMk (cochainsIso₀ A) (cochainsIso₁ A) (cochainsIso₂ A) ⋯ ⋯).hom

@[simp]

theorem groupCohomology.isoShortComplexH1_inv {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (isoShortComplexH1 A).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homMk (cochainsIso₀ A).inv (cochainsIso₁ A).inv (cochainsIso₂ A).inv ⋯ ⋯) ((HomologicalComplex.natIsoSc' (ModuleCat k) (ComplexShape.up ℕ) 0 1 2 isoShortComplexH1._proof_1 isoShortComplexH1._proof_2).inv.app (inhomogeneousCochains A))

@[deprecated groupCohomology.isoShortComplexH1 (since := "2025-07-11")]

def groupCohomology.shortComplexH1Iso {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : HomologicalComplex.sc (inhomogeneousCochains A) 1 ≅ shortComplexH1 A

Alias of groupCohomology.isoShortComplexH1.

---

The short complex A --d₀₁--> Fun(G, A) --d₁₂--> Fun(G × G, A) is isomorphic to the 1st short complex associated to the complex of inhomogeneous cochains of A.

Equations

• @groupCohomology.shortComplexH1Iso = @groupCohomology.isoShortComplexH1

def groupCohomology.isoCocycles₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : cocycles A 1 ≅ ModuleCat.of k ↥(cocycles₁ A)

The 1-cocycles of the complex of inhomogeneous cochains of A are isomorphic to cocycles₁ A, which is a simpler type.

Equations

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

@[simp]

theorem groupCohomology.isoCocycles₁_hom_comp_i {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (isoCocycles₁ A).hom (shortComplexH1 A).moduleCatLeftHomologyData.i = CategoryTheory.CategoryStruct.comp (iCocycles A 1) (cochainsIso₁ A).hom

@[simp]

theorem groupCohomology.isoCocycles₁_hom_comp_i_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : (shortComplexH1 A).X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (isoCocycles₁ A).hom (CategoryTheory.CategoryStruct.comp (shortComplexH1 A).moduleCatLeftHomologyData.i h) = CategoryTheory.CategoryStruct.comp (iCocycles A 1) (CategoryTheory.CategoryStruct.comp (cochainsIso₁ A).hom h)

@[simp]

theorem groupCohomology.isoCocycles₁_hom_comp_i_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : CategoryTheory.ToType (cocycles A 1)) : (ModuleCat.Hom.hom (shortComplexH1 A).g).ker.subtype ((CategoryTheory.ConcreteCategory.hom (isoCocycles₁ A).hom) x) = (CategoryTheory.CategoryStruct.comp (iCocycles A 1) (cochainsIso₁ A).hom) x

@[simp]

theorem groupCohomology.isoCocycles₁_inv_comp_iCocycles {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (isoCocycles₁ A).inv (iCocycles A 1) = CategoryTheory.CategoryStruct.comp (shortComplexH1 A).moduleCatLeftHomologyData.i (cochainsIso₁ A).inv

@[simp]

theorem groupCohomology.isoCocycles₁_inv_comp_iCocycles_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : (inhomogeneousCochains A).X 1 ⟶ Z) : CategoryTheory.CategoryStruct.comp (isoCocycles₁ A).inv (CategoryTheory.CategoryStruct.comp (iCocycles A 1) h) = CategoryTheory.CategoryStruct.comp (shortComplexH1 A).moduleCatLeftHomologyData.i (CategoryTheory.CategoryStruct.comp (cochainsIso₁ A).inv h)

@[simp]

theorem groupCohomology.isoCocycles₁_inv_comp_iCocycles_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : CategoryTheory.ToType (ModuleCat.of k ↥(cocycles₁ A))) : (CategoryTheory.ConcreteCategory.hom (iCocycles A 1)) ((CategoryTheory.ConcreteCategory.hom (isoCocycles₁ A).inv) x) = (CategoryTheory.CategoryStruct.comp (shortComplexH1 A).moduleCatLeftHomologyData.i (cochainsIso₁ A).inv) x

@[simp]

theorem groupCohomology.toCocycles_comp_isoCocycles₁_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (toCocycles A 0 1) (isoCocycles₁ A).hom = CategoryTheory.CategoryStruct.comp (cochainsIso₀ A).hom (shortComplexH1 A).moduleCatLeftHomologyData.f'

@[simp]

theorem groupCohomology.toCocycles_comp_isoCocycles₁_hom_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : ModuleCat.of k ↥(cocycles₁ A) ⟶ Z) : CategoryTheory.CategoryStruct.comp (toCocycles A 0 1) (CategoryTheory.CategoryStruct.comp (isoCocycles₁ A).hom h) = CategoryTheory.CategoryStruct.comp (cochainsIso₀ A).hom (CategoryTheory.CategoryStruct.comp (shortComplexH1 A).moduleCatLeftHomologyData.f' h)

@[simp]

theorem groupCohomology.toCocycles_comp_isoCocycles₁_hom_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : CategoryTheory.ToType ((inhomogeneousCochains A).X 0)) : (CategoryTheory.ConcreteCategory.hom (isoCocycles₁ A).hom) ((CategoryTheory.ConcreteCategory.hom (toCocycles A 0 1)) x) = (CategoryTheory.CategoryStruct.comp (cochainsIso₀ A).hom (shortComplexH1 A).moduleCatLeftHomologyData.f') x

theorem groupCohomology.cocyclesMk₁_eq {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : ↥(cocycles₁ A)) : cocyclesMk ((CategoryTheory.ConcreteCategory.hom (cochainsIso₁ A).inv) ⇑x) ⋯ = (CategoryTheory.ConcreteCategory.hom (isoCocycles₁ A).inv) x

@[deprecated groupCohomology.cocyclesMk₁_eq (since := "2025-07-02")]

theorem groupCohomology.cocyclesMk_1_eq {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : ↥(cocycles₁ A)) : cocyclesMk ((CategoryTheory.ConcreteCategory.hom (cochainsIso₁ A).inv) ⇑x) ⋯ = (CategoryTheory.ConcreteCategory.hom (isoCocycles₁ A).inv) x

Alias of groupCohomology.cocyclesMk₁_eq.

def groupCohomology.isoShortComplexH2 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : HomologicalComplex.sc (inhomogeneousCochains A) 2 ≅ shortComplexH2 A

The short complex Fun(G, A) --d₁₂--> Fun(G × G, A) --dTwo--> Fun(G × G × G, A) is isomorphic to the 2nd short complex associated to the complex of inhomogeneous cochains of A.

Equations

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

@[simp]

theorem groupCohomology.isoShortComplexH2_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (isoShortComplexH2 A).hom = CategoryTheory.CategoryStruct.comp ((HomologicalComplex.natIsoSc' (ModuleCat k) (ComplexShape.up ℕ) 1 2 3 isoShortComplexH2._proof_1 isoShortComplexH2._proof_2).hom.app (inhomogeneousCochains A)) (CategoryTheory.ShortComplex.isoMk (cochainsIso₁ A) (cochainsIso₂ A) (cochainsIso₃ A) ⋯ ⋯).hom

@[simp]

theorem groupCohomology.isoShortComplexH2_inv {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (isoShortComplexH2 A).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homMk (cochainsIso₁ A).inv (cochainsIso₂ A).inv (cochainsIso₃ A).inv ⋯ ⋯) ((HomologicalComplex.natIsoSc' (ModuleCat k) (ComplexShape.up ℕ) 1 2 3 isoShortComplexH2._proof_1 isoShortComplexH2._proof_2).inv.app (inhomogeneousCochains A))

@[deprecated groupCohomology.isoShortComplexH2 (since := "2025-07-11")]

def groupCohomology.shortComplexH2Iso {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : HomologicalComplex.sc (inhomogeneousCochains A) 2 ≅ shortComplexH2 A

Alias of groupCohomology.isoShortComplexH2.

---

The short complex Fun(G, A) --d₁₂--> Fun(G × G, A) --dTwo--> Fun(G × G × G, A) is isomorphic to the 2nd short complex associated to the complex of inhomogeneous cochains of A.

Equations

• @groupCohomology.shortComplexH2Iso = @groupCohomology.isoShortComplexH2

def groupCohomology.isoCocycles₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : cocycles A 2 ≅ ModuleCat.of k ↥(cocycles₂ A)

The 2-cocycles of the complex of inhomogeneous cochains of A are isomorphic to cocycles₂ A, which is a simpler type.

Equations

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

@[simp]

theorem groupCohomology.isoCocycles₂_hom_comp_i {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (isoCocycles₂ A).hom (shortComplexH2 A).moduleCatLeftHomologyData.i = CategoryTheory.CategoryStruct.comp (iCocycles A 2) (cochainsIso₂ A).hom

@[simp]

theorem groupCohomology.isoCocycles₂_hom_comp_i_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : (shortComplexH2 A).X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (isoCocycles₂ A).hom (CategoryTheory.CategoryStruct.comp (shortComplexH2 A).moduleCatLeftHomologyData.i h) = CategoryTheory.CategoryStruct.comp (iCocycles A 2) (CategoryTheory.CategoryStruct.comp (cochainsIso₂ A).hom h)

@[simp]

theorem groupCohomology.isoCocycles₂_hom_comp_i_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : CategoryTheory.ToType (cocycles A 2)) : (ModuleCat.Hom.hom (shortComplexH2 A).g).ker.subtype ((CategoryTheory.ConcreteCategory.hom (isoCocycles₂ A).hom) x) = (CategoryTheory.CategoryStruct.comp (iCocycles A 2) (cochainsIso₂ A).hom) x

@[simp]

theorem groupCohomology.isoCocycles₂_inv_comp_iCocycles {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (isoCocycles₂ A).inv (iCocycles A 2) = CategoryTheory.CategoryStruct.comp (shortComplexH2 A).moduleCatLeftHomologyData.i (cochainsIso₂ A).inv

@[simp]

theorem groupCohomology.isoCocycles₂_inv_comp_iCocycles_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : (inhomogeneousCochains A).X 2 ⟶ Z) : CategoryTheory.CategoryStruct.comp (isoCocycles₂ A).inv (CategoryTheory.CategoryStruct.comp (iCocycles A 2) h) = CategoryTheory.CategoryStruct.comp (shortComplexH2 A).moduleCatLeftHomologyData.i (CategoryTheory.CategoryStruct.comp (cochainsIso₂ A).inv h)

@[simp]

theorem groupCohomology.isoCocycles₂_inv_comp_iCocycles_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : CategoryTheory.ToType (ModuleCat.of k ↥(cocycles₂ A))) : (CategoryTheory.ConcreteCategory.hom (iCocycles A 2)) ((CategoryTheory.ConcreteCategory.hom (isoCocycles₂ A).inv) x) = (CategoryTheory.CategoryStruct.comp (shortComplexH2 A).moduleCatLeftHomologyData.i (cochainsIso₂ A).inv) x

@[simp]

theorem groupCohomology.toCocycles_comp_isoCocycles₂_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (toCocycles A 1 2) (isoCocycles₂ A).hom = CategoryTheory.CategoryStruct.comp (cochainsIso₁ A).hom (shortComplexH2 A).moduleCatLeftHomologyData.f'

@[simp]

theorem groupCohomology.toCocycles_comp_isoCocycles₂_hom_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : ModuleCat.of k ↥(cocycles₂ A) ⟶ Z) : CategoryTheory.CategoryStruct.comp (toCocycles A 1 2) (CategoryTheory.CategoryStruct.comp (isoCocycles₂ A).hom h) = CategoryTheory.CategoryStruct.comp (cochainsIso₁ A).hom (CategoryTheory.CategoryStruct.comp (shortComplexH2 A).moduleCatLeftHomologyData.f' h)

@[simp]

theorem groupCohomology.toCocycles_comp_isoCocycles₂_hom_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : CategoryTheory.ToType ((inhomogeneousCochains A).X 1)) : (CategoryTheory.ConcreteCategory.hom (isoCocycles₂ A).hom) ((CategoryTheory.ConcreteCategory.hom (toCocycles A 1 2)) x) = (CategoryTheory.CategoryStruct.comp (cochainsIso₁ A).hom (shortComplexH2 A).moduleCatLeftHomologyData.f') x

theorem groupCohomology.cocyclesMk₂_eq {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : ↥(cocycles₂ A)) : cocyclesMk ((CategoryTheory.ConcreteCategory.hom (cochainsIso₂ A).inv) ⇑x) ⋯ = (CategoryTheory.ConcreteCategory.hom (isoCocycles₂ A).inv) x

@[deprecated groupCohomology.cocyclesMk₂_eq (since := "2025-07-02")]

theorem groupCohomology.cocyclesMk_2_eq {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : ↥(cocycles₂ A)) : cocyclesMk ((CategoryTheory.ConcreteCategory.hom (cochainsIso₂ A).inv) ⇑x) ⋯ = (CategoryTheory.ConcreteCategory.hom (isoCocycles₂ A).inv) x

Alias of groupCohomology.cocyclesMk₂_eq.

@[reducible, inline]

abbrev groupCohomology.H0 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : ModuleCat k

Shorthand for the 0th group cohomology of a k-linear G-representation A, H⁰(G, A), defined as the 0th cohomology of the complex of inhomogeneous cochains of A.

Equations

• groupCohomology.H0 A = groupCohomology A 0

def groupCohomology.H0Iso {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : H0 A ≅ ModuleCat.of k ↥A.ρ.invariants

The 0th group cohomology of A, defined as the 0th cohomology of the complex of inhomogeneous cochains, is isomorphic to the invariants of the representation on A.

Equations

• groupCohomology.H0Iso A = (groupCohomology.inhomogeneousCochains A).isoHomologyπ₀.symm ≪≫ groupCohomology.cocyclesIso₀ A

@[simp]

theorem groupCohomology.π_comp_H0Iso_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (π A 0) (H0Iso A).hom = (cocyclesIso₀ A).hom

@[simp]

theorem groupCohomology.π_comp_H0Iso_hom_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : ModuleCat.of k ↥A.ρ.invariants ⟶ Z) : CategoryTheory.CategoryStruct.comp (π A 0) (CategoryTheory.CategoryStruct.comp (H0Iso A).hom h) = CategoryTheory.CategoryStruct.comp (cocyclesIso₀ A).hom h

@[simp]

theorem groupCohomology.π_comp_H0Iso_hom_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : CategoryTheory.ToType (cocycles A 0)) : (CategoryTheory.ConcreteCategory.hom (H0Iso A).hom) ((CategoryTheory.ConcreteCategory.hom (π A 0)) x) = (CategoryTheory.ConcreteCategory.hom (cocyclesIso₀ A).hom) x

theorem groupCohomology.H0_induction_on {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {C : ↑(H0 A) → Prop} (x : ↑(H0 A)) (h : ∀ (x : ↥A.ρ.invariants), C ((CategoryTheory.ConcreteCategory.hom (H0Iso A).inv) x)) : C x

def groupCohomology.H0IsoOfIsTrivial {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] : H0 A ≅ A.V

When the representation on A is trivial, then H⁰(G, A) is all of A.

Equations

• groupCohomology.H0IsoOfIsTrivial A = groupCohomology.H0Iso A ≪≫ (LinearEquiv.ofTop A.ρ.invariants ⋯).toModuleIso

@[simp]

theorem groupCohomology.H0IsoOfIsTrivial_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] : (H0IsoOfIsTrivial A).hom = CategoryTheory.CategoryStruct.comp (H0Iso A).hom (shortComplexH0 A).f

theorem groupCohomology.H0IsoOfIsTrivial_hom_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] (x : CategoryTheory.ToType (H0 A)) : (ModuleCat.Hom.hom (shortComplexH0 A).f) ((ModuleCat.Hom.hom (H0Iso A).hom) x) = (CategoryTheory.CategoryStruct.comp (H0Iso A).hom (shortComplexH0 A).f) x

theorem groupCohomology.π_comp_H0IsoOfIsTrivial_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] : CategoryTheory.CategoryStruct.comp (π A 0) (H0IsoOfIsTrivial A).hom = CategoryTheory.CategoryStruct.comp (iCocycles A 0) (cochainsIso₀ A).hom

theorem groupCohomology.π_comp_H0IsoOfIsTrivial_hom_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] {Z : ModuleCat k} (h : A.V ⟶ Z) : CategoryTheory.CategoryStruct.comp (π A 0) (CategoryTheory.CategoryStruct.comp (H0IsoOfIsTrivial A).hom h) = CategoryTheory.CategoryStruct.comp (iCocycles A 0) (CategoryTheory.CategoryStruct.comp (cochainsIso₀ A).hom h)

theorem groupCohomology.π_comp_H0IsoOfIsTrivial_hom_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] (x : CategoryTheory.ToType (cocycles A 0)) : (ModuleCat.Hom.hom (shortComplexH0 A).f) ((CategoryTheory.ConcreteCategory.hom (cocyclesIso₀ A).hom) x) = (CategoryTheory.ConcreteCategory.hom (cochainsIso₀ A).hom) ((CategoryTheory.ConcreteCategory.hom (iCocycles A 0)) x)

@[simp]

theorem groupCohomology.H0IsoOfIsTrivial_inv_apply {k G : Type u} [CommRing k] [Group G] {A : Rep k G} [A.IsTrivial] (x : ↑A.V) : (CategoryTheory.ConcreteCategory.hom (H0IsoOfIsTrivial A).inv) x = (CategoryTheory.ConcreteCategory.hom (H0Iso A).inv) ⟨x, ⋯⟩

@[reducible, inline]

abbrev groupCohomology.H1 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : ModuleCat k

Shorthand for the 1st group cohomology of a k-linear G-representation A, H¹(G, A), defined as the 1st cohomology of the complex of inhomogeneous cochains of A.

Equations

• groupCohomology.H1 A = groupCohomology A 1

def groupCohomology.H1π {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : ModuleCat.of k ↥(cocycles₁ A) ⟶ H1 A

The quotient map from the 1-cocycles of A, as a submodule of G → A, to H¹(G, A).

Equations

• groupCohomology.H1π A = CategoryTheory.CategoryStruct.comp (groupCohomology.isoCocycles₁ A).inv (groupCohomology.π A 1)

instance groupCohomology.instEpiModuleCatH1π {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.Epi (H1π A)

theorem groupCohomology.H1π_eq_zero_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x : ↥(cocycles₁ A)) : (CategoryTheory.ConcreteCategory.hom (H1π A)) x = 0 ↔ ⇑x ∈ coboundaries₁ A

theorem groupCohomology.H1π_eq_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x y : ↥(cocycles₁ A)) : (CategoryTheory.ConcreteCategory.hom (H1π A)) x = (CategoryTheory.ConcreteCategory.hom (H1π A)) y ↔ ⇑x - ⇑y ∈ coboundaries₁ A

theorem groupCohomology.H1_induction_on {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {C : ↑(H1 A) → Prop} (x : ↑(H1 A)) (h : ∀ (x : ↥(cocycles₁ A)), C ((CategoryTheory.ConcreteCategory.hom (H1π A)) x)) : C x

def groupCohomology.H1Iso {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : H1 A ≅ (shortComplexH1 A).moduleCatLeftHomologyData.H

The 1st group cohomology of A, defined as the 1st cohomology of the complex of inhomogeneous cochains, is isomorphic to cocycles₁ A ⧸ coboundaries₁ A, which is a simpler type.

Equations

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

@[simp]

theorem groupCohomology.π_comp_H1Iso_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (π A 1) (H1Iso A).hom = CategoryTheory.CategoryStruct.comp (isoCocycles₁ A).hom (shortComplexH1 A).moduleCatLeftHomologyData.π

@[simp]

theorem groupCohomology.π_comp_H1Iso_hom_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : (shortComplexH1 A).moduleCatLeftHomologyData.H ⟶ Z) : CategoryTheory.CategoryStruct.comp (π A 1) (CategoryTheory.CategoryStruct.comp (H1Iso A).hom h) = CategoryTheory.CategoryStruct.comp (isoCocycles₁ A).hom (CategoryTheory.CategoryStruct.comp (shortComplexH1 A).moduleCatLeftHomologyData.π h)

@[simp]

theorem groupCohomology.π_comp_H1Iso_hom_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : CategoryTheory.ToType (cocycles A 1)) : (CategoryTheory.ConcreteCategory.hom (H1Iso A).hom) ((CategoryTheory.ConcreteCategory.hom (π A 1)) x) = (shortComplexH1 A).moduleCatToCycles.range.mkQ ((CategoryTheory.ConcreteCategory.hom (isoCocycles₁ A).hom) x)

def groupCohomology.H1IsoOfIsTrivial {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] : H1 A ≅ ModuleCat.of k (Additive G →+ ↑A.V)

When A : Rep k G is a trivial representation of G, H¹(G, A) is isomorphic to the group homs G → A.

Equations

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

@[simp]

theorem groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] : CategoryTheory.CategoryStruct.comp (H1π A) (H1IsoOfIsTrivial A).hom = (cocycles₁IsoOfIsTrivial A).hom

@[simp]

theorem groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] {Z : ModuleCat k} (h : ModuleCat.of k (Additive G →+ ↑A.V) ⟶ Z) : CategoryTheory.CategoryStruct.comp (H1π A) (CategoryTheory.CategoryStruct.comp (H1IsoOfIsTrivial A).hom h) = CategoryTheory.CategoryStruct.comp (cocycles₁IsoOfIsTrivial A).hom h

@[simp]

theorem groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] (x : CategoryTheory.ToType (ModuleCat.of k ↥(cocycles₁ A))) : (CategoryTheory.ConcreteCategory.hom (H1IsoOfIsTrivial A).hom) ((CategoryTheory.ConcreteCategory.hom (H1π A)) x) = (CategoryTheory.ConcreteCategory.hom (cocycles₁IsoOfIsTrivial A).hom) x

theorem groupCohomology.H1IsoOfIsTrivial_H1π_apply_apply {k G : Type u} [CommRing k] [Group G] {A : Rep k G} [A.IsTrivial] (f : ↥(cocycles₁ A)) (x : Additive G) : ((CategoryTheory.ConcreteCategory.hom (H1IsoOfIsTrivial A).hom) ((CategoryTheory.ConcreteCategory.hom (H1π A)) f)) x = f (Additive.toMul x)

theorem groupCohomology.H1IsoOfIsTrivial_inv_apply {k G : Type u} [CommRing k] [Group G] {A : Rep k G} [A.IsTrivial] (f : Additive G →+ ↑A.V) : (CategoryTheory.ConcreteCategory.hom (H1IsoOfIsTrivial A).inv) f = (CategoryTheory.ConcreteCategory.hom (H1π A)) ((CategoryTheory.ConcreteCategory.hom (cocycles₁IsoOfIsTrivial A).inv) f)

@[reducible, inline]

abbrev groupCohomology.H2 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : ModuleCat k

Shorthand for the 2nd group cohomology of a k-linear G-representation A, H²(G, A), defined as the 2nd cohomology of the complex of inhomogeneous cochains of A.

Equations

• groupCohomology.H2 A = groupCohomology A 2

def groupCohomology.H2π {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : ModuleCat.of k ↥(cocycles₂ A) ⟶ H2 A

The quotient map from the 2-cocycles of A, as a submodule of G × G → A, to H²(G, A).

Equations

• groupCohomology.H2π A = CategoryTheory.CategoryStruct.comp (groupCohomology.isoCocycles₂ A).inv (groupCohomology.π A 2)

instance groupCohomology.instEpiModuleCatH2π {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.Epi (H2π A)

theorem groupCohomology.H2π_eq_zero_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x : ↥(cocycles₂ A)) : (CategoryTheory.ConcreteCategory.hom (H2π A)) x = 0 ↔ ⇑x ∈ coboundaries₂ A

theorem groupCohomology.H2π_eq_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x y : ↥(cocycles₂ A)) : (CategoryTheory.ConcreteCategory.hom (H2π A)) x = (CategoryTheory.ConcreteCategory.hom (H2π A)) y ↔ ⇑x - ⇑y ∈ coboundaries₂ A

theorem groupCohomology.H2_induction_on {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {C : ↑(H2 A) → Prop} (x : ↑(H2 A)) (h : ∀ (x : ↥(cocycles₂ A)), C ((CategoryTheory.ConcreteCategory.hom (H2π A)) x)) : C x

def groupCohomology.H2Iso {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : H2 A ≅ (shortComplexH2 A).moduleCatLeftHomologyData.H

The 2nd group cohomology of A, defined as the 2nd cohomology of the complex of inhomogeneous cochains, is isomorphic to cocycles₂ A ⧸ coboundaries₂ A, which is a simpler type.

Equations

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

@[simp]

theorem groupCohomology.π_comp_H2Iso_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (π A 2) (H2Iso A).hom = CategoryTheory.CategoryStruct.comp (isoCocycles₂ A).hom (shortComplexH2 A).moduleCatLeftHomologyData.π

@[simp]

theorem groupCohomology.π_comp_H2Iso_hom_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : (shortComplexH2 A).moduleCatLeftHomologyData.H ⟶ Z) : CategoryTheory.CategoryStruct.comp (π A 2) (CategoryTheory.CategoryStruct.comp (H2Iso A).hom h) = CategoryTheory.CategoryStruct.comp (isoCocycles₂ A).hom (CategoryTheory.CategoryStruct.comp (shortComplexH2 A).moduleCatLeftHomologyData.π h)

@[simp]

theorem groupCohomology.π_comp_H2Iso_hom_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : CategoryTheory.ToType (cocycles A 2)) : (CategoryTheory.ConcreteCategory.hom (H2Iso A).hom) ((CategoryTheory.ConcreteCategory.hom (π A 2)) x) = (shortComplexH2 A).moduleCatToCycles.range.mkQ ((CategoryTheory.ConcreteCategory.hom (isoCocycles₂ A).hom) x)