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 #

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

    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

      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

        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} [CommRing k] [Group G] (A : Rep k G) (m : CoeSort.coe A) (g : G) :
          (groupCohomology.dZero A) m g = (A g) m - m
          def groupCohomology.dZero {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep 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
          Instances For
            theorem groupCohomology.dZero_ker_eq_invariants {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) :
            @[simp]
            theorem groupCohomology.dZero_eq_zero {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] :
            @[simp]
            theorem groupCohomology.dOne_apply {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) (f : GCoeSort.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.dOne {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) :
            (GCoeSort.coe A) →ₗ[k] G × GCoeSort.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
            Instances For
              @[simp]
              theorem groupCohomology.dTwo_apply {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) (f : G × GCoeSort.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)
              def groupCohomology.dTwo {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) :
              (G × GCoeSort.coe A) →ₗ[k] G × G × GCoeSort.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.
              Instances For

                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.

                def groupCohomology.oneCocycles {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep 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} [CommRing k] [Group G] (A : Rep k G) :
                  Submodule k (G × GCoeSort.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
                  Instances For
                    theorem groupCohomology.mem_oneCocycles_def {k : Type u} {G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : GCoeSort.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 : Type u} {G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : GCoeSort.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 : 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) :
                    (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} [A.IsTrivial] (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} [A.IsTrivial] (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 : A.IsTrivial] (f : Additive G →+ CoeSort.coe A) (a : Additive G) :
                    @[simp]
                    theorem groupCohomology.oneCocyclesLequivOfIsTrivial_apply_apply {k : Type u} {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

                    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} [CommRing k] [Group G] {A : Rep k G} (f : G × GCoeSort.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 : Type u} {G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : G × GCoeSort.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 : 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) = (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) :
                      (A g) (f (g⁻¹, g)) - f (g, g⁻¹) = f (1, 1) - f (g, 1)

                      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
                      Instances For

                        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
                        Instances For

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

                          Equations
                          Instances For
                            def groupCohomology.oneCoboundariesOfEq {k : Type u} {G : Type u} [CommRing k] [Group G] {A : Rep k G} {f : GCoeSort.coe A} {x : CoeSort.coe A} (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
                            Instances For
                              theorem groupCohomology.oneCoboundariesOfEq_apply {k : Type u} {G : Type u} [CommRing k] [Group G] {A : Rep k G} {f : GCoeSort.coe A} {x : CoeSort.coe A} (hf : ∀ (g : G), (A g) x - x = f g) :

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

                              Equations
                              Instances For
                                def groupCohomology.twoCoboundariesOfEq {k : Type u} {G : Type u} [CommRing k] [Group G] {A : Rep k G} {f : G × GCoeSort.coe A} {x : GCoeSort.coe A} (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
                                Instances For
                                  theorem groupCohomology.twoCoboundariesOfEq_apply {k : Type u} {G : Type u} [CommRing k] [Group G] {A : Rep k G} {f : G × GCoeSort.coe A} {x : GCoeSort.coe A} (hf : ∀ (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
                                  Instances For
                                    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
                                    Instances For
                                      theorem groupCohomology.map_one_of_isOneCocycle {G : Type u_1} {A : Type u_2} [Monoid G] [AddCommGroup A] [MulAction G A] {f : GA} (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 × GA} (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 × GA} (hf : groupCohomology.IsTwoCocycle f) (g : G) :
                                      f (g, 1) = g f (1, 1)
                                      @[simp]
                                      theorem groupCohomology.map_inv_of_isOneCocycle {G : Type u_1} {A : Type u_2} [Group G] [AddCommGroup A] [MulAction G A] {f : GA} (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 × GA} (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 : 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
                                      Instances For
                                        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
                                        Instances For

                                          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
                                          Instances For

                                            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
                                            Instances For

                                              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
                                              Instances For

                                                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
                                                Instances For

                                                  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
                                                  Instances For
                                                    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
                                                    Instances For
                                                      theorem groupCohomology.map_one_of_isMulOneCocycle {G : Type u_1} {M : Type u_2} [Monoid G] [CommGroup M] [MulAction G M] {f : GM} (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 × GM} (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 × GM} (hf : groupCohomology.IsMulTwoCocycle f) (g : G) :
                                                      f (g, 1) = g f (1, 1)
                                                      @[simp]
                                                      theorem groupCohomology.map_inv_of_isMulOneCocycle {G : Type u_1} {M : Type u_2} [Group G] [CommGroup M] [MulAction G M] {f : GM} (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 × GM} (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 : 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
                                                      Instances For
                                                        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
                                                        Instances For

                                                          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
                                                          Instances For

                                                            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
                                                            Instances For

                                                              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
                                                              Instances For

                                                                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
                                                                Instances For
                                                                  @[reducible, inline]
                                                                  abbrev groupCohomology.H0 {k : Type u} {G : Type u} [CommRing k] [Group G] (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
                                                                    @[reducible, inline]
                                                                    abbrev groupCohomology.H1 {k : Type u} {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
                                                                    Instances For

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

                                                                      Equations
                                                                      Instances For
                                                                        @[reducible, inline]
                                                                        abbrev groupCohomology.H2 {k : Type u} {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
                                                                        Instances For

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

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

                                                                            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} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] :
                                                                              (groupCohomology.H0LequivOfIsTrivial A) = A.invariants.subtype
                                                                              theorem groupCohomology.H0LequivOfIsTrivial_apply {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] (x : (groupCohomology.H0 A)) :
                                                                              @[simp]
                                                                              theorem groupCohomology.H0LequivOfIsTrivial_symm_apply {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] (x : 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
                                                                              Instances For
                                                                                @[simp]
                                                                                theorem groupCohomology.H1LequivOfIsTrivial_H1_π_apply_apply {k : Type u} {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)
                                                                                theorem groupCohomology.dZero_comp_H0_subtype {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) :

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

                                                                                Equations
                                                                                Instances For

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

                                                                                      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
                                                                                      Instances For

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

                                                                                        Equations
                                                                                        Instances For
                                                                                          @[simp]
                                                                                          theorem groupCohomology.shortComplexH1Iso_hom {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) :
                                                                                          (groupCohomology.shortComplexH1Iso A).hom = { τ₁ := (groupCohomology.zeroCochainsLequiv A), τ₂ := (groupCohomology.oneCochainsLequiv A), τ₃ := (groupCohomology.twoCochainsLequiv A), comm₁₂ := , comm₂₃ := }

                                                                                          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.
                                                                                          Instances For

                                                                                            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.
                                                                                            Instances For

                                                                                              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.
                                                                                              Instances For

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

                                                                                                Equations
                                                                                                Instances For
                                                                                                  @[simp]
                                                                                                  theorem groupCohomology.shortComplexH2Iso_hom {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) :
                                                                                                  (groupCohomology.shortComplexH2Iso A).hom = { τ₁ := (groupCohomology.oneCochainsLequiv A), τ₂ := (groupCohomology.twoCochainsLequiv A), τ₃ := (groupCohomology.threeCochainsLequiv A), comm₁₂ := , comm₂₃ := }

                                                                                                  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.
                                                                                                  Instances For

                                                                                                    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.
                                                                                                    Instances For

                                                                                                      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.
                                                                                                      Instances For