Documentation

Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

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

Let k be a commutative ring and G a group. This file contains specialised API for the cycles and group homology of a k-linear G-representation A in degrees 0, 1 and 2. In RepresentationTheory/Homological/GroupHomology/Basic.lean, we define the nth group homology of A to be the homology of a complex inhomogeneousChains A, whose objects are (Fin n →₀ G) → A; this is unnecessarily unwieldy in low degree.

TODO #

def groupHomology.chainsIso₀ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [DecidableEq G] :

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

Equations
Instances For

    The 1st object in the complex of inhomogeneous chains of A : Rep k G is isomorphic to G →₀ A as a k-module.

    Equations
    Instances For
      def groupHomology.chainsIso₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [DecidableEq G] :

      The 2nd object in the complex of inhomogeneous chains of A : Rep k G is isomorphic to G² →₀ A as a k-module.

      Equations
      Instances For
        def groupHomology.chainsIso₃ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [DecidableEq G] :

        The 3rd object in the complex of inhomogeneous chains of A : Rep k G is isomorphic to G³ → A as a k-module.

        Equations
        Instances For
          def groupHomology.d₁₀ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :
          ModuleCat.of k (G →₀ A.V) A.V

          The 0th differential in the complex of inhomogeneous chains of A : Rep k G, as a k-linear map (G →₀ A) → A. It sends single g a ↦ ρ_A(g⁻¹)(a) - a.

          Equations
          Instances For
            @[simp]
            theorem groupHomology.d₁₀_single {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (g : G) (a : A.V) :

            The 0th differential in the complex of inhomogeneous chains of a G-representation A as a linear map into the k-submodule of A spanned by elements of the form ρ(g)(x) - x, g ∈ G, x ∈ A.

            Equations
            Instances For
              @[simp]
              def groupHomology.d₂₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :
              ModuleCat.of k (G × G →₀ A.V) ModuleCat.of k (G →₀ A.V)

              The 1st differential in the complex of inhomogeneous chains of A : Rep k G, as a k-linear map (G² →₀ A) → (G →₀ A). It sends a·(g₁, g₂) ↦ ρ_A(g₁⁻¹)(a)·g₂ - a·g₁g₂ + a·g₁.

              Equations
              Instances For
                @[simp]
                theorem groupHomology.d₂₁_single {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g : G × G) (a : A.V) :
                def groupHomology.d₃₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :
                ModuleCat.of k (G × G × G →₀ A.V) ModuleCat.of k (G × G →₀ A.V)

                The 2nd differential in the complex of inhomogeneous chains of A : Rep k G, as a k-linear map (G³ →₀ A) → (G² →₀ A). It sends a·(g₁, g₂, g₃) ↦ ρ_A(g₁⁻¹)(a)·(g₂, g₃) - a·(g₁g₂, g₃) + a·(g₁, g₂g₃) - a·(g₁, g₂).

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem groupHomology.d₃₂_single {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g : G × G × G) (a : A.V) :
                  (CategoryTheory.ConcreteCategory.hom (d₃₂ A)) (Finsupp.single g a) = Finsupp.single (g.2.1, g.2.2) ((A.ρ g.1⁻¹) a) - Finsupp.single (g.1 * g.2.1, g.2.2) a + Finsupp.single (g.1, g.2.1 * g.2.2) a - Finsupp.single (g.1, g.2.1) a

                  Let C(G, A) denote the complex of inhomogeneous chains of A : Rep k G. This lemma says d₁₀ gives a simpler expression for the 0th differential: that is, the following square commutes:

                    C₁(G, A) --d 1 0--> C₀(G, A)
                      |                   |
                      |                   |
                      |                   |
                      v                   v
                    (G →₀ A) ----d₁₀----> A
                  

                  where the vertical arrows are chainsIso₁ and chainsIso₀ respectively.

                  Let C(G, A) denote the complex of inhomogeneous chains of A : Rep k G. This lemma says d₂₁ gives a simpler expression for the 1st differential: that is, the following square commutes:

                    C₂(G, A) --d 2 1--> C₁(G, A)
                      |                    |
                      |                    |
                      |                    |
                      v                    v
                    (G² →₀ A) --d₂₁--> (G →₀ A)
                  

                  where the vertical arrows are chainsIso₂ and chainsIso₁ respectively.

                  Let C(G, A) denote the complex of inhomogeneous chains of A : Rep k G. This lemma says d₃₂ gives a simpler expression for the 2nd differential: that is, the following square commutes:

                     C₃(G, A) --d 3 2--> C₂(G, A)
                      |                    |
                      |                    |
                      |                    |
                      v                    v
                    (G³ →₀ A) --d₃₂--> (G² →₀ A)
                  

                  where the vertical arrows are chainsIso₃ and chainsIso₂ respectively.