The unitary action on ℂℙⁿ in charts, and the invariance of the Fubini–Study form

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 unitary group U(n+1) acts on ℂℙⁿ (Projectivization/Unitary.lean); read from the affine chart i to the affine chart j, a unitary U is the map uTrans U i j : w ↦ coordRatio j (U (insertOne i w)), a linear-fractional map, holomorphic wherever the j-th coordinate of U (insertOne i w) does not vanish. Under it the Fubini–Study potential shifts by -2 log ‖·‖ of that coordinate — an affine, hence pluriharmonic, correction — so the chart form is invariant:

• Kahler.ddcForm_log_norm_eq_zero_of_holomorphic — log ‖f‖ is pluriharmonic off the zeros of a holomorphic f (the linear case ddcForm_log_norm_eq_zero of KahlerPluriharmonic.lean, with L replaced by any holomorphic f; this is what lets the affine coordinate of the unitary action be handled);
• norm_toEuclideanLinearEquiv — a unitary preserves the Euclidean norm;
• uTrans, uTransE — the chart expression of the action; smul_chartInv, chartFun_smul_chartInv — it is what the action does to a chart inverse; contDiffOn_uTrans, contDiffAt_uTransE — holomorphy on its domain;
• fsPotential_uTransE — the potential's pluriharmonic shift;
• ★ fsChartForm_uTransE — the Fubini–Study chart form is invariant under the unitary action, read from chart i to chart j: (U^* ω_j) = ω_i on the overlap;
• ★ fsModelForm_uTrans — the same on the Fin n → ℂ model the manifold is charted on.

Honest scope

⚠️ Chart statements only. The manifold-level statement "fsForm is U(n+1)-invariant" is consumed directly in this chart form by the volume-invariance argument (Instances/ProjectiveSpaceFubiniStudyVolume.lean); no pullback of forms along maps of manifolds is defined here (that general API is not built).

⚠️ The j = i case of the chart transition needed a case split in fsChartForm_transE; the holomorphic-f formulation of pluriharmonicity removes it here.

Provenance and references. The top-power plan (M4); Geometry/Manifold/Instances/ProjectiveSpaceFubiniStudy.lean (the chart-transition invariance this mirrors); Analysis/InnerProductSpace/KahlerPluriharmonic.lean; LinearAlgebra/Projectivization/Unitary.lean (the action); the completed-work ledger.

theorem Kahler.ddcForm_log_norm_eq_zero_of_holomorphic {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {f : E → ℂ} {x : E} (hf : ContDiffAt ℂ ⊤ f x) (hx : f x ≠ 0) : ddcForm (fun (w : E) => Real.log ‖f w‖) x = 0

log ‖f‖ is pluriharmonic off the zeros of a holomorphic f.

theorem Projectivization.norm_toEuclideanLinearEquiv {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin (n + 1)) ℂ)) (v : Ambient n) : ‖(Matrix.UnitaryGroup.toEuclideanLinearEquiv U) v‖ = ‖v‖

A unitary matrix preserves the Euclidean norm.

noncomputable def Projectivization.uTrans {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin (n + 1)) ℂ)) (i j : Fin (n + 1)) : (Fin n → ℂ) → Fin n → ℂ

The chart expression of the unitary action, from chart i to chart j, on the Pi model.

Equations

• Projectivization.uTrans U i j w = Projectivization.coordRatio j ((Matrix.UnitaryGroup.toEuclideanLinearEquiv U) (Projectivization.insertOne i w))

noncomputable def Projectivization.uTransE {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin (n + 1)) ℂ)) (i j : Fin (n + 1)) : EuclideanSpace ℂ (Fin n) → EuclideanSpace ℂ (Fin n)

The same on the Euclidean model.

Equations

• Projectivization.uTransE U i j z = WithLp.toLp 2 (Projectivization.uTrans U i j z.ofLp)

