Products of analytic submanifolds

The product of analytic submanifolds of dimensions d and e in 𝕜ⁿ and 𝕜ᵐ, represented in 𝕜ⁿ⁺ᵐ by concatenating coordinates, is an analytic submanifold of dimension d + e. Analytic functions on the factors pull back along the two coordinate projections, and their pairs are analytic on the product.

The product of two straightening charts initially has two separate blocks of constrained coordinates. A continuous linear change of coordinates groups the free coordinates of both factors first. Thus its image is the coordinate subspace used by IsAnalyticChart, including when either factor has dimension zero or full ambient dimension. Products supply parameter domains for analytic families on submanifolds.

References

• S. G. Krantz and H. R. Parks, A Primer of Real Analytic Functions, second edition, Birkhäuser, 2002, Chapter 2.

theorem TauCeti.IsAnalyticSubmanifold.prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n m d e : ℕ} {S : Set (Fin n → 𝕜)} {T : Set (Fin m → 𝕜)} (hS : IsAnalyticSubmanifold d S) (hT : IsAnalyticSubmanifold e T) : IsAnalyticSubmanifold (d + e) {x : Fin (n + m) → 𝕜 | (fun (i : Fin n) => x (Fin.castAdd m i)) ∈ S ∧ (fun (i : Fin m) => x (Fin.natAdd n i)) ∈ T}

The product of d- and e-dimensional analytic submanifolds is an analytic submanifold of dimension d + e. Its ambient coordinates are concatenated: the first n coordinates belong to S and the final m to T.

theorem TauCeti.AnalyticOnSubmanifold.prodMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n m d e : ℕ} {S : Set (Fin n → 𝕜)} {T : Set (Fin m → 𝕜)} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : (Fin n → 𝕜) → E} {g : (Fin m → 𝕜) → F} (hf : AnalyticOnSubmanifold d f S) (hg : AnalyticOnSubmanifold e g T) (hd : d ≤ n) (he : e ≤ m) : AnalyticOnSubmanifold (d + e) (fun (x : Fin (n + m) → 𝕜) => (f fun (i : Fin n) => x (Fin.castAdd m i), g fun (i : Fin m) => x (Fin.natAdd n i))) {x : Fin (n + m) → 𝕜 | (fun (i : Fin n) => x (Fin.castAdd m i)) ∈ S ∧ (fun (i : Fin m) => x (Fin.natAdd n i)) ∈ T}

Functions analytic on the two factors combine into an analytic function on their product. Only dimension bounds are needed: the functions already supply charts at every point, and neither factor needs to be nonempty.