Identity and open mapping theorems for holomorphic maps

TheoremHolomorphic maps on a connected manifold that agree on a nonempty open set are equal#✓fully proved

Let \(M\) be a connected complex manifold without boundary, modeled on a complex normed space with complex \(C^1\) (that is, holomorphic) transition maps, and let \(F\) be a complex normed space. If two holomorphic (everywhere complex differentiable) maps \(f, g : M \to F\) agree on a nonempty open subset \(U \subseteq M\), then \(f = g\).

theorem eq_of_eqOn_of_isOpen
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
    {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F]
    {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless]
    {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [ConnectedSpace M]
    {f g : M → F} (hf : MDiff f) (hg : MDiff g)
    {U : Set M} (hU_open : IsOpen U) (hU_nonempty : U.Nonempty) (h_eq : EqOn f g U) :
    f = g

Used by 1

Used byIdentity theorem for holomorphic maps

TheoremIdentity theorem for holomorphic maps#✓fully proved

Let \(M\) be a connected complex manifold without boundary, modeled on a complex normed space with complex \(C^1\) (that is, holomorphic) transition maps, and let \(F\) be a complex normed space. If two holomorphic (everywhere complex differentiable) maps \(f, g : M \to F\) agree on a nonempty open subset \(U \subseteq M\), then \(f = g\).

theorem holomorphic_identity_on_connected_complex_manifold
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
    {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F]
    {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless]
    {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [ConnectedSpace M]
    {f g : M → F} (hf : MDiff f) (hg : MDiff g)
    {U : Set M} (hU_open : IsOpen U) (hU_nonempty : U.Nonempty) (h_eq : EqOn f g U) :
    f = g

Sources

O. Forster, Lectures on Riemann Surfaces, identity theorem for holomorphic maps; Lean states connected-complex-manifold vector-valued form. It is MDifferentiable.eq_of_eqOn_of_isOpen, kept under the source's name.

Uses 1

Proof usesHolomorphic maps on a connected manifold that agree on a nonempty open set are equal

TheoremOpen mapping theorem for one-dimensional complex manifolds#✓fully proved

Let \(M\) and \(N\) be complex manifolds without boundary modeled on complex normed spaces of dimension one, with complex \(C^1\) (that is, holomorphic) transition maps, and suppose \(M\) is connected. Then every holomorphic (everywhere complex differentiable) map \(f : M \to N\) that is not constant is an open map.

theorem isOpenMap_of_finrank_eq_one
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E]
    {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] [FiniteDimensional ℂ F]
    {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless]
    {G : Type*} [TopologicalSpace G] {J : ModelWithCorners ℂ F G} [J.Boundaryless]
    {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [ConnectedSpace M]
    {N : Type*} [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N]
    (hE : Module.finrank ℂ E = 1) (hF : Module.finrank ℂ F = 1)
    {f : M → N} (hf : MDiff f) (hf_nonconst : ∃ x y : M, f x ≠ f y) :
    IsOpenMap f

Used by 1

Used byOpen mapping theorem for Riemann surfaces

TheoremOpen mapping theorem for Riemann surfaces#✓fully proved

Let \(M\) and \(N\) be complex manifolds without boundary modeled on complex normed spaces of dimension one, with complex \(C^1\) (that is, holomorphic) transition maps, and suppose \(M\) is connected. Then every holomorphic (everywhere complex differentiable) map \(f : M \to N\) that is not constant is an open map.

theorem holomorphic_open_mapping_one_dim
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E]
    {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] [FiniteDimensional ℂ F]
    {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless]
    {G : Type*} [TopologicalSpace G] {J : ModelWithCorners ℂ F G} [J.Boundaryless]
    {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [ConnectedSpace M]
    {N : Type*} [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N]
    (hE : Module.finrank ℂ E = 1) (hF : Module.finrank ℂ F = 1)
    {f : M → N} (hf : MDiff f) (hf_nonconst : ∃ x y : M, f x ≠ f y) :
    IsOpenMap f

Sources

O. Forster, Lectures on Riemann Surfaces, open mapping theorem for Riemann surfaces; Lean states one-complex-dimensional specialization. It is MDifferentiable.isOpenMap_of_finrank_eq_one, kept under the source's name.

Uses 1

Proof usesOpen mapping theorem for one-dimensional complex manifolds

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.