Documentation

Mathlib.RepresentationTheory.GroupCohomology.Resolution

The structure of the k[G]-module k[Gⁿ] #

This file contains facts about an important k[G]-module structure on k[Gⁿ], where k is a commutative ring and G is a group. The module structure arises from the representation G →* End(k[Gⁿ]) induced by the diagonal action of G on Gⁿ.

In particular, we define an isomorphism of k-linear G-representations between k[Gⁿ⁺¹] and k[G] ⊗ₖ k[Gⁿ] (on which G acts by ρ(g₁)(g₂ ⊗ x) = (g₁ * g₂) ⊗ x).

This allows us to define a k[G]-basis on k[Gⁿ⁺¹], by mapping the natural k[G]-basis of k[G] ⊗ₖ k[Gⁿ] along the isomorphism.

We then define the standard resolution of k as a trivial representation, by taking the alternating face map complex associated to an appropriate simplicial k-linear G-representation. This simplicial object is the linearization of the simplicial G-set given by the universal cover of the classifying space of G, EG. We prove this simplicial G-set EG is isomorphic to the Čech nerve of the natural arrow of G-sets G ⟶ {pt}.

We then use this isomorphism to deduce that as a complex of k-modules, the standard resolution of k as a trivial G-representation is homotopy equivalent to the complex with k at 0 and 0 elsewhere.

Putting this material together allows us to define groupCohomology.projectiveResolution, the standard projective resolution of k as a trivial k-linear G-representation.

Main definitions #

Implementation notes #

We express k[G]-module structures on a module k-module V using the Representation definition. We avoid using instances Module (G →₀ k) V so that we do not run into possible scalar action diamonds.

We also use the category theory library to bundle the type k[Gⁿ] - or more generally k[H] when H has G-action - and the representation together, as a term of type Rep k G, and call it Rep.ofMulAction k G H. This enables us to express the fact that certain maps are G-equivariant by constructing morphisms in the category Rep k G, i.e., representations of G over k.