theorem Projectivization.uTransE_eq {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin (n + 1)) ℂ)) (i j : Fin (n + 1)) : uTransE U i j = ⇑toLpCLM ∘ uTrans U i j ∘ ⇑(PiLp.continuousLinearEquiv 2 ℝ fun (x : Fin n) => ℂ)

theorem Projectivization.smul_chartInv {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin (n + 1)) ℂ)) (i : Fin (n + 1)) (w : Fin n → ℂ) : U • chartInv i w = mk ℂ ((Matrix.UnitaryGroup.toEuclideanLinearEquiv U) (insertOne i w)) ⋯

The action on a chart inverse.

theorem Projectivization.chartFun_smul_chartInv {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin (n + 1)) ℂ)) (i j : Fin (n + 1)) (w : Fin n → ℂ) : chartFun j (U • chartInv i w) = uTrans U i j w

theorem Projectivization.contDiff_uAct_coord {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin (n + 1)) ℂ)) (i k : Fin (n + 1)) : ContDiff ℂ ⊤ fun (w : Fin n → ℂ) => ((Matrix.UnitaryGroup.toEuclideanLinearEquiv U) (insertOne i w)).ofLp k

The coordinates of U (insertOne i w) are holomorphic (affine) in w.

theorem Projectivization.contDiffOn_uTrans {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin (n + 1)) ℂ)) (i j : Fin (n + 1)) : ContDiffOn ℂ ⊤ (uTrans U i j) {w : Fin n → ℂ | ((Matrix.UnitaryGroup.toEuclideanLinearEquiv U) (insertOne i w)).ofLp j ≠ 0}

theorem Projectivization.isOpen_uDomain {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin (n + 1)) ℂ)) (i j : Fin (n + 1)) : IsOpen {w : Fin n → ℂ | ((Matrix.UnitaryGroup.toEuclideanLinearEquiv U) (insertOne i w)).ofLp j ≠ 0}

theorem Projectivization.contDiffAt_uTransE {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin (n + 1)) ℂ)) (i j : Fin (n + 1)) {z : EuclideanSpace ℂ (Fin n)} (hz : ((Matrix.UnitaryGroup.toEuclideanLinearEquiv U) (insertOne i z.ofLp)).ofLp j ≠ 0) : ContDiffAt ℂ ⊤ (uTransE U i j) z

theorem Projectivization.fsPotential_uTransE {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin (n + 1)) ℂ)) (i j : Fin (n + 1)) {z : EuclideanSpace ℂ (Fin n)} (hz : ((Matrix.UnitaryGroup.toEuclideanLinearEquiv U) (insertOne i z.ofLp)).ofLp j ≠ 0) : Kahler.fsPotential (uTransE U i j z) = Kahler.fsPotential z - 2 * Real.log ‖((Matrix.UnitaryGroup.toEuclideanLinearEquiv U) (insertOne i z.ofLp)).ofLp j‖

The potential transforms by a pluriharmonic correction under the unitary action.

theorem Projectivization.fsChartForm_uTransE {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin (n + 1)) ℂ)) (i j : Fin (n + 1)) {z : EuclideanSpace ℂ (Fin n)} (hz : ((Matrix.UnitaryGroup.toEuclideanLinearEquiv U) (insertOne i z.ofLp)).ofLp j ≠ 0) : (Kahler.fsChartForm (uTransE U i j z)).compContinuousLinearMap (fderiv ℝ (uTransE U i j) z) = Kahler.fsChartForm z

★ Invariance of the Fubini–Study chart form under the unitary action, in charts.

theorem Projectivization.fsModelForm_uTrans {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin (n + 1)) ℂ)) (i j : Fin (n + 1)) {w : Fin n → ℂ} (hw : ((Matrix.UnitaryGroup.toEuclideanLinearEquiv U) (insertOne i w)).ofLp j ≠ 0) : (fsModelForm (uTrans U i j w)).compContinuousLinearMap (fderiv ℝ (uTrans U i j) w) = fsModelForm w

★ Invariance of the Fubini–Study model form under the unitary action, on the Pi model.