Complex manifolds, Dolbeault theory, and Kähler geometry

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremOsgood's lemma#

A function of finitely many complex variables which is continuous on an open set and complex differentiable in each variable separately on it is analytic on it.

ContinuousOn.analyticOnNhd_of_differentiableAt_update.{u_1, u_2} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {ι : Type u_2} [Fintype ι]
  [DecidableEq ι] {f : (ι → ℂ) → E} {s : Set (ι → ℂ)} (hc : ContinuousOn f s) (hs : IsOpen s)
  (hd : ∀ y ∈ s, ∀ (i : ι), DifferentiableAt ℂ (fun x => f (Function.update y i x)) (y i)) :
  AnalyticOnNhd ℂ f s

Lean

Formalized in Tau Ceti as ContinuousOn.analyticOnNhd_of_differentiableAt_update.

Other forms

Osgood's lemma. Formalized in Tau Ceti as ContinuousOn.analyticAt_of_differentiableAt_update.

ContinuousOn.analyticAt_of_differentiableAt_update.{u_1, u_2} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℂ E] [CompleteSpace E] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {f : (ι → ℂ) → E}
  {s : Set (ι → ℂ)} {z : ι → ℂ} (hc : ContinuousOn f s) (hs : s ∈ nhds z)
  (hd : ∀ y ∈ s, ∀ (i : ι), DifferentiableAt ℂ (fun x => f (Function.update y i x)) (y i)) :
  AnalyticAt ℂ f z

Sources

• Tau Ceti documentation: ContinuousOn.analyticOnNhd_of_differentiableAt_update
• Source of ContinuousOn.analyticOnNhd_of_differentiableAt_update in TauCeti/Analysis/Complex/CauchyIntegralPolydisc.lean
• Tau Ceti roadmap status: Complex manifolds, Dolbeault theory, and Kähler geometry

LeanContinuousOn.analyticOnNhd_of_differentiableAt_update · ContinuousOn.analyticAt_of_differentiableAt_update

Uses 1 · Used by 13

Proof usesThe Cauchy integral formula on a polydisc

Used byAnalytic Belyi pairs are classified by finite covers of the thrice-punctured sphere · The superelliptic curve is the analytic Belyi pair of the torus triple · A degree-one map is a biholomorphism · Real analytic Weierstrass preparation theorem · Complex analytic Weierstrass division theorem · Complex analytic Weierstrass preparation theorem · Identity theorem · The joint holomorphic implicit function theorem · The Riemann extension theorem across a coordinate hyperplane · A complex manifold is a real-analytic manifold · TauCeti.contDiffGroupoid_eq_of_ne_zero · TauCeti.contMDiff_iff_mdifferentiable · Weierstrass division theorem in holomorphic stalks

TheoremTauCeti.contMDiff_iff_mdifferentiable#

A map between complex manifolds is C^n, for any n ≠ 0, if and only if it is holomorphic.

