The moment map of the torus action on ℂℙⁿ, at manifold level

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

Category: 1-Mathlib (CSD-free; the torus moment map of ℂℙⁿ).

The torus T^{n+1} acts on ℂℙⁿ by p ↦ diag(e^{iθ}) • p. This module proves the moment-map equation for that action on the manifold: the velocity field of the action is the Hamiltonian vector field, for the Fubini–Study form fsForm, of 2 ∑ₖ θₖ · momentMap p k — then its uniqueness, its image, and the invariance of the Fubini–Study volume under the flow it generates.

• torusChartField i θ w — the velocity in the affine chart i, wⱼ ↦ i (θ_{sⱼ} − θᵢ) wⱼ; torusField θ — the same as a family over ℂℙⁿ, read in the chart at each point;
• torusUnitary θ — diag(e^{iθ}) as a unitary; chartFun_torusUnitary_smul (in the chart the action is the coordinatewise phase rotation); ★ hasDerivAt_chartFun_torusUnitary — the field is the velocity of the action: torusChartField is the t-derivative at 0 of t ↦ diag(e^{itθ}) • p read in the chart, and ★★★ isMIntegralCurve_torusUnitary_smul — the orbit t ↦ diag(e^{itθ}) • p is a global integral curve of torusField θ, so torusField is the fundamental vector field;
• torusHamiltonian θ p = 2 ∑ₖ θₖ · momentMap p k, its chart expression torusChartHam = 2N/D (torusHamiltonian_chartInv), the chart derivative (hasFDerivAt_torusChartHam, by the product and inverse rules from hasFDerivAt_normSq_coord), and ★ hasMFDerivAt_torusHamiltonian (the manifold derivative is the chart derivative);
• ★★ fsModelForm_torusChartField — the chart identity ω_w (X_w, v) = dH_w v, a real computation through fsModelForm_apply;
• ★★★ torusField_isHamiltonianVectorField — IsHamiltonianVectorField fsForm (torusField θ) (torusHamiltonian θ): the torus action on ℂℙⁿ is Hamiltonian, with 2 ∑ θₖ momentMap as its Hamiltonian. For θ = eᵢ: the i-th phase rotation is generated by 2 · momentMap · i, on the symplectic manifold. This is the manifold form of the linear-level statement that phase rotation is Hamiltonian;
• G8, uniqueness. momentMap_origin_of_ne, torusHamiltonian_single, ★★ eq_add_const_of_isHamiltonianVectorField — a Hamiltonian is unique up to a constant on ℂℙⁿ: two differentiable Hamiltonians of the same field for the same 2-form family differ by a constant. No connectedness lemma: every affine chart image is all of ℂⁿ (is_const_of_fderiv_eq_zero), and [1 : ⋯ : 1] (allOnes) lies in every chart; and ★★★ eq_torusHamiltonian_of_nonneg_of_sum — the normalisation pins the constant: a non-negative family of Hamiltonians for the phase fields summing to 2 is 2 · momentMap. This is the standard symplectic argument, formalised;
• G9, the image. momentMapSimplex (the moment map's value as a point of the bundled StdSimplex ℝ (Fin (n + 1))), sqrtVec (the vector (√t₀, …, √tₙ)), momentMap_mk_sqrtVec, ★★ momentMapSimplex_surjective and ★★ range_momentMap — the image of the moment map is exactly the standard simplex: the moment map onto the bundled simplex is surjective, and its range as a set of weight vectors is Set.range StdSimplex.weights (range_momentMap_eq_inter spells that out as non-negativity and the sum-one normalisation). ⊆ is the normalisation, ⊇ the ray of (√t₀, …, √tₙ);
• G10, the flow. torusUnitary_zero, torusUnitary_add, torusUnitary_add_smul (the one-parameter group law of t ↦ diag(e^{itθ})), and ★ fsVolume_map_torusUnitary_smul / measurePreserving_torusUnitary_smul — every time-t map of the torus flow preserves the Fubini–Study volume fsVolume n, a corollary of the unitary invariance fsVolume_map_smul.

Honest scope

⚠️ G8 is about the map the action has. It says that the map the torus action has is the momentMap; whether some dynamics generates the torus action is a different question, which nothing here addresses.

⚠️ The factor 2 is convention. fsChartForm carries the -4 of its potential log(1 + ‖z‖²); with that normalisation the generator of the phase rotation is 2 · momentMap. The linear-level statement (IsPhaseHamiltonian, coordEnergy = ‖xᵢ‖²/2) has its own convention; nothing here rescales either, and the statement shows the factor.

⚠️ A family, not a smooth section. torusField is a vector-field family; its smoothness as a section of the tangent bundle is not proved (that is brick G3's plumbing), and nothing here needs it: IsHamiltonianVectorField is pointwise.

⚠️ The polytope by computation, not by convexity. range_momentMap (G9) exhibits the image as the simplex for this action; the Atiyah–Guillemin–Sternberg convexity theorem is neither used nor proved.

⚠️ Liouville for one flow only. fsVolume_map_torusUnitary_smul (G10) is unitary invariance specialised to diag(e^{iθ}). It is not a manifold-level Liouville theorem for Hamiltonian flows (that is HamiltonianFlowVolume.lean's job).

⚠️ The torus here; the general generator in ProjectiveSpaceSchrodingerFlow.lean (G13). For a general Hermitian H the flow exp(-itH) • p is Hamiltonian with Hamiltonian -2 ⟨H⟩ (schrodingerField_isHamiltonianVectorField), and the torus is its diagonal case (schrodingerHamiltonian_neg_diagonal); the torus is what momentMap is about.

Provenance and references. The generator-layer plan (G6, G8–G10); Geometry/Manifold/HamiltonianVectorField.lean (G1); LinearAlgebra/Projectivization/MomentMap.lean (momentMap, momentMap_mk, continuous_momentMap); RecordLayer/CellLawForced.lean (IsPhaseHamiltonian, the linear-level equation); Instances/ProjectiveSpaceFubiniStudyMass.lean (fsModelForm_apply, toLpCLM_apply); Instances/ProjectiveSpaceUnitaryAction.lean (chartFun_smul_chartInv); Instances/ProjectiveSpaceFubiniStudyVolume.lean (fsVolume, fsVolume_map_smul); Mathlib/Geometry/Convex/ConvexSpace/Defs.lean (StdSimplex); the terms register (moment map, Hamiltonian, Liouville); the programme's posits (Posits 1 and 3); the completed-work ledger.

Chart data

def Projectivization.torusChartField {n : ℕ} (i : Fin (n + 1)) (θ : Fin (n + 1) → ℝ) (w : Fin n → ℂ) : Fin n → ℂ

The velocity of the torus action in the affine chart i: wⱼ ↦ i (θ_{s j} − θ_i) wⱼ.

Equations

• Projectivization.torusChartField i θ w j = Complex.I * ↑(θ (i.succAbove j) - θ i) * w j

theorem Projectivization.torusChartField_def {n : ℕ} (i : Fin (n + 1)) (θ : Fin (n + 1) → ℝ) (w : Fin n → ℂ) : torusChartField i θ w = fun (j : Fin n) => Complex.I * ↑(θ (i.succAbove j) - θ i) * w j

torusChartField, unfolded: the definitional equation.

noncomputable def Projectivization.torusChartNum {n : ℕ} (i : Fin (n + 1)) (θ : Fin (n + 1) → ℝ) (w : Fin n → ℂ) : ℝ

N w = θ_i + ∑ⱼ θ_{s j} ‖wⱼ‖².

Equations

• Projectivization.torusChartNum i θ w = θ i + ∑ j : Fin n, θ (i.succAbove j) * ‖w j‖ ^ 2

theorem Projectivization.torusChartNum_def {n : ℕ} (i : Fin (n + 1)) (θ : Fin (n + 1) → ℝ) (w : Fin n → ℂ) : torusChartNum i θ w = θ i + ∑ j : Fin n, θ (i.succAbove j) * ‖w j‖ ^ 2

torusChartNum, unfolded: the definitional equation.

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

D w = 1 + ∑ⱼ ‖wⱼ‖².

Equations

• Projectivization.chartDen w = 1 + ∑ j : Fin n, ‖w j‖ ^ 2

theorem Projectivization.chartDen_def {n : ℕ} (w : Fin n → ℂ) : chartDen w = 1 + ∑ j : Fin n, ‖w j‖ ^ 2

chartDen, unfolded: the definitional equation.

theorem Projectivization.chartDen_pos {n : ℕ} (w : Fin n → ℂ) : 0 < chartDen w

noncomputable def Projectivization.torusChartHam {n : ℕ} (i : Fin (n + 1)) (θ : Fin (n + 1) → ℝ) (w : Fin n → ℂ) : ℝ

The chart Hamiltonian 2 N / D.

Equations

• Projectivization.torusChartHam i θ w = 2 * (Projectivization.torusChartNum i θ w * (Projectivization.chartDen w)⁻¹)

theorem Projectivization.torusChartHam_def {n : ℕ} (i : Fin (n + 1)) (θ : Fin (n + 1) → ℝ) (w : Fin n → ℂ) : torusChartHam i θ w = 2 * (torusChartNum i θ w * (chartDen w)⁻¹)

torusChartHam, unfolded: the definitional equation.

Derivatives in the chart

noncomputable def Projectivization.normSqCoordDeriv {n : ℕ} (j : Fin n) (w : Fin n → ℂ) : (Fin n → ℂ) →L[ℝ] ℝ

The derivative of w ↦ ‖wⱼ‖².

Equations

• Projectivization.normSqCoordDeriv j w = (2 * (w j).re) • Complex.reCLM ∘SL ContinuousLinearMap.proj j + (2 * (w j).im) • Complex.imCLM ∘SL ContinuousLinearMap.proj j

theorem Projectivization.normSqCoordDeriv_apply {n : ℕ} (j : Fin n) (w v : Fin n → ℂ) : (normSqCoordDeriv j w) v = 2 * ((w j).re * (v j).re + (w j).im * (v j).im)

theorem Projectivization.hasFDerivAt_normSq_coord {n : ℕ} (j : Fin n) (w : Fin n → ℂ) : HasFDerivAt (fun (w : Fin n → ℂ) => ‖w j‖ ^ 2) (normSqCoordDeriv j w) w

noncomputable def Projectivization.torusChartNumDeriv {n : ℕ} (i : Fin (n + 1)) (θ : Fin (n + 1) → ℝ) (w : Fin n → ℂ) : (Fin n → ℂ) →L[ℝ] ℝ

The derivative of the numerator N.

Equations

• Projectivization.torusChartNumDeriv i θ w = ∑ j : Fin n, θ (i.succAbove j) • Projectivization.normSqCoordDeriv j w

noncomputable def Projectivization.chartDenDeriv {n : ℕ} (w : Fin n → ℂ) : (Fin n → ℂ) →L[ℝ] ℝ

The derivative of the denominator D.

Equations

• Projectivization.chartDenDeriv w = ∑ j : Fin n, Projectivization.normSqCoordDeriv j w

theorem Projectivization.hasFDerivAt_torusChartNum {n : ℕ} (i : Fin (n + 1)) (θ : Fin (n + 1) → ℝ) (w : Fin n → ℂ) : HasFDerivAt (torusChartNum i θ) (torusChartNumDeriv i θ w) w

theorem Projectivization.hasFDerivAt_chartDen {n : ℕ} (w : Fin n → ℂ) : HasFDerivAt chartDen (chartDenDeriv w) w

noncomputable def Projectivization.torusChartHamDeriv {n : ℕ} (i : Fin (n + 1)) (θ : Fin (n + 1) → ℝ) (w : Fin n → ℂ) : (Fin n → ℂ) →L[ℝ] ℝ

The derivative of the chart Hamiltonian 2 N / D, by the product and inverse rules.

Equations

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

theorem Projectivization.hasFDerivAt_torusChartHam {n : ℕ} (i : Fin (n + 1)) (θ : Fin (n + 1) → ℝ) (w : Fin n → ℂ) : HasFDerivAt (torusChartHam i θ) (torusChartHamDeriv i θ w) w

The pointwise identity ι_X ω = dH in the chart

theorem Projectivization.torusChartHamDeriv_apply {n : ℕ} (i : Fin (n + 1)) (θ : Fin (n + 1) → ℝ) (w v : Fin n → ℂ) : (torusChartHamDeriv i θ w) v = 2 * (torusChartNum i θ w * (-(chartDen w ^ 2)⁻¹ * ∑ j : Fin n, 2 * ((w j).re * (v j).re + (w j).im * (v j).im)) + (chartDen w)⁻¹ * ∑ j : Fin n, θ (i.succAbove j) * (2 * ((w j).re * (v j).re + (w j).im * (v j).im)))

theorem Projectivization.fsModelForm_torusChartField {n : ℕ} (i : Fin (n + 1)) (θ : Fin (n + 1) → ℝ) (w v : Fin n → ℂ) : (fsModelForm w) ![torusChartField i θ w, v] = (torusChartHamDeriv i θ w) v

★★ The chart identity: the Fubini–Study model form pairs the torus velocity with v exactly as the derivative of the chart Hamiltonian does.

The manifold statement

noncomputable def Projectivization.torusField {n : ℕ} (θ : Fin (n + 1) → ℝ) (x : Projectivization ℂ (Ambient n)) : TangentSpace (modelWithCornersSelf ℝ (Fin n → ℂ)) x

The fundamental vector field of the torus action p ↦ diag(e^{iθ}) • p on ℂℙⁿ, read in the chart at each point.

Equations

• Projectivization.torusField θ x = Projectivization.torusChartField x.idx θ (Projectivization.chartFun x.idx x)

noncomputable def Projectivization.torusHamiltonian {n : ℕ} (θ : Fin (n + 1) → ℝ) (p : Projectivization ℂ (Ambient n)) : ℝ

The Hamiltonian of the torus action: 2 ∑ₖ θₖ · momentMap p k.

Equations

• Projectivization.torusHamiltonian θ p = 2 * ∑ k : Fin (n + 1), θ k * p.momentMap k

theorem Projectivization.continuous_torusHamiltonian {n : ℕ} (θ : Fin (n + 1) → ℝ) : Continuous (torusHamiltonian θ)

theorem Projectivization.torusHamiltonian_chartInv {n : ℕ} (θ : Fin (n + 1) → ℝ) (i : Fin (n + 1)) (w : Fin n → ℂ) : torusHamiltonian θ (chartInv i w) = torusChartHam i θ w

theorem Projectivization.hasMFDerivAt_torusHamiltonian {n : ℕ} (θ : Fin (n + 1) → ℝ) (x : Projectivization ℂ (Ambient n)) : HasMFDerivAt% (torusHamiltonian θ) x (torusChartHamDeriv x.idx θ (chartFun x.idx x))

theorem Projectivization.torusField_isHamiltonianVectorField {n : ℕ} (θ : Fin (n + 1) → ℝ) : DifferentialForm.IsHamiltonianVectorField (fun (x : Projectivization ℂ (Ambient n)) => fsForm x) (torusField θ) (torusHamiltonian θ)

★★★ The torus action on ℂℙⁿ is Hamiltonian, with 2 ∑ θₖ momentMap as its Hamiltonian: the moment-map equation ι_X ω_FS = dH on the manifold.

The torus action, and its velocity

noncomputable def Projectivization.torusUnitary {n : ℕ} (θ : Fin (n + 1) → ℝ) : ↥(Matrix.unitaryGroup (Fin (n + 1)) ℂ)

The phase matrix diag(e^{iθₖ}) as a unitary.

Equations

• Projectivization.torusUnitary θ = ⟨Matrix.diagonal fun (k : Fin (n + 1)) => Complex.exp (↑(θ k) * Complex.I), ⋯⟩

theorem Projectivization.torusUnitary_val {n : ℕ} (θ : Fin (n + 1) → ℝ) : ↑(torusUnitary θ) = Matrix.diagonal fun (k : Fin (n + 1)) => Complex.exp (↑(θ k) * Complex.I)

theorem Projectivization.chartFun_torusUnitary_smul {n : ℕ} (θ : Fin (n + 1) → ℝ) (i : Fin (n + 1)) (w : Fin n → ℂ) : chartFun i (torusUnitary θ • chartInv i w) = fun (j : Fin n) => Complex.exp (↑(θ (i.succAbove j)) * Complex.I) * w j / Complex.exp (↑(θ i) * Complex.I)

The torus action in the chart at i, coordinatewise.

theorem Projectivization.hasDerivAt_chartFun_torusUnitary {n : ℕ} (θ : Fin (n + 1) → ℝ) (i : Fin (n + 1)) (w : Fin n → ℂ) : HasDerivAt (fun (t : ℝ) => chartFun i (torusUnitary (t • θ) • chartInv i w)) (torusChartField i θ w) 0

★ The field is the velocity of the action: at every chart point, torusChartField is the t-derivative at 0 of t ↦ diag(e^{itθ}) • p, read in the chart.

Uniqueness: the normalisation pins the moment map (G8)

theorem Projectivization.chartAt_origin_target {n : ℕ} (i : Fin (n + 1)) : (chartAt (Fin n → ℂ) (origin i)).target = Set.univ

def Projectivization.allOnes (n : ℕ) : Ambient n

The point [1 : 1 : ⋯ : 1], which lies in every affine chart.

Equations

• Projectivization.allOnes n = WithLp.toLp 2 fun (x : Fin (n + 1)) => 1

theorem Projectivization.allOnes_ne_zero (n : ℕ) : allOnes n ≠ 0

theorem Projectivization.mk_allOnes_mem_chartSource {n : ℕ} (i : Fin (n + 1)) : mk ℂ (allOnes n) ⋯ ∈ chartSource i

theorem Projectivization.momentMap_origin_of_ne {n : ℕ} (j k : Fin (n + 1)) (h : k ≠ j) : (origin j).momentMap k = 0

The k-th moment-map coordinate vanishes at the j-th chart origin, k ≠ j.

theorem Projectivization.torusHamiltonian_single {n : ℕ} (k : Fin (n + 1)) (p : Projectivization ℂ (Ambient n)) : torusHamiltonian (Pi.single k 1) p = 2 * p.momentMap k

theorem Projectivization.mdifferentiable_torusHamiltonian {n : ℕ} (θ : Fin (n + 1) → ℝ) : MDiff (torusHamiltonian θ)

theorem Projectivization.eq_add_const_of_isHamiltonianVectorField {n : ℕ} {α : (x : Projectivization ℂ (Ambient n)) → TangentSpace (modelWithCornersSelf ℝ (Fin n → ℂ)) x [⋀^Fin 2]→L[ℝ] Bundle.Trivial (Projectivization ℂ (Ambient n)) ℝ x} {X : (x : Projectivization ℂ (Ambient n)) → TangentSpace (modelWithCornersSelf ℝ (Fin n → ℂ)) x} {H K : Projectivization ℂ (Ambient n) → ℝ} (hH : MDiff H) (hK : MDiff K) (h : DifferentialForm.IsHamiltonianVectorField α X H) (h' : DifferentialForm.IsHamiltonianVectorField α X K) : ∃ (c : ℝ), ∀ (p : Projectivization ℂ (Ambient n)), H p = K p + c

★★ A Hamiltonian is unique up to a constant on ℂℙⁿ: two differentiable Hamiltonians of the same field for the same 2-form family differ by a constant. No connectedness lemma is used: every affine chart image is all of ℂⁿ, and [1 : ⋯ : 1] lies in every chart.

theorem Projectivization.eq_torusHamiltonian_of_nonneg_of_sum {n : ℕ} (H : Fin (n + 1) → Projectivization ℂ (Ambient n) → ℝ) (hdiff : ∀ (k : Fin (n + 1)), MDiff (H k)) (hham : ∀ (k : Fin (n + 1)), DifferentialForm.IsHamiltonianVectorField (fun (x : Projectivization ℂ (Ambient n)) => fsForm x) (torusField (Pi.single k 1)) (H k)) (hnn : ∀ (k : Fin (n + 1)) (p : Projectivization ℂ (Ambient n)), 0 ≤ H k p) (hsum : ∀ (p : Projectivization ℂ (Ambient n)), ∑ k : Fin (n + 1), H k p = 2) (k : Fin (n + 1)) (p : Projectivization ℂ (Ambient n)) : H k p = torusHamiltonian (Pi.single k 1) p

★★★ The normalisation pins the constant. A family of Hamiltonians for the phase fields that is non-negative and sums to 2 (the form's scale) is 2 · momentMap: the Hamiltonian family of the torus action, and with it the moment map, is unique.

The image of the moment map is the standard simplex (G9)

The standard simplex is Mathlib's bundled StdSimplex ℝ (Fin (n + 1)) (namespace Convexity): a point is a finitely supported family of non-negative weights summing to 1, read as a function through .weights. Mathlib deprecated the Set-level simplex on 2026-08-29 with StdSimplex.range_toFun_comp_weights as the successor of its membership predicate, and the statements below are written against that successor (BACKLOG #27, HY-6, restated 2026-10-23): the moment map factors through the bundled simplex (momentMapSimplex), that factorisation is surjective, and the image of the moment map as a set of weight vectors is the range of StdSimplex.weights. Nothing is weakened: the two inclusions are the ones proved at the Lean v4.33.0 pin, with the simplex now a type rather than a set.

noncomputable def Projectivization.momentMapSimplex {n : ℕ} (p : Projectivization ℂ (Ambient n)) : Convexity.StdSimplex ℝ (Fin (n + 1))

The value of the moment map as a point of the bundled standard simplex: momentMap_nonneg and momentMap_sum_eq_one are its two fields.

Equations

• p.momentMapSimplex = { weights := Finsupp.equivFunOnFinite.symm p.momentMap, nonneg := ⋯, total := ⋯ }

@[simp]

theorem Projectivization.weights_momentMapSimplex {n : ℕ} (p : Projectivization ℂ (Ambient n)) : ⇑p.momentMapSimplex.weights = p.momentMap

theorem Projectivization.momentMap_mem_range_weights {n : ℕ} (p : Projectivization ℂ (Ambient n)) : p.momentMap ∈ Set.range fun (t : Convexity.StdSimplex ℝ (Fin (n + 1))) => ⇑t.weights

Every value of the moment map is a weight vector of the standard simplex.

noncomputable def Projectivization.sqrtVec {n : ℕ} (t : Fin (n + 1) → ℝ) : Ambient n

The vector (√t₀, …, √tₙ): the representative whose ray realises the weight vector t.

Equations

• Projectivization.sqrtVec t = WithLp.toLp 2 fun (k : Fin (n + 1)) => ↑√(t k)

theorem Projectivization.norm_sqrtVec_apply_sq {n : ℕ} (t : Fin (n + 1) → ℝ) (k : Fin (n + 1)) (ht : 0 ≤ t k) : ‖(sqrtVec t).ofLp k‖ ^ 2 = t k

theorem Projectivization.norm_sqrtVec_sq {n : ℕ} (t : Convexity.StdSimplex ℝ (Fin (n + 1))) : ‖sqrtVec ⇑t.weights‖ ^ 2 = 1

theorem Projectivization.sqrtVec_ne_zero {n : ℕ} (t : Convexity.StdSimplex ℝ (Fin (n + 1))) : sqrtVec ⇑t.weights ≠ 0

theorem Projectivization.momentMap_mk_sqrtVec {n : ℕ} (t : Convexity.StdSimplex ℝ (Fin (n + 1))) : (mk ℂ (sqrtVec ⇑t.weights) ⋯).momentMap = ⇑t.weights

The ray of (√t₀, …, √tₙ) maps to the weight vector t.

theorem Projectivization.momentMapSimplex_mk_sqrtVec {n : ℕ} (t : Convexity.StdSimplex ℝ (Fin (n + 1))) : (mk ℂ (sqrtVec ⇑t.weights) ⋯).momentMapSimplex = t

The ray of (√t₀, …, √tₙ) maps to the simplex point t itself.

theorem Projectivization.momentMapSimplex_surjective {n : ℕ} : Function.Surjective momentMapSimplex

★★ The moment map onto the standard simplex is surjective — the moment polytope of the torus action on ℂℙⁿ, by direct computation: every simplex point is the image of the ray of (√t₀, …, √tₙ). The Atiyah–Guillemin–Sternberg convexity theorem is neither used nor proved.

theorem Projectivization.range_momentMap {n : ℕ} : Set.range momentMap = Set.range fun (t : Convexity.StdSimplex ℝ (Fin (n + 1))) => ⇑t.weights

★★ The image of the moment map is exactly the standard simplex, as sets of weight vectors: ⊆ is the normalisation, ⊇ is the ray of (√t₀, …, √tₙ).

theorem Projectivization.range_momentMap_eq_inter {n : ℕ} : Set.range momentMap = (⋂ (i : Fin (n + 1)), {s : Fin (n + 1) → ℝ | 0 ≤ s i}) ∩ {s : Fin (n + 1) → ℝ | ∑ i : Fin (n + 1), s i = 1}

The image of the moment map, spelled out: the non-negative weight vectors summing to 1 (StdSimplex.range_toFun_comp_weights, the successor of the Set-level simplex).

The torus flow preserves the Fubini–Study volume (G10)

theorem Projectivization.torusUnitary_zero {n : ℕ} : torusUnitary 0 = 1

theorem Projectivization.torusUnitary_add {n : ℕ} (θ θ' : Fin (n + 1) → ℝ) : torusUnitary (θ + θ') = torusUnitary θ * torusUnitary θ'

theorem Projectivization.torusUnitary_add_smul {n : ℕ} (θ : Fin (n + 1) → ℝ) (s t : ℝ) : torusUnitary ((s + t) • θ) = torusUnitary (s • θ) * torusUnitary (t • θ)

The one-parameter group law of the torus flow t ↦ diag(e^{itθ}): the maps torusUnitary (t • θ) compose as a flow.

The torus orbits are integral curves of the torus field (G16)

theorem Projectivization.continuous_torusUnitary_smul {n : ℕ} (θ : Fin (n + 1) → ℝ) : Continuous fun (t : ℝ) => torusUnitary (t • θ)

The torus flow t ↦ diag(e^{itθ}) is continuous in time.

theorem Projectivization.isMIntegralCurve_torusUnitary_smul {n : ℕ} (θ : Fin (n + 1) → ℝ) (p : Projectivization ℂ (Ambient n)) : IsMIntegralCurve (fun (t : ℝ) => torusUnitary (t • θ) • p) (torusField θ)

★★★ The torus orbit is the integral curve of the torus field: t ↦ diag(e^{itθ}) • p is a global integral curve of torusField θ, for every p. The route of isMIntegralCurve_schrodingerUnitary_smul: in the chart at diag(e^{itθ}) • p the curve is s ↦ chartFun (diag(e^{i(s-t)θ}) • q), whose derivative at s = t is the chart velocity (hasDerivAt_chartFun_torusUnitary, shifted by the group law torusUnitary_add_smul).

theorem Projectivization.fsVolume_map_torusUnitary_smul {n : ℕ} (θ : Fin (n + 1) → ℝ) : MeasureTheory.Measure.map (fun (p : Projectivization ℂ (Ambient n)) => torusUnitary θ • p) (fsVolume n) = fsVolume n

★ The torus flow preserves the Fubini–Study volume: every map p ↦ diag(e^{iθ}) • p — in particular every time-t map diag(e^{itθ}) of the flow of torusField (isMIntegralCurve_torusUnitary_smul) — preserves fsVolume n. A corollary of the unitary invariance fsVolume_map_smul: Liouville in the dynamics sense for this one flow, with no manifold-level flow theory (G5) involved.

theorem Projectivization.measurePreserving_torusUnitary_smul {n : ℕ} (θ : Fin (n + 1) → ℝ) : MeasureTheory.MeasurePreserving (fun (p : Projectivization ℂ (Ambient n)) => torusUnitary θ • p) (fsVolume n) (fsVolume n)

The same, as a measure-preserving map.