Holomorphic germs as germs of functions

An element of the stalk at x of the holomorphic structure sheaf is represented by a holomorphic function on some open neighbourhood of x. Forgetting everything but its values near x gives a germ of functions in Mathlib's sense, along 𝓝 x or along any finer filter, for instance the punctured neighbourhood filter 𝓝[≠] x. This file constructs that comparison as a ring homomorphism TauCeti.holomorphicStructureSheaf.toFilterGerm I X x l hl and proves:

• toFilterGerm_germ: the germ of a section is the germ of any function agreeing with it on the domain of the section;
• toFilterGerm_nhds_injective: a holomorphic germ is determined by its germ along 𝓝 x; in particular it vanishes exactly when a representative vanishes near x (eq_zero_iff_of_toFilterGerm_eq);
• toFilterGerm_ringEquivCast: transporting a germ along an equality of points with RingEquiv.cast keeps its representative;
• toFilterGerm_nhdsNE_injective: when x is not isolated, it is even determined by its germ along the punctured neighbourhoods 𝓝[≠] x, by continuity;
• exists_toFilterGerm_nhds_eq_iff: the image of the comparison along 𝓝 x consists of the germs of the functions which are complex analytic (ContMDiffAt at order ω) near x (and on a complex normed space, exists_analyticAt_toFilterGerm_eq, exists_toFilterGerm_eq_of_analyticAt, and exists_toFilterGerm_nhds_eq_iff_analyticAt express this directly via AnalyticAt);
• eval_eq_of_toFilterGerm_eq: the value of a holomorphic germ is the value of any function with the same germ;
• toFilterGerm_stalkPrecomp: pulling a holomorphic germ back along a complex analytic map f is composition of germs with f;
• quotientMk_comp_stalkPrecomp_bijective: if an ideal of germs at p on a normed space consists of the germs vanishing along a local holomorphic section σ of a holomorphic map π, then pulling back along π identifies the germs at π p with the quotient by that ideal. This computes local rings of analytic subsets that are locally graphs. The inverse is composition with σ (toFilterGerm_eq_comp_of_quotientMk_stalkPrecomp_eq).

The holomorphic germ of a globally analytic function is germOfContMDiff.

This is the bridge between the categorical stalk and concrete function germs, used to compare holomorphic germs with meromorphic germs on punctured neighbourhoods.

noncomputable def TauCeti.holomorphicStructureSheaf.toFilterGerm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℂ E H) (X : Type) [TopologicalSpace X] [ChartedSpace H X] (x : X) (l : Filter X) (hl : l ≤ nhds x) : ↑((holomorphicStructureSheaf I X).presheaf.stalk x) →+* l.Germ ℂ

The comparison of holomorphic germs at x with germs of functions along a filter l finer than 𝓝 x: the germ of a section is the germ along l of any function agreeing with the section on its domain (toFilterGerm_germ).

theorem TauCeti.holomorphicStructureSheaf.toFilterGerm_germ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {x : X} {l : Filter X} (hl : l ≤ nhds x) {U : TopologicalSpace.Opens X} (hx : x ∈ U) (f : ↑((holomorphicStructureSheaf I X).obj.obj (Opposite.op U))) (g : X → ℂ) (hfg : ∀ (y : ↥U), toFun I X (Opposite.op U) f y = g ↑y) : (toFilterGerm I X x l hl) ((CategoryTheory.ConcreteCategory.hom ((holomorphicStructureSheaf I X).presheaf.germ U x hx)) f) = ↑g

The germ of a section is the germ of any function agreeing with the section on its domain.

noncomputable def TauCeti.holomorphicStructureSheaf.germOfContMDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] (f : X → ℂ) (hf : ContMDiff I (modelWithCornersSelf ℂ ℂ) ⊤ f) (x : X) : ↑((holomorphicStructureSheaf I X).presheaf.stalk x)

The holomorphic germ at x of a function which is complex analytic on all of X.

@[simp]

theorem TauCeti.holomorphicStructureSheaf.toFilterGerm_germOfContMDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] (f : X → ℂ) (hf : ContMDiff I (modelWithCornersSelf ℂ ℂ) ⊤ f) {x : X} {l : Filter X} (hl : l ≤ nhds x) : (toFilterGerm I X x l hl) (germOfContMDiff f hf x) = ↑f

