The Fubini–Study form as a global smooth 2-form on ℂℙⁿ

TERM-SCOPE(Kahler) — this module uses the restricted sense of "Kahler"; the source repository's terms register records what is backed and what is not.

Category: 1-Mathlib (CSD-free; upstream target Mathlib.Geometry.Manifold).

DifferentialForm.lean made "a smooth 2-form on ℂℙⁿ" a type and exhibited the zero form. This module exhibits the one that matters: the Fubini–Study form, assembled from the chart forms fsChartForm = dd^c log(1 + ‖z‖²) of KahlerPotential.lean using the chart invariance fsModelForm_transP of ProjectiveSpaceFubiniStudy.lean.

• fsSection — the family: at x, the model form read in the chart the atlas chose at x (TangentSpace 𝓘(ℝ, Fin n → ℂ) x is Fin n → ℂ definitionally, so no transport is needed);
• ★ localRep_fsSection — the local-representative identity: in the trivialisation of the alternating bundle over the chart at x₀, the section reads as the model form in that chart at every y of the chart domain. This is where chart invariance is spent: the tangent coordinate change is the derivative of the chart transition (extChartAt_trans_eq, VectorBundleCore.trivializationAt_symmL), and the pullback of the form along it is the form (fsModelForm_transP);
• ★ contMDiffAt_fsSection / contMDiff_fsSection — smoothness, from the local representative and contDiff_fsModelForm (the model form is C^∞: dd^c of a C^∞ potential, pulled back along a linear map);
• ★★ fsForm — the Fubini–Study form as a C^∞ global 2-form on ℂℙⁿ, a term of DifferentialForm 𝓘(ℝ, Fin n → ℂ) (ℙ ℂ (Ambient n)) ∞ (Fin 2) ℝ;
• ★★ contMDiff_omega_fsForm / fsFormAnalytic — the Fubini–Study form is analytic (G12, 2026-09-10): the same chain at ω — the potential is analytic (contDiff_omega_fsPotential), dd^c and the pullback are generic in the order (contDiff_omega_fsChartForm, contDiff_omega_fsModelForm), and the chart is analytic because the manifold is (contMDiffAt_omega_fsSection); fsFormAnalytic is the section as a term of the ω type;
• ★★ fsForm_ne_zero — it is not the zero form (n ≥ 1): at a chart origin it is -4 times the flat fundamental form (fsChartForm_zero), which pairs e with i • e to ‖e‖²;
• ★★★ fsForm_mextDeriv — d ω_FS = 0 on ℂℙⁿ: the Fubini–Study form is closed at manifold level, for the exterior derivative mextDeriv of ExteriorDerivative.lean (step (2b)). Its local representative in every chart is the flat chart form fsModelForm (localRep_fsSection), whose flat d vanishes (extDeriv_fsChartForm, MG-4) — so the manifold statement is the flat one read through the chart, which is what mextDeriv is.

Honest scope

⚠️ Two orders, one section. fsForm is the C^∞ form the downstream predicates (IsSymplectic, IsAlmostKahler, the Hamiltonian layer) are stated on, and fsFormAnalytic is the same section as a term of the ω type (fsFormAnalytic_apply); nothing downstream is restated at ω. Analyticity of the chart transitions is instIsManifoldReal; analyticity of the section is contMDiff_omega_fsForm.

⚠️ Real smooth, not holomorphic. The section is over the real model 𝓘(ℝ, Fin n → ℂ); the form is real-valued and ℝ-alternating, as a Kähler form is. No (1,1)-type statement is made on the manifold.

Closed here; the rest downstream. d fsForm = 0 is fsForm_mextDeriv; non-degeneracy at every point is fsForm_nondegenerate (ProjectiveSpaceFubiniStudySymplectic.lean) and the top-power identity ωⁿ = (4π)ⁿ μ_FS is fsVolume_eq_smul_fsMeasure (ProjectiveSpaceFubiniStudyMass.lean). fsForm_ne_zero is a non-vacuity certificate at one point, nothing more.

