Germs of local biholomorphisms

This file packages the small amount of local-coordinate infrastructure needed by the holomorphic constant-rank theorem. A LocalBiholomorphAt E F a b consists of analytic maps in both directions, carrying a to b, whose two composites agree with the identity on neighborhoods of the relevant base points.

structure LocalComplexGeometry.LocalBiholomorphAt (E : Type u_1) (F : Type u_2) [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] (a : E) (b : F) : Type (max u_1 u_2)

An analytic isomorphism between neighborhoods of a and b.

The maps are globally defined representatives. The inverse identities are germ identities, which is the appropriate local notion and avoids choosing particular open neighborhoods in the structure.

• toFun : E → F

  The forward map representing the local biholomorphism.

• invFun : F → E

  The inverse map representing the local biholomorphism.

• map_source : self.toFun a = b
• map_target : self.invFun b = a
• analyticAt_toFun : AnalyticAt ℂ self.toFun a
• analyticAt_invFun : AnalyticAt ℂ self.invFun b
• left_inv : (fun (x : E) => self.invFun (self.toFun x)) =ᶠ[nhds a] fun (x : E) => x
• right_inv : (fun (y : F) => self.toFun (self.invFun y)) =ᶠ[nhds b] fun (y : F) => y

@[simp]

theorem LocalComplexGeometry.LocalBiholomorphAt.toFun_source {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] {a : E} {b : F} (e : LocalBiholomorphAt E F a b) : e.toFun a = b

@[simp]

theorem LocalComplexGeometry.LocalBiholomorphAt.invFun_target {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] {a : E} {b : F} (e : LocalBiholomorphAt E F a b) : e.invFun b = a

theorem LocalComplexGeometry.LocalBiholomorphAt.toFun_tendsto {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] {a : E} {b : F} (e : LocalBiholomorphAt E F a b) : Filter.Tendsto e.toFun (nhds a) (nhds b)

The forward representative tends to the target base point.

theorem LocalComplexGeometry.LocalBiholomorphAt.invFun_tendsto {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] {a : E} {b : F} (e : LocalBiholomorphAt E F a b) : Filter.Tendsto e.invFun (nhds b) (nhds a)

The inverse representative tends to the source base point.

theorem LocalComplexGeometry.LocalBiholomorphAt.eventually_toFun_mem {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] {a : E} {b : F} (e : LocalBiholomorphAt E F a b) {s : Set F} (hs : s ∈ nhds b) : ∀ᶠ (x : E) in nhds a, e.toFun x ∈ s

A target neighborhood contains the forward image eventually.

theorem LocalComplexGeometry.LocalBiholomorphAt.eventually_invFun_mem {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] {a : E} {b : F} (e : LocalBiholomorphAt E F a b) {s : Set E} (hs : s ∈ nhds a) : ∀ᶠ (y : F) in nhds b, e.invFun y ∈ s

A source neighborhood contains the inverse image eventually.

theorem LocalComplexGeometry.LocalBiholomorphAt.exists_mem_nhds_injOn {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] {a : E} {b : F} (e : LocalBiholomorphAt E F a b) : ∃ s ∈ nhds a, Set.InjOn e.toFun s

The forward representative is injective on some neighborhood of its source.

theorem LocalComplexGeometry.LocalBiholomorphAt.eventually_bijective_fderiv_toFun {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] {a : E} {b : F} [CompleteSpace E] [CompleteSpace F] (e : LocalBiholomorphAt E F a b) : ∀ᶠ (x : E) in nhds a, Function.Bijective ⇑(fderiv ℂ e.toFun x)

The derivative of a local biholomorphism is eventually a linear isomorphism. The conclusion is stated as bijectivity so it does not require choosing continuous-linear equivalences at every nearby point.

def LocalComplexGeometry.LocalBiholomorphAt.refl (E : Type u_4) [NormedAddCommGroup E] [NormedSpace ℂ E] (a : E) : LocalBiholomorphAt E E a a

The identity germ is a local biholomorphism.

Equations

• One or more equations did not get rendered due to their size.

def LocalComplexGeometry.LocalBiholomorphAt.symm {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] {a : E} {b : F} (e : LocalBiholomorphAt E F a b) : LocalBiholomorphAt F E b a

Reverse a local biholomorphism.

Equations

• e.symm = { toFun := e.invFun, invFun := e.toFun, map_source := ⋯, map_target := ⋯, analyticAt_toFun := ⋯, analyticAt_invFun := ⋯, left_inv := ⋯, right_inv := ⋯ }

