Documentation

Mathlib.RepresentationTheory.GroupCohomology.LowDegree

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

Let k be a commutative ring and G a group. This file gives simple expressions for the group cohomology of a k-linear G-representation A in degrees 0, 1 and 2.

In RepresentationTheory.GroupCohomology.Basic, 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. Moreover, cohomology of a complex is defined as an abstract cokernel, whereas the definitions here are explicit quotients of cocycles by coboundaries.

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 oneCocycles 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 RepresentationTheory.GroupCohomology.Basic, groupCohomology.cocycles A n and groupCohomology A n, and the nCocycles and Hn A in this file, for n = 0, 1, 2.

Main definitions #

TODO #

def groupCohomology.zeroCochainsLequiv {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :

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

Equations
def groupCohomology.oneCochainsLequiv {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :
((inhomogeneousCochains A).X 1) ≃ₗ[k] GA.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
def groupCohomology.twoCochainsLequiv {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :
((inhomogeneousCochains A).X 2) ≃ₗ[k] G × GA.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
def groupCohomology.threeCochainsLequiv {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :
((inhomogeneousCochains A).X 3) ≃ₗ[k] G × G × GA.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.dZero {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :
A.V →ₗ[k] GA.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
@[simp]
theorem groupCohomology.dZero_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (m : A.V) (g : G) :
(dZero A) m g = (A.ρ g) m - m
@[simp]
theorem groupCohomology.dZero_eq_zero {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] :
dZero A = 0
def groupCohomology.dOne {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :
(GA.V) →ₗ[k] G × GA.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.dOne A = { toFun := fun (f : GA.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.dOne_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (f : GA.V) (g : G × G) :
(dOne A) f g = (A.ρ g.1) (f g.2) - f (g.1 * g.2) + f g.1
def groupCohomology.dTwo {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :
(G × GA.V) →ₗ[k] G × G × GA.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.dTwo_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (f : G × GA.V) (g : G × G × G) :
(dTwo A) f g = (A.ρ g.1) (f (g.2.1, g.2.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)

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

  C⁰(G, A) ---d⁰---> C¹(G, A)
  |                    |
  |                    |
  |                    |
  v                    v
  A ---- dZero ---> Fun(G, A)

where the vertical arrows are zeroCochainsLequiv and oneCochainsLequiv respectively.

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

  C¹(G, A) ---d¹-----> C²(G, A)
    |                      |
    |                      |
    |                      |
    v                      v
  Fun(G, A) -dOne-> Fun(G × G, A)

where the vertical arrows are oneCochainsLequiv and twoCochainsLequiv respectively.

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

      C²(G, A) -------d²-----> C³(G, A)
        |                         |
        |                         |
        |                         |
        v                         v
  Fun(G × G, A) --dTwo--> Fun(G × G × G, A)

where the vertical arrows are twoCochainsLequiv and threeCochainsLequiv respectively.

theorem groupCohomology.dOne_comp_dZero {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :
theorem groupCohomology.dTwo_comp_dOne {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :
def groupCohomology.oneCocycles {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :
Submodule k (GA.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
def groupCohomology.twoCocycles {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :
Submodule k (G × GA.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
@[simp]
theorem groupCohomology.oneCocycles.coe_mk {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : GA.V) (hf : f oneCocycles A) :
f, hf = f
@[simp]
theorem groupCohomology.oneCocycles.val_eq_coe {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : (oneCocycles A)) :
f = f
theorem groupCohomology.oneCocycles_ext {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f₁ f₂ : (oneCocycles A)} (h : ∀ (g : G), f₁ g = f₂ g) :
f₁ = f₂
theorem groupCohomology.mem_oneCocycles_def {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : GA.V) :
f oneCocycles A ∀ (g h : G), (A.ρ g) (f h) - f (g * h) + f g = 0
theorem groupCohomology.mem_oneCocycles_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : GA.V) :
f oneCocycles A ∀ (g h : G), f (g * h) = (A.ρ g) (f h) + f g
@[simp]
theorem groupCohomology.oneCocycles_map_one {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : (oneCocycles A)) :
f 1 = 0
@[simp]
theorem groupCohomology.oneCocycles_map_inv {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : (oneCocycles A)) (g : G) :
(A.ρ g) (f g⁻¹) = -f g
theorem groupCohomology.oneCocycles_map_mul_of_isTrivial {k G : Type u} [CommRing k] [Group G] {A : Rep k G} [A.IsTrivial] (f : (oneCocycles A)) (g h : G) :
f (g * h) = f g + f h

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.oneCocyclesLequivOfIsTrivial_symm_apply_coe {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [hA : A.IsTrivial] (f : Additive G →+ A.V) (a : Additive G) :
@[simp]
theorem groupCohomology.oneCocyclesLequivOfIsTrivial_apply_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [hA : A.IsTrivial] (f : (oneCocycles A)) (a✝ : Additive G) :
((oneCocyclesLequivOfIsTrivial A) f) a✝ = (f Additive.toMul) a✝
@[simp]
theorem groupCohomology.twoCocycles.coe_mk {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : G × GA.V) (hf : f twoCocycles A) :
f, hf = f
@[simp]
theorem groupCohomology.twoCocycles.val_eq_coe {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : (twoCocycles A)) :
f = f
theorem groupCohomology.twoCocycles_ext {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f₁ f₂ : (twoCocycles A)} (h : ∀ (g h : G), f₁ (g, h) = f₂ (g, h)) :
f₁ = f₂
theorem groupCohomology.mem_twoCocycles_def {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : G × GA.V) :
f twoCocycles 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_twoCocycles_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : G × GA.V) :
f twoCocycles A ∀ (g h j : G), f (g * h, j) + f (g, h) = (A.ρ g) (f (h, j)) + f (g, h * j)
theorem groupCohomology.twoCocycles_map_one_fst {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : (twoCocycles A)) (g : G) :
f (1, g) = f (1, 1)
theorem groupCohomology.twoCocycles_map_one_snd {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : (twoCocycles A)) (g : G) :
f (g, 1) = (A.ρ g) (f (1, 1))
theorem groupCohomology.twoCocycles_ρ_map_inv_sub_map_inv {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : (twoCocycles A)) (g : G) :
(A.ρ g) (f (g⁻¹, g)) - f (g, g⁻¹) = f (1, 1) - f (g, 1)
def groupCohomology.oneCoboundaries {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :

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
def groupCohomology.twoCoboundaries {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :

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
def groupCohomology.oneCoboundariesOfMemRange {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f : GA.V} (h : f LinearMap.range (dZero A)) :

Makes a 1-coboundary out of f ∈ Im(d⁰).

Equations
theorem groupCohomology.oneCoboundaries_of_mem_range_apply {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f : GA.V} (h : f LinearMap.range (dZero A)) :
def groupCohomology.oneCoboundariesOfEq {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f : GA.V} {x : A.V} (hf : ∀ (g : G), (A.ρ g) x - x = f g) :

Makes a 1-coboundary out of f : G → A and x such that ρ(g)(x) - x = f(g) for all g : G.

Equations
theorem groupCohomology.oneCoboundariesOfEq_apply {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f : GA.V} {x : A.V} (hf : ∀ (g : G), (A.ρ g) x - x = f g) :
(oneCoboundariesOfEq hf) = f
theorem groupCohomology.mem_oneCoboundaries_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : (oneCocycles A)) :
f oneCoboundaries A ∃ (x : A.V), ∀ (g : G), (A.ρ g) x - x = f g
def groupCohomology.twoCoboundariesOfMemRange {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f : G × GA.V} (h : f LinearMap.range (dOne A)) :

Makes a 2-coboundary out of f ∈ Im(d¹).

Equations
theorem groupCohomology.twoCoboundariesOfMemRange_apply {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f : G × GA.V} (h : f LinearMap.range (dOne A)) :
def groupCohomology.twoCoboundariesOfEq {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f : G × GA.V} {x : GA.V} (hf : ∀ (g h : G), (A.ρ g) (x h) - x (g * h) + x g = f (g, h)) :

Makes a 2-coboundary out of f : G × G → A and x : G → A such that ρ(g)(x(h)) - x(gh) + x(g) = f(g, h) for all g, h : G.

Equations
theorem groupCohomology.twoCoboundariesOfEq_apply {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f : G × GA.V} {x : GA.V} (hf : ∀ (g h : G), (A.ρ g) (x h) - x (g * h) + x g = f (g, h)) :
(twoCoboundariesOfEq hf) = f
theorem groupCohomology.mem_twoCoboundaries_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : (twoCocycles A)) :
f twoCoboundaries A ∃ (x : GA.V), ∀ (g h : G), (A.ρ g) (x h) - x (g * h) + x g = f (g, h)
def groupCohomology.IsOneCocycle {G : Type u_1} {A : Type u_2} [Mul G] [AddCommGroup A] [SMul G A] (f : GA) :

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

Equations
def groupCohomology.IsTwoCocycle {G : Type u_1} {A : Type u_2} [Mul G] [AddCommGroup A] [SMul G A] (f : G × GA) :

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
theorem groupCohomology.map_one_of_isOneCocycle {G : Type u_1} {A : Type u_2} [Monoid G] [AddCommGroup A] [MulAction G A] {f : GA} (hf : IsOneCocycle f) :
f 1 = 0
theorem groupCohomology.map_one_fst_of_isTwoCocycle {G : Type u_1} {A : Type u_2} [Monoid G] [AddCommGroup A] [MulAction G A] {f : G × GA} (hf : IsTwoCocycle f) (g : G) :
f (1, g) = f (1, 1)
theorem groupCohomology.map_one_snd_of_isTwoCocycle {G : Type u_1} {A : Type u_2} [Monoid G] [AddCommGroup A] [MulAction G A] {f : G × GA} (hf : IsTwoCocycle f) (g : G) :
f (g, 1) = g f (1, 1)
theorem groupCohomology.map_inv_of_isOneCocycle {G : Type u_1} {A : Type u_2} [Group G] [AddCommGroup A] [MulAction G A] {f : GA} (hf : IsOneCocycle f) (g : G) :
g f g⁻¹ = -f g
theorem groupCohomology.smul_map_inv_sub_map_inv_of_isTwoCocycle {G : Type u_1} {A : Type u_2} [Group G] [AddCommGroup A] [MulAction G A] {f : G × GA} (hf : IsTwoCocycle f) (g : G) :
g f (g⁻¹, g) - f (g, g⁻¹) = f (1, 1) - f (g, 1)
def groupCohomology.IsOneCoboundary {G : Type u_1} {A : Type u_2} [AddCommGroup A] [SMul G A] (f : GA) :

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
def groupCohomology.IsTwoCoboundary {G : Type u_1} {A : Type u_2} [Mul G] [AddCommGroup A] [SMul G A] (f : G × GA) :

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

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

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

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

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

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

def groupCohomology.IsMulOneCocycle {G : Type u_1} {M : Type u_2} [Mul G] [CommGroup M] [SMul G M] (f : GM) :

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
def groupCohomology.IsMulTwoCocycle {G : Type u_1} {M : Type u_2} [Mul G] [CommGroup M] [SMul G M] (f : G × GM) :

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
theorem groupCohomology.map_one_of_isMulOneCocycle {G : Type u_1} {M : Type u_2} [Monoid G] [CommGroup M] [MulAction G M] {f : GM} (hf : IsMulOneCocycle f) :
f 1 = 1
theorem groupCohomology.map_one_fst_of_isMulTwoCocycle {G : Type u_1} {M : Type u_2} [Monoid G] [CommGroup M] [MulAction G M] {f : G × GM} (hf : IsMulTwoCocycle f) (g : G) :
f (1, g) = f (1, 1)
theorem groupCohomology.map_one_snd_of_isMulTwoCocycle {G : Type u_1} {M : Type u_2} [Monoid G] [CommGroup M] [MulAction G M] {f : G × GM} (hf : IsMulTwoCocycle f) (g : G) :
f (g, 1) = g f (1, 1)
theorem groupCohomology.map_inv_of_isMulOneCocycle {G : Type u_1} {M : Type u_2} [Group G] [CommGroup M] [MulAction G M] {f : GM} (hf : IsMulOneCocycle f) (g : G) :
g f g⁻¹ = (f g)⁻¹
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 × GM} (hf : IsMulTwoCocycle f) (g : G) :
g f (g⁻¹, g) / f (g, g⁻¹) = f (1, 1) / f (g, 1)
def groupCohomology.IsMulOneCoboundary {G : Type u_1} {M : Type u_2} [CommGroup M] [SMul G M] (f : GM) :

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
def groupCohomology.IsMulTwoCoboundary {G : Type u_1} {M : Type u_2} [Mul G] [CommGroup M] [SMul G M] (f : G × GM) :

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

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

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

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

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
@[reducible, inline]
abbrev groupCohomology.H0 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :
Submodule k A.V

We define the 0th group cohomology of a k-linear G-representation A, H⁰(G, A), to be the invariants of the representation, Aᴳ.

Equations
@[reducible, inline]
abbrev groupCohomology.H1 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :

We define the 1st group cohomology of a k-linear G-representation A, H¹(G, A), to be 1-cocycles (i.e. Z¹(G, A) := Ker(d¹ : Fun(G, A) → Fun(G², A)) modulo 1-coboundaries (i.e. B¹(G, A) := Im(d⁰: A → Fun(G, A))).

Equations
def groupCohomology.H1_π {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :

The quotient map Z¹(G, A) → H¹(G, A).

Equations
@[reducible, inline]
abbrev groupCohomology.H2 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :

We define the 2nd group cohomology of a k-linear G-representation A, H²(G, A), to be 2-cocycles (i.e. Z²(G, A) := Ker(d² : Fun(G², A) → Fun(G³, A)) modulo 2-coboundaries (i.e. B²(G, A) := Im(d¹: Fun(G, A) → Fun(G², A))).

Equations
def groupCohomology.H2_π {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :

The quotient map Z²(G, A) → H²(G, A).

Equations
def groupCohomology.H0LequivOfIsTrivial {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] :
(H0 A) ≃ₗ[k] A.V

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

Equations
theorem groupCohomology.H0LequivOfIsTrivial_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] (x : (H0 A)) :
@[simp]
theorem groupCohomology.H0LequivOfIsTrivial_symm_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] (x : 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
@[simp]
theorem groupCohomology.H1LequivOfIsTrivial_H1_π_apply_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] (f : (oneCocycles A)) (x : Additive G) :

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

Equations

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.
def groupCohomology.isoH0 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :

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

The short complex A --dZero--> Fun(G, A) --dOne--> Fun(G × G, A).

Equations

The short complex A --dZero--> Fun(G, A) --dOne--> 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.shortComplexH1Iso_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :
(shortComplexH1Iso A).hom = { τ₁ := ModuleCat.ofHom (zeroCochainsLequiv A), τ₂ := ModuleCat.ofHom (oneCochainsLequiv A), τ₃ := ModuleCat.ofHom (twoCochainsLequiv A), comm₁₂ := , comm₂₃ := }

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

Equations
  • One or more equations did not get rendered due to their size.
def groupCohomology.isoH1 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :

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

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

The short complex Fun(G, A) --dOne--> Fun(G × G, A) --dTwo--> Fun(G × G × G, A).

Equations

The short complex Fun(G, A) --dOne--> 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.shortComplexH2Iso_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :
(shortComplexH2Iso A).hom = { τ₁ := ModuleCat.ofHom (oneCochainsLequiv A), τ₂ := ModuleCat.ofHom (twoCochainsLequiv A), τ₃ := ModuleCat.ofHom (threeCochainsLequiv A), comm₁₂ := , comm₂₃ := }

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

Equations
  • One or more equations did not get rendered due to their size.
def groupCohomology.isoH2 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :

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

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