Holomorphic rational representations

Every rational representation of GL n ℂ has complex-analytic matrix coefficients. For a normed complex carrier, it gives a complex-analytic homomorphism into the invertible continuous linear operators, with their native open-submanifold structure. Rationality supplies the finite dimensionality and completeness of the carrier.

Main results

• TauCeti.IsRationalRep.contMDiff_dual_apply: matrix coefficients are complex analytic.
• TauCeti.IsRationalRep.contMDiff_toContinuousLinearMap: so is the operator-valued action.
• TauCeti.IsRationalRep.contMDiff_toHomUnits: holomorphy with values in the invertible operators.

References

• T. Bröcker and T. tom Dieck, Representations of Compact Lie Groups, Springer GTM 98 (1985), Chapter III, §8, Proposition (8.6), pp.154–155: algebraic matrix coefficients yield a holomorphic representation; Proposition (8.7) identifies the classical complexifications.

theorem TauCeti.IsRationalRep.contMDiff_dual_apply {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (h : IsRationalRep ρ) (f : Module.Dual ℂ W) (w : W) : ContMDiff (modelWithCornersSelf ℂ (Matrix (Fin n) (Fin n) ℂ)) (modelWithCornersSelf ℂ ℂ) ⊤ fun (g : GL (Fin n) ℂ) => f ((ρ g) w)

Every matrix coefficient of a rational representation is complex analytic.

theorem TauCeti.IsRationalRep.contMDiff_toContinuousLinearMap {n : ℕ} {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] {σ : Representation ℂ (GL (Fin n) ℂ) V} (h : IsRationalRep σ) : have x := ⋯; ContMDiff (modelWithCornersSelf ℂ (Matrix (Fin n) (Fin n) ℂ)) (modelWithCornersSelf ℂ (V →L[ℂ] V)) ⊤ fun (g : GL (Fin n) ℂ) => (Module.End.toContinuousLinearMap V) (σ g)

A rational representation is complex analytic as a family of continuous linear operators. The finite-dimensional structure needed for the conversion is supplied by rationality.

theorem TauCeti.IsRationalRep.contMDiff_toHomUnits {n : ℕ} {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] {σ : Representation ℂ (GL (Fin n) ℂ) V} (h : IsRationalRep σ) : have x := ⋯; have x := ⋯; ContMDiff (modelWithCornersSelf ℂ (Matrix (Fin n) (Fin n) ℂ)) (modelWithCornersSelf ℂ (V →L[ℂ] V)) ⊤ ⇑((Module.End.toContinuousLinearMap V).toMulEquiv.toMonoidHom.comp σ).toHomUnits

A rational representation gives a holomorphic homomorphism into the invertible continuous linear operators. Its carrier's finite dimensionality and completeness follow from rationality.