Morphisms into 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.

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.

Equations

• One or more equations did not get rendered due to their size.

@[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.