Descent of rotation-invariant functions through u ↦ u ^ m

The group rootsOfUnity m ℂ of m-th roots of unity acts on ℂ by rotations, and u ↦ u ^ m is the orbit map of this action (SubMulAction.rootsOfUnityQuotientHomeomorph). This file shows that the orbit map is also the quotient map holomorphically: a function invariant under the rotations factors as f u = g (u ^ m), where g is holomorphic, analytic, or meromorphic whenever f is, and the orders of vanishing satisfy ord₀ f = m * ord₀ g.

This is the local model for descending invariant functions to the quotient of a Riemann surface at a point whose stabilizer is cyclic of order m. In a coordinate centred at the fixed point in which a generator acts by a primitive m-th root of unity, an invariant function descends to the quotient coordinate w = u ^ m, and its order at the fixed point is m times the order of the descended function.

The descended function TauCeti.descendPow m f evaluates f at the principal m-th root w ^ (1 / m). It satisfies descendPow m f (u ^ m) = f u at every point u at which f is invariant under the rotations (TauCeti.descendPow_pow), and it undoes pulling back along u ↦ u ^ m (TauCeti.descendPow_comp_pow), so the choice of branch is invisible in the results.

Main declarations

• TauCeti.descendPow: the descent of a function through u ↦ u ^ m.
• TauCeti.descendPow_pow: descendPow m f (u ^ m) = f u when f is invariant at u.
• TauCeti.eq_descendPow_iff: the criterion for a globally invariant function to factor through the power map.
• TauCeti.differentiableOn_descendPow: the descent of a function holomorphic and invariant on an open set s is holomorphic on the open set (· ^ m) '' s.
• TauCeti.analyticAt_descendPow and TauCeti.meromorphicAt_descendPow: the descent of a function analytic, respectively meromorphic, at 0 and invariant near 0 is analytic, respectively meromorphic, at 0.
• TauCeti.analyticOrderAt_descendPow_mul and TauCeti.meromorphicOrderAt_descendPow_mul: the order of f at 0 is m times the order of its descent at 0.

References

• Hershel M. Farkas and Irwin Kra, Riemann Surfaces, second edition, Chapter I §§4–5.
• Rick Miranda, Algebraic Curves and Riemann Surfaces, Chapter III §3.

noncomputable def TauCeti.descendPow {E : Type u_1} (m : ℕ) [NeZero m] (f : ℂ → E) (w : ℂ) : E

The descent of a function f : ℂ → E through u ↦ u ^ m: its value at w is the value of f at the principal m-th root of w, for nonzero m. When f is invariant under the m-th roots of unity on a set s, this is the function on (· ^ m) '' s through which f factors on s (TauCeti.descendPow_pow).

Equations

• TauCeti.descendPow m f w = f (w ^ (↑↑⟨m, ⋯⟩)⁻¹)

theorem TauCeti.descendPow_apply {E : Type u_1} {m : ℕ} [NeZero m] (f : ℂ → E) (w : ℂ) : descendPow m f w = f (w ^ (↑m)⁻¹)

@[simp]

theorem TauCeti.descendPow_comp_pow {E : Type u_1} {m : ℕ} [NeZero m] (g : ℂ → E) : (descendPow m fun (u : ℂ) => g (u ^ m)) = g

Descending a function pulled back along u ↦ u ^ m recovers the function.

@[simp]

theorem TauCeti.descendPow_smul_comp_pow {E : Type u_1} {m : ℕ} [NeZero m] [SMul ℂ E] (φ : ℂ → ℂ) (f : ℂ → E) : (descendPow m fun (u : ℂ) => φ (u ^ m) • f u) = fun (w : ℂ) => φ w • descendPow m f w

Descent through u ↦ u ^ m is linear over functions pulled back along u ↦ u ^ m.

@[simp]

theorem TauCeti.descendPow_pow {E : Type u_1} {m : ℕ} [NeZero m] {f : ℂ → E} {u : ℂ} (hf : ∀ (ζ : ↥(rootsOfUnity m ℂ)), f (ζ • u) = f u) : descendPow m f (u ^ m) = f u

If f takes the same value at all rotations of u by m-th roots of unity, then the descent of f takes that value at u ^ m.

theorem TauCeti.eq_descendPow_iff {E : Type u_1} {m : ℕ} [NeZero m] {f g : ℂ → E} (hf : ∀ (u : ℂ) (ζ : ↥(rootsOfUnity m ℂ)), f (ζ • u) = f u) : g = descendPow m f ↔ ∀ (u : ℂ), g (u ^ m) = f u

