The punctured unit disc as a complex manifold

The inclusion of the punctured unit disc into the complex plane is an open embedding. Its single chart gives the complex manifold structure used by punctured-disc coordinates.

theorem TauCeti.Complex.UnitDisc.isOpenEmbedding_coe_punctured : Topology.IsOpenEmbedding fun (q : { q : Complex.UnitDisc // q ≠ 0 }) => ↑↑q

The punctured unit disc is an open subset of the complex plane.

theorem TauCeti.Complex.UnitDisc.exists_coe_punctured_eq {q : ℂ} (hq : q ≠ 0) (hq1 : ‖q‖ < 1) : ∃ (q' : { q : Complex.UnitDisc // q ≠ 0 }), ↑↑q' = q

Every nonzero point of the open unit disc is a point of the punctured unit disc.

instance TauCeti.Complex.UnitDisc.instNonemptyPunctured : Nonempty { q : Complex.UnitDisc // q ≠ 0 }

The unit disc has a point other than its origin.

@[instance_reducible]

noncomputable instance TauCeti.Complex.UnitDisc.instChartedSpacePunctured : ChartedSpace ℂ { q : Complex.UnitDisc // q ≠ 0 }

The complex inclusion is the single chart of the punctured unit disc.

Equations

• TauCeti.Complex.UnitDisc.instChartedSpacePunctured = TauCeti.Complex.UnitDisc.isOpenEmbedding_coe_punctured.singletonChartedSpace

instance TauCeti.Complex.UnitDisc.instIsManifoldPunctured : IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ { q : Complex.UnitDisc // q ≠ 0 }

The punctured unit disc is a complex analytic manifold.

theorem TauCeti.Complex.UnitDisc.extChartAt_coe_punctured (q : { q : Complex.UnitDisc // q ≠ 0 }) : ↑(extChartAt (modelWithCornersSelf ℂ ℂ) q) = fun (p : { q : Complex.UnitDisc // q ≠ 0 }) => ↑↑p

The extended chart of the punctured unit disc is its inclusion into the complex plane.

theorem TauCeti.Complex.UnitDisc.mdifferentiable_coe_punctured : MDiff fun (q : { q : Complex.UnitDisc // q ≠ 0 }) => ↑↑q

The inclusion of the punctured unit disc into the complex plane is holomorphic.