TauCeti.contMDiff_iff_mdifferentiable.{u_1, u_2, u_3, u_4, u_5, u_6} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {H : Type u_2}
  [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless] {M : Type u_3}
  [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {E' : Type u_4} [NormedAddCommGroup E']
  [NormedSpace ℂ E'] [CompleteSpace E'] {H' : Type u_5} [TopologicalSpace H']
  {I' : ModelWithCorners ℂ E' H'} {M' : Type u_6} [TopologicalSpace M'] [ChartedSpace H' M']
  [IsManifold I 1 M] [IsManifold I' 1 M'] {f : M → M'} (hn : n ≠ 0) : ContMDiff I I' n f ↔ MDiff f

Lean

Formalized in Tau Ceti as TauCeti.contMDiff_iff_mdifferentiable.

Sources

• Tau Ceti documentation: TauCeti.contMDiff_iff_mdifferentiable
• Source of TauCeti.contMDiff_iff_mdifferentiable in TauCeti/Geometry/Manifold/Complex/Analytic.lean
• Tau Ceti roadmap status: Complex manifolds, Dolbeault theory, and Kähler geometry

LeanTauCeti.contMDiff_iff_mdifferentiable

Uses 1

Proof usesOsgood's lemma

TheoremA complex manifold is a real-analytic manifold#

A complex manifold modelled on 𝓘(ℂ, E), of class C^m for some m ≠ 0 with E finite-dimensional, is with the same charts a real C^n manifold modelled on 𝓘(ℝ, E) for every n; for n = ω it is real-analytic.

IsManifold.restrictScalars_of_ne_zero.{u_1, u_4} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℂ E] [FiniteDimensional ℂ E] {m : WithTop ℕ∞} (n : WithTop ℕ∞) {M : Type u_4}
  [TopologicalSpace M] [ChartedSpace E M] (hm : m ≠ 0)
  (h : IsManifold (modelWithCornersSelf ℂ E) m M) : IsManifold (modelWithCornersSelf ℝ E) n M

Lean

Formalized in Tau Ceti as IsManifold.restrictScalars_of_ne_zero.

Sources

• Tau Ceti documentation: IsManifold.restrictScalars_of_ne_zero
• Source of IsManifold.restrictScalars_of_ne_zero in TauCeti/Geometry/Manifold/Complex/Analytic.lean
• Tau Ceti roadmap status: Complex manifolds, Dolbeault theory, and Kähler geometry

LeanIsManifold.restrictScalars_of_ne_zero

Uses 1

Proof usesOsgood's lemma

TheoremTauCeti.holomorphicStructureSheaf.isFractionRing_meromorphicGerms#

The field of meromorphic germs at a : ℂ is the fraction field of the ring of holomorphic germs at a.

TauCeti.holomorphicStructureSheaf.isFractionRing_meromorphicGerms (a : ℂ) :
  IsFractionRing
    ↑((TauCeti.holomorphicStructureSheaf (modelWithCornersSelf ℂ ℂ) ℂ).presheaf.stalk a)
    ↥(TauCeti.meromorphicGerms ℂ a)

Lean

Formalized in Tau Ceti as TauCeti.holomorphicStructureSheaf.isFractionRing_meromorphicGerms.

Sources

• Tau Ceti documentation: TauCeti.holomorphicStructureSheaf.isFractionRing_meromorphicGerms
• Source of TauCeti.holomorphicStructureSheaf.isFractionRing_meromorphicGerms in TauCeti/Geometry/Manifold/Complex/StructureSheaf/MeromorphicGerm.lean
• Tau Ceti roadmap status: Complex manifolds, Dolbeault theory, and Kähler geometry

LeanTauCeti.holomorphicStructureSheaf.isFractionRing_meromorphicGerms

TheoremProjectivization.instIsManifold#

Projective space over a nontrivially normed field, with its standard affine charts, is a C^r manifold for every r; for r = ω it is an analytic manifold. Over ℂ this is the standard complex manifold structure on ℂℙⁿ.

Projectivization.instIsManifold.{u_1} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ}
  (r : WithTop ℕ∞) :
  IsManifold (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) r (Projectivization 𝕜 (Fin (n + 1) → 𝕜))

Lean

Formalized in Tau Ceti as Projectivization.instIsManifold.

Sources

• Tau Ceti documentation: Projectivization.instIsManifold
• Source of Projectivization.instIsManifold in TauCeti/Geometry/Manifold/Instances/Projectivization.lean
• Tau Ceti roadmap status: Complex manifolds, Dolbeault theory, and Kähler geometry

LeanProjectivization.instIsManifold

InstanceTauCeti.SmoothForm.instModule#

Scalars acting on the coefficients act on smooth forms, making them a module. For complex coefficients this is the complex vector space of complex-valued smooth forms.

TauCeti.SmoothForm.instModule.{u_1, u_2, u_3, u_7, u_10} {E : Type u_1} {H : Type u_2}
  {M : Type u_3} {F : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H]
  [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [NormedAddCommGroup F]
  [NormedSpace ℝ F] {k : ℕ} [IsManifold I 1 M] {S : Type u_10} [Semiring S] [_root_.Module S F]
  [ContinuousConstSMul S F] [SMulCommClass ℝ S F] : _root_.Module S (TauCeti.SmoothForm I M F k)

Lean

Formalized in Tau Ceti as TauCeti.SmoothForm.instModule.

Sources

• Tau Ceti documentation: TauCeti.SmoothForm.instModule
• Source of TauCeti.SmoothForm.instModule in TauCeti/Geometry/Manifold/DifferentialForm/MapCoeff.lean
• Tau Ceti roadmap status: Complex manifolds, Dolbeault theory, and Kähler geometry

LeanTauCeti.SmoothForm.instModule

Used by 1

Used byThe Jacobi identity for the Jacobi bracket

TheoremTauCeti.contDiffGroupoid_eq_of_ne_zero#

For a boundaryless model on a finite-dimensional complex space, the C^m and C^n groupoids agree whenever m and n are nonzero.

TauCeti.contDiffGroupoid_eq_of_ne_zero.{u_1, u_2} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℂ E] [FiniteDimensional ℂ E] {H : Type u_2} [TopologicalSpace H]
  {I : ModelWithCorners ℂ E H} [I.Boundaryless] {m n : WithTop ℕ∞} (hm : m ≠ 0) (hn : n ≠ 0) :
  contDiffGroupoid m I = contDiffGroupoid n I

Lean

Formalized in Tau Ceti as TauCeti.contDiffGroupoid_eq_of_ne_zero.

Sources

• Tau Ceti documentation: TauCeti.contDiffGroupoid_eq_of_ne_zero
• Source of TauCeti.contDiffGroupoid_eq_of_ne_zero in TauCeti/Geometry/Manifold/Complex/Analytic.lean
• Tau Ceti roadmap status: Complex manifolds, Dolbeault theory, and Kähler geometry

LeanTauCeti.contDiffGroupoid_eq_of_ne_zero

Uses 1

Proof usesOsgood's lemma

TheoremThe Cauchy integral formula on a polydisc#

If f is complex differentiable on the closed polydisc with center c and polyradius R, then for every w in the open polydisc, the integral of (∏ i, (z i - w i))⁻¹ • f z over the distinguished boundary T(c, R) is (2πi)ⁿ • f w.

DifferentiableOn.torusIntegral_prod_sub_inv_smul.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℂ E] {n : ℕ} [CompleteSpace E] {f : (Fin n → ℂ) → E} {c w : Fin n → ℂ}
  {R : Fin n → ℝ} (hd : DifferentiableOn ℂ f (Set.univ.pi fun i => Metric.closedBall (c i) (R i)))
  (hw : w ∈ Set.univ.pi fun i => Metric.ball (c i) (R i)) :
  (∯ (z : Fin n → ℂ) in T(c, R), (∏ i, (z i - w i))⁻¹ • f z) = (2 * ↑Real.pi * Complex.I) ^ n • f w

