ℂℙⁿ with the Fubini–Study form is a symplectic manifold

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).

Glossary: https://glossary.constraintsurfacedynamics.com/kahler-form/ Plain-language, CSD-role and formal statements of the Kahler form, with this module as its Lean anchor (fsForm_isKahler). Kept symmetric by scripts/check-glossary.sh.

ProjectiveSpaceFubiniStudyForm.lean built the Fubini–Study form fsForm as a C^∞ global 2-form on ℂℙⁿ and proved it closed (fsForm_mextDeriv). This module proves it non-degenerate at every point and concludes that ℂℙⁿ is a symplectic manifold:

• Kahler.metric_mul_fundamentalForm_complexStructure_sub — the taming bracket of the chart form's components, g(x,v) ω(x,Jv) − g(x,Jv) ω(x,v) = |⟪x,v⟫|²;
• Kahler.fsChartForm_apply_complexStructure — hence fsChartForm x (v, Jv) = -4 (1+‖x‖²)⁻² ((1+‖x‖²) ‖v‖² − |⟪x,v⟫|²) at every chart point;
• ★ Kahler.fsChartForm_complexStructure_self_neg — taming at every chart point: for v ≠ 0 that value is negative, by Cauchy–Schwarz (|⟪x,v⟫|² ≤ ‖x‖² ‖v‖² < (1+‖x‖²) ‖v‖²). At the origin it is -4 ‖v‖², the flat taming identity fundamentalForm_complexStructure_self scaled by the normalisation of fsChartForm_zero;
• ★★ fsForm_nondegenerate — non-degeneracy of the Fubini–Study form at every point of ℂℙⁿ: the section at x is the model form at x's own chart coordinate, so the witness is i • v in the model;
• ★★★ fsForm_isSymplectic — ℂℙⁿ with the Fubini–Study form is a symplectic manifold (DifferentialForm.IsSymplectic: closed by fsForm_mextDeriv, non-degenerate by fsForm_nondegenerate). Real dimension 2n, even, as the word requires;
• G7 (2026-09-09). fsJ (J = i· on each tangent space), fsJ_fsJ (J² = -1), ★ fsForm_smul_I_smul_I (ω is J-invariant, a (1,1)-form), and ★★ fsForm_isAlmostKahler — ℂℙⁿ with the Fubini–Study form and J = i· is almost Kähler (DifferentialForm.IsAlmostKahler: symplectic, J² = -1, J-invariant, J-tamed), with the compatible metric g = ω (J ·, ·) positive definite (fsForm_metric_self_pos); and ★ fderiv_chart_transition_smul_I / fsJ_symmL — J is the complex structure of the atlas: the chart transitions are holomorphic (contDiffOn_uTrans), so their derivatives are ℂ-linear and J = i· reads as i· in every chart;
• G14a (2026-09-10). modelJ (i· on the model as a real-linear map) and ★★★ fsForm_isKahler — ℂℙⁿ with the Fubini–Study form and J = i· is a Kähler manifold (DifferentialForm.IsKahler: almost Kähler, and J is the complex structure of the holomorphic atlas, by fsJ_symmL);
• G15 (2026-09-10). fsJL (J = i· as a continuous linear map on each tangent space) and ★★ contMDiff_fsJL — J is a C^∞ section of Hom(TM, TM), constant i· in every chart;
• G14b (2026-09-10). ★★ nijenhuis_fsJ_eq_zero — the Nijenhuis tensor of J = i· vanishes (IsKahler.nijenhuis_eq_zero on fsForm_isKahler): ℂℙⁿ is Kähler in the tensor sense too.

Honest scope

⚠️ Kähler in the atlas sense. fsForm_isKahler packages symplectic + compatible J + J is the complex structure of the holomorphic atlas (fsJ_symmL, fderiv_chart_transition_smul_I), which is the textbook definition. The tensor formulation of integrability (a vanishing Nijenhuis tensor) is nijenhuis_fsJ_eq_zero (G14b). J as a smooth section of the endomorphism bundle is contMDiff_fsJL (G15), for the linear-map version fsJL of fsJ. The pointwise triple IsFubiniStudyKahler on the flat model is the origin's case.

The volume is elsewhere. Non-degeneracy plus closedness does not by itself produce the top-power identity; that is fsVolume_eq_smul_fsMeasure in ProjectiveSpaceFubiniStudyMass.lean, which this file imports.

⚠️ Sign convention. With fsChartForm = dd^c log(1+‖z‖²) the taming value ω (v, J v) is negative (-4 at the origin); the almost Kähler predicate absorbs it by the metric convention g = ω (J ·, ·), so ω (J v, v) > 0. Nothing downstream depends on the sign, only on non-vanishing.

