The volume of the top power of the Fubini–Study form

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

Category: 1-Mathlib (CSD-free).

The uniqueness route to the Fubini–Study volume. The 2n-form fsTopForm n (the n-th exterior power of the Fubini–Study form, ProjectiveSpaceFubiniStudyForm.lean) has a measure on ℂℙⁿ (TopFormMeasure.lean, against Lebesgue measure on the model Fin n → ℂ and the affine chart cover). This module shows it is U(n+1)-invariant, finite and nonzero, and concludes:

• stdBasis n — the standard real basis of Fin n → ℂ, indexed by Fin (2n);
• fsVolume n — the volume measure of the top power of the Fubini–Study form;
• chartAt_smul_comp_symm, smul_symm_mem_source_iff — the chart expression of U • · is uTrans U (idx x₀) (idx z), defined where the action lands in the target chart;
• localRep_fsSection', localRep_fsTopForm — the local representative of the top power in every chart is the flat power of the model form;
• ★★ fsVolume_map_smul — fsVolume n is invariant under the unitary group (topFormMeasure_map_eq with the chart invariance fsModelForm_uTrans lifted to the top power by wedgePow_compContinuousLinearMap);
• ★ isFiniteMeasure_fsVolume — it is finite (isFiniteMeasure_topFormMeasure: locally finite on a compact manifold);
• fsVolumeNormalized n — the normalised volume, with fsVolumeNormalized_map_smul; isProbabilityMeasure_fsVolumeNormalized_of_ne_zero and fsVolumeNormalized_eq_fsMeasure_of_ne_zero are the conclusions under the premise fsVolume n ≠ 0 (fsMeasure_unique applied to a U(n+1)-invariant probability measure);
• The flat count — stdForm n (the standard symplectic form on the model, fundamentalFormAlt through toLpCLM; fsModelForm_zero: the model form at the origin is -4 • stdForm n), pairFamily a (the k standard pairs (e_{a i}, i e_{a i})), isWeightedPairTuple_pairFamily (they are a pair tuple for stdForm, WedgePowPairs.lean), and ★★ wedgePow_stdForm_pairFamily — the k-th power of the standard symplectic form on k distinct standard pairs is k!, the general count wedgePow_apply_of_isPairTuple (by induction on k through the shuffle sum wedge_mul_apply_weightedPairs: each of the k + 1 surviving classes removes one pair and contributes k!). On the standard basis (stdBasis_eq_pairFamily), ★★ wedgePow_fsModelForm_zero_stdBasis: the coefficient of the top power at the origin is (-4)ⁿ · n!, in particular nonzero;
• ★★ fsVolume_ne_zero — the volume is nonzero (topFormMeasure_ne_zero_of_localRep_ne_zero at the origin of the chart at origin 0), so isProbabilityMeasure_fsVolumeNormalized holds unconditionally;
• ★★★ fsVolumeNormalized_eq_fsMeasure — the normalised volume of the top power of the Fubini–Study form IS the Fubini–Study measure, fsMeasure p₀, for every base point p₀. No premise.

Honest scope

⚠️ No constant here. The identity of this module is for the normalised measure; (-4)ⁿ n! is the coefficient at one point, not the total mass. The mass, (4π)ⁿ, and the identity with its constant are ProjectiveSpaceFubiniStudyMass.lean.

⚠️ n ≥ 1 is not assumed and not needed: for n = 0 the manifold is a point, the top power is the constant 0-form 1 (wedgePow_stdForm_pairFamily at k = 0), and every statement holds.

⚠️ The count here is for the standard form on the standard pairs; the general count on a weighted pair tuple is WedgePowPairs.lean, and fsModelForm w away from w = 0 is ProjectiveSpaceFubiniStudyMass.lean (the measure argument here needs one point).

Provenance and references. The top-power plan (M5, M6); Geometry/Manifold/TopFormMeasure.lean (topFormMeasure_map_eq, isFiniteMeasure_topFormMeasure, topFormMeasure_ne_zero_of_localRep_ne_zero); Geometry/Manifold/WedgePowPairs.lean (wedgePow_apply_of_isPairTuple); Geometry/Manifold/Instances/ProjectiveSpaceUnitaryAction.lean (fsModelForm_uTrans); Geometry/Manifold/WedgeForm.lean (localRep_wedgePow, wedgePow_compContinuousLinearMap); LinearAlgebra/Projectivization/FubiniStudyUnique.lean (★★ fsMeasure_unique); the terms register (Liouville); the completed-work ledger.

noncomputable def Projectivization.stdBasis (n : ℕ) : Module.Basis (Fin (2 * n)) ℝ (Fin n → ℂ)

The standard real basis of the model Fin n → ℂ, indexed by Fin (2n).

Equations

• Projectivization.stdBasis n = (Pi.basis fun (x : Fin n) => Complex.basisOneI).reindex (Complex.sigmaFinTwoEquiv n)

