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

Later this file will contain an identification between the definition in RepresentationTheory.GroupCohomology.Basic, groupCohomology A n, and the Hn A in this file, for n = 0, 1, 2.

## Main definitions #

• groupCohomology.H0 A: the invariants Aᴳ of the G-representation on A.
• groupCohomology.H1 A: 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))).
• groupCohomology.H2 A: 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))).
• groupCohomology.H1LequivOfIsTrivial: the isomorphism H¹(G, A) ≃ Hom(G, A) when the representation on A is trivial.

## TODO #

• Identify Hn A as defined in this file with groupCohomology A n for n = 0, 1, 2.
• Hilbert's theorem 90
• The relationship between H2 and group extensions
• The inflation-restriction exact sequence
• Nonabelian group cohomology
def groupCohomology.zeroCochainsLequiv {k : Type u} {G : Type u} [] [] (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
Instances For
def groupCohomology.oneCochainsLequiv {k : Type u} {G : Type u} [] [] (A : Rep k G) :

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
Instances For
def groupCohomology.twoCochainsLequiv {k : Type u} {G : Type u} [] [] (A : Rep k G) :
≃ₗ[k] G × G

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
Instances For
def groupCohomology.threeCochainsLequiv {k : Type u} {G : Type u} [] [] (A : Rep k G) :
≃ₗ[k] G × G × G

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
Instances For
@[simp]
theorem groupCohomology.dZero_apply {k : Type u} {G : Type u} [] [] (A : Rep k G) (m : ) (g : G) :
m g = (() g) m - m
def groupCohomology.dZero {k : Type u} {G : Type u} [] [] (A : Rep k G) :
→ₗ[k] G

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
• One or more equations did not get rendered due to their size.
Instances For
theorem groupCohomology.dZero_ker_eq_invariants {k : Type u} {G : Type u} [] [] (A : Rep k G) :
@[simp]
theorem groupCohomology.dZero_eq_zero {k : Type u} {G : Type u} [] [] (A : Rep k G) [] :
@[simp]
theorem groupCohomology.dOne_apply {k : Type u} {G : Type u} [] [] (A : Rep k G) (f : G) (g : G × G) :
f g = (() g.1) (f g.2) - f (g.1 * g.2) + f g.1
def groupCohomology.dOne {k : Type u} {G : Type u} [] [] (A : Rep k G) :
(G) →ₗ[k] G × G

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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem groupCohomology.dTwo_apply {k : Type u} {G : Type u} [] [] (A : Rep k G) (f : G × G) (g : G × G × G) :
f g = (() 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)
def groupCohomology.dTwo {k : Type u} {G : Type u} [] [] (A : Rep k G) :
(G × G) →ₗ[k] G × G × G

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.
Instances For
theorem groupCohomology.dZero_comp_eq {k : Type u} {G : Type u} [] [] (A : Rep k G) :

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.

theorem groupCohomology.dOne_comp_eq {k : Type u} {G : Type u} [] [] (A : Rep k G) :

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.

theorem groupCohomology.dTwo_comp_eq {k : Type u} {G : Type u} [] [] (A : Rep k G) :

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 : Type u} {G : Type u} [] [] (A : Rep k G) :
theorem groupCohomology.dTwo_comp_dOne {k : Type u} {G : Type u} [] [] (A : Rep k G) :
def groupCohomology.oneCocycles {k : Type u} {G : Type u} [] [] (A : Rep k G) :
Submodule k (G)

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
Instances For
def groupCohomology.twoCocycles {k : Type u} {G : Type u} [] [] (A : Rep k G) :
Submodule k (G × G)

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
Instances For
theorem groupCohomology.mem_oneCocycles_def {k : Type u} {G : Type u} [] [] {A : Rep k G} (f : G) :
∀ (g h : G), (() g) (f h) - f (g * h) + f g = 0
theorem groupCohomology.mem_oneCocycles_iff {k : Type u} {G : Type u} [] [] {A : Rep k G} (f : G) :
∀ (g h : G), f (g * h) = (() g) (f h) + f g
@[simp]
theorem groupCohomology.oneCocycles_map_one {k : Type u} {G : Type u} [] [] {A : Rep k G} (f : ) :
f 1 = 0
@[simp]
theorem groupCohomology.oneCocycles_map_inv {k : Type u} {G : Type u} [] [] {A : Rep k G} (f : ) (g : G) :
(() g) (f g⁻¹) = -f g
theorem groupCohomology.oneCocycles_map_mul_of_isTrivial {k : Type u} {G : Type u} [] [] {A : Rep k G} [] (f : ) (g : G) (h : G) :
f (g * h) = f g + f h
theorem groupCohomology.mem_oneCocycles_of_addMonoidHom {k : Type u} {G : Type u} [] [] {A : Rep k G} [] (f : ) :
@[simp]
theorem groupCohomology.oneCocyclesLequivOfIsTrivial_symm_apply_coe {k : Type u} {G : Type u} [] [] (A : Rep k G) [hA : ] (f : ) (a : ) :
= f a
@[simp]
theorem groupCohomology.oneCocyclesLequivOfIsTrivial_apply_apply {k : Type u} {G : Type u} [] [] (A : Rep k G) [hA : ] (f : ) :
∀ (a : ), = (f Additive.toMul) a
def groupCohomology.oneCocyclesLequivOfIsTrivial {k : Type u} {G : Type u} [] [] (A : Rep k G) [hA : ] :

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.
Instances For
theorem groupCohomology.mem_twoCocycles_def {k : Type u} {G : Type u} [] [] {A : Rep k G} (f : G × G) :
∀ (g h j : G), (() g) (f (h, j)) - f (g * h, j) + f (g, h * j) - f (g, h) = 0
theorem groupCohomology.mem_twoCocycles_iff {k : Type u} {G : Type u} [] [] {A : Rep k G} (f : G × G) :
∀ (g h j : G), f (g * h, j) + f (g, h) = (() g) (f (h, j)) + f (g, h * j)
theorem groupCohomology.twoCocycles_map_one_fst {k : Type u} {G : Type u} [] [] {A : Rep k G} (f : ) (g : G) :
f (1, g) = f (1, 1)
theorem groupCohomology.twoCocycles_map_one_snd {k : Type u} {G : Type u} [] [] {A : Rep k G} (f : ) (g : G) :
f (g, 1) = (() g) (f (1, 1))
theorem groupCohomology.twoCocycles_ρ_map_inv_sub_map_inv {k : Type u} {G : Type u} [] [] {A : Rep k G} (f : ) (g : G) :
(() g) (f (g⁻¹, g)) - f (g, g⁻¹) = f (1, 1) - f (g, 1)
def groupCohomology.oneCoboundaries {k : Type u} {G : Type u} [] [] (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
• One or more equations did not get rendered due to their size.
Instances For
def groupCohomology.twoCoboundaries {k : Type u} {G : Type u} [] [] (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
• One or more equations did not get rendered due to their size.
Instances For
theorem groupCohomology.mem_oneCoboundaries_of_dZero_apply {k : Type u} {G : Type u} [] [] {A : Rep k G} (x : ) :
{ val := , property := (_ : = 0 x) }
theorem groupCohomology.mem_oneCoboundaries_of_mem_range {k : Type u} {G : Type u} [] [] {A : Rep k G} (f : G) (h : ) :
{ val := f, property := (_ : ) }
theorem groupCohomology.mem_range_of_mem_oneCoboundaries {k : Type u} {G : Type u} [] [] {A : Rep k G} (f : ) (h : ) :
theorem groupCohomology.oneCoboundaries_eq_bot_of_isTrivial {k : Type u} {G : Type u} [] [] (A : Rep k G) [] :
theorem groupCohomology.mem_twoCoboundaries_of_dOne_apply {k : Type u} {G : Type u} [] [] {A : Rep k G} (x : G) :
{ val := x, property := (_ : = 0 x) }
theorem groupCohomology.mem_twoCoboundaries_of_mem_range {k : Type u} {G : Type u} [] [] {A : Rep k G} (f : G × G) (h : ) :
{ val := f, property := (_ : ) }
theorem groupCohomology.mem_range_of_mem_twoCoboundaries {k : Type u} {G : Type u} [] [] {A : Rep k G} (f : ) (h : ) :
@[inline, reducible]
abbrev groupCohomology.H0 {k : Type u} {G : Type u} [] [] (A : Rep k G) :

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
Instances For
@[inline, reducible]
abbrev groupCohomology.H1 {k : Type u} {G : Type u} [] [] (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
Instances For
def groupCohomology.H1_π {k : Type u} {G : Type u} [] [] (A : Rep k G) :

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

Equations
Instances For
@[inline, reducible]
abbrev groupCohomology.H2 {k : Type u} {G : Type u} [] [] (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
Instances For
def groupCohomology.H2_π {k : Type u} {G : Type u} [] [] (A : Rep k G) :

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

Equations
Instances For
def groupCohomology.H0LequivOfIsTrivial {k : Type u} {G : Type u} [] [] (A : Rep k G) [] :

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

Equations
Instances For
@[simp]
theorem groupCohomology.H0LequivOfIsTrivial_eq_subtype {k : Type u} {G : Type u} [] [] (A : Rep k G) [] :
theorem groupCohomology.H0LequivOfIsTrivial_apply {k : Type u} {G : Type u} [] [] (A : Rep k G) [] (x : ) :
@[simp]
theorem groupCohomology.H0LequivOfIsTrivial_symm_apply {k : Type u} {G : Type u} [] [] (A : Rep k G) [] (x : ) :
= x
def groupCohomology.H1LequivOfIsTrivial {k : Type u} {G : Type u} [] [] (A : Rep k G) [] :

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.
Instances For
theorem groupCohomology.H1LequivOfIsTrivial_comp_H1_π {k : Type u} {G : Type u} [] [] (A : Rep k G) [] :
@[simp]
theorem groupCohomology.H1LequivOfIsTrivial_H1_π_apply_apply {k : Type u} {G : Type u} [] [] (A : Rep k G) [] (f : ) (x : ) :
() x = f (Additive.toMul x)
@[simp]
theorem groupCohomology.H1LequivOfIsTrivial_symm_apply {k : Type u} {G : Type u} [] [] (A : Rep k G) [] (f : ) :