Group homology and cohomology

TheoremInvariance of group cohomology under group isomorphism#✓fully proved

Group cohomology is invariant under group isomorphism.

theorem nonempty_linearEquiv_of_iso_res_mulEquiv
    {k G H : Type u} [CommRing k] [Group G] [Group H]
    (e : G ≃* H) (A : Rep k G) (B : Rep k H) (φ : A ≅ Rep.res e.toMonoidHom B) (n : ℕ) :
    ∃ ψ : groupCohomology A n ≃ₗ[k] groupCohomology B n,
      ∀ x : groupCohomology B n,
        ψ.symm x =
          (groupCohomology.map e.toMonoidHom
            (φ.inv : Rep.res e.toMonoidHom B ⟶ A) n).hom x

DefinitionGroup homology of a direct sum#✓fully proved

Let \(k\) be a commutative ring, \(G\) a group, \(A\) and \(B\) representations of \(G\) over \(k\), and \(n \in \mathbb{N}\), and write \(H_n(G, M)\) for the \(n\)th group homology of a representation \(M\). This is the isomorphism \(H_n(G, A \oplus B) \cong H_n(G, A) \oplus H_n(G, B)\) obtained by applying the \(n\)th group homology functor, which is additive, to the biproduct \(A \oplus B\).

noncomputable def biprodIso (k G : Type u) [CommRing k] [Group G]
    (A B : Rep k G) (n : ℕ) :
    groupHomology (A ⊞ B) n ≅ groupHomology A n ⊞ groupHomology B n :=
  (functor k G n).mapBiprod A B

Sources

• NumberTheoryI, Section 23.4, Corollary 23.22.

Used by 6

Used byForward map of the direct-sum isomorphism in group homology · Direct-sum isomorphism in group homology and the first projection · Direct-sum isomorphism in group homology and the second projection · Inverse map of the direct-sum isomorphism in group homology · Direct-sum isomorphism in group homology and the first inclusion · Direct-sum isomorphism in group homology and the second inclusion

TheoremForward map of the direct-sum isomorphism in group homology#✓fully proved

Let \(k\) be a commutative ring, \(G\) a group, \(A\) and \(B\) representations of \(G\) over \(k\), and \(n \in \mathbb{N}\), and write \(H_n(G, M)\) for the \(n\)th group homology of a representation \(M\). The forward map of the isomorphism \(H_n(G, A \oplus B) \cong H_n(G, A) \oplus H_n(G, B)\) is the map into the biproduct whose components are the maps \(H_n(G, A \oplus B) \to H_n(G, A)\) and \(H_n(G, A \oplus B) \to H_n(G, B)\) induced by the projections \(A \oplus B \to A\) and \(A \oplus B \to B\).

theorem biprodIso_hom (k G : Type u) [CommRing k] [Group G]
    (A B : Rep k G) (n : ℕ) :
    (biprodIso k G A B n).hom =
      biprod.lift (groupHomology.map (MonoidHom.id G) biprod.fst n)
        (groupHomology.map (MonoidHom.id G) biprod.snd n)

Uses 1 · Used by 2

Statement usesGroup homology of a direct sum

Used byDirect-sum isomorphism in group homology and the first projection · Direct-sum isomorphism in group homology and the second projection

TheoremInverse map of the direct-sum isomorphism in group homology#✓fully proved

Let \(k\) be a commutative ring, \(G\) a group, \(A\) and \(B\) representations of \(G\) over \(k\), and \(n \in \mathbb{N}\), and write \(H_n(G, M)\) for the \(n\)th group homology of a representation \(M\). The inverse map of the isomorphism \(H_n(G, A \oplus B) \cong H_n(G, A) \oplus H_n(G, B)\) is the map out of the biproduct whose components are the maps \(H_n(G, A) \to H_n(G, A \oplus B)\) and \(H_n(G, B) \to H_n(G, A \oplus B)\) induced by the inclusions \(A \to A \oplus B\) and \(B \to A \oplus B\).

theorem biprodIso_inv (k G : Type u) [CommRing k] [Group G]
    (A B : Rep k G) (n : ℕ) :
    (biprodIso k G A B n).inv =
      biprod.desc (groupHomology.map (MonoidHom.id G) biprod.inl n)
        (groupHomology.map (MonoidHom.id G) biprod.inr n)

Uses 1 · Used by 2

Statement usesGroup homology of a direct sum

