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

• groupCohomology.threeCochainsLequiv A = LinearEquiv.funCongrLeft k (CoeSort.coe A) ((Equiv.piFinSucc 2 G).trans (Equiv.prodCongr (Equiv.refl G) (piFinTwoEquiv fun (x : Fin 2) => G))).symm

@[simp]

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

def groupCohomology.dZero {k : Type u} {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

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

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

@[simp]

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

@[simp]

theorem groupCohomology.dOne_apply {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) (f : G → CoeSort.coe A) (g : G × G) : (groupCohomology.dOne A) f g = ((Rep.ρ A) g.1) (f g.2) - f (g.1 * g.2) + f g.1

def groupCohomology.dOne {k : Type u} {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

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

@[simp]

theorem groupCohomology.dTwo_apply {k : Type u} {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 = ((Rep.ρ 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)

def groupCohomology.dTwo {k : Type u} {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.

theorem groupCohomology.dZero_comp_eq {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) : LinearMap.comp (groupCohomology.dZero A) ↑(groupCohomology.zeroCochainsLequiv A) = LinearMap.comp (↑(groupCohomology.oneCochainsLequiv A)) (HomologicalComplex.d (groupCohomology.inhomogeneousCochains A) 0 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.

theorem groupCohomology.dOne_comp_eq {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) : LinearMap.comp (groupCohomology.dOne A) ↑(groupCohomology.oneCochainsLequiv A) = LinearMap.comp (↑(groupCohomology.twoCochainsLequiv A)) (HomologicalComplex.d (groupCohomology.inhomogeneousCochains A) 1 2)

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} [CommRing k] [Group G] (A : Rep k G) : LinearMap.comp (groupCohomology.dTwo A) ↑(groupCohomology.twoCochainsLequiv A) = LinearMap.comp (↑(groupCohomology.threeCochainsLequiv A)) (HomologicalComplex.d (groupCohomology.inhomogeneousCochains A) 2 3)

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} [CommRing k] [Group G] (A : Rep k G) : LinearMap.comp (groupCohomology.dOne A) (groupCohomology.dZero A) = 0

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

def groupCohomology.oneCocycles {k : Type u} {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 : Type u} {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)

theorem groupCohomology.mem_oneCocycles_def {k : Type u} {G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : G → CoeSort.coe A) : f ∈ groupCohomology.oneCocycles A ↔ ∀ (g h : G), ((Rep.ρ A) g) (f h) - f (g * h) + f g = 0

theorem groupCohomology.mem_oneCocycles_iff {k : Type u} {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) = ((Rep.ρ A) g) (f h) + f g

@[simp]

theorem groupCohomology.oneCocycles_map_one {k : Type u} {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 : Type u} {G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : ↥(groupCohomology.oneCocycles A)) (g : G) : ((Rep.ρ A) g) (↑f g⁻¹) = -↑f g

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

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

@[simp]

theorem groupCohomology.oneCocyclesLequivOfIsTrivial_symm_apply_coe {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) [hA : Rep.IsTrivial A] (f : Additive G →+ CoeSort.coe A) (a : Additive G) : ↑((LinearEquiv.symm (groupCohomology.oneCocyclesLequivOfIsTrivial A)) f) a = f a

@[simp]

theorem groupCohomology.oneCocyclesLequivOfIsTrivial_apply_apply {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) [hA : Rep.IsTrivial A] (f : ↥(groupCohomology.oneCocycles A)) : ∀ (a : Additive G), ((groupCohomology.oneCocyclesLequivOfIsTrivial A) f) a = (↑f ∘ ⇑Additive.toMul) a

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

theorem groupCohomology.mem_twoCocycles_def {k : Type u} {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), ((Rep.ρ A) 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} [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) = ((Rep.ρ A) g) (f (h, j)) + f (g, h * j)

theorem groupCohomology.twoCocycles_map_one_fst {k : Type u} {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 : Type u} {G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : ↥(groupCohomology.twoCocycles A)) (g : G) : ↑f (g, 1) = ((Rep.ρ A) g) (↑f (1, 1))

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

def groupCohomology.oneCoboundaries {k : Type u} {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

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

def groupCohomology.twoCoboundaries {k : Type u} {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

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

theorem groupCohomology.mem_oneCoboundaries_of_dZero_apply {k : Type u} {G : Type u} [CommRing k] [Group G] {A : Rep k G} (x : CoeSort.coe A) : { val := (groupCohomology.dZero A) x, property := (_ : (LinearMap.comp (groupCohomology.dOne A) (groupCohomology.dZero A)) x = 0 x) } ∈ groupCohomology.oneCoboundaries A

theorem groupCohomology.mem_oneCoboundaries_of_mem_range {k : Type u} {G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : G → CoeSort.coe A) (h : f ∈ LinearMap.range (groupCohomology.dZero A)) : { val := f, property := (_ : f ∈ LinearMap.ker (groupCohomology.dOne A)) } ∈ groupCohomology.oneCoboundaries A

theorem groupCohomology.mem_range_of_mem_oneCoboundaries {k : Type u} {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 : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) [Rep.IsTrivial A] : groupCohomology.oneCoboundaries A = ⊥

theorem groupCohomology.mem_twoCoboundaries_of_dOne_apply {k : Type u} {G : Type u} [CommRing k] [Group G] {A : Rep k G} (x : G → CoeSort.coe A) : { val := (groupCohomology.dOne A) x, property := (_ : (LinearMap.comp (groupCohomology.dTwo A) (groupCohomology.dOne A)) x = 0 x) } ∈ groupCohomology.twoCoboundaries A

theorem groupCohomology.mem_twoCoboundaries_of_mem_range {k : Type u} {G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : G × G → CoeSort.coe A) (h : f ∈ LinearMap.range (groupCohomology.dOne A)) : { val := f, property := (_ : f ∈ LinearMap.ker (groupCohomology.dTwo A)) } ∈ groupCohomology.twoCoboundaries A

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

@[inline, reducible]

abbrev groupCohomology.H0 {k : Type u} {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 = Representation.invariants (Rep.ρ A)

@[inline, reducible]

abbrev groupCohomology.H1 {k : Type u} {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 : Type u} {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 = Submodule.mkQ (groupCohomology.oneCoboundaries A)

@[inline, reducible]

abbrev groupCohomology.H2 {k : Type u} {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 : Type u} {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 = Submodule.mkQ (groupCohomology.twoCoboundaries A)

def groupCohomology.H0LequivOfIsTrivial {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) [Rep.IsTrivial A] : ↥(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) (_ : Representation.invariants (Rep.ρ A) = ⊤)

@[simp]

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

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

@[simp]

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

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

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

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

@[simp]

theorem groupCohomology.H1LequivOfIsTrivial_H1_π_apply_apply {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) [Rep.IsTrivial A] (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 : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) [Rep.IsTrivial A] (f : Additive G →+ CoeSort.coe A) : (LinearEquiv.symm (groupCohomology.H1LequivOfIsTrivial A)) f = (groupCohomology.H1_π A) ((LinearEquiv.symm (groupCohomology.oneCocyclesLequivOfIsTrivial A)) f)