⚠️ The chart chosen at x is idx x, a choice function. fsSection is defined through it; localRep_fsSection is what shows the value does not depend on the choice.

Provenance and references. Geometry/Manifold/DifferentialForm.lean (the type; step (2a)); the generator-layer plan (G12, the analytic upgrade); Geometry/Manifold/ExteriorDerivative.lean (mextDeriv, d ∘ d = 0; step (2b)); Geometry/Manifold/Instances/ProjectiveSpaceFubiniStudy.lean (chart invariance); Geometry/Manifold/Instances/ProjectiveSpace.lean (the atlas); Analysis/InnerProductSpace/KahlerPotential.lean (fsChartForm, fsChartForm_zero); the Mathlib-gaps register (Kahler / symplectic manifold API); the backlog (XL, "Manifold exterior calculus"); the completed-work ledger.

The family

noncomputable def Projectivization.fsSection {n : ℕ} (x : Projectivization ℂ (Ambient n)) : TangentSpace (modelWithCornersSelf ℝ (Fin n → ℂ)) x [⋀^Fin 2]→L[ℝ] Bundle.Trivial (Projectivization ℂ (Ambient n)) ℝ x

The Fubini–Study form as a family over ℂℙⁿ: at x, the model form at x's own chart coordinate (TangentSpace 𝓘(ℝ, Fin n → ℂ) x is definitionally Fin n → ℂ).

Equations

• x.fsSection = Projectivization.fsModelForm (Projectivization.chartFun x.idx x)

theorem Projectivization.extChartAt_trans_eq {n : ℕ} (x₀ y : Projectivization ℂ (Ambient n)) : ↑(extChartAt (modelWithCornersSelf ℝ (Fin n → ℂ)) y) ∘ ↑(extChartAt (modelWithCornersSelf ℝ (Fin n → ℂ)) x₀).symm = transP x₀.idx y.idx

The chart transition between the charts at x₀ and y, as extChartAt sees it, IS the model transition transP.

The local representative

theorem Projectivization.localRep_fsSection {n : ℕ} (x₀ y : Projectivization ℂ (Ambient n)) (hy : y ∈ (chartAt (Fin n → ℂ) x₀).source) : (↑(trivializationAt ((Fin n → ℂ) [⋀^Fin 2]→L[ℝ] ℝ) (fun (p : Projectivization ℂ (Ambient n)) => TangentSpace (modelWithCornersSelf ℝ (Fin n → ℂ)) p [⋀^Fin 2]→L[ℝ] Bundle.Trivial (Projectivization ℂ (Ambient n)) ℝ p) x₀) ⟨y, y.fsSection⟩).2 = fsModelForm (chartFun x₀.idx y)

★ The local-representative identity. In the trivialisation of the alternating bundle over the chart at x₀, the section reads as the model form in that chart, at every point of the chart domain. Chart invariance (fsModelForm_transP) is spent exactly here.

Smoothness of the model form

theorem Projectivization.fsChartForm_eq_alternatizeUncurryFinCLM_fderiv {n : ℕ} : Kahler.fsChartForm = fun (x : EuclideanSpace ℂ (Fin n)) => (ContinuousAlternatingMap.alternatizeUncurryFinCLM ℝ (EuclideanSpace ℂ (Fin n)) ℝ) (fderiv ℝ (Kahler.dcForm Kahler.fsPotential) x)

The chart form is the alternatization of the derivative of d^c fsPotential — dd^c of the potential, in the shape the smoothness lemmas need.

theorem Projectivization.contDiff_fsChartForm {n : ℕ} : ContDiff ℝ (↑⊤) Kahler.fsChartForm

The chart form is C^∞: dd^c of the C^∞ potential, i.e. the alternatization of the derivative of d^c fsPotential.

theorem Projectivization.contDiff_fsModelForm {n : ℕ} : ContDiff ℝ (↑⊤) fsModelForm

The model form is C^∞: the chart form pulled back along the linear identification toLpCLM.

The global section

