The unitary action preserves the Fubini–Study form in charts

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

ProjectiveSpaceFubiniStudyVolume.lean proves fsVolume_map_smul by feeding topFormMeasure_map_eq the chart form of "U preserves ω_FS^{∧n}". This module states the same fact for the 2-form itself, in the vocabulary of FormInvariance.lean, so that products of ℂℙⁿ with other factors can inherit it:

• ★ preservesLocalRep_fsForm_smul — U^* ω_FS = ω_FS in charts: through two affine charts the action is uTrans, analytic where defined, and it pulls the model form back to itself (fsModelForm_uTrans).

References: Geometry/Manifold/Instances/ProjectiveSpaceFubiniStudyVolume.lean (fsVolume_map_smul, chartAt_smul_comp_symm, localRep_fsSection'); Geometry/Manifold/Instances/ProjectiveSpaceUnitaryAction.lean (fsModelForm_uTrans); Geometry/Manifold/FormInvariance.lean; specs/BACKLOG.md (#29); specs/future-work.md.

theorem Projectivization.preservesLocalRep_fsForm_smul {n : ℕ} (U : ↥(Matrix.unitaryGroup (Fin (n + 1)) ℂ)) : DifferentialForm.PreservesLocalRep (fun (x : Projectivization ℂ (Ambient n)) => fsForm x) fun (p : Projectivization ℂ (Ambient n)) => U • p

★ The unitary action preserves the Fubini–Study form in charts.