Finite direct sums of representations

A morphism into a finite direct sum is determined by its component morphisms. The resulting linear equivalence lets dimension computations use a concrete direct-sum representation without replacing it by a categorical biproduct.

The natural identification with a dependent product conjugates the direct-sum action to the componentwise action, so finite direct sums can also be studied through product linear maps.

theorem Representation.conj_directSum_linearEquivFunOnFintype {k : Type u_1} {G : Type u_2} {ι : Type u_3} [CommSemiring k] [Monoid G] [Fintype ι] {V : ι → Type u_4} [(i : ι) → AddCommMonoid (V i)] [(i : ι) → Module k (V i)] (ρ : (i : ι) → Representation k G (V i)) (g : G) : (DirectSum.linearEquivFunOnFintype k ι V).conj ((directSum ρ) g) = LinearMap.piMap fun (i : ι) => (ρ i) g

The finite direct-sum action becomes the componentwise action under the natural identification with the dependent product.

noncomputable def Rep.homDirectSumLinearEquiv {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {ι : Type v} [Fintype ι] (A : Rep k G) (B : ι → Rep k G) : (A ⟶ of (Representation.directSum fun (i : ι) => (B i).ρ)) ≃ₗ[k] (i : ι) → A ⟶ B i

Morphisms into a finite direct sum are families of morphisms into its summands.

@[simp]

theorem Rep.homDirectSumLinearEquiv_apply {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {ι : Type v} [Fintype ι] (A : Rep k G) (B : ι → Rep k G) (φ : A ⟶ of (Representation.directSum fun (i : ι) => (B i).ρ)) (i : ι) (x : ↑A) : (Hom.hom ((A.homDirectSumLinearEquiv B) φ i)) x = ((Hom.hom φ) x) i

A component morphism evaluates to the corresponding coordinate in the direct sum.

@[simp]

theorem Rep.homDirectSumLinearEquiv_symm_apply {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {ι : Type v} [Fintype ι] (A : Rep k G) (B : ι → Rep k G) (φ : (i : ι) → A ⟶ B i) (x : ↑A) (i : ι) : ((Hom.hom ((A.homDirectSumLinearEquiv B).symm φ)) x) i = (Hom.hom (φ i)) x

The inverse assembles the supplied component morphisms.

@[simp]

theorem Rep.homDirectSumLinearEquiv_comp {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {ι : Type v} [Fintype ι] (A : Rep k G) (B : ι → Rep k G) {A' : Rep k G} (f : A' ⟶ A) (φ : A ⟶ of (Representation.directSum fun (i : ι) => (B i).ρ)) (i : ι) : (A'.homDirectSumLinearEquiv B) (CategoryTheory.CategoryStruct.comp f φ) i = CategoryTheory.CategoryStruct.comp f ((A.homDirectSumLinearEquiv B) φ i)

Taking a component commutes with precomposition.