Documentation

Mathlib.RepresentationTheory.GroupCohomology.LowDegree

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

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

In RepresentationTheory.GroupCohomology.Basic, we define the nth group cohomology of A to be the cohomology of a complex inhomogeneousCochains A, whose objects are (Fin n → G) → A; this is unnecessarily unwieldy in low degree. Moreover, cohomology of a complex is defined as an abstract cokernel, whereas the definitions here are explicit quotients of cocycles by coboundaries.

We also show that when the representation on A is trivial, H¹(G, A) ≃ Hom(G, A).

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

Main definitions #

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 = ((Rep.ρ 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
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem groupCohomology.dZero_eq_zero {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) [Rep.IsTrivial A] :
            @[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 = ((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) :
            (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
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem groupCohomology.dTwo_apply {k : Type u} {G : Type u} [CommRing k] [Group G] (A : Rep k G) (f : G × GCoeSort.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 × 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), ((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 : GCoeSort.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
                    @[simp]

                    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), ((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 × GCoeSort.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)

                      The 1-coboundaries B¹(G, A) of A : Rep k G, defined as the image of the map A → Fun(G, A) sending (a, g) ↦ ρ_A(g)(a) - a.

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

                        The 2-coboundaries B²(G, A) of A : Rep k G, defined as the image of the map Fun(G, A) → Fun(G × G, A) sending (f, (g₁, g₂)) ↦ ρ_A(g₁)(f(g₂)) - f(g₁g₂) + f(g₁).

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[inline, reducible]
                          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
                            @[inline, reducible]
                            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
                                @[inline, reducible]
                                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

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

                                    Equations
                                    Instances For

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

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        @[simp]