The holomorphic germ of a globally analytic function f is the germ of f.

theorem TauCeti.holomorphicStructureSheaf.exists_toFilterGerm_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] (x : X) (s : ↑((holomorphicStructureSheaf I X).presheaf.stalk x)) : ∃ (f : X → ℂ), (∀ᶠ (y : X) in nhds x, ContMDiffAt I (modelWithCornersSelf ℂ ℂ) ⊤ f y) ∧ ∀ (l : Filter X) (hl : l ≤ nhds x), (toFilterGerm I X x l hl) s = ↑f

Every holomorphic germ at x is represented by a function which is complex analytic near x, simultaneously along every filter finer than 𝓝 x.

theorem TauCeti.holomorphicStructureSheaf.exists_toFilterGerm_eq_of_eventually_contMDiffAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {x : X} {f : X → ℂ} (hf : ∀ᶠ (y : X) in nhds x, ContMDiffAt I (modelWithCornersSelf ℂ ℂ) ⊤ f y) : ∃ (s : ↑((holomorphicStructureSheaf I X).presheaf.stalk x)), ∀ (l : Filter X) (hl : l ≤ nhds x), (toFilterGerm I X x l hl) s = ↑f

A function which is complex analytic near x has a holomorphic germ at x, with the same germ as the function along every filter finer than 𝓝 x.

theorem TauCeti.holomorphicStructureSheaf.exists_toFilterGerm_eq_analyticAt (a : ℂ) (s : ↑((holomorphicStructureSheaf (modelWithCornersSelf ℂ ℂ) ℂ).presheaf.stalk a)) : ∃ (f : ℂ → ℂ), AnalyticAt ℂ f a ∧ ∀ (l : Filter ℂ) (hl : l ≤ nhds a), (toFilterGerm (modelWithCornersSelf ℂ ℂ) ℂ a l hl) s = ↑f

Every holomorphic germ on the complex line has an analytic representative, simultaneously along every filter finer than the neighbourhood filter.

theorem TauCeti.holomorphicStructureSheaf.eventually_contMDiffAt_of_analyticAt {f : ℂ → ℂ} {a : ℂ} (hf : AnalyticAt ℂ f a) : ∀ᶠ (z : ℂ) in nhds a, ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f z

A function analytic at a point of the complex line is manifold analytic near that point.

theorem TauCeti.holomorphicStructureSheaf.toFilterGerm_nhds_injective {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] (x : X) : Function.Injective ⇑(toFilterGerm I X x (nhds x) ⋯)

A holomorphic germ is determined by its germ along 𝓝 x.

theorem TauCeti.holomorphicStructureSheaf.eq_zero_iff_of_toFilterGerm_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {x : X} {s : ↑((holomorphicStructureSheaf I X).presheaf.stalk x)} {f : X → ℂ} (h : (toFilterGerm I X x (nhds x) ⋯) s = ↑f) : s = 0 ↔ f =ᶠ[nhds x] 0

A holomorphic germ vanishes exactly when a function with the same germ along 𝓝 x vanishes near x.

