Short exact sequences of trivial representations

Equipping a module with the trivial action of a monoid G is a functor Rep.trivialFunctor k G : ModuleCat k ⥤ Rep k G. It is additive, and it carries a short exact sequence of k-modules to a short exact sequence of trivial representations, because exactness, injectivity and surjectivity in Rep k G are tested on underlying modules.

The case of interest is the sequence 0 → ℤ → ℚ → ℚ/ℤ → 0 with ℚ/ℤ realized as the rational circle AddCircle (1 : ℚ). With trivial action of a group G, its connecting maps in group cohomology send a character G → ℚ/ℤ to a class in H²(G, ℤ).

Main definitions

• Rep.ratAddCircleShortComplex: the short complex ℤ → ℚ → ℚ/ℤ of trivial integral representations of G.

Main results

• Rep.shortExact_map_trivialFunctor: the trivial-action functor preserves short exactness.
• Rep.ratAddCircleShortComplex_shortExact: 0 → ℤ → ℚ → ℚ/ℤ → 0 is short exact as a sequence of trivial representations.
• Rep.ratAddCircleShortComplex_f_hom_apply, Rep.ratAddCircleShortComplex_g_hom_apply: its maps are the inclusion of the integers and reduction modulo 1.

instance Rep.instAdditiveModuleCatTrivialFunctor_tauCeti {k : Type u} [Ring k] {G : Type v} [Monoid G] : (trivialFunctor k G).Additive

The trivial-action functor is additive.

theorem Rep.shortExact_map_trivialFunctor {k : Type u} [Ring k] {G : Type v} [Monoid G] {S : CategoryTheory.ShortComplex (ModuleCat k)} (hS : S.ShortExact) : (S.map (trivialFunctor k G)).ShortExact

The trivial-action functor carries a short exact sequence of modules to a short exact sequence of trivial representations.

@[reducible, inline]

abbrev Rep.ratAddCircleShortComplex (G : Type v) [Monoid G] : CategoryTheory.ShortComplex (Rep ℤ G)

The short complex ℤ → ℚ → ℚ/ℤ of trivial integral representations of G, with ℚ/ℤ the rational circle AddCircle (1 : ℚ): the inclusion of the integers followed by reduction modulo 1.

theorem Rep.ratAddCircleShortComplex_shortExact (G : Type v) [Monoid G] : (ratAddCircleShortComplex G).ShortExact

The sequence 0 → ℤ → ℚ → ℚ/ℤ → 0 of trivial integral representations is short exact.

theorem Rep.ratAddCircleShortComplex_f_hom_apply (G : Type v) [Monoid G] (n : ℤ) : (Hom.hom (ratAddCircleShortComplex G).f) n = ↑n

The first map of ℤ → ℚ → ℚ/ℤ is the inclusion of the integers.

theorem Rep.ratAddCircleShortComplex_g_hom_apply (G : Type v) [Monoid G] (q : ℚ) : (Hom.hom (ratAddCircleShortComplex G).g) q = ↑q

The second map of ℤ → ℚ → ℚ/ℤ is reduction modulo 1.