The Fubini–Study chart form is invariant under the chart transitions of ℂℙⁿ

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

The mathematical heart of "the Fubini–Study form is a global object on ℂℙⁿ". The chart form fsChartForm = dd^c log(1 + ‖z‖²) (KahlerPotential.lean) is defined chart by chart; this module proves that the affine-chart transitions of ProjectiveSpace.lean carry the form in chart j to the form in chart i:

• fsPotential_transE — under the transition i → j the potential changes by -2 log ‖zⱼ‖, a pluriharmonic correction (the classical 1 + ‖τ z‖² = (1 + ‖z‖²)/‖zⱼ‖²);
• ★ fsChartForm_transE — hence the form is invariant, τ^* ω_j = ω_i on the overlap: dd^c naturality (ddcForm_comp), linearity in the potential, and pluriharmonicity of log ‖L ·‖ for the coordinate functional L (ddcForm_log_norm_eq_zero); the j = i case is the identity transition;
• ★ fsModelForm_transP — the same on the Fin n → ℂ model the manifold is charted on, the form a bundle argument consumes.

Honest scope

Invariance of a family of flat forms under flat maps — exactly what assembling a global section of the alternating bundle on ℂℙⁿ needs; that assembly (the bundle-level local-representative identity and the section's smoothness) is ProjectiveSpaceFubiniStudyForm.lean (fsForm). Still no exterior derivative on the manifold (step (2b)): nothing here states dω = 0 on ℂℙⁿ.

Provenance and references. KahlerPotential.lean; KahlerPluriharmonic.lean; Geometry/Manifold/Instances/ProjectiveSpace.lean; Geometry/Manifold/Instances/ProjectiveSpaceFubiniStudyForm.lean (the consumer); the completed-work ledger.

theorem Kahler.ddcForm_congr {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {K₁ K₂ : E → ℝ} {x : E} (h : K₁ =ᶠ[nhds x] K₂) : ddcForm K₁ x = ddcForm K₂ x

L3: dd^c only sees the potential near the point.

noncomputable def Projectivization.transE {n : ℕ} (i j : Fin (n + 1)) : EuclideanSpace ℂ (Fin n) → EuclideanSpace ℂ (Fin n)

The chart transition i → j, read on the Euclidean model.

Equations

• Projectivization.transE i j z = WithLp.toLp 2 (Projectivization.coordRatio j (Projectivization.insertOne i z.ofLp))

theorem Projectivization.norm_sq_insertOne {n : ℕ} (i : Fin (n + 1)) (w : Fin n → ℂ) : ‖insertOne i w‖ ^ 2 = 1 + ∑ k : Fin n, ‖w k‖ ^ 2

theorem Projectivization.norm_sq_toLp_coordRatio {n : ℕ} (j : Fin (n + 1)) (v : Ambient n) : ‖WithLp.toLp 2 (coordRatio j v)‖ ^ 2 = (‖v‖ ^ 2 - ‖v.ofLp j‖ ^ 2) / ‖v.ofLp j‖ ^ 2

theorem Projectivization.fsPotential_toLp_coordRatio {n : ℕ} (j : Fin (n + 1)) (v : Ambient n) (hv : v.ofLp j ≠ 0) : Kahler.fsPotential (WithLp.toLp 2 (coordRatio j v)) = Real.log (‖v‖ ^ 2) - 2 * Real.log ‖v.ofLp j‖

theorem Projectivization.contDiffAt_transE {n : ℕ} (i j : Fin (n + 1)) {z : EuclideanSpace ℂ (Fin n)} (hz : (insertOne i z.ofLp).ofLp j ≠ 0) : ContDiffAt ℂ ⊤ (transE i j) z

theorem Projectivization.coordRatio_insertOne_self {n : ℕ} (i : Fin (n + 1)) (w : Fin n → ℂ) : coordRatio i (insertOne i w) = w

L1: the transition from a chart to itself is the identity.

theorem Projectivization.transE_self {n : ℕ} (i : Fin (n + 1)) : transE i i = id

theorem Projectivization.fsPotential_transE {n : ℕ} (i j : Fin (n + 1)) {z : EuclideanSpace ℂ (Fin n)} (hz : (insertOne i z.ofLp).ofLp j ≠ 0) : Kahler.fsPotential (transE i j z) = Kahler.fsPotential z - 2 * Real.log ‖(insertOne i z.ofLp).ofLp j‖

L4: the potential transforms by a pluriharmonic correction.

theorem Projectivization.fsChartForm_transE {n : ℕ} (i j : Fin (n + 1)) {z : EuclideanSpace ℂ (Fin n)} (hz : (insertOne i z.ofLp).ofLp j ≠ 0) : (Kahler.fsChartForm (transE i j z)).compContinuousLinearMap (fderiv ℝ (transE i j) z) = Kahler.fsChartForm z

★ L5: chart invariance of the Fubini–Study form. The pullback of the chart-j form along the transition from chart i is the chart-i form, wherever the transition is defined.

The form on the Fin n → ℂ model, and its invariance there

@[reducible, inline]

noncomputable abbrev Projectivization.toLpCLM {n : ℕ} : (Fin n → ℂ) →L[ℝ] EuclideanSpace ℂ (Fin n)

The Euclidean structure map, as an ℝ-continuous-linear map from the Pi model.

Equations

• Projectivization.toLpCLM = ↑(PiLp.continuousLinearEquiv 2 ℝ fun (x : Fin n) => ℂ).symm

noncomputable def Projectivization.fsModelForm {n : ℕ} (w : Fin n → ℂ) : (Fin n → ℂ) [⋀^Fin 2]→L[ℝ] ℝ

The Fubini–Study chart form transported to the Fin n → ℂ model.

Equations

• Projectivization.fsModelForm w = (Kahler.fsChartForm (Projectivization.toLpCLM w)).compContinuousLinearMap Projectivization.toLpCLM

noncomputable def Projectivization.transP {n : ℕ} (i j : Fin (n + 1)) : (Fin n → ℂ) → Fin n → ℂ

The Pi-model transition.

Equations

• Projectivization.transP i j w = Projectivization.coordRatio j (Projectivization.insertOne i w)

theorem Projectivization.transE_eq {n : ℕ} (i j : Fin (n + 1)) : transE i j = ⇑toLpCLM ∘ transP i j ∘ ⇑(PiLp.continuousLinearEquiv 2 ℝ fun (x : Fin n) => ℂ)

theorem Projectivization.fsModelForm_transP {n : ℕ} (i j : Fin (n + 1)) {w : Fin n → ℂ} (hw : (insertOne i w).ofLp j ≠ 0) : (fsModelForm (transP i j w)).compContinuousLinearMap (fderiv ℝ (transP i j) w) = fsModelForm w

★ B3c-1: chart invariance on the Pi model.