noncomputable def Projectivization.fsVolume (n : ℕ) : MeasureTheory.Measure (Projectivization ℂ (Ambient n))

The volume of the top power of the Fubini–Study form: the measure of the 2n-form fsTopForm n on ℂℙⁿ, against Lebesgue measure on the model and the affine chart cover.

Equations

• One or more equations did not get rendered due to their size.

fsVolume is the canonical measure of its top form

topFormMeasure takes a Haar measure and a basis; fsVolume uses Lebesgue measure and the standard basis. Lebesgue measure IS the standard basis' own Haar measure (stdBasis_addHaar), so by topFormMeasure_addHaar_basis the choice of basis is immaterial: fsVolume is the intrinsic measure of fsTopForm (fsVolume_eq_topFormMeasure_addHaar).

theorem Projectivization.stdBasis_addHaar (n : ℕ) : (stdBasis n).addHaar = MeasureTheory.volume

★ The standard basis' Haar measure is Lebesgue measure on Fin n → ℂ (Complex.addHaar_pi_basisOneI_reindex).

theorem Projectivization.fsVolume_eq_topFormMeasure_addHaar {n : ℕ} (b : Module.Basis (Fin (2 * n)) ℝ (Fin n → ℂ)) : fsVolume n = DifferentialForm.topFormMeasure b.addHaar b (fun (x : Projectivization ℂ (Ambient n)) => (fsTopForm n) x) (affineChartCover n)

★ fsVolume is the canonical measure of fsTopForm: against any basis of the model and that basis' own Haar measure, the glued measure is fsVolume.

The action in charts

theorem Projectivization.chartAt_smul_comp_symm {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin (n + 1)) ℂ)) (x₀ z : Projectivization ℂ (Ambient n)) : ↑(chartAt (Fin n → ℂ) z) ∘ (fun (p : Projectivization ℂ (Ambient n)) => U • p) ∘ ↑(chartAt (Fin n → ℂ) x₀).symm = uTrans U x₀.idx z.idx

The chart expression of the unitary action, from the chart at x₀ to the chart at z, is uTrans U (idx x₀) (idx z).

theorem Projectivization.smul_symm_mem_source_iff {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin (n + 1)) ℂ)) (x₀ z : Projectivization ℂ (Ambient n)) (w : Fin n → ℂ) : U • ↑(chartAt (Fin n → ℂ) x₀).symm w ∈ (chartAt (Fin n → ℂ) z).source ↔ ((Matrix.UnitaryGroup.toEuclideanLinearEquiv U) (insertOne x₀.idx w)).ofLp z.idx ≠ 0

Local representatives of the form and its top power

theorem Projectivization.localRep_fsSection' {n : ℕ} (x₀ : Projectivization ℂ (Ambient n)) (w : Fin n → ℂ) : DifferentialForm.localRep fsSection x₀ w = fsModelForm w

The local representative of the Fubini–Study section, in localRep form.

theorem Projectivization.localRep_fsTopForm {n : ℕ} (x₀ : Projectivization ℂ (Ambient n)) (w : Fin n → ℂ) : DifferentialForm.localRep (fun (x : Projectivization ℂ (Ambient n)) => (fsTopForm n) x) x₀ w = (fsModelForm w).wedgePow n

The local representative of the top power is the flat power of the model form.

Invariance and finiteness

theorem Projectivization.fsVolume_map_smul {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin (n + 1)) ℂ)) : MeasureTheory.Measure.map (fun (p : Projectivization ℂ (Ambient n)) => U • p) (fsVolume n) = fsVolume n

★★ The Fubini–Study volume is invariant under the unitary group.

instance Projectivization.isFiniteMeasure_fsVolume (n : ℕ) : MeasureTheory.IsFiniteMeasure (fsVolume n)

★ The Fubini–Study volume is a finite measure (ℂℙⁿ is compact and the density is continuous).

The normalised volume and the identity

noncomputable def Projectivization.fsVolumeNormalized (n : ℕ) : MeasureTheory.Measure (Projectivization ℂ (Ambient n))

The Fubini–Study volume, normalised to total mass one.

Equations

• Projectivization.fsVolumeNormalized n = ((Projectivization.fsVolume n) Set.univ)⁻¹ • Projectivization.fsVolume n

theorem Projectivization.fsVolumeNormalized_map_smul {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin (n + 1)) ℂ)) : MeasureTheory.Measure.map (fun (p : Projectivization ℂ (Ambient n)) => U • p) (fsVolumeNormalized n) = fsVolumeNormalized n

theorem Projectivization.isProbabilityMeasure_fsVolumeNormalized_of_ne_zero {n : ℕ} (hne : fsVolume n ≠ 0) : MeasureTheory.IsProbabilityMeasure (fsVolumeNormalized n)

If the volume is nonzero, its normalisation is a probability measure.