Lean

Formalized in Tau Ceti as DifferentiableOn.torusIntegral_prod_sub_inv_smul.

Other forms

The Cauchy integral formula on a polydisc, for separately holomorphic functions. Formalized in Tau Ceti as ContinuousOn.torusIntegral_prod_sub_inv_smul.

ContinuousOn.torusIntegral_prod_sub_inv_smul.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℂ E] {n : ℕ} [CompleteSpace E] {f : (Fin n → ℂ) → E} {c w : Fin n → ℂ}
  {R : Fin n → ℝ} (hc : ContinuousOn f (Set.univ.pi fun i => Metric.closedBall (c i) (R i)))
  (hd :
    ∀ z ∈ Set.univ.pi fun i => Metric.closedBall (c i) (R i),
      ∀ (i : Fin n),
        z i ∈ Metric.ball (c i) (R i) →
          DifferentiableAt ℂ (fun x => f (Function.update z i x)) (z i))
  (hw : w ∈ Set.univ.pi fun i => Metric.ball (c i) (R i)) :
  (∯ (z : Fin n → ℂ) in T(c, R), (∏ i, (z i - w i))⁻¹ • f z) = (2 * ↑Real.pi * Complex.I) ^ n • f w

Sources

• Tau Ceti documentation: DifferentiableOn.torusIntegral_prod_sub_inv_smul
• Source of DifferentiableOn.torusIntegral_prod_sub_inv_smul in TauCeti/Analysis/Complex/CauchyIntegralPolydisc.lean

LeanDifferentiableOn.torusIntegral_prod_sub_inv_smul · ContinuousOn.torusIntegral_prod_sub_inv_smul

Used by 1

Used byOsgood's lemma

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.