The Schrödinger field on ℂℙⁿ is holomorphic, and its flow is holomorphic and Killing

TERM-SCOPE(Hamiltonian) TERM-SCOPE(Kahler) — this module uses the restricted senses of "Hamiltonian" and "Kähler"; specs/TERMS.md records what is backed and what is not.

Category: 1-Mathlib (CSD-free; upstream target Mathlib.Geometry.Manifold.Instances).

KG-3′ (specs/BACKLOG.md #30). ProjectiveSpaceFubiniStudySymplectic.lean made ℂℙⁿ a Kähler manifold with J = i· in every chart (fsForm_isKahler), and ProjectiveSpaceSchrodingerFlow.lean made the Schrödinger flow p ↦ exp(-itH) • p the Hamiltonian flow of −2⟨H⟩ for the Fubini–Study form. The one step of the Ashtekar–Schilling route that the flow's unitarity carries but no theorem yet stated is that this Hamiltonian vector field is holomorphic, equivalently (by the Kähler compatibility) Killing. Both are here:

• ★ hasMFDerivAt_smul, isHolomorphicMap_smul — the unitary action on ℂℙⁿ is a holomorphic map: in charts it is uTrans U, ℂ-differentiable, so its manifold derivative commutes with J = i·;
• ★ fsForm_smul_mfderiv — the unitary action is symplectic at bundle level, U^* ω_FS = ω_FS (fsModelForm_uTrans read through the tangent spaces);
• ★ fsMetric_smul_mfderiv — the unitary action is an isometry of the Fubini–Study metric g = ω_FS (J ·, ·) (IsAlmostKahler.metric_mfderiv_eq);
• ★★ isHolomorphicMap_hamiltonianFlow_schrodinger, fsMetric_hamiltonianFlow_schrodinger — the Hamiltonian flow of −2⟨H⟩ is holomorphic and Killing at every time, through hamiltonianFlow_schrodingerHamiltonian;
• chartField_schrodingerField — the Schrödinger field read in any affine chart is schrodingerChartField in that chart (uniqueness of the local Hamiltonian vector);
• differentiableAt_schrodingerChartField — the chart field is ℂ-differentiable (it is a quadratic polynomial with complex coefficients);
• ★★ isHolomorphicVectorField_schrodingerField — X_{−2⟨H⟩} is a holomorphic vector field of the Kähler manifold ℂℙⁿ: in every chart its derivative commutes with i·.

Honest scope

⚠️ Holomorphic in the atlas sense (IsHolomorphicVectorField, HolomorphicVectorField.lean): the chart-by-chart statement, which on the holomorphic atlas of ℂℙⁿ is the standard notion. No Lie derivative L_X J is built; the flow-level statements need none.

⚠️ Hermitian H only, as everywhere in the Schrödinger module (hH : H.IsHermitian); the chart-field lemmas hold for any H.

References: Geometry/Manifold/Instances/ProjectiveSpaceSchrodingerFlow.lean (schrodingerField, hamiltonianFlow_schrodingerHamiltonian); Geometry/Manifold/Instances/ProjectiveSpaceFubiniStudySymplectic.lean (fsJ, fsForm_isKahler, fderiv_chart_transition_smul_I); Geometry/Manifold/Instances/ProjectiveSpaceUnitaryAction.lean (uTrans, fsModelForm_uTrans); Geometry/Manifold/HolomorphicVectorField.lean; specs/BACKLOG.md (#30); specs/future-work.md (KG-3).

The unitary action is holomorphic, symplectic and Killing

theorem Projectivization.chartFun_mem_uDomain {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin (n + 1)) ℂ)) (x : Projectivization ℂ (Ambient n)) : ((Matrix.UnitaryGroup.toEuclideanLinearEquiv U) (insertOne x.idx (chartFun x.idx x))).ofLp (U • x).idx ≠ 0

The chart point of x lies in the domain where the chart expression of U • from the chart at x to the chart at U • x is defined.

theorem Projectivization.differentiableAt_uTrans_chartFun {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin (n + 1)) ℂ)) (x : Projectivization ℂ (Ambient n)) : DifferentiableAt ℂ (uTrans U x.idx (U • x).idx) (chartFun x.idx x)

The chart expression of the unitary action is ℂ-differentiable at the chart point.

theorem Projectivization.hasMFDerivAt_smul {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin (n + 1)) ℂ)) (x : Projectivization ℂ (Ambient n)) : HasMFDerivAt% (fun (p : Projectivization ℂ (Ambient n)) => U • p) x (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ (uTrans U x.idx (U • x).idx) (chartFun x.idx x)))

★ The manifold derivative of the unitary action is the real restriction of the complex derivative of its chart expression uTrans U.

theorem Projectivization.mfderiv_smul_eq {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin (n + 1)) ℂ)) (x : Projectivization ℂ (Ambient n)) : (mfderiv% fun (p : Projectivization ℂ (Ambient n)) => U • p) x = ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ (uTrans U x.idx (U • x).idx) (chartFun x.idx x))

