General facts about induced representations

Mathlib's Rep.ind φ induces a representation along an arbitrary homomorphism of groups φ : G →* H, and Rep.indMap φ induces an intertwiner along it. This file collects the general properties of that construction that Mathlib does not record and that the rest of TauCeti/RepresentationTheory/Induction/ needs, independently of any finiteness assumption on the groups or on the representations.

Main statements

• Rep.indMap_add: inducing an intertwiner along φ is additive, and Rep.indFunctor_additive: the same fact as a CategoryTheory.Functor.Additive instance for Rep.indFunctor.

theorem Rep.indMap_add {k : Type u} {G : Type v} {H : Type w} [CommRing k] [Group G] [Group H] (φ : G →* H) {A B : Rep k G} (f g : A ⟶ B) : indMap φ (f + g) = indMap φ f + indMap φ g

Induction of intertwiners is additive: for any homomorphism of groups φ : G →* H, Rep.indMap φ (f + g) = Rep.indMap φ f + Rep.indMap φ g.

instance Rep.indFunctor_additive {k : Type u} {G : Type v} {H : Type w} [CommRing k] [Group G] [Group H] (φ : G →* H) : (indFunctor k φ).Additive

Induction along a homomorphism of groups is an additive functor, the functorial form of Rep.indMap_add.