Documentation

TauCeti.RepresentationTheory.Homological.GroupHomology.Augmentation

The augmentation connecting map in first group homology #

The connecting map of the augmentation sequence sends the first-homology class of g ⊗ a to the coinvariant class of [g⁻¹] a - [1] a. The same formula holds after restricting the sequence to a subgroup. These formulas identify the connecting-map images of the classes g ⊗ a in H₀(G, I_G) and H₀(S, I_G), which is how the transfer on first homology is compared with the group-theoretic transfer (Verlagerung) in TauCeti.RepresentationTheory.Homological.GroupHomology.Transfer.Abelianization.

Main results #

References #

source
theorem TauCeti.groupHomology.δ_mkH1OfIsTrivial {k G : Type u} [CommRing k] [Group G] (g : G) (a : k) :
(CategoryTheory.ConcreteCategory.hom (groupHomology.δ ⋯ 1 0 ⋯)) (((groupHomology.mkH1OfIsTrivial (Rep.trivial k G k)) (Additive.ofMul (Abelianization.of g))) a) = (CategoryTheory.ConcreteCategory.hom (groupHomology.H0π (Rep.augmentationIdeal k G))) (AugmentationIdeal.singleSub k G a g⁻¹)

The augmentation connecting map sends g ⊗ a to the class of [g⁻¹] a - [1] a.

source
theorem TauCeti.groupHomology.δ_res_mkH1OfIsTrivial {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) (hAug : { X₁ := Rep.augmentationIdeal k G, X₂ := Rep.leftRegular k G, X₃ := Rep.trivial k G k, f := Rep.augmentationι k G, g := Rep.augmentation k G, zero := ⋯ }.ShortExact) (s : ↥S) (a : k) :
(CategoryTheory.ConcreteCategory.hom (groupHomology.δ ⋯ 1 0 ⋯)) (((groupHomology.mkH1OfIsTrivial (Rep.res S.subtype (Rep.trivial k G k))) (Additive.ofMul (Abelianization.of s))) a) = (CategoryTheory.ConcreteCategory.hom (groupHomology.H0π (Rep.res S.subtype (Rep.augmentationIdeal k G)))) (AugmentationIdeal.singleSub k G a ↑s⁻¹)

The restricted augmentation connecting map sends s ⊗ a to the class of [s⁻¹] a - [1] a. The short exactness witness may be transported from Rep.augmentationSES_shortExact through Rep.augmentationSES_def.