theorem Projectivization.fsVolumeNormalized_eq_fsMeasure_of_ne_zero {n : ℕ} (hne : fsVolume n ≠ 0) (p₀ : Projectivization ℂ (EuclideanSpace ℂ (Fin (n + 1)))) : fsVolumeNormalized n = Matrix.UnitaryGroup.fsMeasure p₀

★★ The identity under the premise that the volume is nonzero: fsMeasure_unique applied to a U(n+1)-invariant probability measure. The premise is discharged below (fsVolume_ne_zero).

The flat count: the top power of the model form at the origin (M6(b))

noncomputable def Projectivization.stdForm (n : ℕ) : (Fin n → ℂ) [⋀^Fin 2]→L[ℝ] ℝ

The standard symplectic form on the model Fin n → ℂ: the flat fundamental form Kahler.fundamentalFormAlt read through toLpCLM.

Equations

• Projectivization.stdForm n = Kahler.fundamentalFormAlt.compContinuousLinearMap Projectivization.toLpCLM

theorem Projectivization.fsModelForm_zero {n : ℕ} : fsModelForm 0 = -4 • stdForm n

At the origin the model form is -4 times the standard form (fsChartForm_zero).

theorem Projectivization.stdForm_single {n : ℕ} (j j' : Fin n) (x y : ℂ) : (stdForm n) ![Pi.single j x, Pi.single j' y] = if j = j' then ((starRingEnd ℂ) x * y).im else 0

The standard form on two coordinate vectors: Im (conj x · y) on the same coordinate, 0 on different ones.

theorem Projectivization.im_conj_mul_pairs (a b : Fin 2) : ((starRingEnd ℂ) (![1, Complex.I] a) * ![1, Complex.I] b).im = ContinuousAlternatingMap.pairSign a b

On the pair (1, i) the imaginary part of conj · × · is pairSign.

def Projectivization.pairFamily {n k : ℕ} (a : Fin k → Fin n) : Fin (2 * k) → Fin n → ℂ

The family of k standard pairs (e_{a i}, i • e_{a i}), in order.

Equations

• Projectivization.pairFamily a p = Pi.single (a (ContinuousAlternatingMap.pairIdx p)) (![1, Complex.I] (ContinuousAlternatingMap.memIdx p))

theorem Projectivization.pairFamily_def {n k : ℕ} (a : Fin k → Fin n) : pairFamily a = fun (p : Fin (2 * k)) => Pi.single (a (ContinuousAlternatingMap.pairIdx p)) (![1, Complex.I] (ContinuousAlternatingMap.memIdx p))

pairFamily, unfolded: the definitional equation.

theorem Projectivization.isWeightedPairTuple_pairFamily {n k : ℕ} (a : Fin k → Fin n) (ha : Function.Injective a) : (stdForm n).IsWeightedPairTuple (fun (x : Fin k) => 1) (pairFamily a)

The standard pairs are a pair tuple for the standard form (all weights 1).

theorem Projectivization.wedgePow_stdForm_pairFamily {n : ℕ} (k : ℕ) (a : Fin k → Fin n) (ha : Function.Injective a) : ((stdForm n).wedgePow k) (pairFamily a) = ↑k.factorial

★★ The count. The k-th power of the standard symplectic form on k distinct standard pairs is k! (wedgePow_apply_of_isPairTuple).

theorem Projectivization.stdBasis_eq_pairFamily {n : ℕ} (p : Fin (2 * n)) : (stdBasis n) p = pairFamily id p

The standard basis is the pair family of the identity.

theorem Projectivization.wedgePow_fsModelForm_zero_stdBasis {n : ℕ} : ((fsModelForm 0).wedgePow n) ⇑(stdBasis n) = (-4) ^ n * ↑n.factorial

★★ The coefficient of the top power at the origin, on the standard basis, is (-4)ⁿ · n!.

theorem Projectivization.wedgePow_fsModelForm_zero_stdBasis_ne_zero {n : ℕ} : ((fsModelForm 0).wedgePow n) ⇑(stdBasis n) ≠ 0

Non-vanishing, and the identity

theorem Projectivization.fsVolume_ne_zero (n : ℕ) : fsVolume n ≠ 0

★★ The Fubini–Study volume is nonzero: the coefficient of the top power against the standard basis at the origin of the chart at origin 0 is (-4)ⁿ · n!.

instance Projectivization.isProbabilityMeasure_fsVolumeNormalized (n : ℕ) : MeasureTheory.IsProbabilityMeasure (fsVolumeNormalized n)

The normalised Fubini–Study volume is a probability measure.

theorem Projectivization.fsVolumeNormalized_eq_fsMeasure {n : ℕ} (p₀ : Projectivization ℂ (EuclideanSpace ℂ (Fin (n + 1)))) : fsVolumeNormalized n = Matrix.UnitaryGroup.fsMeasure p₀

★★★ The normalised volume of the top power of the Fubini–Study form is the Fubini–Study measure, for every base point p₀.