The Riemannian volume of the Fubini–Study metric is the symplectic volume over n!

Category: 1-Mathlib (the Kähler identity vol_g = ω^{∧n}/n! on ℂℙⁿ; G17 of the generator-layer plan §9).

TERM-SCOPE(Kahler) TERM-SCOPE(Liouville) — this module identifies the Riemannian and symplectic readings of the Fubini–Study volume; the source repository's terms register records what is backed.

The compatible metric of the almost Kähler structure of ℂℙⁿ (G7) is the Fubini–Study metric g = ω(J·,·). Its Riemannian volume (RiemannianVolume.lean: the chart densities √det G glued along the affine cover) is identified with the measure of the top power of the Fubini–Study form:

• fsMetric — the Fubini–Study metric g x u v = fsForm x (J u, v), definitionally the metric of fsForm_isAlmostKahler;
• fsModelMetric w — the model metric g_w(u, v) = ω_w(i·u, v) on Fin n → ℂ, as a real bilinear form; ★ localRep_fsMetric — in every affine chart the Fubini–Study metric reads as the model metric (J = i· in every chart, fsJ_symmL, and the form reads as the model form, localRep_fsSection);
• ★★ det_toMatrix_fsModelMetric — the Gram determinant of the model metric against the standard basis is (4ⁿ (1 + ‖w‖²)^{-(n+1)})², by the route of wedgePow_fsModelForm_stdBasis: rotate w to the first axis by a unitary (fsModelMetric_mulVec; the real determinant of a unitary is 1), where the metric is the pullback of the metric at the origin along the diagonal scaling (fsModelMetric_single, normSq_det_fsScale), and at the origin the Gram matrix is 4·1 (toMatrix_fsModelMetric_zero);
• ★★ chartDensity_fsMetric — the Riemannian chart density is 1/n! times the density of ω_FS^{∧n}, in every chart (√det G = 4ⁿ (1 + ‖w‖²)^{-(n+1)} against |coeff| = 4ⁿ n! (1 + ‖w‖²)^{-(n+1)});
• ★★★ riemannianVolume_fsMetric — the Riemannian volume of the Fubini–Study metric IS fsVolume n / n!, the Kähler identity vol_g = ω^{∧n}/n! at the level of measures; and ★★★ riemannianVolume_fsMetric_eq_smul_fsMeasure — with the constant, vol_g = ((4π)ⁿ/n!) · μ_FS: the Fubini–Study measure is the normalised Riemannian volume of the Fubini–Study metric, the reading TERMS.md had listed as not established;
• Q30 / G17b (2026-09-11). isBilinear_fsMetric and ★ riemannianVolume_fsMetric_congr_cover — the identification holds for every chart cover, not only the affine one: the Riemannian volume of the Fubini–Study metric is canonical (MetricFamily.riemannianVolume_congr_cover).

Honest scope

⚠️ Densities, against the standard basis. RiemannianVolume.lean defines the Riemannian volume through Gram densities against a basis of the model; since Q30 it proves the construction is cover-independent for bilinear families, and isBilinear_fsMetric supplies bilinearity here, so riemannianVolume_fsMetric_congr_cover holds for every cover. Basis-independence of the Gram construction (a change of basis rescales √det G by |det| of the change-of-basis matrix, which μ.IsAddHaarMeasure absorbs) is not stated: nothing consumes it. The identity vol_g = ω^{∧n}/n! is proved at the level of chart densities, not as an identity of volume forms (no orientation is chosen).

⚠️ Conventions. The (4π)ⁿ and the n! are fsChartForm = dd^c log(1 + ‖z‖²)'s -4 and the top power's n! (fsVolume_eq_smul_fsMeasure); the textbook ω^{∧n}/n! is a renormalisation.

Provenance and references. The generator-layer plan (G17); the terms register (Fubini–Study, Kähler, Liouville); Geometry/Manifold/RiemannianVolume.lean; Instances/ProjectiveSpaceFubiniStudyMass.lean (the rotation route, det_mulVecCLM, fsScale); Instances/ProjectiveSpaceFubiniStudySymplectic.lean (fsJ, fsJ_symmL, fsForm_isAlmostKahler).

The Fubini–Study metric and its model

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

The Fubini–Study metric g x u v = ω_FS (J u, v): the compatible metric of the almost Kähler structure of ℂℙⁿ.

Equations

• x.fsMetric u v = (Projectivization.fsForm x) ![x.fsJ u, v]

theorem Projectivization.fsMetric_eq_metric {n : ℕ} : fsMetric = ⋯.metric

