Complex projective space is an analytic manifold

TERM-SCOPE(Kahler) — "top-power identity" appears below in the restricted sense the terms register records, and in the negative: the identity is what this module does NOT prove. (Repository bookkeeping; it goes with the References block if this is sent upstream.)

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

At the pin, Projectivization carries a topology (staged in this repository), a measurable space, a metric — and no charted-space instance anywhere, so ℂℙⁿ was not a manifold in Lean and nothing on it could be differentiated. MATHLIB-ABSENT(ChartedSpace.projectivization)

This module builds the standard affine atlas and both instances:

• Projectivization.chartAtIdx i — the affine chart on {p | pᵢ ≠ 0}, [z₀ : ⋯ : zₙ] ↦ (z_{σᵢ(0)}/zᵢ, …, z_{σᵢ(n-1)}/zᵢ) where σᵢ = Fin.succAbove i skips the i-th slot, with inverse w ↦ [Fin.insertNth i 1 w];
• ★ Projectivization.instChartedSpace — ℂℙⁿ is a charted space;
• ★ Projectivization.instIsManifold — and an analytic (ω) manifold, not merely C^∞: the transition maps are ratios of coordinates of Fin.insertNth i 1 w, so each is a quotient of an affine function by a nonvanishing affine function.

Design notes

Why rep rather than a quotient lift. The chart map is defined on the chosen representative (Projectivization.rep), which makes well-definedness free but says nothing about continuity — rep is a choice function. Continuity is recovered separately, from mk' being an open quotient map (isQuotientMap_mk', staged here) restricted to the open chart source: Topology.IsQuotientMap.restrictPreimage_isOpen turns continuity of the chart into continuity of the ratio map on nonzero vectors, which is elementary.

Why the model space is Fin n → ℂ and not EuclideanSpace ℂ (Fin n). At the pin WithLp is a genuine structure rather than a type synonym, so every element of EuclideanSpace must be built through WithLp.toLp and every chart formula would carry that wrapper. The sup-norm Pi type is norm-equivalent, carries the same smooth and analytic structure, and keeps the charts readable. The ambient space stays EuclideanSpace ℂ (Fin (n+1)), which is what the projective space of interest is built on.

Honest scope

• This is ℂℙⁿ over ℂ, on the Euclidean ambient space. The same charts work over any nontrivially normed field and for ℙ 𝕜 (Fin (n+1) → 𝕜); that generalisation is not made here and is a natural follow-up.
• Nothing about forms. Making ℂℙⁿ a manifold does not give differential forms on manifolds — that is step (2) of the plan and is upstream's own stated TODO. In particular the top-power identity ω^(N-1)/(N-1)! = μ_FS is still not provable; what steps (0) and (1) between them buy is that it can be said.
• No relation to the Fubini–Study metric or measure is proved here. The charted structure is topological/analytic only; that μ_FS is the Liouville volume of the induced form remains open (step (3)).