theorem Projectivization.isHolomorphicMap_smul {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin (n + 1)) ℂ)) : DifferentialForm.IsHolomorphicMap fsJ fun (p : Projectivization ℂ (Ambient n)) => U • p

★ The unitary action is a holomorphic map of ℂℙⁿ: its derivative commutes with J = i·.

theorem Projectivization.fsForm_smul_mfderiv {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin (n + 1)) ℂ)) (x : Projectivization ℂ (Ambient n)) (a b : TangentSpace (modelWithCornersSelf ℝ (Fin n → ℂ)) x) : (fsForm (U • x)) ![((mfderiv% fun (p : Projectivization ℂ (Ambient n)) => U • p) x) a, ((mfderiv% fun (p : Projectivization ℂ (Ambient n)) => U • p) x) b] = (fsForm x) ![a, b]

★ The unitary action is symplectic at bundle level: U^* ω_FS = ω_FS, read on the tangent spaces.

theorem Projectivization.fsMetric_smul_mfderiv {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin (n + 1)) ℂ)) (x : Projectivization ℂ (Ambient n)) (a b : TangentSpace (modelWithCornersSelf ℝ (Fin n → ℂ)) x) : ⋯.metric (U • x) (((mfderiv% fun (p : Projectivization ℂ (Ambient n)) => U • p) x) a) (((mfderiv% fun (p : Projectivization ℂ (Ambient n)) => U • p) x) b) = ⋯.metric x a b

★ The unitary action is an isometry of the Fubini–Study metric g = ω_FS (J ·, ·): symplectic and holomorphic, hence Killing.

The Hamiltonian flow of −2⟨H⟩ is holomorphic and Killing

theorem Projectivization.hamiltonianFlow_schrodingerHamiltonian_eq {n : ℕ} {H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ} (hH : H.IsHermitian) (t : ℝ) : ⋯.hamiltonianFlow ⋯ t = fun (p : Projectivization ℂ (Ambient n)) => Matrix.schrodingerUnitary hH t • p

theorem Projectivization.isHolomorphicMap_hamiltonianFlow_schrodinger {n : ℕ} {H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ} (hH : H.IsHermitian) (t : ℝ) : DifferentialForm.IsHolomorphicMap fsJ (⋯.hamiltonianFlow ⋯ t)

★★ The Hamiltonian flow of −2⟨H⟩ on ℂℙⁿ is holomorphic at every time: its derivative commutes with J = i·.

theorem Projectivization.fsMetric_hamiltonianFlow_schrodinger {n : ℕ} {H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ} (hH : H.IsHermitian) (t : ℝ) (x : Projectivization ℂ (Ambient n)) (a b : TangentSpace (modelWithCornersSelf ℝ (Fin n → ℂ)) x) : ⋯.metric (⋯.hamiltonianFlow ⋯ t x) ((mfderiv% (⋯.hamiltonianFlow ⋯ t) x) a) ((mfderiv% (⋯.hamiltonianFlow ⋯ t) x) b) = ⋯.metric x a b

★★ The Hamiltonian flow of −2⟨H⟩ on ℂℙⁿ is Killing at every time: it preserves the Fubini–Study metric.

The Schrödinger field is a holomorphic vector field

theorem Projectivization.chartField_schrodingerField {n : ℕ} {H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ} (hH : H.IsHermitian) (x₀ : Projectivization ℂ (Ambient n)) (w : Fin n → ℂ) : chartField (schrodingerField H) x₀ w = schrodingerChartField H x₀.idx w

The Schrödinger field read in the affine chart at x₀ is schrodingerChartField in that chart, at every point of the chart: both are the local Hamiltonian vector of −2⟨H⟩ for the model form, which is unique.

theorem Projectivization.differentiableAt_mulVec_insertOne {n : ℕ} (H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ) (i k : Fin (n + 1)) (w : Fin n → ℂ) : DifferentiableAt ℂ (fun (w : Fin n → ℂ) => H.mulVec (insertOne i w).ofLp k) w

The entry k of H (insertOne i w) is a ℂ-affine function of w.

theorem Projectivization.differentiableAt_schrodingerChartField {n : ℕ} (H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ) (i : Fin (n + 1)) (w : Fin n → ℂ) : DifferentiableAt ℂ (schrodingerChartField H i) w

The Schrödinger chart field is ℂ-differentiable: a quadratic polynomial in w with complex coefficients.

theorem Projectivization.isHolomorphicVectorField_schrodingerField {n : ℕ} {H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ} (hH : H.IsHermitian) : DifferentialForm.IsHolomorphicVectorField modelJ (schrodingerField H)

★★ The Schrödinger field is a holomorphic vector field of the Kähler manifold ℂℙⁿ: in every affine chart its derivative commutes with J = i·. With schrodingerField_eq_hamiltonianVectorField, the Hamiltonian vector field of −2⟨H⟩ is holomorphic.