Restriction and continuous extension of holomorphic maps

Restriction is a continuous linear map, injective from a connected larger domain when the smaller domain is nonempty. When it is surjective, its inverse is continuous for the compact-open topology, by the Fréchet open-mapping argument for complete metrizable topological vector spaces. Reference: [Scheidemann][Scheidemann2005] (2005), Proposition 2.1.3 and Exercise 2.1.13.

Main results

holomorphicRestrictCLM is restriction as a continuous linear map. exists_holomorphicRestrictionEquiv is a compact-open isomorphism when restriction is bijective. HolomorphicAlgebra is the scalar holomorphic algebra, with holomorphicRestrictAlgHom and holomorphicRestrictionAlgEquiv as the algebraic restriction maps. exists_holomorphicAlgebraEquiv_of_commonExtension is an algebra isomorphism from a common extension domain.

References

• [V. Scheidemann, Introduction to Complex Analysis in Several Variables][Scheidemann2005]

def SeveralComplexVariables.holomorphicRestrictCLM {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] {U V : TopologicalSpace.Opens E} (hVU : V ≤ U) : HolomorphicMap U F →L[ℂ] HolomorphicMap V F

Restriction as a continuous complex-linear operator between compact-open spaces.

Equations

• SeveralComplexVariables.holomorphicRestrictCLM hVU = { toFun := SeveralComplexVariables.holomorphicRestrict hVU, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

theorem SeveralComplexVariables.holomorphicRestrict_surjective {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] {U V : TopologicalSpace.Opens E} (hVU : V ≤ U) (hext : ∀ (f : E → F), AnalyticOnNhd ℂ f ↑V → ∃ (g : E → F), AnalyticOnNhd ℂ g ↑U ∧ Set.EqOn g f ↑V) : Function.Surjective (holomorphicRestrict hVU)

An ambient extension theorem makes restriction surjective on the bundled spaces.

theorem SeveralComplexVariables.holomorphicRestrict_injective {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] {U V : TopologicalSpace.Opens E} (hVU : V ≤ U) (hc : IsPreconnected ↑U) (hne : (↑V).Nonempty) : Function.Injective (holomorphicRestrict hVU)

On a connected larger domain, restriction to a nonempty open subset is injective.

theorem SeveralComplexVariables.holomorphicRestrict_injective_of_subset_closure {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] {U V : TopologicalSpace.Opens E} (hVU : V ≤ U) (hd : ↑U ⊆ closure ↑V) : Function.Injective (holomorphicRestrict hVU)

Restriction to a dense open subset is injective, without connectedness or nonemptiness assumptions on either domain. Continuity of the holomorphic representatives suffices.

theorem SeveralComplexVariables.exists_holomorphicRestrictionEquiv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] {U V : TopologicalSpace.Opens E} [FiniteDimensional ℂ E] [CompleteSpace F] (hVU : V ≤ U) (hc : IsPreconnected ↑U) (hne : (↑V).Nonempty) (hs : Function.Surjective (holomorphicRestrict hVU)) : ∃ (e : HolomorphicMap U F ≃L[ℂ] HolomorphicMap V F), ⇑e = holomorphicRestrict hVU

Surjective restriction is a continuous linear equivalence under the identity-theorem hypotheses, by the open-mapping theorem for complete metrizable compact-open spaces. Banach-valued targets need not be finite dimensional.

@[reducible]

def SeveralComplexVariables.holomorphicSubalgebra {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (U : TopologicalSpace.Opens E) : Subalgebra ℂ C(↥U, ℂ)

Scalar holomorphic functions form a subalgebra of continuous functions.

Equations

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

@[reducible, inline]

abbrev SeveralComplexVariables.HolomorphicAlgebra {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (U : TopologicalSpace.Opens E) : Type u_1

The scalar holomorphic algebra has the same underlying type as the holomorphic space.

Equations

• SeveralComplexVariables.HolomorphicAlgebra U = ↥(SeveralComplexVariables.holomorphicSubalgebra U)

noncomputable def SeveralComplexVariables.holomorphicRestrictAlgHom {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U V : TopologicalSpace.Opens E} (hVU : V ≤ U) : HolomorphicAlgebra U →ₐ[ℂ] HolomorphicAlgebra V

Restriction preserves multiplication and constants as well as linear operations.

Equations

• SeveralComplexVariables.holomorphicRestrictAlgHom hVU = { toFun := SeveralComplexVariables.holomorphicRestrict hVU, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem SeveralComplexVariables.holomorphicRestrictAlgHom_coe {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U V : TopologicalSpace.Opens E} (hVU : V ≤ U) : ⇑(holomorphicRestrictAlgHom hVU) = holomorphicRestrict hVU

The algebra homomorphism has the same underlying function as ordinary restriction.

noncomputable def SeveralComplexVariables.holomorphicRestrictionAlgEquiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U V : TopologicalSpace.Opens E} (hVU : V ≤ U) (hc : IsPreconnected ↑U) (hne : (↑V).Nonempty) (hs : Function.Surjective (holomorphicRestrict hVU)) : HolomorphicAlgebra U ≃ₐ[ℂ] HolomorphicAlgebra V

The algebraic restriction equivalence associated to surjectivity. Its continuity in both directions is supplied by exists_holomorphicRestrictionEquiv.

Equations

• SeveralComplexVariables.holomorphicRestrictionAlgEquiv hVU hc hne hs = AlgEquiv.ofBijective (SeveralComplexVariables.holomorphicRestrictAlgHom hVU) ⋯

theorem SeveralComplexVariables.continuous_holomorphicRestrictionAlgEquiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U V : TopologicalSpace.Opens E} [FiniteDimensional ℂ E] (hVU : V ≤ U) (hc : IsPreconnected ↑U) (hne : (↑V).Nonempty) (hs : Function.Surjective (holomorphicRestrict hVU)) : Continuous ⇑(holomorphicRestrictionAlgEquiv hVU hc hne hs) ∧ Continuous ⇑(holomorphicRestrictionAlgEquiv hVU hc hne hs).symm

The scalar algebra equivalence is continuous in both directions for the compact-open topology, using the Fréchet open-mapping theorem for inverse continuity.

theorem SeveralComplexVariables.exists_holomorphicAlgebraEquiv_of_commonExtension {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U V : TopologicalSpace.Opens E} [FiniteDimensional ℂ E] (h : IsCommonAnalyticExtension ↑V ↑U) (hc : IsPreconnected ↑U) (hne : (↑V).Nonempty) : ∃ (e : HolomorphicAlgebra U ≃ₐ[ℂ] HolomorphicAlgebra V), ⇑e = holomorphicRestrict ⋯ ∧ Continuous ⇑e ∧ Continuous ⇑e.symm

A common scalar extension pair gives an isomorphism of topological holomorphic algebras. The connected larger set and nonempty smaller set ensure uniqueness.