Analyticity of rational functions on the general linear group

A rational function on GLₙ(𝕜) over a complete nontrivially normed field, expressed as a polynomial in matrix entries divided by a power of the determinant, is analytic in the native open-submanifold structure.

Main results

• TauCeti.Matrix.GeneralLinearGroup.contMDiff_of_mem_rationalFunctions: analyticity of every rational function on GL n 𝕜.

References

• Mathlib.Analysis.Analytic.Polynomial, for polynomial analyticity over complete normed fields.

• 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 are holomorphic.

theorem TauCeti.Matrix.GeneralLinearGroup.contMDiff_of_mem_rationalFunctions {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {n : ℕ} {f : GL (Fin n) 𝕜 → 𝕜} (hf : f ∈ rationalFunctions 𝕜 n) : have x := ⋯; ContMDiff (modelWithCornersSelf 𝕜 (Matrix (Fin n) (Fin n) 𝕜)) (modelWithCornersSelf 𝕜 𝕜) ⊤ f

Rational functions on the general linear group over a complete normed field are analytic.