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

• 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.
• groupCohomology.isoHn for n = 0, 1, 2: an isomorphism groupCohomology A n ≅ groupCohomology.Hn A.

TODO

• The relationship between H2 and group extensions
• The inflation-restriction exact sequence
• Nonabelian group cohomology

def groupCohomology.zeroCochainsLequiv {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : ↑((groupCohomology.inhomogeneousCochains A).X 0) ≃ₗ[k] CoeSort.coe A

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

Equations

• groupCohomology.zeroCochainsLequiv A = LinearEquiv.funUnique (Fin 0 → G) k (CoeSort.coe A)

def groupCohomology.oneCochainsLequiv {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : ↑((groupCohomology.inhomogeneousCochains A).X 1) ≃ₗ[k] G → CoeSort.coe A

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.oneCochainsLequiv A = LinearEquiv.funCongrLeft k (CoeSort.coe A) (Equiv.funUnique (Fin 1) G).symm

def groupCohomology.twoCochainsLequiv {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : ↑((groupCohomology.inhomogeneousCochains A).X 2) ≃ₗ[k] G × G → CoeSort.coe A

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.twoCochainsLequiv A = LinearEquiv.funCongrLeft k (CoeSort.coe A) (piFinTwoEquiv fun (x : Fin 2) => G).symm

def groupCohomology.threeCochainsLequiv {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : ↑((groupCohomology.inhomogeneousCochains A).X 3) ≃ₗ[k] G × G × G → CoeSort.coe A

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) : CoeSort.coe A →ₗ[k] G → CoeSort.coe A

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.dZero A = { toFun := fun (m : CoeSort.coe A) (g : G) => (A.ρ g) m - m, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem groupCohomology.dZero_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (m : CoeSort.coe A) (g : G) : (groupCohomology.dZero A) m g = (A.ρ g) m - m

theorem groupCohomology.dZero_ker_eq_invariants {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : LinearMap.ker (groupCohomology.dZero A) = A.ρ.invariants

@[simp]

theorem groupCohomology.dZero_eq_zero {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] : groupCohomology.dZero A = 0

def groupCohomology.dOne {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (G → CoeSort.coe A) →ₗ[k] G × G → CoeSort.coe A

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 : G → CoeSort.coe A) (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 : G → CoeSort.coe A) (g : G × G) : (groupCohomology.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 × G → CoeSort.coe A) →ₗ[k] G × G × G → CoeSort.coe A

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 × G → CoeSort.coe A) (g : G × G × G) : (groupCohomology.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)

theorem groupCohomology.dZero_comp_eq {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : groupCohomology.dZero A ∘ₗ ↑(groupCohomology.zeroCochainsLequiv A) = ↑(groupCohomology.oneCochainsLequiv A) ∘ₗ ((groupCohomology.inhomogeneousCochains A).d 0 1).hom

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 G : Type u} [CommRing k] [Group G] (A : Rep k G) : groupCohomology.dOne A ∘ₗ ↑(groupCohomology.oneCochainsLequiv A) = ↑(groupCohomology.twoCochainsLequiv A) ∘ₗ ((groupCohomology.inhomogeneousCochains A).d 1 2).hom

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 G : Type u} [CommRing k] [Group G] (A : Rep k G) : groupCohomology.dTwo A ∘ₗ ↑(groupCohomology.twoCochainsLequiv A) = ↑(groupCohomology.threeCochainsLequiv A) ∘ₗ ((groupCohomology.inhomogeneousCochains A).d 2 3).hom

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) : groupCohomology.dOne A ∘ₗ groupCohomology.dZero A = 0

theorem groupCohomology.dTwo_comp_dOne {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : groupCohomology.dTwo A ∘ₗ groupCohomology.dOne A = 0

def groupCohomology.oneCocycles {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : Submodule k (G → CoeSort.coe A)

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.oneCocycles A = LinearMap.ker (groupCohomology.dOne A)

def groupCohomology.twoCocycles {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : Submodule k (G × G → CoeSort.coe A)

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.twoCocycles A = LinearMap.ker (groupCohomology.dTwo A)

instance groupCohomology.instFunLikeSubtypeForallCoeRepMemSubmoduleOneCocycles {k G : Type u} [CommRing k] [Group G] {A : Rep k G} : FunLike (↥(groupCohomology.oneCocycles A)) G (CoeSort.coe A)

Equations

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

@[simp]

theorem groupCohomology.oneCocycles.coe_mk {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : G → CoeSort.coe A) (hf : f ∈ groupCohomology.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 : ↥(groupCohomology.oneCocycles A)) : ↑f = ⇑f

theorem groupCohomology.oneCocycles_ext {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f₁ f₂ : ↥(groupCohomology.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 : G → CoeSort.coe A) : f ∈ groupCohomology.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 : G → CoeSort.coe A) : f ∈ groupCohomology.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 : ↥(groupCohomology.oneCocycles A)) : f 1 = 0

@[simp]

theorem groupCohomology.oneCocycles_map_inv {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : ↥(groupCohomology.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 : ↥(groupCohomology.oneCocycles A)) (g h : G) : f (g * h) = f g + f h

theorem groupCohomology.mem_oneCocycles_of_addMonoidHom {k G : Type u} [CommRing k] [Group G] {A : Rep k G} [A.IsTrivial] (f : Additive G →+ CoeSort.coe A) : ⇑f ∘ ⇑Additive.ofMul ∈ groupCohomology.oneCocycles A

def groupCohomology.oneCocyclesLequivOfIsTrivial {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [hA : A.IsTrivial] : ↥(groupCohomology.oneCocycles A) ≃ₗ[k] Additive G →+ CoeSort.coe A

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_apply_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [hA : A.IsTrivial] (f : ↥(groupCohomology.oneCocycles A)) (a✝ : Additive G) : ((groupCohomology.oneCocyclesLequivOfIsTrivial A) f) a✝ = (⇑f ∘ ⇑Additive.toMul) a✝

@[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 →+ CoeSort.coe A) (a : Additive G) : ↑((groupCohomology.oneCocyclesLequivOfIsTrivial A).symm f) a = f a

instance groupCohomology.instFunLikeSubtypeForallProdCoeRepMemSubmoduleTwoCocycles {k G : Type u} [CommRing k] [Group G] {A : Rep k G} : FunLike (↥(groupCohomology.twoCocycles A)) (G × G) (CoeSort.coe A)

Equations

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

@[simp]

theorem groupCohomology.twoCocycles.coe_mk {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : G × G → CoeSort.coe A) (hf : f ∈ groupCohomology.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 : ↥(groupCohomology.twoCocycles A)) : ↑f = ⇑f

theorem groupCohomology.twoCocycles_ext {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f₁ f₂ : ↥(groupCohomology.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 × G → CoeSort.coe A) : f ∈ groupCohomology.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 × G → CoeSort.coe A) : f ∈ groupCohomology.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 : ↥(groupCohomology.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 : ↥(groupCohomology.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 : ↥(groupCohomology.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) : Submodule k ↥(groupCohomology.oneCocycles A)

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.oneCoboundaries A = LinearMap.range (LinearMap.codRestrict (groupCohomology.oneCocycles A) (groupCohomology.dZero A) ⋯)

def groupCohomology.twoCoboundaries {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : Submodule k ↥(groupCohomology.twoCocycles A)

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.twoCoboundaries A = LinearMap.range (LinearMap.codRestrict (groupCohomology.twoCocycles A) (groupCohomology.dOne A) ⋯)

def groupCohomology.oneCoboundariesOfMemRange {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f : G → CoeSort.coe A} (h : f ∈ LinearMap.range (groupCohomology.dZero A)) : ↥(groupCohomology.oneCoboundaries A)

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

Equations

• groupCohomology.oneCoboundariesOfMemRange h = ⟨⟨f, ⋯⟩, ⋯⟩

theorem groupCohomology.oneCoboundaries_of_mem_range_apply {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f : G → CoeSort.coe A} (h : f ∈ LinearMap.range (groupCohomology.dZero A)) : ↑↑(groupCohomology.oneCoboundariesOfMemRange h) = f

def groupCohomology.oneCoboundariesOfEq {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f : G → CoeSort.coe A} {x : CoeSort.coe A} (hf : ∀ (g : G), (A.ρ g) x - x = f g) : ↥(groupCohomology.oneCoboundaries A)

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

Equations

• groupCohomology.oneCoboundariesOfEq hf = groupCohomology.oneCoboundariesOfMemRange ⋯

theorem groupCohomology.oneCoboundariesOfEq_apply {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f : G → CoeSort.coe A} {x : CoeSort.coe A} (hf : ∀ (g : G), (A.ρ g) x - x = f g) : ↑↑(groupCohomology.oneCoboundariesOfEq hf) = f

theorem groupCohomology.mem_range_of_mem_oneCoboundaries {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f : ↥(groupCohomology.oneCocycles A)} (h : f ∈ groupCohomology.oneCoboundaries A) : ↑f ∈ LinearMap.range (groupCohomology.dZero A)

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

theorem groupCohomology.mem_oneCoboundaries_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : ↥(groupCohomology.oneCocycles A)) : f ∈ groupCohomology.oneCoboundaries A ↔ ∃ (x : CoeSort.coe A), ∀ (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 × G → CoeSort.coe A} (h : f ∈ LinearMap.range (groupCohomology.dOne A)) : ↥(groupCohomology.twoCoboundaries A)

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

Equations

• groupCohomology.twoCoboundariesOfMemRange h = ⟨⟨f, ⋯⟩, ⋯⟩

theorem groupCohomology.twoCoboundariesOfMemRange_apply {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f : G × G → CoeSort.coe A} (h : f ∈ LinearMap.range (groupCohomology.dOne A)) : ↑↑(groupCohomology.twoCoboundariesOfMemRange h) = f

def groupCohomology.twoCoboundariesOfEq {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f : G × G → CoeSort.coe A} {x : G → CoeSort.coe A} (hf : ∀ (g h : G), (A.ρ g) (x h) - x (g * h) + x g = f (g, h)) : ↥(groupCohomology.twoCoboundaries A)

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

• groupCohomology.twoCoboundariesOfEq hf = groupCohomology.twoCoboundariesOfMemRange ⋯

theorem groupCohomology.twoCoboundariesOfEq_apply {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f : G × G → CoeSort.coe A} {x : G → CoeSort.coe A} (hf : ∀ (g h : G), (A.ρ g) (x h) - x (g * h) + x g = f (g, h)) : ↑↑(groupCohomology.twoCoboundariesOfEq hf) = f

theorem groupCohomology.mem_range_of_mem_twoCoboundaries {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {f : ↥(groupCohomology.twoCocycles A)} (h : f ∈ groupCohomology.twoCoboundaries A) : (groupCohomology.twoCocycles A).subtype f ∈ LinearMap.range (groupCohomology.dOne A)

theorem groupCohomology.mem_twoCoboundaries_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : ↥(groupCohomology.twoCocycles A)) : f ∈ groupCohomology.twoCoboundaries A ↔ ∃ (x : G → CoeSort.coe A), ∀ (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 : 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.IsOneCocycle f = ∀ (g h : G), f (g * h) = g • f h + f g

def groupCohomology.IsTwoCocycle {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.IsTwoCocycle 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_isOneCocycle {G : Type u_1} {A : Type u_2} [Monoid G] [AddCommGroup A] [MulAction G A] {f : G → A} (hf : groupCohomology.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 × G → A} (hf : groupCohomology.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 × G → A} (hf : groupCohomology.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 : G → A} (hf : groupCohomology.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 × G → A} (hf : groupCohomology.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 : 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.IsOneCoboundary f = ∃ (x : A), ∀ (g : G), g • x - x = f g

def groupCohomology.IsTwoCoboundary {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.IsTwoCoboundary f = ∃ (x : G → A), ∀ (g h : G), g • x h - x (g * h) + x g = f (g, h)

def groupCohomology.oneCocyclesOfIsOneCocycle {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 : groupCohomology.IsOneCocycle f) : ↥(groupCohomology.oneCocycles (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.oneCocyclesOfIsOneCocycle hf = ⟨f, ⋯⟩

theorem groupCohomology.isOneCocycle_of_oneCocycles {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (f : ↥(groupCohomology.oneCocycles (Rep.ofDistribMulAction k G A))) : groupCohomology.IsOneCocycle ⇑f

def groupCohomology.oneCoboundariesOfIsOneCoboundary {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 : groupCohomology.IsOneCoboundary f) : ↥(groupCohomology.oneCoboundaries (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.oneCoboundariesOfIsOneCoboundary hf = groupCohomology.oneCoboundariesOfMemRange ⋯

theorem groupCohomology.isOneCoboundary_of_oneCoboundaries {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (f : ↥(groupCohomology.oneCoboundaries (Rep.ofDistribMulAction k G A))) : groupCohomology.IsOneCoboundary ↑↑f

def groupCohomology.twoCocyclesOfIsTwoCocycle {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 : groupCohomology.IsTwoCocycle f) : ↥(groupCohomology.twoCocycles (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.twoCocyclesOfIsTwoCocycle hf = ⟨f, ⋯⟩

theorem groupCohomology.isTwoCocycle_of_twoCocycles {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (f : ↥(groupCohomology.twoCocycles (Rep.ofDistribMulAction k G A))) : groupCohomology.IsTwoCocycle ⇑f

def groupCohomology.twoCoboundariesOfIsTwoCoboundary {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 : groupCohomology.IsTwoCoboundary f) : ↥(groupCohomology.twoCoboundaries (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.twoCoboundariesOfIsTwoCoboundary hf = groupCohomology.twoCoboundariesOfMemRange ⋯

theorem groupCohomology.isTwoCoboundary_of_twoCoboundaries {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (f : ↥(groupCohomology.twoCoboundaries (Rep.ofDistribMulAction k G A))) : groupCohomology.IsTwoCoboundary ↑↑f

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 : 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.IsMulOneCocycle f = ∀ (g h : G), f (g * h) = g • f h * f g

def groupCohomology.IsMulTwoCocycle {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.IsMulTwoCocycle 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_isMulOneCocycle {G : Type u_1} {M : Type u_2} [Monoid G] [CommGroup M] [MulAction G M] {f : G → M} (hf : groupCohomology.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 × G → M} (hf : groupCohomology.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 × G → M} (hf : groupCohomology.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 : G → M} (hf : groupCohomology.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 × G → M} (hf : groupCohomology.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 : 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.IsMulOneCoboundary f = ∃ (x : M), ∀ (g : G), g • x / x = f g

def groupCohomology.IsMulTwoCoboundary {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.IsMulTwoCoboundary f = ∃ (x : G → M), ∀ (g h : G), g • x h / x (g * h) * x g = f (g, h)

def groupCohomology.oneCocyclesOfIsMulOneCocycle {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] {f : G → M} (hf : groupCohomology.IsMulOneCocycle f) : ↥(groupCohomology.oneCocycles (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.oneCocyclesOfIsMulOneCocycle hf = ⟨⇑Additive.ofMul ∘ f, ⋯⟩

theorem groupCohomology.isMulOneCocycle_of_oneCocycles {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] (f : ↥(groupCohomology.oneCocycles (Rep.ofMulDistribMulAction G M))) : groupCohomology.IsMulOneCocycle (⇑Additive.toMul ∘ ⇑f)

def groupCohomology.oneCoboundariesOfIsMulOneCoboundary {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] {f : G → M} (hf : groupCohomology.IsMulOneCoboundary f) : ↥(groupCohomology.oneCoboundaries (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.oneCoboundariesOfIsMulOneCoboundary hf = groupCohomology.oneCoboundariesOfMemRange ⋯

theorem groupCohomology.isMulOneCoboundary_of_oneCoboundaries {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] (f : ↥(groupCohomology.oneCoboundaries (Rep.ofMulDistribMulAction G M))) : groupCohomology.IsMulOneCoboundary (⇑Additive.ofMul ∘ ↑↑f)

def groupCohomology.twoCocyclesOfIsMulTwoCocycle {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] {f : G × G → M} (hf : groupCohomology.IsMulTwoCocycle f) : ↥(groupCohomology.twoCocycles (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.twoCocyclesOfIsMulTwoCocycle hf = ⟨⇑Additive.ofMul ∘ f, ⋯⟩

theorem groupCohomology.isMulTwoCocycle_of_twoCocycles {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] (f : ↥(groupCohomology.twoCocycles (Rep.ofMulDistribMulAction G M))) : groupCohomology.IsMulTwoCocycle (⇑Additive.toMul ∘ ⇑f)

def groupCohomology.twoCoboundariesOfIsMulTwoCoboundary {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] {f : G × G → M} (hf : groupCohomology.IsMulTwoCoboundary f) : ↥(groupCohomology.twoCoboundaries (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.twoCoboundariesOfIsMulTwoCoboundary hf = groupCohomology.twoCoboundariesOfMemRange ⋯

theorem groupCohomology.isMulTwoCoboundary_of_twoCoboundaries {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M] (f : ↥(groupCohomology.twoCoboundaries (Rep.ofMulDistribMulAction G M))) : groupCohomology.IsMulTwoCoboundary (⇑Additive.toMul ∘ ↑↑f)

@[reducible, inline]

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

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

• groupCohomology.H0 A = A.ρ.invariants

@[reducible, inline]

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

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

• groupCohomology.H1 A = (↥(groupCohomology.oneCocycles A) ⧸ groupCohomology.oneCoboundaries A)

def groupCohomology.H1_π {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : ↥(groupCohomology.oneCocycles A) →ₗ[k] groupCohomology.H1 A

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

Equations

• groupCohomology.H1_π A = (groupCohomology.oneCoboundaries A).mkQ

@[reducible, inline]

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

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

• groupCohomology.H2 A = (↥(groupCohomology.twoCocycles A) ⧸ groupCohomology.twoCoboundaries A)

def groupCohomology.H2_π {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : ↥(groupCohomology.twoCocycles A) →ₗ[k] groupCohomology.H2 A

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

Equations

• groupCohomology.H2_π A = (groupCohomology.twoCoboundaries A).mkQ

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

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

Equations

• groupCohomology.H0LequivOfIsTrivial A = LinearEquiv.ofTop (groupCohomology.H0 A) ⋯

@[simp]

theorem groupCohomology.H0LequivOfIsTrivial_eq_subtype {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] : ↑(groupCohomology.H0LequivOfIsTrivial A) = A.ρ.invariants.subtype

theorem groupCohomology.H0LequivOfIsTrivial_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] (x : ↥(groupCohomology.H0 A)) : (groupCohomology.H0LequivOfIsTrivial A) x = ↑x

@[simp]

theorem groupCohomology.H0LequivOfIsTrivial_symm_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] (x : CoeSort.coe A) : ↑((groupCohomology.H0LequivOfIsTrivial A).symm x) = x

def groupCohomology.H1LequivOfIsTrivial {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] : groupCohomology.H1 A ≃ₗ[k] Additive G →+ CoeSort.coe A

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

Equations

• groupCohomology.H1LequivOfIsTrivial A = ((groupCohomology.oneCoboundaries A).quotEquivOfEqBot ⋯).trans (groupCohomology.oneCocyclesLequivOfIsTrivial A)

theorem groupCohomology.H1LequivOfIsTrivial_comp_H1_π {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] : ↑(groupCohomology.H1LequivOfIsTrivial A) ∘ₗ groupCohomology.H1_π A = ↑(groupCohomology.oneCocyclesLequivOfIsTrivial A)

@[simp]

theorem groupCohomology.H1LequivOfIsTrivial_H1_π_apply_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] (f : ↥(groupCohomology.oneCocycles A)) (x : Additive G) : ((groupCohomology.H1LequivOfIsTrivial A) ((groupCohomology.H1_π A) f)) x = f (Additive.toMul x)

@[simp]

theorem groupCohomology.H1LequivOfIsTrivial_symm_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] (f : Additive G →+ CoeSort.coe A) : (groupCohomology.H1LequivOfIsTrivial A).symm f = (groupCohomology.H1_π A) ((groupCohomology.oneCocyclesLequivOfIsTrivial A).symm f)

theorem groupCohomology.dZero_comp_H0_subtype {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : groupCohomology.dZero A ∘ₗ (groupCohomology.H0 A).subtype = 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

• groupCohomology.shortComplexH0 A = CategoryTheory.ShortComplex.moduleCatMk (groupCohomology.H0 A).subtype (groupCohomology.dZero A) ⋯

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

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

def groupCohomology.dZeroArrowIso {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.Arrow.mk ((groupCohomology.inhomogeneousCochains A).d 0 1) ≅ CategoryTheory.Arrow.mk (ModuleCat.ofHom (groupCohomology.dZero A))

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

• groupCohomology.dZeroArrowIso A = CategoryTheory.Arrow.isoMk (groupCohomology.zeroCochainsLequiv A).toModuleIso (groupCohomology.oneCochainsLequiv A).toModuleIso ⋯

@[simp]

theorem groupCohomology.dZeroArrowIso_inv_right {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (groupCohomology.dZeroArrowIso A).inv.right = (groupCohomology.oneCochainsLequiv A).toModuleIso.inv

@[simp]

theorem groupCohomology.dZeroArrowIso_inv_left {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (groupCohomology.dZeroArrowIso A).inv.left = (groupCohomology.zeroCochainsLequiv A).toModuleIso.inv

@[simp]

theorem groupCohomology.dZeroArrowIso_hom_right {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (groupCohomology.dZeroArrowIso A).hom.right = (groupCohomology.oneCochainsLequiv A).toModuleIso.hom

@[simp]

theorem groupCohomology.dZeroArrowIso_hom_left {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (groupCohomology.dZeroArrowIso A).hom.left = (groupCohomology.zeroCochainsLequiv A).toModuleIso.hom

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

theorem groupCohomology.isoZeroCocycles_hom_comp_subtype {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (groupCohomology.isoZeroCocycles A).hom (ModuleCat.ofHom A.ρ.invariants.subtype) = CategoryTheory.CategoryStruct.comp (groupCohomology.iCocycles A 0) (groupCohomology.zeroCochainsLequiv A).toModuleIso.hom

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

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.isoH0 A = (groupCohomology.inhomogeneousCochains A).isoHomologyπ₀.symm ≪≫ groupCohomology.isoZeroCocycles A

theorem groupCohomology.groupCohomologyπ_comp_isoH0_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (groupCohomologyπ A 0) (groupCohomology.isoH0 A).hom = (groupCohomology.isoZeroCocycles A).hom

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

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

Equations

• groupCohomology.shortComplexH1 A = CategoryTheory.ShortComplex.moduleCatMk (groupCohomology.dZero A) (groupCohomology.dOne A) ⋯

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

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) : (groupCohomology.shortComplexH1Iso A).hom = { τ₁ := (groupCohomology.zeroCochainsLequiv A).toModuleIso.hom, τ₂ := (groupCohomology.oneCochainsLequiv A).toModuleIso.hom, τ₃ := (groupCohomology.twoCochainsLequiv A).toModuleIso.hom, comm₁₂ := ⋯, comm₂₃ := ⋯ }

@[simp]

theorem groupCohomology.shortComplexH1Iso_inv {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (groupCohomology.shortComplexH1Iso A).inv = CategoryTheory.ShortComplex.homMk (groupCohomology.zeroCochainsLequiv A).toModuleIso.inv (groupCohomology.oneCochainsLequiv A).toModuleIso.inv (groupCohomology.twoCochainsLequiv A).toModuleIso.inv ⋯ ⋯

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

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.

theorem groupCohomology.isoOneCocycles_hom_comp_subtype {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (groupCohomology.isoOneCocycles A).hom (ModuleCat.ofHom (groupCohomology.oneCocycles A).subtype) = CategoryTheory.CategoryStruct.comp (groupCohomology.iCocycles A 1) (groupCohomology.oneCochainsLequiv A).toModuleIso.hom

theorem groupCohomology.toCocycles_comp_isoOneCocycles_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (groupCohomology.toCocycles A 0 1) (groupCohomology.isoOneCocycles A).hom = CategoryTheory.CategoryStruct.comp (groupCohomology.zeroCochainsLequiv A).toModuleIso.hom (ModuleCat.ofHom (groupCohomology.shortComplexH1 A).moduleCatToCycles)

def groupCohomology.isoH1 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : groupCohomology A 1 ≅ ModuleCat.of k (groupCohomology.H1 A)

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.

theorem groupCohomology.groupCohomologyπ_comp_isoH1_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (groupCohomologyπ A 1) (groupCohomology.isoH1 A).hom = CategoryTheory.CategoryStruct.comp (groupCohomology.isoOneCocycles A).hom (groupCohomology.shortComplexH1 A).moduleCatHomologyπ

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) --dOne--> Fun(G × G, A) --dTwo--> Fun(G × G × G, A).

Equations

• groupCohomology.shortComplexH2 A = CategoryTheory.ShortComplex.moduleCatMk (groupCohomology.dOne A) (groupCohomology.dTwo A) ⋯

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

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) : (groupCohomology.shortComplexH2Iso A).hom = { τ₁ := (groupCohomology.oneCochainsLequiv A).toModuleIso.hom, τ₂ := (groupCohomology.twoCochainsLequiv A).toModuleIso.hom, τ₃ := (groupCohomology.threeCochainsLequiv A).toModuleIso.hom, comm₁₂ := ⋯, comm₂₃ := ⋯ }

@[simp]

theorem groupCohomology.shortComplexH2Iso_inv {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (groupCohomology.shortComplexH2Iso A).inv = CategoryTheory.ShortComplex.homMk (groupCohomology.oneCochainsLequiv A).toModuleIso.inv (groupCohomology.twoCochainsLequiv A).toModuleIso.inv (groupCohomology.threeCochainsLequiv A).toModuleIso.inv ⋯ ⋯

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

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.

theorem groupCohomology.isoTwoCocycles_hom_comp_subtype {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (groupCohomology.isoTwoCocycles A).hom (ModuleCat.ofHom (groupCohomology.twoCocycles A).subtype) = CategoryTheory.CategoryStruct.comp (groupCohomology.iCocycles A 2) (groupCohomology.twoCochainsLequiv A).toModuleIso.hom

theorem groupCohomology.toCocycles_comp_isoTwoCocycles_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (groupCohomology.toCocycles A 1 2) (groupCohomology.isoTwoCocycles A).hom = CategoryTheory.CategoryStruct.comp (groupCohomology.oneCochainsLequiv A).toModuleIso.hom (ModuleCat.ofHom (groupCohomology.shortComplexH2 A).moduleCatToCycles)

def groupCohomology.isoH2 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : groupCohomology A 2 ≅ ModuleCat.of k (groupCohomology.H2 A)

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.

theorem groupCohomology.groupCohomologyπ_comp_isoH2_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (groupCohomologyπ A 2) (groupCohomology.isoH2 A).hom = CategoryTheory.CategoryStruct.comp (groupCohomology.isoTwoCocycles A).hom (groupCohomology.shortComplexH2 A).moduleCatHomologyπ