theorem Projectivization.contMDiffAt_fsSection {n : ℕ} (x₀ : Projectivization ℂ (Ambient n)) : ContMDiffAt (modelWithCornersSelf ℝ (Fin n → ℂ)) ((modelWithCornersSelf ℝ (Fin n → ℂ)).prod (modelWithCornersSelf ℝ ((Fin n → ℂ) [⋀^Fin 2]→L[ℝ] ℝ))) (↑⊤) (fun (x : Projectivization ℂ (Ambient n)) => ⟨x, x.fsSection⟩) x₀

★ fsSection is a C^∞ section at every point: in the chart at x₀ it is the model form composed with the chart (localRep_fsSection), and both are smooth.

theorem Projectivization.contMDiff_fsSection {n : ℕ} : ContMDiff (modelWithCornersSelf ℝ (Fin n → ℂ)) ((modelWithCornersSelf ℝ (Fin n → ℂ)).prod (modelWithCornersSelf ℝ ((Fin n → ℂ) [⋀^Fin 2]→L[ℝ] ℝ))) ↑⊤ fun (x : Projectivization ℂ (Ambient n)) => ⟨x, x.fsSection⟩

★ fsSection is a C^∞ section.

noncomputable def Projectivization.fsForm {n : ℕ} : DifferentialForm (modelWithCornersSelf ℝ (Fin n → ℂ)) (Projectivization ℂ (Ambient n)) (↑⊤) (Fin 2) ℝ

★★ The Fubini–Study form as a C^∞ global 2-form on ℂℙⁿ.

Equations

• Projectivization.fsForm = { toFun := Projectivization.fsSection, contMDiff_toFun := ⋯ }

@[simp]

theorem Projectivization.fsForm_apply {n : ℕ} (x : Projectivization ℂ (Ambient n)) : fsForm x = x.fsSection

★ Analyticity: the section is ω, not merely C^∞ (G12)

The manifold is analytic (instIsManifoldReal) and so is the potential (contDiff_omega_fsPotential); every step of the C^∞ chain above is generic in the order, so the same chain at ω makes fsForm an analytic form.

theorem Projectivization.contDiff_omega_fsChartForm {n : ℕ} : ContDiff ℝ ⊤ Kahler.fsChartForm

★ The chart form is analytic: dd^c of the analytic potential.

theorem Projectivization.contDiff_omega_fsModelForm {n : ℕ} : ContDiff ℝ ⊤ fsModelForm

★ The model form is analytic: the chart form pulled back along the linear identification.

theorem Projectivization.contMDiffAt_omega_fsSection {n : ℕ} (x₀ : Projectivization ℂ (Ambient n)) : ContMDiffAt (modelWithCornersSelf ℝ (Fin n → ℂ)) ((modelWithCornersSelf ℝ (Fin n → ℂ)).prod (modelWithCornersSelf ℝ ((Fin n → ℂ) [⋀^Fin 2]→L[ℝ] ℝ))) ⊤ (fun (x : Projectivization ℂ (Ambient n)) => ⟨x, x.fsSection⟩) x₀

★ fsSection is an analytic section at every point: the proof of contMDiffAt_fsSection, at ω (the chart is analytic because the manifold is).

theorem Projectivization.contMDiff_omega_fsSection {n : ℕ} : ContMDiff (modelWithCornersSelf ℝ (Fin n → ℂ)) ((modelWithCornersSelf ℝ (Fin n → ℂ)).prod (modelWithCornersSelf ℝ ((Fin n → ℂ) [⋀^Fin 2]→L[ℝ] ℝ))) ⊤ fun (x : Projectivization ℂ (Ambient n)) => ⟨x, x.fsSection⟩

★ fsSection is an analytic section.

theorem Projectivization.contMDiff_omega_fsForm {n : ℕ} : ContMDiff (modelWithCornersSelf ℝ (Fin n → ℂ)) ((modelWithCornersSelf ℝ (Fin n → ℂ)).prod (modelWithCornersSelf ℝ ((Fin n → ℂ) [⋀^Fin 2]→L[ℝ] ℝ))) ⊤ fun (x : Projectivization ℂ (Ambient n)) => ⟨x, fsForm x⟩

