Conjugate germs and the étale space

Step 6 of Rado/PLAN.md: harmonic conjugates normalized by Re F = u exactly (IsConjugate; existence on chart balls from Mathlib's Re-of-holomorphic, rigidity up to imaginary constants via the open mapping theorem), and the étale space ConjEtale u Y of conjugate germs: sheets over preconnected opens form a basis, the projection is an open local homeomorphism trivialized over conjugate neighbourhoods, the space is Hausdorff (identity theorem), the germ evaluation map is continuous with discrete fibers (isolated zeros; a constant germ would force u to be constant), and every connected component projects onto all of a connected base.

Conjugate germs and the étale space

def Rado.IsConjugate {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (u : X → ℝ) (F : X → ℂ) (V : Set X) : Prop

F is a holomorphic conjugate-package for u on V: holomorphic with Re F = u there.

Equations

• Rado.IsConjugate u F V = (Rado.HolomorphicOn F V ∧ ∀ x ∈ V, (F x).re = u x)

theorem Rado.exists_conjugate {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] {u : X → ℝ} {s : Set X} (hu : SurfaceHarmonicOn u s) (hs : IsOpen s) {x : X} (hx : x ∈ s) : ∃ (V : Set X) (F : X → ℂ), IsOpen V ∧ IsPreconnected V ∧ x ∈ V ∧ V ⊆ s ∧ IsConjugate u F V

Existence of conjugates on small connected neighbourhoods of any point of a harmonic function's domain (Schwarz integral in a chart; InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq).

theorem Rado.IsConjugate.eventuallyEq_add_const {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] {u : X → ℝ} {F G : X → ℂ} {V W : Set X} (hV : IsOpen V) (hW : IsOpen W) (hF : IsConjugate u F V) (hG : IsConjugate u G W) {y : X} (hyV : y ∈ V) (hyW : y ∈ W) : ∃ (t : ℝ), F =ᶠ[nhds y] fun (z : X) => G z + ↑t * Complex.I

Local rigidity: two conjugates near a point agree near that point up to an imaginary constant; in particular a conjugate germ over a preconnected open V extends to all of V once one conjugate exists on V.

theorem Rado.IsConjugate.add_const_mul_I {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {u : X → ℝ} {F : X → ℂ} {V : Set X} (hF : IsConjugate u F V) (t : ℝ) : IsConjugate u (fun (z : X) => F z + ↑t * Complex.I) V

Adding an imaginary constant preserves conjugacy.

theorem Rado.IsConjugate.mono {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {u : X → ℝ} {F : X → ℂ} {V W : Set X} (hF : IsConjugate u F V) (hWV : W ⊆ V) : IsConjugate u F W

Conjugates restrict to subsets.

theorem Rado.IsConjugate.exists_sub_const {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] {u : X → ℝ} {F G : X → ℂ} {V : Set X} (hV : IsOpen V) (hVc : IsPreconnected V) (hF : IsConjugate u F V) (hG : IsConjugate u G V) : ∃ (t : ℝ), Set.EqOn G (fun (z : X) => F z + ↑t * Complex.I) V

Rigidity: two conjugates on a preconnected open set differ by an imaginary constant.

theorem Rado.SurfaceHarmonicOn.eqOn_const_of_locallyConstant {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] {u : X → ℝ} {s : Set X} (hu : SurfaceHarmonicOn u s) (hs : IsOpen s) (hsc : IsPreconnected s) {y : X} (hy : y ∈ s) (hloc : ∀ᶠ (z : X) in nhds y, u z = u y) : Set.EqOn u (fun (x : X) => u y) s

A harmonic function that is locally constant near an accumulation of constancy cannot avoid being constant: on a preconnected open set, if u is locally constant near one point, it is constant. (Via conjugates and the identity theorem for the chart derivative.)

noncomputable def Rado.germValue {X : Type u_1} [TopologicalSpace X] {y : X} (γ : (nhds y).Germ ℂ) : ℂ

The value of a germ at the base point of its filter (well defined because every neighbourhood of y contains y).

Equations

• Rado.germValue γ = γ.liftOn (fun (f : X → ℂ) => f y) ⋯

@[simp]

theorem Rado.germValue_coe {X : Type u_1} [TopologicalSpace X] {y : X} (F : X → ℂ) : germValue ↑F = F y

theorem Rado.isOpen_eventuallyEq_nhds {X : Type u_1} [TopologicalSpace X] {F G : X → ℂ} : IsOpen {x : X | F =ᶠ[nhds x] G}

The set of points where two functions have the same germ is open.

def Rado.ConjEtale {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (u : X → ℝ) (Y : Set X) : Type u_1

The étale space of conjugate germs of u over Y: pairs of a point y ∈ Y and the germ at y of a conjugate of u defined on some open neighbourhood inside Y.

Equations

• Rado.ConjEtale u Y = { p : (y : X) × (nhds y).Germ ℂ // p.fst ∈ Y ∧ ∃ (V : Set X) (F : X → ℂ), IsOpen V ∧ p.fst ∈ V ∧ V ⊆ Y ∧ Rado.IsConjugate u F V ∧ p.snd = ↑F }

def Rado.ConjEtale.sheet {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {u : X → ℝ} {Y : Set X} (V : Set X) (F : X → ℂ) : Set (ConjEtale u Y)

The sheet of a conjugate F over V.

Equations

• Rado.ConjEtale.sheet V F = {q : Rado.ConjEtale u Y | (↑q).fst ∈ V ∧ (↑q).snd = ↑F}

def Rado.ConjEtale.basicSets {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (u : X → ℝ) (Y : Set X) : Set (Set (ConjEtale u Y))

Basic open sets: sheets of conjugates over preconnected opens inside Y.

Equations

• Rado.ConjEtale.basicSets u Y = {S : Set (Rado.ConjEtale u Y) | ∃ (V : Set X) (F : X → ℂ), IsOpen V ∧ IsPreconnected V ∧ V ⊆ Y ∧ Rado.IsConjugate u F V ∧ S = Rado.ConjEtale.sheet V F}

@[instance_reducible]

instance Rado.ConjEtale.instTopologicalSpace {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {u : X → ℝ} {Y : Set X} : TopologicalSpace (ConjEtale u Y)

Equations

• Rado.ConjEtale.instTopologicalSpace = TopologicalSpace.generateFrom (Rado.ConjEtale.basicSets u Y)

def Rado.ConjEtale.proj {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {u : X → ℝ} {Y : Set X} (q : ConjEtale u Y) : X

The projection to the surface.

Equations

• q.proj = (↑q).fst

noncomputable def Rado.ConjEtale.eval {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {u : X → ℝ} {Y : Set X} (q : ConjEtale u Y) : ℂ

The evaluation map.

Equations

• q.eval = Rado.germValue (↑q).snd

theorem Rado.ConjEtale.mem_sheet_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {u : X → ℝ} {Y V : Set X} {F : X → ℂ} {q : ConjEtale u Y} : q ∈ sheet V F ↔ (↑q).fst ∈ V ∧ (↑q).snd = ↑F

Membership in a sheet, unfolded.

theorem Rado.ConjEtale.isOpen_of_mem_basicSets {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {u : X → ℝ} {Y : Set X} {S : Set (ConjEtale u Y)} (hS : S ∈ basicSets u Y) : IsOpen S

Basic sets are open.

theorem Rado.ConjEtale.isTopologicalBasis_basicSets {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {u : X → ℝ} {Y : Set X} : TopologicalSpace.IsTopologicalBasis (basicSets u Y)

The sheets form a topological basis.

theorem Rado.ConjEtale.continuous_proj {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {u : X → ℝ} {Y : Set X} : Continuous proj

theorem Rado.ConjEtale.isOpenMap_proj {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {u : X → ℝ} {Y : Set X} : IsOpenMap proj

theorem Rado.ConjEtale.injOn_proj_sheet {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {u : X → ℝ} {Y V : Set X} {F : X → ℂ} : Set.InjOn proj (sheet V F)

proj restricted to a sheet is injective (germs of a single F).

theorem Rado.ConjEtale.t2Space {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {u : X → ℝ} {Y : Set X} [T2Space X] : T2Space (ConjEtale u Y)

Hausdorffness of the étale space (identity theorem).

theorem Rado.ConjEtale.exists_mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] {u : X → ℝ} {Y : Set X} (hu : SurfaceHarmonicOn u Y) (hY : IsOpen Y) {y : X} (hy : y ∈ Y) : ∃ (q : ConjEtale u Y), q.proj = y

Every point of Y has a conjugate germ over it.

theorem Rado.ConjEtale.locallyCompactSpace {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {u : X → ℝ} {Y : Set X} : LocallyCompactSpace (ConjEtale u Y)

The étale space inherits the local properties needed by Poincaré–Volterra: local compactness, local connectedness, local second countability.

theorem Rado.ConjEtale.locallyConnectedSpace {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {u : X → ℝ} {Y : Set X} : LocallyConnectedSpace (ConjEtale u Y)

theorem Rado.ConjEtale.locally_secondCountable {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {u : X → ℝ} {Y : Set X} (q : ConjEtale u Y) : ∃ (U : Set (ConjEtale u Y)), q ∈ U ∧ IsOpen U ∧ SecondCountableTopology ↑U

theorem Rado.ConjEtale.continuous_eval {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {u : X → ℝ} {Y : Set X} : Continuous eval

theorem Rado.ConjEtale.eval_discrete_fibers {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] {u : X → ℝ} {Y : Set X} (hu : SurfaceHarmonicOn u Y) (hY : IsOpen Y) (hYc : IsPreconnected Y) {x₀ x₁ : X} (h₀ : x₀ ∈ Y) (h₁ : x₁ ∈ Y) (hne : u x₀ ≠ u x₁) (q : ConjEtale u Y) : ∃ U ∈ nhds q, ∀ w ∈ U, w.eval = q.eval → w = q

Discreteness of the fibers of eval: if evaluation were constant near a germ, u would be locally constant near the base point, hence constant on all of connected Y (SurfaceHarmonicOn.eqOn_const_of_locallyConstant) — contradicting nonconstancy.

theorem Rado.ConjEtale.surjOn_proj_connectedComponent {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] {u : X → ℝ} {Y : Set X} (hu : SurfaceHarmonicOn u Y) (hY : IsOpen Y) (hYc : IsPreconnected Y) (q₀ : ConjEtale u Y) : Set.SurjOn proj (connectedComponent q₀) Y

Over a connected Y, every connected component of the étale space projects onto all of Y (openness and closedness of the image of a component, via local triviality of proj over small preconnected chart neighbourhoods).