Used byDirect-sum isomorphism in group homology and the first inclusion · Direct-sum isomorphism in group homology and the second inclusion

TheoremDirect-sum isomorphism in group homology and the first projection#✓fully proved

Let \(k\) be a commutative ring, \(G\) a group, \(A\) and \(B\) representations of \(G\) over \(k\), and \(n \in \mathbb{N}\), and write \(H_n(G, M)\) for the \(n\)th group homology of a representation \(M\). The isomorphism \(H_n(G, A \oplus B) \cong H_n(G, A) \oplus H_n(G, B)\) followed by the projection onto \(H_n(G, A)\) equals the map \(H_n(G, A \oplus B) \to H_n(G, A)\) induced by the projection \(A \oplus B \to A\).

theorem biprodIso_hom_fst (k G : Type u) [CommRing k] [Group G]
    (A B : Rep k G) (n : ℕ) :
    (biprodIso k G A B n).hom ≫ biprod.fst =
      groupHomology.map (MonoidHom.id G) biprod.fst n

Uses 2

Statement usesGroup homology of a direct sum

Proof usesForward map of the direct-sum isomorphism in group homology

TheoremDirect-sum isomorphism in group homology and the second projection#✓fully proved

Let \(k\) be a commutative ring, \(G\) a group, \(A\) and \(B\) representations of \(G\) over \(k\), and \(n \in \mathbb{N}\), and write \(H_n(G, M)\) for the \(n\)th group homology of a representation \(M\). The isomorphism \(H_n(G, A \oplus B) \cong H_n(G, A) \oplus H_n(G, B)\) followed by the projection onto \(H_n(G, B)\) equals the map \(H_n(G, A \oplus B) \to H_n(G, B)\) induced by the projection \(A \oplus B \to B\).

theorem biprodIso_hom_snd (k G : Type u) [CommRing k] [Group G]
    (A B : Rep k G) (n : ℕ) :
    (biprodIso k G A B n).hom ≫ biprod.snd =
      groupHomology.map (MonoidHom.id G) biprod.snd n

Uses 2

Statement usesGroup homology of a direct sum

Proof usesForward map of the direct-sum isomorphism in group homology

TheoremDirect-sum isomorphism in group homology and the first inclusion#✓fully proved

Let \(k\) be a commutative ring, \(G\) a group, \(A\) and \(B\) representations of \(G\) over \(k\), and \(n \in \mathbb{N}\), and write \(H_n(G, M)\) for the \(n\)th group homology of a representation \(M\). The inclusion of \(H_n(G, A)\) into \(H_n(G, A) \oplus H_n(G, B)\) followed by the inverse of the isomorphism \(H_n(G, A \oplus B) \cong H_n(G, A) \oplus H_n(G, B)\) equals the map \(H_n(G, A) \to H_n(G, A \oplus B)\) induced by the inclusion \(A \to A \oplus B\).

theorem biprodIso_inv_inl (k G : Type u) [CommRing k] [Group G]
    (A B : Rep k G) (n : ℕ) :
    biprod.inl ≫ (biprodIso k G A B n).inv =
      groupHomology.map (MonoidHom.id G) biprod.inl n

Uses 2

Statement usesGroup homology of a direct sum

Proof usesInverse map of the direct-sum isomorphism in group homology

TheoremDirect-sum isomorphism in group homology and the second inclusion#✓fully proved

Let \(k\) be a commutative ring, \(G\) a group, \(A\) and \(B\) representations of \(G\) over \(k\), and \(n \in \mathbb{N}\), and write \(H_n(G, M)\) for the \(n\)th group homology of a representation \(M\). The inclusion of \(H_n(G, B)\) into \(H_n(G, A) \oplus H_n(G, B)\) followed by the inverse of the isomorphism \(H_n(G, A \oplus B) \cong H_n(G, A) \oplus H_n(G, B)\) equals the map \(H_n(G, B) \to H_n(G, A \oplus B)\) induced by the inclusion \(B \to A \oplus B\).

theorem biprodIso_inv_inr (k G : Type u) [CommRing k] [Group G]
    (A B : Rep k G) (n : ℕ) :
    biprod.inr ≫ (biprodIso k G A B n).inv =
      groupHomology.map (MonoidHom.id G) biprod.inr n

Uses 2

Statement usesGroup homology of a direct sum

Proof usesInverse map of the direct-sum isomorphism in group homology

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.