noncomputable def Projectivization.fsModelMetric {n : ℕ} (w : Fin n → ℂ) : LinearMap.BilinForm ℝ (Fin n → ℂ)

The model metric g_w(u, v) = ω_w(i·u, v) on Fin n → ℂ, as a real bilinear form.

Equations

• Projectivization.fsModelMetric w = LinearMap.mk₂ ℝ (fun (u v : Fin n → ℂ) => (Projectivization.fsModelForm w) ![Complex.I • u, v]) ⋯ ⋯ ⋯ ⋯

@[simp]

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

theorem Projectivization.fsForm_symmL_symmL {n : ℕ} (x₀ y : Projectivization ℂ (Ambient n)) (hy : y ∈ (chartAt (Fin n → ℂ) x₀).source) (a b : Fin n → ℂ) : (fsForm y) ![(Bundle.Trivialization.symmL ℝ (trivializationAt (Fin n → ℂ) (TangentSpace (modelWithCornersSelf ℝ (Fin n → ℂ))) x₀) y) a, (Bundle.Trivialization.symmL ℝ (trivializationAt (Fin n → ℂ) (TangentSpace (modelWithCornersSelf ℝ (Fin n → ℂ))) x₀) y) b] = (fsModelForm (↑(chartAt (Fin n → ℂ) x₀) y)) ![a, b]

The form read through the tangent trivialisation of the chart at x₀ is the model form: the pointwise content of localRep_fsSection.

theorem Projectivization.localRep_fsMetric {n : ℕ} (x₀ : Projectivization ℂ (Ambient n)) {w : Fin n → ℂ} (hw : w ∈ (chartAt (Fin n → ℂ) x₀).target) (u v : Fin n → ℂ) : MetricFamily.localRep fsMetric x₀ w u v = ((fsModelMetric w) u) v

★ In every affine chart the Fubini–Study metric reads as the model metric: J = i· in the chart (fsJ_symmL) and the form reads as the model form.

theorem Projectivization.gram_fsMetric {n : ℕ} (x₀ : Projectivization ℂ (Ambient n)) {w : Fin n → ℂ} (hw : w ∈ (chartAt (Fin n → ℂ) x₀).target) : MetricFamily.gram (stdBasis n) fsMetric x₀ w = (LinearMap.BilinForm.toMatrix (stdBasis n)) (fsModelMetric w)

The Gram determinant, by rotation to the first axis

noncomputable def Projectivization.mulVecL {n : ℕ} (A : Matrix (Fin n) (Fin n) ℂ) : (Fin n → ℂ) →ₗ[ℝ] Fin n → ℂ

A complex matrix acting on the pi model, as a real linear map (mulVecCLM, forgotten).

Equations

• Projectivization.mulVecL A = ↑(Projectivization.mulVecCLM A)

theorem Projectivization.mulVecL_apply {n : ℕ} (A : Matrix (Fin n) (Fin n) ℂ) (v : Fin n → ℂ) : (mulVecL A) v = A.mulVec v

theorem Projectivization.det_mulVecL {n : ℕ} (A : Matrix (Fin n) (Fin n) ℂ) : LinearMap.det (mulVecL A) = Complex.normSq A.det

theorem Projectivization.fsModelMetric_mulVec {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin n) ℂ)) (w : Fin n → ℂ) : (fsModelMetric ((↑U).mulVec w)).comp (mulVecL ↑U) (mulVecL ↑U) = fsModelMetric w

The unitary action commutes with i·, so the rotation invariance of the form (fsModelForm_mulVec) is a rotation invariance of the metric.

theorem Projectivization.det_toMatrix_fsModelMetric_mulVec {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin n) ℂ)) (w : Fin n → ℂ) : ((LinearMap.BilinForm.toMatrix (stdBasis n)) (fsModelMetric w)).det = ((LinearMap.BilinForm.toMatrix (stdBasis n)) (fsModelMetric ((↑U).mulVec w))).det

theorem Projectivization.fsModelMetric_single {n : ℕ} [NeZero n] (r : ℝ) : fsModelMetric (Pi.single 0 ↑r) = (fsModelMetric 0).comp (mulVecL (fsScale r)) (mulVecL (fsScale r))

At r e₀ the model metric is the pullback of the model metric at the origin along the diagonal scaling (fsModelForm_single; the scaling is real-diagonal, so it commutes with i·).

theorem Projectivization.det_toMatrix_fsModelMetric_single {n : ℕ} [NeZero n] (r : ℝ) : ((LinearMap.BilinForm.toMatrix (stdBasis n)) (fsModelMetric (Pi.single 0 ↑r))).det = ((1 + r ^ 2)⁻¹ ^ (n + 1)) ^ 2 * ((LinearMap.BilinForm.toMatrix (stdBasis n)) (fsModelMetric 0)).det