Provenance and references. The Mathlib-gaps register (Kahler / symplectic manifold API, step (0)); the backlog (XL, "Manifold exterior calculus"); CsdLean4/Mathlib/LinearAlgebra/Projectivization/Topology.lean (the quotient topology and isQuotientMap_mk'); Mathlib.Geometry.Manifold.Instances.Sphere (the analogous construction upstream, from stereographic projection).

@[reducible, inline]

abbrev Projectivization.Ambient (n : ℕ) : Type

The ambient coordinate space of ℂℙⁿ.

Equations

• Projectivization.Ambient n = EuclideanSpace ℂ (Fin (n + 1))

The affine chart, on representatives

noncomputable def Projectivization.coordRatio {n : ℕ} (i : Fin (n + 1)) (v : Ambient n) : Fin n → ℂ

The affine chart formula on a representative: divide the other coordinates by the i-th one.

Equations

• Projectivization.coordRatio i v j = v.ofLp (i.succAbove j) / v.ofLp i

theorem Projectivization.coordRatio_def {n : ℕ} (i : Fin (n + 1)) (v : Ambient n) : coordRatio i v = fun (j : Fin n) => v.ofLp (i.succAbove j) / v.ofLp i

coordRatio, unfolded: the definitional equation.

noncomputable def Projectivization.insertOne {n : ℕ} (i : Fin (n + 1)) (w : Fin n → ℂ) : Ambient n

Insert 1 in slot i: the affine section of the i-th chart.

Equations

• Projectivization.insertOne i w = WithLp.toLp 2 (i.insertNth 1 w)

theorem Projectivization.insertOne_def {n : ℕ} (i : Fin (n + 1)) (w : Fin n → ℂ) : insertOne i w = WithLp.toLp 2 (i.insertNth 1 w)

insertOne, unfolded: the definitional equation.

@[simp]

theorem Projectivization.insertOne_apply_same {n : ℕ} (i : Fin (n + 1)) (w : Fin n → ℂ) : (insertOne i w).ofLp i = 1

@[simp]

theorem Projectivization.insertOne_apply_succAbove {n : ℕ} (i : Fin (n + 1)) (w : Fin n → ℂ) (j : Fin n) : (insertOne i w).ofLp (i.succAbove j) = w j

theorem Projectivization.insertOne_ne_zero {n : ℕ} (i : Fin (n + 1)) (w : Fin n → ℂ) : insertOne i w ≠ 0

theorem Projectivization.smul_ofLp {n : ℕ} (c : ℂ) (v : Ambient n) (k : Fin (n + 1)) : (c • v).ofLp k = c * v.ofLp k

theorem Projectivization.coordRatio_smul {n : ℕ} (a : ℂˣ) (i : Fin (n + 1)) (v : Ambient n) : coordRatio i (a • v) = coordRatio i v

Coordinate ratios do not see the choice of representative.

The chart maps on ℂℙⁿ

noncomputable def Projectivization.chartFun {n : ℕ} (i : Fin (n + 1)) (p : Projectivization ℂ (Ambient n)) : Fin n → ℂ

The i-th affine chart of ℂℙⁿ. Well defined because coordRatio is representative-independent.

Equations

• Projectivization.chartFun i p = Projectivization.coordRatio i p.rep

noncomputable def Projectivization.chartInv {n : ℕ} (i : Fin (n + 1)) (w : Fin n → ℂ) : Projectivization ℂ (Ambient n)

The inverse of the i-th affine chart.

Equations

• Projectivization.chartInv i w = Projectivization.mk ℂ (Projectivization.insertOne i w) ⋯

theorem Projectivization.chartInv_def {n : ℕ} (i : Fin (n + 1)) (w : Fin n → ℂ) : chartInv i w = mk ℂ (insertOne i w) ⋯

chartInv, unfolded: the definitional equation.

def Projectivization.chartSource {n : ℕ} (i : Fin (n + 1)) : Set (Projectivization ℂ (Ambient n))

The domain of the i-th chart: the points whose i-th coordinate does not vanish.

Equations

• Projectivization.chartSource i = {p : Projectivization ℂ (Projectivization.Ambient n) | p.rep.ofLp i ≠ 0}

theorem Projectivization.chartFun_mk {n : ℕ} (i : Fin (n + 1)) (v : Ambient n) (hv : v ≠ 0) : chartFun i (mk ℂ v hv) = coordRatio i v

theorem Projectivization.rep_ne_zero_iff {n : ℕ} (i : Fin (n + 1)) (v : Ambient n) (hv : v ≠ 0) : (mk ℂ v hv).rep.ofLp i ≠ 0 ↔ v.ofLp i ≠ 0

theorem Projectivization.mem_chartSource_mk {n : ℕ} (i : Fin (n + 1)) (v : Ambient n) (hv : v ≠ 0) : mk ℂ v hv ∈ chartSource i ↔ v.ofLp i ≠ 0

theorem Projectivization.preimage_chartSource {n : ℕ} (i : Fin (n + 1)) : mk' ℂ ⁻¹' chartSource i = {v : { v : Ambient n // v ≠ 0 } | (↑v).ofLp i ≠ 0}

theorem Projectivization.continuous_coord {n : ℕ} (k : Fin (n + 1)) : Continuous fun (v : { v : Ambient n // v ≠ 0 }) => (↑v).ofLp k

theorem Projectivization.isOpen_chartSource {n : ℕ} (i : Fin (n + 1)) : IsOpen (chartSource i)

The chart domain is open: its mk'-preimage is a nonvanishing-coordinate condition, and mk' is a quotient map.

The chart is a homeomorphism onto its image

theorem Projectivization.chartFun_chartInv {n : ℕ} (i : Fin (n + 1)) (w : Fin n → ℂ) : chartFun i (chartInv i w) = w

theorem Projectivization.continuous_insertOne {n : ℕ} (i : Fin (n + 1)) : Continuous (insertOne i)

theorem Projectivization.continuous_chartInv {n : ℕ} (i : Fin (n + 1)) : Continuous (chartInv i)

theorem Projectivization.insertOne_chartFun {n : ℕ} (i : Fin (n + 1)) (p : Projectivization ℂ (Ambient n)) (hp : p.rep.ofLp i ≠ 0) : insertOne i (chartFun i p) = (p.rep.ofLp i)⁻¹ • p.rep

On the chart domain the affine section recovers the representative up to scale.

theorem Projectivization.chartInv_chartFun {n : ℕ} (i : Fin (n + 1)) (p : Projectivization ℂ (Ambient n)) (hp : p.rep.ofLp i ≠ 0) : chartInv i (chartFun i p) = p

theorem Projectivization.continuousOn_chartFun {n : ℕ} (i : Fin (n + 1)) : ContinuousOn (chartFun i) (chartSource i)

Continuity of the chart map. The chart is defined through rep, which is a choice function and carries no continuity of its own; what supplies it is that mk' restricted to the (open) chart domain is still a quotient map.

theorem Projectivization.chartInv_mem_chartSource {n : ℕ} (i : Fin (n + 1)) (w : Fin n → ℂ) : chartInv i w ∈ chartSource i

noncomputable def Projectivization.chartAtIdx {n : ℕ} (i : Fin (n + 1)) : OpenPartialHomeomorph (Projectivization ℂ (Ambient n)) (Fin n → ℂ)

★ The i-th affine chart of ℂℙⁿ, as an open partial homeomorphism onto Fin n → ℂ.

Equations

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

The charted space and manifold instances

theorem Projectivization.exists_ne_zero_coord {n : ℕ} (p : Projectivization ℂ (Ambient n)) : ∃ (i : Fin (n + 1)), p.rep.ofLp i ≠ 0

noncomputable def Projectivization.idx {n : ℕ} (p : Projectivization ℂ (Ambient n)) : Fin (n + 1)

Some coordinate index at which the point does not vanish; the chart chosen at p.

Equations

• p.idx = ⋯.choose

theorem Projectivization.idx_spec {n : ℕ} (p : Projectivization ℂ (Ambient n)) : p.rep.ofLp p.idx ≠ 0

@[instance_reducible]

noncomputable instance Projectivization.instChartedSpace {n : ℕ} : ChartedSpace (Fin n → ℂ) (Projectivization ℂ (Ambient n))

★ Complex projective space is a charted space, on the standard affine atlas.

Equations

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

theorem Projectivization.contDiff_insertOne_coord {n : ℕ} (i m : Fin (n + 1)) : ContDiff ℂ ⊤ fun (w : Fin n → ℂ) => (insertOne i w).ofLp m

Each coordinate of the affine section is analytic in the chart variable: it is either the constant 1 or a coordinate projection.

theorem Projectivization.contDiffOn_transition {n : ℕ} (i j : Fin (n + 1)) : ContDiffOn ℂ ⊤ (fun (w : Fin n → ℂ) => coordRatio j (insertOne i w)) {w : Fin n → ℂ | (insertOne i w).ofLp j ≠ 0}

The transition maps are analytic: each component is a ratio of two coordinates of insertNth i 1 w, and the denominator does not vanish on the overlap.

instance Projectivization.instIsManifold {n : ℕ} : IsManifold (modelWithCornersSelf ℂ (Fin n → ℂ)) ⊤ (Projectivization ℂ (Ambient n))

★ Complex projective space is an analytic manifold.

Not merely C^∞: the transition maps are quotients of coordinates of Fin.insertNth i 1 w with nonvanishing denominators, so ω comes out of the same argument.

instance Projectivization.instIsManifoldReal {n : ℕ} : IsManifold (modelWithCornersSelf ℝ (Fin n → ℂ)) ⊤ (Projectivization ℂ (Ambient n))

★ The same atlas, read over ℝ. A ℂ-analytic manifold is ℝ-analytic (ContDiffOn.restrict_scalars), and the real structure is the one a real differential form — the Fubini–Study form is ℝ-bilinear, not ℂ-bilinear — has to live on.