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.

Given an additive abelian group A with an appropriate scalar action of G, we provide support for turning a finsupp f : G →₀ A satisfying the 1-cycle identity into an element of the cycles₁ of the representation on A corresponding to the scalar action. We also do this for 0-boundaries, 1-boundaries, 2-cycles and 2-boundaries.

The file also contains an identification between the definitions in RepresentationTheory/Homological/GroupHomology/Basic.lean, groupHomology.cycles A n, and the cyclesₙ in this file for n = 1, 2, as well as an isomorphism groupHomology.cycles A 0 ≅ A.V. Moreover, we provide API for the natural maps cyclesₙ A → Hn A for n = 1, 2.

We show that when the representation on A is trivial, H₁(G, A) ≃+ Gᵃᵇ ⊗[ℤ] A.

Main definitions #

def groupHomology.chainsIso₀ {k G : Type u} [CommRing k] [Group G] (A : Rep k 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
    def groupHomology.chainsIso₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :

    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) :

      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) :

        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 is defined by 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 is defined by 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 is defined by 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.

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

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

                    The short complex (G² →₀ A) --d₂₁--> (G →₀ A) --d₁₀--> A.

                    Equations
                    Instances For

                      The short complex (G³ →₀ A) --d₃₂--> (G² →₀ A) --d₂₁--> (G →₀ A).

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        def groupHomology.cycles₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :
                        Submodule k (G →₀ A.V)

                        The 1-cycles Z₁(G, A) of A : Rep k G, defined as the kernel of the map (G →₀ A) → A defined by single g a ↦ ρ_A(g⁻¹)(a) - a.

                        Equations
                        Instances For
                          def groupHomology.cycles₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :
                          Submodule k (G × G →₀ A.V)

                          The 2-cycles Z₂(G, A) of A : Rep k G, defined as the kernel of the map (G² →₀ A) → (G →₀ A) defined by a·(g₁, g₂) ↦ ρ_A(g₁⁻¹)(a)·g₂ - a·g₁g₂ + a·g₁.

                          Equations
                          Instances For
                            theorem groupHomology.mem_cycles₁_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x : G →₀ A.V) :
                            x cycles₁ A (x.sum fun (g : G) (a : A.V) => (A.ρ g⁻¹) a) = x.sum fun (x : G) (a : A.V) => a
                            theorem groupHomology.single_mem_cycles₁_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g : G) (a : A.V) :
                            theorem groupHomology.single_mem_cycles₁_of_mem_invariants {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g : G) (a : A.V) (ha : a A.ρ.invariants) :

                            The natural inclusion Z₁(G, A) ⟶ C₁(G, A) is an isomorphism when the representation on A is trivial.

                            Equations
                            Instances For
                              theorem groupHomology.mem_cycles₂_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x : G × G →₀ A.V) :
                              x cycles₂ A (x.sum fun (g : G × G) (a : A.V) => Finsupp.single g.2 ((A.ρ g.1⁻¹) a) + Finsupp.single g.1 a) = x.sum fun (g : G × G) (a : A.V) => Finsupp.single (g.1 * g.2) a
                              theorem groupHomology.single_mem_cycles₂_iff_inv {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g : G × G) (a : A.V) :
                              theorem groupHomology.single_mem_cycles₂_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g : G × G) (a : A.V) :
                              Finsupp.single g a cycles₂ A Finsupp.single (g.1 * g.2) ((A.ρ g.1) a) = Finsupp.single g.2 a + Finsupp.single g.1 ((A.ρ g.1) a)
                              def groupHomology.boundaries₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :
                              Submodule k (G →₀ A.V)

                              The 1-boundaries B₁(G, A) of A : Rep k G, defined as the image of the map (G² →₀ A) → (G →₀ A) defined by a·(g₁, g₂) ↦ ρ_A(g₁⁻¹)(a)·g₂ - a·g₁g₂ + a·g₁.

                              Equations
                              Instances For
                                def groupHomology.boundaries₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :
                                Submodule k (G × G →₀ A.V)

                                The 2-boundaries B₂(G, A) of A : Rep k G, defined as the image of the map (G³ →₀ A) → (G² →₀ A) defined by a·(g₁, g₂, g₃) ↦ ρ_A(g₁⁻¹)(a)·(g₂, g₃) - a·(g₁g₂, g₃) + a·(g₁, g₂g₃) - a·(g₁, g₂).

                                Equations
                                Instances For
                                  theorem groupHomology.mem_cycles₁_of_mem_boundaries₁ {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : G →₀ A.V) (h : f boundaries₁ A) :
                                  @[reducible, inline]
                                  abbrev groupHomology.boundariesToCycles₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :

                                  The natural inclusion B₁(G, A) →ₗ[k] Z₁(G, A).

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem groupHomology.boundariesToCycles₁_apply {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x : (boundaries₁ A)) :
                                    ((boundariesToCycles₁ A) x) = x
                                    theorem groupHomology.mem_cycles₂_of_mem_boundaries₂ {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x : G × G →₀ A.V) (h : x boundaries₂ A) :
                                    @[reducible, inline]
                                    abbrev groupHomology.boundariesToCycles₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :

                                    The natural inclusion B₂(G, A) →ₗ[k] Z₂(G, A).

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem groupHomology.boundariesToCycles₂_apply {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x : (boundaries₂ A)) :
                                      ((boundariesToCycles₂ A) x) = x
                                      def groupHomology.IsCycle₁ {G : Type u_1} {A : Type u_2} [Inv G] [AddCommGroup A] [SMul G A] (x : G →₀ A) :

                                      A finsupp ∑ aᵢ·gᵢ : G →₀ A satisfies the 1-cycle condition if ∑ gᵢ⁻¹ • aᵢ = ∑ aᵢ.

                                      Equations
                                      Instances For
                                        def groupHomology.IsCycle₂ {G : Type u_1} {A : Type u_2} [Mul G] [Inv G] [AddCommGroup A] [SMul G A] (x : G × G →₀ A) :

                                        A finsupp ∑ aᵢ·(gᵢ, hᵢ) : G × G →₀ A satisfies the 2-cycle condition if ∑ (gᵢ⁻¹ • aᵢ)·hᵢ + aᵢ·gᵢ = ∑ aᵢ·gᵢhᵢ.

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem groupHomology.single_isCycle₁_iff {G : Type u_1} {A : Type u_2} [Group G] [AddCommGroup A] [DistribMulAction G A] (g : G) (a : A) :
                                          theorem groupHomology.single_isCycle₂_iff_inv {G : Type u_1} {A : Type u_2} [Group G] [AddCommGroup A] [DistribMulAction G A] (g : G × G) (a : A) :
                                          @[simp]
                                          theorem groupHomology.single_isCycle₂_iff {G : Type u_1} {A : Type u_2} [Group G] [AddCommGroup A] [DistribMulAction G A] (g : G × G) (a : A) :
                                          IsCycle₂ (Finsupp.single g a) Finsupp.single g.2 a + Finsupp.single g.1 (g.1 a) = Finsupp.single (g.1 * g.2) (g.1 a)
                                          def groupHomology.IsBoundary₀ (G : Type u_1) {A : Type u_2} [Inv G] [AddCommGroup A] [SMul G A] (a : A) :

                                          A term x : A satisfies the 0-boundary condition if there exists a finsupp ∑ aᵢ·gᵢ : G →₀ A such that ∑ gᵢ⁻¹ • aᵢ - aᵢ = x.

                                          Equations
                                          Instances For
                                            def groupHomology.IsBoundary₁ {G : Type u_1} {A : Type u_2} [Mul G] [Inv G] [AddCommGroup A] [SMul G A] (x : G →₀ A) :

                                            A finsupp x : G →₀ A satisfies the 1-boundary condition if there's a finsupp ∑ aᵢ·(gᵢ, hᵢ) : G × G →₀ A such that ∑ (gᵢ⁻¹ • aᵢ)·hᵢ - aᵢ·gᵢhᵢ + aᵢ·gᵢ = x.

                                            Equations
                                            Instances For
                                              def groupHomology.IsBoundary₂ {G : Type u_1} {A : Type u_2} [Mul G] [Inv G] [AddCommGroup A] [SMul G A] (x : G × G →₀ A) :

                                              A finsupp x : G × G →₀ A satsfies the 2-boundary condition if there's a finsupp ∑ aᵢ·(gᵢ, hᵢ, jᵢ) : G × G × G →₀ A such that ∑ (gᵢ⁻¹ • aᵢ)·(hᵢ, jᵢ) - aᵢ·(gᵢhᵢ, jᵢ) + aᵢ·(gᵢ, hᵢjᵢ) - aᵢ·(gᵢ, hᵢ) = x.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                theorem groupHomology.isBoundary₀_iff (G : Type u_1) {A : Type u_2} [Group G] [AddCommGroup A] [DistribMulAction G A] (a : A) :
                                                IsBoundary₀ G a ∃ (x : G →₀ A), (x.sum fun (g : G) (z : A) => g z - z) = a
                                                theorem groupHomology.isBoundary₁_iff {G : Type u_1} {A : Type u_2} [Group G] [AddCommGroup A] [DistribMulAction G A] (x : G →₀ A) :
                                                IsBoundary₁ x ∃ (y : G × G →₀ A), (y.sum fun (g : G × G) (a : A) => Finsupp.single g.2 a - Finsupp.single (g.1 * g.2) (g.1 a) + Finsupp.single g.1 (g.1 a)) = x
                                                theorem groupHomology.isBoundary₂_iff {G : Type u_1} {A : Type u_2} [Group G] [AddCommGroup A] [DistribMulAction G A] (x : G × G →₀ A) :
                                                IsBoundary₂ x ∃ (y : G × G × G →₀ A), (y.sum fun (g : G × G × G) (a : A) => Finsupp.single (g.2.1, g.2.2) a - Finsupp.single (g.1 * g.2.1, g.2.2) (g.1 a) + Finsupp.single (g.1, g.2.1 * g.2.2) (g.1 a) - Finsupp.single (g.1, g.2.1) (g.1 a)) = x

                                                Given a k-module A with a compatible DistribMulAction of G, and a term x : A satisfying the 0-boundary condition, this produces an element of the kernel of the quotient map A → A_G 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 finsupp x : G →₀ A satisfying the 1-cycle condition, produces a 1-cycle for the representation on A induced by the DistribMulAction.

                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem groupHomology.cyclesOfIsCycle₁_coe {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (x : G →₀ A) (hx : IsCycle₁ x) :
                                                    (cyclesOfIsCycle₁ x hx) = x

                                                    Given a k-module A with a compatible DistribMulAction of G, and a finsupp x : G →₀ A satisfying the 1-boundary condition, produces a 1-boundary 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 finsupp x : G × G →₀ A satisfying the 2-cycle condition, produces a 2-cycle for the representation on A induced by the DistribMulAction.

                                                      Equations
                                                      Instances For
                                                        @[simp]
                                                        theorem groupHomology.cyclesOfIsCycle₂_coe {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (x : G × G →₀ A) (hx : IsCycle₂ x) :
                                                        (cyclesOfIsCycle₂ x hx) = x

                                                        Given a k-module A with a compatible DistribMulAction of G, and a finsupp x : G × G →₀ A satisfying the 2-boundary condition, produces a 2-boundary for the representation on A induced by the DistribMulAction.

                                                        Equations
                                                        Instances For
                                                          def groupHomology.cyclesIso₀ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :
                                                          cycles A 0 A.V

                                                          The 0-cycles of the complex of inhomogeneous chains of A are isomorphic to A.

                                                          Equations
                                                          Instances For

                                                            The arrow (G →₀ A) --d₁₀--> A is isomorphic to the differential (inhomogeneousChains A).d 1 0 of the complex of inhomogeneous chains of A.

                                                            Equations
                                                            Instances For

                                                              The 0-cycles of the complex of inhomogeneous chains of A are isomorphic to A.ρ.coinvariants, which is a simpler type.

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

                                                                The short complex (G² →₀ A) --d₂₁--> (G →₀ A) --d₁₀--> A is isomorphic to the 1st short complex associated to the complex of inhomogeneous chains of A.

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  def groupHomology.isoCycles₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :

                                                                  The 1-cycles of the complex of inhomogeneous chains of A are isomorphic to cycles₁ A, which is a simpler type.

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

                                                                    The short complex (G³ →₀ A) --d₃₂--> (G² →₀ A) --d₂₁--> (G →₀ A) is isomorphic to the 2nd short complex associated to the complex of inhomogeneous chains of A.

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      def groupHomology.isoCycles₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :

                                                                      The 2-cycles of the complex of inhomogeneous chains of A are isomorphic to cycles₂ A, which is a simpler type.

                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        @[reducible, inline]
                                                                        abbrev groupHomology.H0 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :

                                                                        Shorthand for the 0th group homology of a k-linear G-representation A, H₀(G, A), defined as the 0th homology of the complex of inhomogeneous chains of A.

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

                                                                          The 0th group homology of A, defined as the 0th homology of the complex of inhomogeneous chains, is isomorphic to the invariants of the representation on A.

                                                                          Equations
                                                                          Instances For
                                                                            def groupHomology.H0π {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :
                                                                            A.V H0 A

                                                                            The quotient map from A to H₀(G, A).

                                                                            Equations
                                                                            Instances For
                                                                              theorem groupHomology.H0_induction_on {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {C : (H0 A)Prop} (x : (H0 A)) (h : ∀ (x : A.V), C ((CategoryTheory.ConcreteCategory.hom (H0π A)) x)) :
                                                                              C x
                                                                              def groupHomology.H0IsoOfIsTrivial {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] :
                                                                              H0 A A.V

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

                                                                              Equations
                                                                              Instances For
                                                                                @[reducible, inline]
                                                                                abbrev groupHomology.H1 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :

                                                                                Shorthand for the 1st group homology of a k-linear G-representation A, H₁(G, A), defined as the 1st homology of the complex of inhomogeneous chains of A.

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

                                                                                  The quotient map from the 1-cycles of A, as a submodule of G →₀ A, to H₁(G, A).

                                                                                  Equations
                                                                                  Instances For
                                                                                    theorem groupHomology.H1_induction_on {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {C : (H1 A)Prop} (x : (H1 A)) (h : ∀ (x : (cycles₁ A)), C ((CategoryTheory.ConcreteCategory.hom (H1π A)) x)) :
                                                                                    C x

                                                                                    The 1st group homology of A, defined as the 1st homology of the complex of inhomogeneous chains, is isomorphic to cycles₁ A ⧸ boundaries₁ A, which is a simpler type.

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

                                                                                      If a G-representation on A is trivial, this is the natural map Gᵃᵇ → A → H₁(G, A) sending ⟦g⟧, a to ⟦single g a⟧.

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

                                                                                        If a G-representation on A is trivial, this is the natural map H₁(G, A) → Gᵃᵇ ⊗[ℤ] A sending ⟦single g a⟧ to ⟦g⟧ ⊗ₜ a.

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

                                                                                          If a G-representation on A is trivial, this is the group isomorphism between H₁(G, A) ≃+ Gᵃᵇ ⊗[ℤ] A defined by ⟦single g a⟧ ↦ ⟦g⟧ ⊗ a.

                                                                                          Equations
                                                                                          Instances For
                                                                                            theorem groupHomology.H1AddEquivOfIsTrivial_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] (a✝ : (H1 A)) :
                                                                                            @[reducible, inline]
                                                                                            abbrev groupHomology.H2 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :

                                                                                            Shorthand for the 2nd group homology of a k-linear G-representation A, H₂(G, A), defined as the 2nd homology of the complex of inhomogeneous chains of A.

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

                                                                                              The quotient map from the 2-cycles of A, as a submodule of G × G →₀ A, to H₂(G, A).

                                                                                              Equations
                                                                                              Instances For
                                                                                                theorem groupHomology.H2_induction_on {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {C : (H2 A)Prop} (x : (H2 A)) (h : ∀ (x : (cycles₂ A)), C ((CategoryTheory.ConcreteCategory.hom (H2π A)) x)) :
                                                                                                C x

                                                                                                The 2nd group homology of A, defined as the 2nd homology of the complex of inhomogeneous chains, is isomorphic to cycles₂ A ⧸ boundaries₂ A, which is a simpler type.

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