The Gram matrix at the origin is 4·1

theorem Projectivization.fsModelMetric_zero_apply {n : ℕ} (u v : Fin n → ℂ) : ((fsModelMetric 0) u) v = 4 * (inner ℂ (toLpCLM u) (toLpCLM v)).re

At the origin the model metric is four times the real part of the inner product.

theorem Projectivization.stdBasis_inner_re {n : ℕ} (p q : Fin (2 * n)) : (inner ℂ (toLpCLM ((stdBasis n) p)) (toLpCLM ((stdBasis n) q))).re = if p = q then 1 else 0

The standard basis is orthonormal for the real part of the inner product: p = 2·(p/2) + p%2.

theorem Projectivization.toMatrix_fsModelMetric_zero {n : ℕ} : (LinearMap.BilinForm.toMatrix (stdBasis n)) (fsModelMetric 0) = 4 • 1

theorem Projectivization.det_toMatrix_fsModelMetric_zero {n : ℕ} : ((LinearMap.BilinForm.toMatrix (stdBasis n)) (fsModelMetric 0)).det = 4 ^ (2 * n)

The Gram determinant everywhere

theorem Projectivization.det_toMatrix_fsModelMetric {n : ℕ} (w : Fin n → ℂ) : ((LinearMap.BilinForm.toMatrix (stdBasis n)) (fsModelMetric w)).det = (4 ^ n * (1 + ‖toLpCLM w‖ ^ 2)⁻¹ ^ (n + 1)) ^ 2

★★ The Gram determinant of the model metric against the standard basis is (4ⁿ (1 + ‖w‖²)^{-(n+1)})², everywhere on the chart.

The Riemannian density is the top-form density over n!

theorem Projectivization.chartDensity_fsMetric {n : ℕ} (x₀ : Projectivization ℂ (Ambient n)) {w : Fin n → ℂ} (hw : w ∈ (chartAt (Fin n → ℂ) x₀).target) : MetricFamily.chartDensity (stdBasis n) fsMetric x₀ w = (↑n.factorial)⁻¹ * DifferentialForm.chartDensity (stdBasis n) (fun (x : Projectivization ℂ (Ambient n)) => (fsTopForm n) x) x₀ w

★★ The Riemannian chart density of the Fubini–Study metric is 1/n! times the density of ω_FS^{∧n}, in every affine chart.

theorem Projectivization.riemannianVolume_fsMetric {n : ℕ} : MetricFamily.riemannianVolume MeasureTheory.volume (stdBasis n) fsMetric (affineChartCover n) = (↑n.factorial)⁻¹ • fsVolume n

★★★ The Riemannian volume of the Fubini–Study metric IS the symplectic volume over n!: vol_g = fsVolume n / n! — the Kähler identity vol_g = ω^{∧n}/n! at the level of measures.

theorem Projectivization.riemannianVolume_fsMetric_eq_smul_fsMeasure {n : ℕ} (p₀ : Projectivization ℂ (EuclideanSpace ℂ (Fin (n + 1)))) : MetricFamily.riemannianVolume MeasureTheory.volume (stdBasis n) fsMetric (affineChartCover n) = ENNReal.ofReal ((4 * Real.pi) ^ n / ↑n.factorial) • Matrix.UnitaryGroup.fsMeasure p₀

★★★ The Fubini–Study measure is the normalised Riemannian volume of the Fubini–Study metric: vol_g = ((4π)ⁿ/n!) · μ_FS.

The Fubini–Study metric is bilinear, so its Riemannian volume is canonical (Q30)

theorem Projectivization.isBilinear_fsMetric {n : ℕ} : MetricFamily.IsBilinear fsMetric

The Fubini–Study metric is bilinear at every point: fsJ is ℝ-linear (it is i·) and fsForm x is bilinear (apply_add_left and friends).

theorem Projectivization.riemannianVolume_fsMetric_congr_cover {n : ℕ} (c : ChartCover (Fin n → ℂ) (Projectivization ℂ (Ambient n))) : MetricFamily.riemannianVolume MeasureTheory.volume (stdBasis n) fsMetric c = (↑n.factorial)⁻¹ • fsVolume n

★ The Riemannian volume of the Fubini–Study metric is canonical: it does not depend on the chart cover (riemannianVolume_congr_cover, from bilinearity) — so riemannianVolume_fsMetric is a statement about the Riemannian volume, not about the affine cover's.