English
The determinant of the complex-conjugation linear map on C over R is −1.
Русский
Определитель линейного отображения комплексного сопряжения на ℂ над ℝ равен −1.
LaTeX
$$$\\det(\\operatorname{conjLIE}) = -1$$$
Lean4
/-- The *open mapping theorem* for holomorphic functions, local version: is a function `g : E → ℂ`
is analytic at a point `z₀`, then either it is constant in a neighborhood of `z₀`, or it maps every
neighborhood of `z₀` to a neighborhood of `z₀`. For the particular case of a holomorphic function on
`ℂ`, see `AnalyticAt.eventually_constant_or_nhds_le_map_nhds_aux`. -/
theorem eventually_constant_or_nhds_le_map_nhds {z₀ : E} (hg : AnalyticAt ℂ g z₀) :
(∀ᶠ z in 𝓝 z₀, g z = g z₀) ∨ 𝓝 (g z₀) ≤ map g (𝓝 z₀) := by
/- The idea of the proof is to use the one-dimensional version applied to the restriction of `g`
to lines going through `z₀` (indexed by `sphere (0 : E) 1`). If the restriction is eventually
constant along each of these lines, then the identity theorem implies that `g` is constant on
any ball centered at `z₀` on which it is analytic, and in particular `g` is eventually constant.
If on the other hand there is one line along which `g` is not eventually constant, then the
one-dimensional version of the open mapping theorem can be used to conclude. -/
let ray : E → ℂ → E := fun z t => z₀ + t • z
let gray : E → ℂ → ℂ := fun z => g ∘ ray z
obtain ⟨r, hr, hgr⟩ := isOpen_iff.mp (isOpen_analyticAt ℂ g) z₀ hg
have h1 : ∀ z ∈ sphere (0 : E) 1, AnalyticOnNhd ℂ (gray z) (ball 0 r) :=
by
refine fun z hz t ht => AnalyticAt.comp ?_ ?_
· exact hgr (by simpa [ray, norm_smul, mem_sphere_zero_iff_norm.mp hz] using ht)
· exact analyticAt_const.add ((ContinuousLinearMap.smulRight (ContinuousLinearMap.id ℂ ℂ) z).analyticAt t)
by_cases h : ∀ z ∈ sphere (0 : E) 1, ∀ᶠ t in 𝓝 0, gray z t = gray z 0
· left
-- If g is eventually constant along every direction, then it is eventually constant
refine eventually_of_mem (ball_mem_nhds z₀ hr) fun z hz => ?_
refine (eq_or_ne z z₀).casesOn (congr_arg g) fun h' => ?_
replace h' : ‖z - z₀‖ ≠ 0 := by simpa only [Ne, norm_eq_zero, sub_eq_zero]
let w : E := ‖z - z₀‖⁻¹ • (z - z₀)
have h3 : ∀ t ∈ ball (0 : ℂ) r, gray w t = g z₀ :=
by
have e1 : IsPreconnected (ball (0 : ℂ) r) := (convex_ball 0 r).isPreconnected
have e2 : w ∈ sphere (0 : E) 1 := by simp [w, norm_smul, inv_mul_cancel₀ h']
specialize h1 w e2
apply h1.eqOn_of_preconnected_of_eventuallyEq analyticOnNhd_const e1 (mem_ball_self hr)
simpa [ray, gray] using h w e2
have h4 : ‖z - z₀‖ < r := by simpa [dist_eq_norm] using mem_ball.mp hz
replace h4 : ↑‖z - z₀‖ ∈ ball (0 : ℂ) r := by simpa
simpa only [ray, gray, w, smul_smul, mul_inv_cancel₀ h', one_smul, add_sub_cancel, Function.comp_apply,
coe_smul] using h3 (↑‖z - z₀‖) h4
· right
-- Otherwise, it is open along at least one direction and that implies the result
push_neg at h
obtain ⟨z, hz, hrz⟩ := h
specialize h1 z hz 0 (mem_ball_self hr)
have h7 := h1.eventually_constant_or_nhds_le_map_nhds_aux.resolve_left hrz
rw [show gray z 0 = g z₀ by simp [gray, ray], ← map_compose] at h7
refine h7.trans (map_mono ?_)
have h10 : Continuous fun t : ℂ => z₀ + t • z := continuous_const.add (continuous_id'.smul continuous_const)
simpa using h10.tendsto 0