Provenance and references. Geometry/Manifold/SymplecticForm.lean (the predicate); Geometry/Manifold/HamiltonianVectorField.lean (IsAlmostKahler, apply_swap); Instances/ProjectiveSpaceUnitaryAction.lean (contDiffOn_uTrans, chartFun_smul_chartInv); Geometry/Manifold/Instances/ProjectiveSpaceFubiniStudyForm.lean (fsForm, fsForm_mextDeriv); Analysis/InnerProductSpace/KahlerPotential.lean (fsChartForm_apply); Analysis/InnerProductSpace/KahlerForm.lean (the taming identity, complexStructure); the Mathlib-gaps register (Kahler / symplectic manifold API); the backlog (XL, "Manifold exterior calculus"); the terms register ("symplectic / manifold"); the completed-work ledger.

theorem Kahler.metric_mul_fundamentalForm_complexStructure_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (x v : E) : metric x v * fundamentalForm x (complexStructure v) - metric x (complexStructure v) * fundamentalForm x v = Complex.normSq (inner ℂ x v)

The taming bracket of the Fubini–Study chart-form components: g(x,v) ω(x,Jv) − g(x,Jv) ω(x,v) = |⟪x,v⟫|².

theorem Kahler.fsChartForm_apply_complexStructure {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (x v : E) : (fsChartForm x) ![v, complexStructure v] = -4 * (1 + ‖x‖ ^ 2)⁻¹ ^ 2 * ((1 + ‖x‖ ^ 2) * ‖v‖ ^ 2 - Complex.normSq (inner ℂ x v))

Taming at every chart point: fsChartForm x (v, Jv) = -4 (1+‖x‖²)⁻² ((1+‖x‖²) ‖v‖² − |⟪x,v⟫|²).

theorem Kahler.fsChartForm_complexStructure_self_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (x : E) {v : E} (hv : v ≠ 0) : (fsChartForm x) ![v, complexStructure v] < 0

★ Taming at every chart point: for v ≠ 0, fsChartForm x (v, Jv) < 0 (Cauchy–Schwarz: |⟪x,v⟫|² ≤ ‖x‖² ‖v‖² < (1+‖x‖²) ‖v‖²).

theorem Projectivization.fsModelForm_smul_I_neg {n : ℕ} (w : Fin n → ℂ) {v : Fin n → ℂ} (hv : v ≠ 0) : (fsModelForm w) ![v, Complex.I • v] < 0

Taming for the model form: fsModelForm w (v, i • v) < 0 for v ≠ 0.

theorem Projectivization.fsSection_smul_I_neg {n : ℕ} (x : Projectivization ℂ (Ambient n)) {v : Fin n → ℂ} (hv : v ≠ 0) : x.fsSection ![v, Complex.I • v] < 0

Taming for the section, in the model: fsSection x (v, i • v) < 0 for v ≠ 0.

theorem Projectivization.fsForm_nondegenerate {n : ℕ} (x : Projectivization ℂ (Ambient n)) (v : TangentSpace (modelWithCornersSelf ℝ (Fin n → ℂ)) x) (hv : v ≠ 0) : ∃ (w : TangentSpace (modelWithCornersSelf ℝ (Fin n → ℂ)) x), (fsForm x) ![v, w] ≠ 0

★★ Non-degeneracy of the Fubini–Study form at every point of ℂℙⁿ.

theorem Projectivization.fsForm_isSymplectic (n : ℕ) : fsForm.IsSymplectic

★★★ ℂℙⁿ with the Fubini–Study form is a symplectic manifold: closed (fsForm_mextDeriv) and non-degenerate at every point (fsForm_nondegenerate).

The almost Kähler structure of ℂℙⁿ: J = i· (G7)

@[reducible, inline]

abbrev Projectivization.tangentToModel {n : ℕ} {x : Projectivization ℂ (Ambient n)} (v : TangentSpace (modelWithCornersSelf ℝ (Fin n → ℂ)) x) : Fin n → ℂ

Definitional identification of a tangent vector of ℂℙⁿ with a model vector (the model carries the ℂ-action the tangent space does not expose).

Equations

• Projectivization.tangentToModel v = v

def Projectivization.fsJ {n : ℕ} (x : Projectivization ℂ (Ambient n)) (v : TangentSpace (modelWithCornersSelf ℝ (Fin n → ℂ)) x) : TangentSpace (modelWithCornersSelf ℝ (Fin n → ℂ)) x

The complex structure of ℂℙⁿ: multiplication by i on each tangent space, read in the chart at the point.

Equations

• x.fsJ v = Complex.I • Projectivization.tangentToModel v

theorem Projectivization.fsJ_fsJ {n : ℕ} (x : Projectivization ℂ (Ambient n)) (v : TangentSpace (modelWithCornersSelf ℝ (Fin n → ℂ)) x) : x.fsJ (x.fsJ v) = -v

theorem Projectivization.fsModelForm_smul_I_smul_I {n : ℕ} (w u v : Fin n → ℂ) : (fsModelForm w) ![Complex.I • u, Complex.I • v] = (fsModelForm w) ![u, v]

J-invariance of the model form: fsModelForm w (i • u, i • v) = fsModelForm w (u, v).

theorem Projectivization.fsForm_smul_I_smul_I {n : ℕ} (x : Projectivization ℂ (Ambient n)) (u v : TangentSpace (modelWithCornersSelf ℝ (Fin n → ℂ)) x) : (fsForm x) ![x.fsJ u, x.fsJ v] = (fsForm x) ![u, v]

★ J-invariance of the Fubini–Study form: it is a (1,1)-form.

J is the complex structure of the atlas

theorem Projectivization.chartAtIdx_transition_eq_uTrans {n : ℕ} (i : Fin (n + 1)) (y : Projectivization ℂ (Ambient n)) : ↑(chartAt (Fin n → ℂ) y) ∘ ↑(chartAtIdx i).symm = uTrans 1 i y.idx

The transition from the i-th affine chart to the chart at y is the unitary-action chart map for U = 1.

theorem Projectivization.chart_transition_eq_uTrans {n : ℕ} (x₀ y : Projectivization ℂ (Ambient n)) : ↑(chartAt (Fin n → ℂ) y) ∘ ↑(chartAt (Fin n → ℂ) x₀).symm = uTrans 1 x₀.idx y.idx

The chart transition of ℂℙⁿ is the unitary-action chart map for U = 1.

theorem Projectivization.fderiv_chartAtIdx_transition_smul_I {n : ℕ} (i : Fin (n + 1)) (y : Projectivization ℂ (Ambient n)) {w : Fin n → ℂ} (hy : ↑(chartAtIdx i).symm w ∈ (chartAt (Fin n → ℂ) y).source) (v : Fin n → ℂ) : (fderiv ℝ (↑(chartAt (Fin n → ℂ) y) ∘ ↑(chartAtIdx i).symm) w) (Complex.I • v) = Complex.I • (fderiv ℝ (↑(chartAt (Fin n → ℂ) y) ∘ ↑(chartAtIdx i).symm) w) v

★ J is the complex structure of the atlas: the derivative of the transition from any affine chart chartAtIdx i to the chart at y is ℂ-linear, because the transitions are holomorphic (contDiffOn_uTrans). So J = i· in one chart is J = i· in every chart.

theorem Projectivization.fderiv_chart_transition_smul_I {n : ℕ} (x₀ y : Projectivization ℂ (Ambient n)) {w : Fin n → ℂ} (hy : ↑(chartAt (Fin n → ℂ) x₀).symm w ∈ (chartAt (Fin n → ℂ) y).source) (v : Fin n → ℂ) : (fderiv ℝ (↑(chartAt (Fin n → ℂ) y) ∘ ↑(chartAt (Fin n → ℂ) x₀).symm) w) (Complex.I • v) = Complex.I • (fderiv ℝ (↑(chartAt (Fin n → ℂ) y) ∘ ↑(chartAt (Fin n → ℂ) x₀).symm) w) v

The same for the chart at x₀ (chartAt E x₀ = chartAtIdx (idx x₀)).

theorem Projectivization.fsJ_symmL {n : ℕ} (x₀ y : Projectivization ℂ (Ambient n)) (hy : y ∈ (chartAt (Fin n → ℂ) x₀).source) (v : Fin n → ℂ) : y.fsJ ((Bundle.Trivialization.symmL ℝ (trivializationAt (Fin n → ℂ) (TangentSpace (modelWithCornersSelf ℝ (Fin n → ℂ))) x₀) y) v) = (Bundle.Trivialization.symmL ℝ (trivializationAt (Fin n → ℂ) (TangentSpace (modelWithCornersSelf ℝ (Fin n → ℂ))) x₀) y) (Complex.I • v)

★ J commutes with the tangent trivialisation: in the chart at x₀, J y is still i· for every y in the chart source.

theorem Projectivization.fsJ_localTriv_symmL {n : ℕ} (e : ↑(atlas (Fin n → ℂ) (Projectivization ℂ (Ambient n)))) (y : Projectivization ℂ (Ambient n)) (hy : y ∈ (↑e).source) (v : Fin n → ℂ) : y.fsJ ((Bundle.Trivialization.symmL ℝ ((tangentBundleCore (modelWithCornersSelf ℝ (Fin n → ℂ)) (Projectivization ℂ (Ambient n))).localTriv e) y) v) = (Bundle.Trivialization.symmL ℝ ((tangentBundleCore (modelWithCornersSelf ℝ (Fin n → ℂ)) (Projectivization ℂ (Ambient n))).localTriv e) y) (Complex.I • v)

★ J commutes with the tangent trivialisation of every chart of the atlas: J = i· in every affine chart, not only in the charts chartAt picks.

noncomputable def Projectivization.modelJ {n : ℕ} : (Fin n → ℂ) →L[ℝ] Fin n → ℂ

The complex structure of the model Fin n → ℂ: multiplication by i, as a real-linear map.

Equations

• Projectivization.modelJ = ContinuousLinearMap.restrictScalars ℝ (Complex.I • ContinuousLinearMap.id ℂ (Fin n → ℂ))

@[simp]

theorem Projectivization.modelJ_apply {n : ℕ} (v : Fin n → ℂ) : modelJ v = Complex.I • v

J as a smooth section of the endomorphism bundle (G15)

noncomputable def Projectivization.fsJL {n : ℕ} (x : Projectivization ℂ (Ambient n)) : TangentSpace (modelWithCornersSelf ℝ (Fin n → ℂ)) x →L[ℝ] TangentSpace (modelWithCornersSelf ℝ (Fin n → ℂ)) x

J = i· on each tangent space, as a continuous linear map: the section of Hom(TM, TM).

Equations

• x.fsJL = Projectivization.modelJ

@[simp]

theorem Projectivization.fsJL_apply {n : ℕ} (x : Projectivization ℂ (Ambient n)) (v : TangentSpace (modelWithCornersSelf ℝ (Fin n → ℂ)) x) : x.fsJL v = x.fsJ v

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

★★ J is a smooth section of Hom(TM, TM) on ℂℙⁿ: in every chart it is the constant i· (contMDiff_hom_section_of_localTriv_symmL on fsJ_localTriv_symmL).

★★★ ℂℙⁿ is almost Kähler, and Kähler (G14a)

theorem Projectivization.fsForm_isAlmostKahler (n : ℕ) : fsForm.IsAlmostKahler fsJ

★★ ℂℙⁿ with the Fubini–Study form and J = i· is almost Kähler: symplectic (fsForm_isSymplectic), J² = -1, ω is J-invariant, and ω (J v, v) > 0 — the taming fsSection_smul_I_neg, its sign (the -4 of the potential) absorbed by the metric convention g = ω (J ·, ·).

theorem Projectivization.fsForm_metric_self_pos {n : ℕ} (x : Projectivization ℂ (Ambient n)) {v : TangentSpace (modelWithCornersSelf ℝ (Fin n → ℂ)) x} (hv : v ≠ 0) : 0 < ⋯.metric x v v

The compatible metric of ℂℙⁿ is positive definite: the Fubini–Study metric, up to the convention.

theorem Projectivization.fsForm_isKahler (n : ℕ) : fsForm.IsKahler fsJ modelJ

★★★ ℂℙⁿ with the Fubini–Study form and J = i· is a Kähler manifold: almost Kähler (fsForm_isAlmostKahler), and J is the complex structure of the holomorphic atlas — i· in every chart of the atlas (fsJ_localTriv_symmL, from the holomorphy of the transitions contDiffOn_uTrans). Kähler in the atlas sense of DifferentialForm.IsKahler; the tensor sense is G14b.

The Nijenhuis tensor of J = i· vanishes (G14b)

theorem Projectivization.nijenhuis_fsJ_eq_zero {n : ℕ} {V W : (x : Projectivization ℂ (Ambient n)) → TangentSpace (modelWithCornersSelf ℝ (Fin n → ℂ)) x} (x₀ : Projectivization ℂ (Ambient n)) (hV : (MDiffAt fun (x : Projectivization ℂ (Ambient n)) => ⟨x, V x⟩) x₀) (hW : (MDiffAt fun (x : Projectivization ℂ (Ambient n)) => ⟨x, W x⟩) x₀) : DifferentialForm.nijenhuis fsJ V W x₀ = 0

★★ J = i· is integrable in the tensor sense on ℂℙⁿ: its Nijenhuis tensor vanishes on vector fields differentiable at the point (IsKahler.nijenhuis_eq_zero on fsForm_isKahler).