theorem TauCeti.holomorphicStructureSheaf.toFilterGerm_ringEquivCast {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {x y : X} (h : x = y) {s : ↑((holomorphicStructureSheaf I X).presheaf.stalk x)} {f : X → ℂ} (hs : (toFilterGerm I X x (nhds x) ⋯) s = ↑f) : (toFilterGerm I X y (nhds y) ⋯) ((RingEquiv.cast h) s) = ↑f

Transporting a holomorphic germ along an equality of points x = y with RingEquiv.cast keeps its representative. This lets coordinate changes that fix a point only propositionally compare germs at the two descriptions of the point.

theorem TauCeti.holomorphicStructureSheaf.toFilterGerm_nhdsNE_injective {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] (x : X) [(nhdsWithin x {x}ᶜ).NeBot] : Function.Injective ⇑(toFilterGerm I X x (nhdsWithin x {x}ᶜ) ⋯)

At a point which is not isolated, a holomorphic germ is determined by its germ on the punctured neighbourhoods of the point, by continuity.

theorem TauCeti.holomorphicStructureSheaf.exists_toFilterGerm_nhds_eq_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {x : X} {f : X → ℂ} : (∃ (s : ↑((holomorphicStructureSheaf I X).presheaf.stalk x)), (toFilterGerm I X x (nhds x) ⋯) s = ↑f) ↔ ∀ᶠ (y : X) in nhds x, ContMDiffAt I (modelWithCornersSelf ℂ ℂ) ⊤ f y

A function has a holomorphic germ at x with the same germ along 𝓝 x exactly when it is complex analytic near x.

theorem TauCeti.holomorphicStructureSheaf.eval_eq_of_toFilterGerm_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {x : X} {s : ↑((holomorphicStructureSheaf I X).presheaf.stalk x)} {f : X → ℂ} (h : (toFilterGerm I X x (nhds x) ⋯) s = ↑f) : (eval I X x) s = f x

The value of a holomorphic germ is the value at the base point of any function with the same germ along 𝓝 x.

@[simp]

theorem TauCeti.holomorphicStructureSheaf.eval_germOfContMDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] (f : X → ℂ) (hf : ContMDiff I (modelWithCornersSelf ℂ ℂ) ⊤ f) (x : X) : (eval I X x) (germOfContMDiff f hf x) = f x

The value of the holomorphic germ of a globally analytic function f at x is f x.

theorem TauCeti.holomorphicStructureSheaf.toFilterGerm_stalkPrecomp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ℂ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners ℂ E' H'} {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] (f : X → Y) (hf : ContMDiff I J ⊤ f) (x : X) (s : ↑((holomorphicStructureSheaf J Y).presheaf.stalk (f x))) : (toFilterGerm I X x (nhds x) ⋯) ((stalkPrecomp I X f hf x) s) = ((toFilterGerm J Y (f x) (nhds (f x)) ⋯) s).compTendsto f ⋯

The germ of the pullback of a holomorphic germ along a complex analytic map f is the composition with f of the germ.

@[simp]

