Kähler potentials: dd^c forms are closed, and the Fubini–Study chart form

Category: 1-Mathlib-staging (CSD-free; differential forms on normed spaces).

KahlerClosed.lean proved dω = 0 for the constant fundamental form — the flat statement, where closedness is immediate because the form does not vary. This module takes the next step of the A4/KG-1 narrowing (specs/mathlib-gaps-plan.md MG-4): the non-constant form built from a Kähler potential, and in particular the genuine Fubini–Study form of an affine chart, whose potential is log (1 + ‖z‖²).

The route is exactness rather than computation. Mathlib's pin carries d² = 0 (extDeriv_extDeriv), so a form presented as d of something is closed for free. The dd^c construction does exactly that:

• dForm K — the 1-form dK, packaged through ofSubsingletonLIE; dForm_eq_extDeriv checks it really is the exterior derivative of the 0-form K (extDeriv_constOfIsEmpty), so the packaging is not ad hoc.
• dcForm K — the twisted differential d^c K, i.e. (d^cK)_x v = (dK)_x (Jv), using the complex structure J u = i • u bundled as a real-linear map (complexStructureL).
• ddcForm K := extDeriv (dcForm K) — the dd^c 2-form of the potential.
• ★ extDeriv_ddcForm — dd^c K is closed for every smooth potential K.
• fsPotential z = log (1 + ‖z‖²), contDiff_fsPotential — the Fubini–Study chart potential is smooth (1 + ‖z‖² ≥ 1 > 0, so the logarithm never meets its singularity).
• ★★ extDeriv_fsChartForm — the Fubini–Study chart form is closed.

⚠️ Honest scope — read before citing

• The chart form is DEFINED by its potential, fsChartForm := ddcForm fsPotential. That is the standard potential-theoretic definition of the Fubini–Study form on an affine chart (up to the usual normalisation constant, which closedness does not see). ★ The identification is now proved (2026-09-01, fsChartForm_apply): the second-derivative computation on log (1 + ‖z‖²) is carried out, giving the components in terms of Kahler.metric and Kahler.fundamentalForm, and at the chart origin fsChartForm 0 = (-4 : ℝ) • fundamentalFormAlt (fsChartForm_zero) — the literal identification with the constant fundamental form.
• Still the chart, not the quotient. Everything lives on the flat model E; forms on the manifold ℂℙ^{N-1} remain outside Mathlib's API (its own DifferentialForm/Basic.lean TODO). The Q8/KG-1 gap is now narrowed to the quotient/manifold glue alone, the identification above having landed; the top-power volume identity is untouched (KahlerVolumeForced.lean forces the volume independently), and it is the one that would need a wedge API.
• No wedge-product API exists upstream, which is why the coordinate route (ω = i∂∂̄K expanded in a basis) is not taken; there are no ∂/∂̄ operators in Mathlib either.

References

KahlerClosed.lean (the constant/flat case this extends), KahlerForm.lean (complexStructure, fundamentalForm), MATHLIB-GAPS.md (the Kähler-manifold row this narrows), specs/mathlib-gaps-plan.md (MG-4).

The complex structure as a real-linear continuous map

noncomputable def Kahler.complexStructureL {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] : E →L[ℝ] E

The complex structure J, bundled: multiplication by i, as a continuous ℝ-linear map. The bundled companion of Kahler.complexStructure.

Equations

• Kahler.complexStructureL = ContinuousLinearMap.restrictScalars ℝ (Complex.I • ContinuousLinearMap.id ℂ E)

@[simp]

theorem Kahler.complexStructureL_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (u : E) : complexStructureL u = Complex.I • u