An isomorphism of G-sets Gⁿ⁺¹ ≅ G × Gⁿ, where G acts by left multiplication on Gⁿ⁺¹ and G but trivially on Gⁿ. The map sends (g₀, ..., gₙ) ↦ (g₀, (g₀⁻¹g₁, g₁⁻¹g₂, ..., gₙ₋₁⁻¹gₙ)), and the inverse is (g₀, (g₁, ..., gₙ)) ↦ (g₀, g₀g₁, g₀g₁g₂, ..., g₀g₁...gₙ).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem groupCohomology.resolution.actionDiagonalSucc_hom_apply {G : Type u} [Group G] {n : } (f : Fin (n + 1)G) :
    (groupCohomology.resolution.actionDiagonalSucc G n).hom.hom f = (f 0, fun (i : Fin n) => (f i.castSucc)⁻¹ * f i.succ)

    An isomorphism of k-linear representations of G from k[Gⁿ⁺¹] to k[G] ⊗ₖ k[Gⁿ] (on which G acts by ρ(g₁)(g₂ ⊗ x) = (g₁ * g₂) ⊗ x) sending (g₀, ..., gₙ) to g₀ ⊗ (g₀⁻¹g₁, g₁⁻¹g₂, ..., gₙ₋₁⁻¹gₙ). The inverse sends g₀ ⊗ (g₁, ..., gₙ) to (g₀, g₀g₁, ..., g₀g₁...gₙ).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem groupCohomology.resolution.diagonalSucc_hom_single {k : Type u} {G : Type u} [CommRing k] {n : } [Group G] (f : Fin (n + 1)G) (a : k) :
      (groupCohomology.resolution.diagonalSucc k G n).hom.hom (Finsupp.single f a) = Finsupp.single (f 0) 1 ⊗ₜ[k] Finsupp.single (fun (i : Fin n) => (f i.castSucc)⁻¹ * f i.succ) a
      theorem groupCohomology.resolution.diagonalSucc_inv_single_left {k : Type u} {G : Type u} [CommRing k] {n : } [Group G] (g : G) (f : (Fin nG) →₀ k) (r : k) :
      (groupCohomology.resolution.diagonalSucc k G n).inv.hom (Finsupp.single g r ⊗ₜ[k] f) = ((Finsupp.lift ((Fin (n + 1)G) →₀ k) k (Fin nG)) fun (f : Fin nG) => Finsupp.single (g Fin.partialProd f) r) f
      theorem groupCohomology.resolution.diagonalSucc_inv_single_right {k : Type u} {G : Type u} [CommRing k] {n : } [Group G] (g : G →₀ k) (f : Fin nG) (r : k) :
      (groupCohomology.resolution.diagonalSucc k G n).inv.hom (g ⊗ₜ[k] Finsupp.single f r) = ((Finsupp.lift ((Fin (n + 1)G) →₀ k) k G) fun (a : G) => Finsupp.single (a Fin.partialProd f) r) g

      The k[G]-linear isomorphism k[G] ⊗ₖ k[Gⁿ] ≃ k[Gⁿ⁺¹], where the k[G]-module structure on the lefthand side is TensorProduct.leftModule, whilst that of the righthand side comes from Representation.asModule. Allows us to use Algebra.TensorProduct.basis to get a k[G]-basis of the righthand side.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def groupCohomology.resolution.ofMulActionBasis (k : Type u) (G : Type u) [CommRing k] (n : ) [Group G] :
        Basis (Fin nG) (MonoidAlgebra k G) (Representation.ofMulAction k G (Fin (n + 1)G)).asModule

        A k[G]-basis of k[Gⁿ⁺¹], coming from the k[G]-linear isomorphism k[G] ⊗ₖ k[Gⁿ] ≃ k[Gⁿ⁺¹].

        Equations
        Instances For
          noncomputable def Rep.diagonalHomEquiv {k : Type u} {G : Type u} [CommRing k] (n : ) [Group G] (A : Rep k G) :
          (Rep.ofMulAction k G (Fin (n + 1)G) A) ≃ₗ[k] (Fin nG)CoeSort.coe A

          Given a k-linear G-representation A, the set of representation morphisms Hom(k[Gⁿ⁺¹], A) is k-linearly isomorphic to the set of functions Gⁿ → A.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem Rep.diagonalHomEquiv_apply {k : Type u} {G : Type u} [CommRing k] {n : } [Group G] {A : Rep k G} (f : Rep.ofMulAction k G (Fin (n + 1)G) A) (x : Fin nG) :

            Given a k-linear G-representation A, diagonalHomEquiv is a k-linear isomorphism of the set of representation morphisms Hom(k[Gⁿ⁺¹], A) with Fun(Gⁿ, A). This lemma says that this sends a morphism of representations f : k[Gⁿ⁺¹] ⟶ A to the function (g₁, ..., gₙ) ↦ f(1, g₁, g₁g₂, ..., g₁g₂...gₙ).

            theorem Rep.diagonalHomEquiv_symm_apply {k : Type u} {G : Type u} [CommRing k] {n : } [Group G] {A : Rep k G} (f : (Fin nG)CoeSort.coe A) (x : Fin (n + 1)G) :
            ((Rep.diagonalHomEquiv n A).symm f).hom (Finsupp.single x 1) = (A (x 0)) (f fun (i : Fin n) => (x i.castSucc)⁻¹ * x i.succ)

            Given a k-linear G-representation A, diagonalHomEquiv is a k-linear isomorphism of the set of representation morphisms Hom(k[Gⁿ⁺¹], A) with Fun(Gⁿ, A). This lemma says that the inverse map sends a function f : Gⁿ → A to the representation morphism sending (g₀, ... gₙ) ↦ ρ(g₀)(f(g₀⁻¹g₁, g₁⁻¹g₂, ..., gₙ₋₁⁻¹gₙ)), where ρ is the representation attached to A.

            theorem Rep.diagonalHomEquiv_symm_partialProd_succ {k : Type u} {G : Type u} [CommRing k] {n : } [Group G] {A : Rep k G} (f : (Fin nG)CoeSort.coe A) (g : Fin (n + 1)G) (a : Fin (n + 1)) :
            ((Rep.diagonalHomEquiv n A).symm f).hom (Finsupp.single (Fin.partialProd g a.succ.succAbove) 1) = f (a.contractNth (fun (x x_1 : G) => x * x_1) g)

            Auxiliary lemma for defining group cohomology, used to show that the isomorphism diagonalHomEquiv commutes with the differentials in two complexes which compute group cohomology.

            The simplicial G-set sending [n] to Gⁿ⁺¹ equipped with the diagonal action of G.

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

              When the category is G-Set, cechNerveTerminalFrom of G with the left regular action is isomorphic to EG, the universal cover of the classifying space of G as a simplicial G-set.

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

                As a simplicial set, cechNerveTerminalFrom of a monoid G is isomorphic to the universal cover of the classifying space of G as a simplicial set.

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

                  The universal cover of the classifying space of G as a simplicial set, augmented by the map from Fin 1 → G to the terminal object in Type u.

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

                    The augmented Čech nerve of the map from Fin 1 → G to the terminal object in Type u has an extra degeneracy.

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

                      The universal cover of the classifying space of G as a simplicial set, augmented by the map from Fin 1 → G to the terminal object in Type u, has an extra degeneracy.

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

                        The free functor Type u ⥤ ModuleCat.{u} k applied to the universal cover of the classifying space of G as a simplicial set, augmented by the map from Fin 1 → G to the terminal object in Type u.

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

                          If we augment the universal cover of the classifying space of G as a simplicial set by the map from Fin 1 → G to the terminal object in Type u, then apply the free functor Type u ⥤ ModuleCat.{u} k, the resulting augmented simplicial k-module has an extra degeneracy.

                          Equations
                          Instances For

                            The standard resolution of k as a trivial representation, defined as the alternating face map complex of a simplicial k-linear G-representation.

                            Equations
                            Instances For
                              def groupCohomology.resolution.d (k : Type u) [CommRing k] (G : Type u) (n : ) :
                              ((Fin (n + 1)G) →₀ k) →ₗ[k] (Fin nG) →₀ k

                              The k-linear map underlying the differential in the standard resolution of k as a trivial k-linear G-representation. It sends (g₀, ..., gₙ) ↦ ∑ (-1)ⁱ • (g₀, ..., ĝᵢ, ..., gₙ).

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[simp]
                                theorem groupCohomology.resolution.d_of {k : Type u} [CommRing k] {G : Type u} {n : } (c : Fin (n + 1)G) :
                                (groupCohomology.resolution.d k G n) (Finsupp.single c 1) = Finset.univ.sum fun (p : Fin (n + 1)) => Finsupp.single (c p.succAbove) ((-1) ^ p)
                                def groupCohomology.resolution.xIso (k : Type u) (G : Type u) [CommRing k] [Monoid G] (n : ) :
                                (groupCohomology.resolution k G).X n Rep.ofMulAction k G (Fin (n + 1)G)

                                The nth object of the standard resolution of k is definitionally isomorphic to k[Gⁿ⁺¹] equipped with the representation induced by the diagonal action of G.

                                Equations
                                Instances For
                                  theorem groupCohomology.resolution.d_eq (k : Type u) (G : Type u) [CommRing k] [Monoid G] (n : ) :

                                  Simpler expression for the differential in the standard resolution of k as a G-representation. It sends (g₀, ..., gₙ₊₁) ↦ ∑ (-1)ⁱ • (g₀, ..., ĝᵢ, ..., gₙ₊₁).

                                  The standard resolution of k as a trivial representation as a complex of k-modules.

                                  Equations
                                  Instances For

                                    If we apply the free functor Type u ⥤ ModuleCat.{u} k to the universal cover of the classifying space of G as a simplicial set, then take the alternating face map complex, the result is isomorphic to the standard resolution of the trivial G-representation k as a complex of k-modules.

                                    Equations
                                    Instances For

                                      As a complex of k-modules, the standard resolution of the trivial G-representation k is homotopy equivalent to the complex which is k at 0 and 0 elsewhere.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        def groupCohomology.resolution.ε (k : Type u) (G : Type u) [CommRing k] [Monoid G] :
                                        Rep.ofMulAction k G (Fin 1G) Rep.trivial k G k

                                        The hom of k-linear G-representations k[G¹] → k sending ∑ nᵢgᵢ ↦ ∑ nᵢ.

                                        Equations
                                        Instances For

                                          The homotopy equivalence of complexes of k-modules between the standard resolution of k as a trivial G-representation, and the complex which is k at 0 and 0 everywhere else, acts as ∑ nᵢgᵢ ↦ ∑ nᵢ : k[G¹] → k at 0.

                                          The chain map from the standard resolution of k to k[0] given by ∑ nᵢgᵢ ↦ ∑ nᵢ in degree zero.

                                          Equations
                                          Instances For

                                            The standard projective resolution of k as a trivial k-linear G-representation.

                                            Equations
                                            Instances For
                                              Equations
                                              • =
                                              def groupCohomology.extIso (k : Type u) (G : Type u) [CommRing k] [Group G] (V : Rep k G) (n : ) :
                                              ((Ext k (Rep k G) n).obj { unop := Rep.trivial k G k }).obj V HomologicalComplex.homology ((groupCohomology.resolution k G).linearYonedaObj k V) n

                                              Given a k-linear G-representation V, Extⁿ(k, V) (where k is a trivial k-linear G-representation) is isomorphic to the nth cohomology group of Hom(P, V), where P is the standard resolution of k called groupCohomology.resolution k G.

                                              Equations
                                              Instances For