The affine atlas of ℂℙⁿ as a finite chart cover #
Category: 1-Mathlib (CSD-free).
The non-vacuity witness for ChartCover (TopFormMeasure.lean) on ℂℙⁿ: the n + 1 affine charts
of ℂℙⁿ
(ProjectiveSpace.lean) are the charts at the chart origins origin i
(ProjectiveSpaceFubiniStudyForm.lean), and every point has a non-vanishing coordinate, so they
cover.
Projectivization.affineChartCover n : ChartCover (Fin n → ℂ) (ℙ ℂ (Ambient n));affineChartCover_m— it hasn + 1charts.
With it, DifferentialForm.topFormMeasure volume e s (affineChartCover n) is a measure on
ℂℙⁿ for every top-form family s — the object the volume modules evaluate on the wedge power
of the Fubini–Study form.
Honest scope #
⚠️ Only the cover. No top form on ℂℙⁿ is built here (the wedge of sections is M2), no measure is
evaluated, and nothing is said about the Fubini–Study measure.
Provenance and references. The top-power plan (M3, and the ℂℙⁿ instance of the cover);
Geometry/Manifold/TopFormMeasure.lean; Geometry/Manifold/Instances/ProjectiveSpace.lean
(chartAtIdx, idx, exists_ne_zero_coord);
Geometry/Manifold/Instances/ProjectiveSpaceFubiniStudyForm.lean (origin, idx_origin);
the completed-work ledger.
The affine atlas of ℂℙⁿ as a finite chart cover: the charts at the n + 1 chart origins.
Equations
- Projectivization.affineChartCover n = { m := n + 1, pt := fun (i : Fin (n + 1)) => Projectivization.origin i, cover := ⋯ }