theorem Kahler.complexStructureL_eq_complexStructure {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (u : E) : complexStructureL u = complexStructure u

d, d^c and dd^c of a potential

noncomputable def Kahler.packL {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] : (E →L[ℝ] ℝ) →L[ℝ] E [⋀^Fin 1]→L[ℝ] ℝ

The packaging of a functional as a continuous alternating 1-form, bundled as a continuous linear map (the vehicle for transporting smoothness).

Equations

• Kahler.packL = ↑↑(ContinuousAlternatingMap.ofSubsingletonLIE 0)

@[simp]

theorem Kahler.packL_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (f : E →L[ℝ] ℝ) (v : Fin 1 → E) : (packL f) v = f (v 0)

noncomputable def Kahler.dForm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (K : E → ℝ) : E → E [⋀^Fin 1]→L[ℝ] ℝ

The 1-form dK of a real potential, packaged as a continuous alternating 1-form.

Equations

• Kahler.dForm K x = Kahler.packL (fderiv ℝ K x)

theorem Kahler.dForm_eq_extDeriv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (K : E → ℝ) (x : E) : dForm K x = extDeriv (fun (y : E) => ContinuousAlternatingMap.constOfIsEmpty ℝ E (Fin 0) (K y)) x

The packaging is honest: dForm K is the exterior derivative of the 0-form K.

noncomputable def Kahler.dcForm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (K : E → ℝ) : E → E [⋀^Fin 1]→L[ℝ] ℝ

The twisted differential d^c K: (d^cK)_x v = (dK)_x (J v), the 1-form obtained by precomposing dK with the complex structure.

Equations

• Kahler.dcForm K x = Kahler.packL (fderiv ℝ K x ∘SL Kahler.complexStructureL)

@[simp]

theorem Kahler.dcForm_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (K : E → ℝ) (x : E) (v : Fin 1 → E) : (dcForm K x) v = (fderiv ℝ K x) (Complex.I • v 0)

noncomputable def Kahler.ddcForm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (K : E → ℝ) : E → E [⋀^Fin 2]→L[ℝ] ℝ

The dd^c two-form of a potential.

Equations

• Kahler.ddcForm K = extDeriv (Kahler.dcForm K)

Smoothness, and ★ closedness

noncomputable def Kahler.compJL {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] : (E →L[ℝ] ℝ) →L[ℝ] E →L[ℝ] ℝ

Precomposition with the complex structure, as a continuous linear map on 1-forms' underlying functionals — the vehicle for transporting smoothness through d^c.

Equations

• Kahler.compJL = (ContinuousLinearMap.compL ℝ E E ℝ).flip Kahler.complexStructureL

@[simp]

theorem Kahler.compJL_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (f : E →L[ℝ] ℝ) : compJL f = f ∘SL complexStructureL

theorem Kahler.contDiff_dcForm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {K : E → ℝ} (hK : ContDiff ℝ (↑⊤) K) : ContDiff ℝ (↑⊤) (dcForm K)

d^c K is smooth when K is: the derivative of a smooth map is smooth, and both the precomposition with J and the alternating-form packaging are continuous linear.

theorem Kahler.extDeriv_ddcForm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {K : E → ℝ} (hK : ContDiff ℝ (↑⊤) K) : extDeriv (ddcForm K) = 0

★ The dd^c form of any smooth potential is closed. Immediate from d² = 0 once the form is presented as an exterior derivative — which is what the dd^c construction does.

The Fubini–Study chart potential

noncomputable def Kahler.fsPotential {E : Type u_1} [NormedAddCommGroup E] (z : E) : ℝ

The Fubini–Study Kähler potential of an affine chart: K z = log (1 + ‖z‖²).

Equations

• Kahler.fsPotential z = Real.log (1 + ‖z‖ ^ 2)

theorem Kahler.contDiff_fsPotential {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] : ContDiff ℝ (↑⊤) fsPotential

The Fubini–Study potential is smooth: 1 + ‖z‖² ≥ 1, so the logarithm stays away from its singularity, and ‖·‖² is smooth on an inner-product space.

noncomputable def Kahler.fsChartForm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] : E → E [⋀^Fin 2]→L[ℝ] ℝ

The Fubini–Study form of an affine chart, defined by its potential.

Equations

• Kahler.fsChartForm = Kahler.ddcForm Kahler.fsPotential

theorem Kahler.extDeriv_fsChartForm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] : extDeriv fsChartForm = 0

★★ The Fubini–Study chart form is closed: dω = 0 for the genuine (non-constant) Fubini–Study form of an affine chart, not merely for the constant form on the tangent model.

The form is the one defined by the Fubini–Study potential; fsChartForm_apply below computes its components and fsChartForm_zero identifies it at the chart origin with Kahler.fundamentalFormAlt, so this is closedness of an identified object, not of an opaque one. ⚠️ The manifold statement on ℂℙ^{N-1} remains Mathlib-blocked.

★ The identification: what fsChartForm actually IS, in components

extDeriv_fsChartForm says a form defined by a potential is closed. That is only worth having once the form is identified, and until now nothing computed its pointwise value — so the closedness was true of an object never evaluated. These lemmas close that gap: the dd^c of the Fubini–Study potential is computed in components, and at the chart origin it is the constant fundamental form of KahlerForm.lean up to the normalisation -4.

noncomputable def Kahler.metricCLM {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (x : E) : E →L[ℝ] ℝ

v ↦ g x v = re ⟪x, v⟫, bundled.

Equations

• Kahler.metricCLM x = Complex.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ ((innerSL ℂ) x)

@[simp]

theorem Kahler.metricCLM_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (x v : E) : (metricCLM x) v = metric x v

theorem Kahler.hasFDerivAt_one_add_normSq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (x : E) : HasFDerivAt (fun (y : E) => 1 + ‖y‖ ^ 2) (2 • metricCLM x) x

theorem Kahler.hasFDerivAt_fsPotential {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (x : E) : HasFDerivAt fsPotential ((2 * (1 + ‖x‖ ^ 2)⁻¹) • metricCLM x) x

theorem Kahler.dcForm_fsPotential_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (x : E) (v : Fin 1 → E) : (dcForm fsPotential x) v = -(2 * (1 + ‖x‖ ^ 2)⁻¹) * fundamentalForm x (v 0)

★ B2: the twisted differential of the FS potential in closed form.

theorem Kahler.fderiv_dcForm_fsPotential_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (x : E) (u : Fin 1 → E) (w : E) : (fderiv ℝ (fun (y : E) => (dcForm fsPotential y) u) x) w = -(2 * (1 + ‖x‖ ^ 2)⁻¹) * fundamentalForm w (u 0) + 4 * (1 + ‖x‖ ^ 2)⁻¹ ^ 2 * fundamentalForm x (u 0) * metric x w

B3: the derivative of y ↦ (d^c K)_y u, evaluated.

theorem Kahler.fsChartForm_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (x : E) (v : Fin 2 → E) : (fsChartForm x) v = -4 * ((1 + ‖x‖ ^ 2)⁻¹ * fundamentalForm (v 0) (v 1) - (1 + ‖x‖ ^ 2)⁻¹ ^ 2 * (metric x (v 0) * fundamentalForm x (v 1) - metric x (v 1) * fundamentalForm x (v 0)))

★★ B4: the Fubini–Study chart form, in components.

theorem Kahler.fsChartForm_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] : fsChartForm 0 = -4 • fundamentalFormAlt

★★ B5: at the chart origin the FS chart form IS the constant fundamental form, up to the normalisation -4.