Documentation

TauCeti.RepresentationTheory.Homological.Resolution

The bar resolution along a group homomorphism #

Let f : H →* G be a homomorphism of groups. The bar resolution Rep.barComplex k H of the trivial representation k of H maps to the restriction along f of the bar resolution of G: in degree n a basis element (h₁, …, hₙ) is sent to (f h₁, …, f hₙ). This file constructs that chain map, TauCeti.Rep.barComplex.resChainMap, and checks that it lies over the identity of k. When restriction along f preserves projectives, it is therefore a morphism of projective resolutions of the trivial representation.

To make the last statement checkable, the file also computes the augmentations of Mathlib's standard and bar resolutions on basis elements: both send a basis element with coefficient r to r. On the way it records the value of the comparison Rep.diagonalSuccIsoFree between the bar and standard resolutions on basis elements, (g, (g₁, …, gₙ)) ↦ g • (1, g₁, g₁g₂, …, g₁⋯gₙ).

The chain map is what identifies Mathlib's Shapiro isomorphism groupCohomology.coindIso, which is defined through Ext, with an explicit map on inhomogeneous cochains.

Main definitions #

Main results #

References #

source
theorem TauCeti.Rep.diagonalSuccIsoFree_inv_hom_single {k G : Type u} [CommRing k] [Group G] (m : ℕ) (x : Fin m → G) (g : G) (r : k) :
(Rep.Hom.hom (Rep.diagonalSuccIsoFree k G m).inv) (Finsupp.single x (MonoidAlgebra.single g r)) = MonoidAlgebra.single (g • Fin.partialProd x) r

The comparison Rep.diagonalSuccIsoFree between the bar and standard resolutions sends the basis element (g₁, …, gₘ) with coefficient r • g to g • (1, g₁, g₁g₂, …, g₁⋯gₘ) with coefficient r.

source
theorem TauCeti.Rep.standardResolution_π_f_zero_single {k G : Type u} [CommRing k] [Group G] (y : Fin 1 → G) (r : k) :
(Rep.Hom.hom ((Rep.standardResolution k G).π.f 0)) (MonoidAlgebra.single y r) = r

The augmentation of the standard resolution sends a basis element with coefficient r to r.

source
theorem TauCeti.Rep.barResolution_π_f_zero_single {k G : Type u} [CommRing k] [Group G] (x : Fin 0 → G) (g : G) (r : k) :
(Rep.Hom.hom ((Rep.barResolution k G).π.f 0)) (Finsupp.single x (MonoidAlgebra.single g r)) = r

The augmentation of the bar resolution sends a basis element with coefficient r to r.

source
noncomputable def TauCeti.Rep.barComplex.resHom {k G H : Type u} [CommRing k] [Group G] [Group H] (f : H →* G) (n : ℕ) :
Rep.free k H (Fin n → H) ⟶ Rep.res f (Rep.free k G (Fin n → G))

The degree-n component of the map from the bar resolution of H to the restriction along f : H →* G of the bar resolution of G: it sends the basis element (h₁, …, hₙ) to (f h₁, …, f hₙ).

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Rep.barComplex.resHom_single {k G H : Type u} [CommRing k] [Group G] [Group H] (f : H →* G) (n : ℕ) (x : Fin n → H) (h : H) (r : k) :
    (Rep.Hom.hom (resHom f n)) (Finsupp.single x (MonoidAlgebra.single h r)) = Finsupp.single (⇑f ∘ x) (MonoidAlgebra.single (f h) r)

    resHom f n applies f to the tuple and to the group coefficient of a basis element.

    source
    theorem TauCeti.Rep.barComplex.d_comp_resHom {k G H : Type u} [CommRing k] [Group G] [Group H] (f : H →* G) (n : ℕ) :
    CategoryTheory.CategoryStruct.comp (Rep.barComplex.d k H n) (resHom f n) = CategoryTheory.CategoryStruct.comp (resHom f (n + 1)) ((Rep.resFunctor f).map (Rep.barComplex.d k G n))

    The components resHom f n commute with the bar differentials.

    source
    noncomputable def TauCeti.Rep.barComplex.resChainMap {k G H : Type u} [CommRing k] [Group G] [Group H] (f : H →* G) :
    Rep.barComplex k H ⟶ ((Rep.resFunctor f).mapHomologicalComplex (ComplexShape.down ℕ)).obj (Rep.barComplex k G)

    The bar resolution along a group homomorphism. The chain map from the bar resolution of H to the restriction along f : H →* G of the bar resolution of G, sending (h₁, …, hₙ) to (f h₁, …, f hₙ) in every degree.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.Rep.barComplex.resChainMap_f {k G H : Type u} [CommRing k] [Group G] [Group H] (f : H →* G) (n : ℕ) :
      (resChainMap f).f n = resHom f n

      The components of resChainMap f are the maps resHom f n.

      source
      theorem TauCeti.Rep.barComplex.resChainMap_f_zero_comp_π {k G H : Type u} [CommRing k] [Group G] [Group H] (f : H →* G) [(Rep.resFunctor f).PreservesProjectiveObjects] :
      CategoryTheory.CategoryStruct.comp ((resChainMap f).f 0) (((Rep.resFunctor f).mapProjectiveResolution (Rep.barResolution k G)).π.f 0) = (Rep.barResolution k H).π.f 0

      The bar resolution along a group homomorphism lies over the identity of k: when restriction along f : H →* G preserves projectives, this is a morphism from the bar resolution of H to the restriction of the bar resolution of G, both viewed as projective resolutions of the trivial representation of H.