For a globally rotation-invariant function, a function is its descent precisely when its pullback along u ↦ u ^ m is the original function.

theorem TauCeti.descendPow_pow_eventuallyEq {E : Type u_1} {m : ℕ} [NeZero m] {f : ℂ → E} (hf : ∀ᶠ (u : ℂ) in nhdsWithin 0 {0}ᶜ, ∀ (ζ : ↥(rootsOfUnity m ℂ)), f (ζ • u) = f u) : (fun (u : ℂ) => descendPow m f (u ^ m)) =ᶠ[nhds 0] f

A function invariant under the m-th roots of unity on a punctured neighbourhood of 0 agrees near 0 with the pullback of its descent along u ↦ u ^ m.

theorem TauCeti.differentiableAt_descendPow_pow {E : Type u_1} {m : ℕ} [NeZero m] [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {u : ℂ} (hf : ∀ᶠ (v : ℂ) in nhds u, ∀ (ζ : ↥(rootsOfUnity m ℂ)), f (ζ • v) = f v) (hu : u ≠ 0) (hfu : DifferentiableAt ℂ f u) : DifferentiableAt ℂ (descendPow m f) (u ^ m)

Away from 0, the descent of a function invariant under the m-th roots of unity near u is complex differentiable at u ^ m when the function is complex differentiable at u.

theorem TauCeti.differentiableOn_descendPow {E : Type u_1} {m : ℕ} [NeZero m] [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {s : Set ℂ} {f : ℂ → E} (hs : IsOpen s) (hfd : DifferentiableOn ℂ f s) (hf : ∀ u ∈ s, ∀ (ζ : ↥(rootsOfUnity m ℂ)), f (ζ • u) = f u) : DifferentiableOn ℂ (descendPow m f) ((fun (x : ℂ) => x ^ m) '' s)

The descent of a function holomorphic on an open set s and invariant under the m-th roots of unity at every point of s is holomorphic on the open set (· ^ m) '' s.

theorem TauCeti.analyticAt_descendPow {E : Type u_1} {m : ℕ} [NeZero m] [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} (hfa : AnalyticAt ℂ f 0) (hf : ∀ᶠ (u : ℂ) in nhdsWithin 0 {0}ᶜ, ∀ (ζ : ↥(rootsOfUnity m ℂ)), f (ζ • u) = f u) : AnalyticAt ℂ (descendPow m f) 0

The descent of a function analytic at 0 and invariant under the m-th roots of unity near 0 is analytic at 0.

theorem TauCeti.meromorphicAt_descendPow {E : Type u_1} {m : ℕ} [NeZero m] [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} (hfm : MeromorphicAt f 0) (hf : ∀ᶠ (u : ℂ) in nhdsWithin 0 {0}ᶜ, ∀ (ζ : ↥(rootsOfUnity m ℂ)), f (ζ • u) = f u) : MeromorphicAt (descendPow m f) 0

The descent of a function meromorphic at 0 and invariant under the m-th roots of unity near 0 is meromorphic at 0.

theorem TauCeti.analyticOrderAt_descendPow_mul {E : Type u_1} {m : ℕ} [NeZero m] [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} (hfa : AnalyticAt ℂ f 0) (hf : ∀ᶠ (u : ℂ) in nhdsWithin 0 {0}ᶜ, ∀ (ζ : ↥(rootsOfUnity m ℂ)), f (ζ • u) = f u) : analyticOrderAt (descendPow m f) 0 * ↑m = analyticOrderAt f 0

The order of vanishing at 0 of a function analytic at 0 and invariant under the m-th roots of unity near 0 is m times the order of vanishing of its descent.

theorem TauCeti.meromorphicOrderAt_descendPow_mul {E : Type u_1} {m : ℕ} [NeZero m] [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} (hfm : MeromorphicAt f 0) (hf : ∀ᶠ (u : ℂ) in nhdsWithin 0 {0}ᶜ, ∀ (ζ : ↥(rootsOfUnity m ℂ)), f (ζ • u) = f u) : meromorphicOrderAt (descendPow m f) 0 * ↑m = meromorphicOrderAt f 0

The meromorphic order at 0 of a function meromorphic at 0 and invariant under the m-th roots of unity near 0 is m times the meromorphic order of its descent.