theorem LocalComplexGeometry.LocalBiholomorphAt.eventually_bijective_fderiv_invFun {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] {a : E} {b : F} [CompleteSpace E] [CompleteSpace F] (e : LocalBiholomorphAt E F a b) : ∀ᶠ (y : F) in nhds b, Function.Bijective ⇑(fderiv ℂ e.invFun y)

The derivative of the inverse representative is eventually bijective.

def LocalComplexGeometry.LocalBiholomorphAt.trans {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [NormedAddCommGroup G] [NormedSpace ℂ G] {a : E} {b : F} {c : G} (e : LocalBiholomorphAt E F a b) (h : LocalBiholomorphAt F G b c) : LocalBiholomorphAt E G a c

Compose two local biholomorphisms with matching middle base point.

Equations

• e.trans h = { toFun := h.toFun ∘ e.toFun, invFun := e.invFun ∘ h.invFun, map_source := ⋯, map_target := ⋯, analyticAt_toFun := ⋯, analyticAt_invFun := ⋯, left_inv := ⋯, right_inv := ⋯ }

def LocalComplexGeometry.LocalBiholomorphAt.ofContinuousLinearEquiv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] (e : E ≃L[ℂ] F) (a : E) : LocalBiholomorphAt E F a (e a)

A continuous complex-linear equivalence, based at an arbitrary point.

Equations

• One or more equations did not get rendered due to their size.

def LocalComplexGeometry.LocalBiholomorphAt.ofContinuousLinearEquivAtZero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] (e : E ≃L[ℂ] F) : LocalBiholomorphAt E F 0 0

A continuous complex-linear equivalence regarded as a biholomorphic germ at the origin in both spaces.

Equations

• One or more equations did not get rendered due to their size.

def LocalComplexGeometry.LocalBiholomorphAt.affine {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] (e : E ≃L[ℂ] F) (a : E) (b : F) : LocalBiholomorphAt E F a b

The affine biholomorphism with linear part e sending a to b.

Equations

• One or more equations did not get rendered due to their size.

def LocalComplexGeometry.LocalBiholomorphAt.translation {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (a b : E) : LocalBiholomorphAt E E a b

Translation carrying a to b.

Equations

• LocalComplexGeometry.LocalBiholomorphAt.translation a b = LocalComplexGeometry.LocalBiholomorphAt.affine (ContinuousLinearEquiv.refl ℂ E) a b

def LocalComplexGeometry.LocalBiholomorphAt.fiberShearAtZero {X : Type u_4} {Y : Type u_5} [NormedAddCommGroup X] [NormedSpace ℂ X] [NormedAddCommGroup Y] [NormedSpace ℂ Y] (h : X → Y) (hh : AnalyticAt ℂ h 0) (h0 : h 0 = 0) : LocalBiholomorphAt (X × Y) (X × Y) 0 0

A triangular analytic change of coordinates on a product, subtracting an analytic function from the second coordinate.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LocalComplexGeometry.LocalBiholomorphAt.ofAnalyticAtOfFDerivEquiv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace E] {f : E → F} {a : E} (hf : AnalyticAt ℂ f a) (e : E ≃L[ℂ] F) (he : fderiv ℂ f a = ↑e) : LocalBiholomorphAt E F a (f a)

An analytic map with an explicitly invertible derivative is locally biholomorphic.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LocalComplexGeometry.LocalBiholomorphAt.ofAnalyticAtOfBijectiveFDeriv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace E] [CompleteSpace F] {f : E → F} {a : E} (hf : AnalyticAt ℂ f a) (hbij : Function.Bijective ⇑(fderiv ℂ f a)) : LocalBiholomorphAt E F a (f a)

An analytic map with bijective derivative is locally biholomorphic.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LocalComplexGeometry.LocalBiholomorphAt.ofAnalyticAtOfBijectiveFDerivToZero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace E] [CompleteSpace F] {f : E → F} {a : E} (hf : AnalyticAt ℂ f a) (hbij : Function.Bijective ⇑(fderiv ℂ f a)) : LocalBiholomorphAt E F a 0

The normalized inverse-function-theorem chart, sending a to the origin.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LocalComplexGeometry.LocalBiholomorphAt.ofAnalyticAtOfBijectiveFDerivCentered {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace E] [CompleteSpace F] {f : E → F} {a : E} (hf : AnalyticAt ℂ f a) (hbij : Function.Bijective ⇑(fderiv ℂ f a)) : LocalBiholomorphAt E F 0 0

The fully centered inverse-function-theorem chart. Its forward representative is locally the map x ↦ f (x + a) - f a, so both marked base points are the origin.

Equations

• One or more equations did not get rendered due to their size.