Nonconstant holomorphic functions are open maps

Stream: Is there code for X?

[Kalle Kytölä]

Before coming to my actual #xy, the following seems like it should be trivial to do:

How should one interpret a nonzero complex number as a continuous linear automorphism of $\mathbb{C}$? For example, do we have something that achieves the second of the following two? For comparison, the first one is found by library_search, but it only interprets a nonzero complex number as a linear automorphism of $\mathbb{C}$ without bundled continuity.

import analysis.complex.schwarz

noncomputable theory

example : ℂˣ →* (ℂ ≃ₗ[ℂ] ℂ) := distrib_mul_action.to_module_aut ℂ ℂ

example : ℂˣ →* (ℂ ≃L[ℂ] ℂ) := by sorry

[Kalle Kytölä]

The first #xy step for the above is that I'd like to have the following easy special case of the open mapping theorem, and I have trouble feeding into the inverse function theorem (docs#has_strict_fderiv_at.to_local_homeomorph) the fact that a non-zero complex derivative is an invertible fderivative:

import analysis.complex.schwarz

noncomputable theory

open metric function set
open_locale topological_space

lemma image_nhds_of_deriv_nonzero
  {g : ℂ → ℂ} {w : ℂ} (dg_nonzero : deriv g w ≠ 0) (dg_strict : has_strict_deriv_at g (deriv g w) w)
  {W : set ℂ} (W_nhd : W ∈ 𝓝 w) :
  g '' W ∈ 𝓝 (g w) :=
begin
  have dg_strict' := dg_strict.has_strict_fderiv_at,
  have key := has_strict_fderiv_at.to_local_homeomorph g,
  -- I'd like the next argument in `key` to be `dg_strict'`, but that
  -- is not a coercion of a continuous linear equivalence.
  sorry,
end

[Kalle Kytölä]

The main #xy is: do we have the open mapping theorem for nonconstant holomorphic functions (on a connected open set, say)?

[Kalle Kytölä]

I guess yet another way of phrasing the question is: is there a deriv-version (as opposed to the fderiv formulation) of docs#has_strict_fderiv_at.to_local_homeomorph?

[Sebastien Gouezel]

You can do it with:

import analysis.complex.schwarz

noncomputable theory

open metric function set
open_locale topological_space

lemma image_nhds_of_deriv_nonzero
  {g : ℂ → ℂ} {g' w : ℂ} (hg' : g' ≠ 0)
  (dg_strict : has_strict_deriv_at g g' w)
  {W : set ℂ} (W_nhd : W ∈ 𝓝 w) :
  g '' W ∈ 𝓝 (g w) :=
begin
  let u : ℂ ≃L[ℂ] ℂ :=
    (linear_map.linear_equiv_of_injective (algebra.lmul_left ℂ g')
      (algebra.lmul_left_injective hg') rfl).to_continuous_linear_equiv,
  have A : has_strict_fderiv_at g (u : ℂ →L[ℂ] ℂ) w,
  { convert dg_strict.has_strict_fderiv_at,
    ext1 x,
    simp only [continuous_linear_equiv.coe_coe, linear_equiv.coe_to_continuous_linear_equiv',
      linear_map.linear_equiv_of_injective_apply, algebra.lmul_left_apply, mul_one,
      continuous_linear_map.smul_right_apply, continuous_linear_map.one_apply,
      algebra.id.smul_eq_mul, one_mul] },
  rw ← A.map_nhds_eq_of_equiv,
  exact filter.image_mem_map W_nhd
end

(where the ugly simp only is just to make things fast, but a plain simp works as well).

[Sebastien Gouezel]

(I didn't know the name of algebra.lmul_left, but it was found for me by suggest).
And probably we could add some more API to make this easier, but the current situation is already not too bad I think.

[Sebastien Gouezel]

(And a better way to phrase the conclusion of the lemma is probably to say filter.map g (𝓝 w) = 𝓝 (g w)).