★★ The Fubini–Study form is analytic: the section of fsForm is C^ω, not merely C^∞ — the manifold is analytic and so is the potential.

noncomputable def Projectivization.fsFormAnalytic {n : ℕ} : DifferentialForm (modelWithCornersSelf ℝ (Fin n → ℂ)) (Projectivization ℂ (Ambient n)) ⊤ (Fin 2) ℝ

★★ The Fubini–Study form as an analytic global 2-form on ℂℙⁿ: the section of fsForm, as a term of the ω type.

Equations

• Projectivization.fsFormAnalytic = { toFun := Projectivization.fsSection, contMDiff_toFun := ⋯ }

@[simp]

theorem Projectivization.fsFormAnalytic_apply {n : ℕ} (x : Projectivization ℂ (Ambient n)) : fsFormAnalytic x = fsForm x

Non-vacuity

noncomputable def Projectivization.origin {n : ℕ} (i : Fin (n + 1)) : Projectivization ℂ (Ambient n)

The origin of the i-th affine chart, [0 : … : 1 : … : 0].

Equations

• Projectivization.origin i = Projectivization.mk ℂ (Projectivization.insertOne i 0) ⋯

theorem Projectivization.rep_origin {n : ℕ} (i : Fin (n + 1)) : ∃ (a : ℂ), a ≠ 0 ∧ ∀ (k : Fin (n + 1)), (origin i).rep.ofLp k = a * (insertOne i 0).ofLp k

Any representative of the chart origin is a nonzero multiple of insertOne i 0.

theorem Projectivization.idx_origin {n : ℕ} (i : Fin (n + 1)) : (origin i).idx = i

The atlas has no choice at the chart origin: i is the only coordinate that does not vanish.

theorem Projectivization.chartFun_idx_origin {n : ℕ} (i : Fin (n + 1)) : chartFun (origin i).idx (origin i) = 0

theorem Projectivization.fsSection_origin {n : ℕ} (i : Fin (n + 1)) : (origin i).fsSection = fsModelForm 0

At a chart origin the section is the model form at 0.

theorem Projectivization.fsModelForm_zero_apply {n : ℕ} (v : Fin 2 → Fin n → ℂ) : (fsModelForm 0) v = -4 * Kahler.fundamentalForm (toLpCLM (v 0)) (toLpCLM (v 1))

The model form at 0 is -4 times the flat fundamental form (fsChartForm_zero).

theorem Projectivization.fsForm_ne_zero {n : ℕ} (hn : 0 < n) : fsForm ≠ 0

★★ The Fubini–Study form is not the zero form (for n ≥ 1): at a chart origin it pairs a unit vector e with i • e to -4 ‖e‖² ≠ 0.

Closedness: d ω_FS = 0 on ℂℙⁿ

theorem Projectivization.extDeriv_fsModelForm {n : ℕ} (w : Fin n → ℂ) : extDeriv fsModelForm w = 0

The model form is closed on the flat model: the chart form is (extDeriv_fsChartForm), and the model form is its pullback along the linear identification toLpCLM.

theorem Projectivization.mextDerivFamily_fsSection {n : ℕ} (x : Projectivization ℂ (Ambient n)) : mextDerivFamily fsSection x = 0

★★★ The Fubini–Study form is closed on ℂℙⁿ, pointwise: in the chart at x its local representative is the flat chart form, whose flat d is zero.

theorem Projectivization.fsForm_mextDeriv {n : ℕ} : fsForm.mextDeriv = 0

★★★ d ω_FS = 0 on ℂℙⁿ.

The top power

noncomputable def Projectivization.fsTopForm (n : ℕ) : DifferentialForm (modelWithCornersSelf ℝ (Fin n → ℂ)) (Projectivization ℂ (Ambient n)) (↑⊤) (Fin (2 * n)) ℝ

The top power of the Fubini–Study form, a 2n-form on ℂℙⁿ.

Equations

• Projectivization.fsTopForm n = Projectivization.fsForm.wedgePow n