theorem TauCeti.holomorphicStructureSheaf.stalkPrecomp_germOfContMDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} {X : Type} [TopologicalSpace X] [ChartedSpace H X] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ℂ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners ℂ E' H'} {Y : Type} [TopologicalSpace Y] [ChartedSpace H' Y] (f : X → Y) (hf : ContMDiff I J ⊤ f) (g : Y → ℂ) (hg : ContMDiff J (modelWithCornersSelf ℂ ℂ) ⊤ g) (x : X) : (stalkPrecomp I X f hf x) (germOfContMDiff g hg (f x)) = germOfContMDiff (g ∘ f) ⋯ x

Pulling back the holomorphic germ of a globally analytic function g along a complex analytic map f gives the holomorphic germ of g ∘ f.

theorem TauCeti.holomorphicStructureSheaf.exists_analyticAt_toFilterGerm_eq {V : Type} [NormedAddCommGroup V] [NormedSpace ℂ V] (p : V) (s : ↑((holomorphicStructureSheaf (modelWithCornersSelf ℂ V) V).presheaf.stalk p)) : ∃ (φ : V → ℂ), AnalyticAt ℂ φ p ∧ ∀ (l : Filter V) (hl : l ≤ nhds p), (toFilterGerm (modelWithCornersSelf ℂ V) V p l hl) s = ↑φ

On a complex normed space, every holomorphic germ at p is represented by a function analytic at p, simultaneously along every filter finer than 𝓝 p.

theorem TauCeti.holomorphicStructureSheaf.exists_toFilterGerm_eq_of_analyticAt {V : Type} [NormedAddCommGroup V] [NormedSpace ℂ V] {p : V} {φ : V → ℂ} (hφ : AnalyticAt ℂ φ p) : ∃ (s : ↑((holomorphicStructureSheaf (modelWithCornersSelf ℂ V) V).presheaf.stalk p)), ∀ (l : Filter V) (hl : l ≤ nhds p), (toFilterGerm (modelWithCornersSelf ℂ V) V p l hl) s = ↑φ

On a complex normed space, a function analytic at p has a holomorphic germ at p, with the same germ along every filter finer than 𝓝 p.

theorem TauCeti.holomorphicStructureSheaf.exists_toFilterGerm_nhds_eq_iff_analyticAt {V : Type} [NormedAddCommGroup V] [NormedSpace ℂ V] {p : V} {φ : V → ℂ} : (∃ (s : ↑((holomorphicStructureSheaf (modelWithCornersSelf ℂ V) V).presheaf.stalk p)), (toFilterGerm (modelWithCornersSelf ℂ V) V p (nhds p) ⋯) s = ↑φ) ↔ AnalyticAt ℂ φ p

On a complex normed space, a function has a holomorphic germ at p with the same germ along 𝓝 p exactly when it is analytic at p.

Germs along a holomorphic section

theorem TauCeti.holomorphicStructureSheaf.toFilterGerm_eq_comp_of_quotientMk_stalkPrecomp_eq {V W : Type} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] {π : V → W} (hπ : ContMDiff (modelWithCornersSelf ℂ V) (modelWithCornersSelf ℂ W) ⊤ π) {σ : W → V} {p : V} (hπσ : ∀ᶠ (w : W) in nhds (π p), π (σ w) = w) (J : Ideal ↑((holomorphicStructureSheaf (modelWithCornersSelf ℂ V) V).presheaf.stalk p)) (hJ : ∀ (g : ↑((holomorphicStructureSheaf (modelWithCornersSelf ℂ V) V).presheaf.stalk p)) (G : V → ℂ), (toFilterGerm (modelWithCornersSelf ℂ V) V p (nhds p) ⋯) g = ↑G → (g ∈ J ↔ ∀ᶠ (w : W) in nhds (π p), G (σ w) = 0)) {h : ↑((holomorphicStructureSheaf (modelWithCornersSelf ℂ W) W).presheaf.stalk (π p))} {g : ↑((holomorphicStructureSheaf (modelWithCornersSelf ℂ V) V).presheaf.stalk p)} {G : V → ℂ} (hgG : (toFilterGerm (modelWithCornersSelf ℂ V) V p (nhds p) ⋯) g = ↑G) (hhg : (Ideal.Quotient.mk J) ((stalkPrecomp (modelWithCornersSelf ℂ V) V π hπ p) h) = (Ideal.Quotient.mk J) g) : (toFilterGerm (modelWithCornersSelf ℂ W) W (π p) (nhds (π p)) ⋯) h = ↑(G ∘ σ)

Inverting pullback along a holomorphic section. Let σ be a local section of π : V → W near π p, and J an ideal of the holomorphic germs at p consisting exactly of the germs vanishing along σ. If the pullback along π of a germ h at π p agrees modulo J with a germ represented by G, then h is represented by G ∘ σ.

theorem TauCeti.holomorphicStructureSheaf.quotientMk_comp_stalkPrecomp_bijective {V W : Type} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] {π : V → W} (hπ : ContMDiff (modelWithCornersSelf ℂ V) (modelWithCornersSelf ℂ W) ⊤ π) {σ : W → V} {p : V} (hσ : ContDiffAt ℂ ⊤ σ (π p)) (hπσ : ∀ᶠ (w : W) in nhds (π p), π (σ w) = w) (J : Ideal ↑((holomorphicStructureSheaf (modelWithCornersSelf ℂ V) V).presheaf.stalk p)) (hJ : ∀ (g : ↑((holomorphicStructureSheaf (modelWithCornersSelf ℂ V) V).presheaf.stalk p)) (G : V → ℂ), (toFilterGerm (modelWithCornersSelf ℂ V) V p (nhds p) ⋯) g = ↑G → (g ∈ J ↔ ∀ᶠ (w : W) in nhds (π p), G (σ w) = 0)) : Function.Bijective ⇑((Ideal.Quotient.mk J).comp (stalkPrecomp (modelWithCornersSelf ℂ V) V π hπ p))

Germs on the image of a holomorphic section. Let π : V → W be holomorphic and σ a local holomorphic section of π near π p. If an ideal J of the holomorphic germs at p consists exactly of the germs vanishing along σ, then pulling back along π identifies the holomorphic germs at π p with the germs at p modulo J.