Homogeneous-coordinate charts on complex projective space

On the open set where the homogeneous coordinate k is nonzero, the ratios X_j / X_k give a homeomorphism with complex affine space. These charts are constructed directly on the circle quotient of the unit sphere. The inverse inserts a coordinate equal to one and normalizes the resulting vector to unit length. The other coordinates may vanish.

The chart sources cover projective space, including in dimension zero. Their overlap functions are the usual homogeneous ratios; these formulas provide the complex atlas and the comparison with homogeneous-coordinate charts of toric projective space.

References

• D. Cox, J. Little and H. Schenck, Toric Varieties, §§3.1 and 3.4.

noncomputable def TauCeti.ComplexProjectiveSpace.ratio {n : ℕ} (k j : Fin (n + 1)) : ComplexProjectiveSpace n → ℂ

The homogeneous ratio X_j / X_k. Outside the chart X_k ≠ 0 it is zero, following the convention for division in ℂ.

@[simp]

theorem TauCeti.ComplexProjectiveSpace.ratio_mk {n : ℕ} (k j : Fin (n + 1)) (v : ↑(Metric.sphere 0 1)) : ratio k j (mk n v) = (↑v).ofLp j / (↑v).ofLp k

Homogeneous ratios can be computed on any unit-vector representative.

def TauCeti.ComplexProjectiveSpace.affineOpen {n : ℕ} (k : Fin (n + 1)) : Set (ComplexProjectiveSpace n)

The standard affine open where the kth homogeneous coordinate is nonzero.

@[simp]

theorem TauCeti.ComplexProjectiveSpace.mem_affineOpen_iff {n : ℕ} (k : Fin (n + 1)) (p : ComplexProjectiveSpace n) : p ∈ affineOpen k ↔ ratio k k p ≠ 0

A standard affine open is characterized by the nonvanishing of its normalizing ratio.

theorem TauCeti.ComplexProjectiveSpace.mk_mem_affineOpen_iff {n : ℕ} (k : Fin (n + 1)) (v : ↑(Metric.sphere 0 1)) : mk n v ∈ affineOpen k ↔ (↑v).ofLp k ≠ 0

The class of a unit vector lies in the kth affine open exactly when its kth coordinate is nonzero.

@[simp]

theorem TauCeti.ComplexProjectiveSpace.ratio_self_eq_one {n : ℕ} (k : Fin (n + 1)) {p : ComplexProjectiveSpace n} (hp : p ∈ affineOpen k) : ratio k k p = 1

The normalizing homogeneous ratio is one on its affine chart domain.

theorem TauCeti.ComplexProjectiveSpace.isOpen_affineOpen {n : ℕ} (k : Fin (n + 1)) : IsOpen (affineOpen k)

The homogeneous-coordinate chart domains are open for the sphere-quotient topology.

theorem TauCeti.ComplexProjectiveSpace.exists_mem_affineOpen {n : ℕ} (p : ComplexProjectiveSpace n) : ∃ (k : Fin (n + 1)), p ∈ affineOpen k

Every projective point has a nonzero homogeneous coordinate.

theorem TauCeti.ComplexProjectiveSpace.continuousOn_ratio {n : ℕ} (k j : Fin (n + 1)) : ContinuousOn (ratio k j) (affineOpen k)

Homogeneous ratios are continuous on any chart where their denominator is nonzero.

noncomputable def TauCeti.ComplexProjectiveSpace.affineParam {n : ℕ} (k : Fin (n + 1)) (z : Fin n → ℂ) : ComplexProjectiveSpace n

The projective point whose kth coordinate is one and whose remaining coordinates are z. The representative is normalized only to meet the unit-sphere carrier.

@[simp]

theorem TauCeti.ComplexProjectiveSpace.ratio_affineParam {n : ℕ} (k l j : Fin (n + 1)) (z : Fin n → ℂ) : ratio l j (affineParam k z) = k.insertNth 1 z j / k.insertNth 1 z l

The homogeneous ratios of a standard affine parametrization are ratios of its inserted coordinates.

theorem TauCeti.ComplexProjectiveSpace.continuous_affineParam {n : ℕ} (k : Fin (n + 1)) : Continuous (affineParam k)

Standard affine parametrizations are continuous, including on all coordinate hyperplanes.

@[simp]

theorem TauCeti.ComplexProjectiveSpace.affineParam_ratio {n : ℕ} (k : Fin (n + 1)) {p : ComplexProjectiveSpace n} (hp : p ∈ affineOpen k) : (affineParam k fun (j : Fin n) => ratio k (k.succAbove j) p) = p

Homogeneous ratios recover a point on their affine domain.

noncomputable def TauCeti.ComplexProjectiveSpace.affineChart {n : ℕ} (k : Fin (n + 1)) : OpenPartialHomeomorph (ComplexProjectiveSpace n) (Fin n → ℂ)

The standard homogeneous-ratio chart on the sphere-quotient projective space.

@[simp]

theorem TauCeti.ComplexProjectiveSpace.affineChart_source {n : ℕ} (k : Fin (n + 1)) : (affineChart k).source = affineOpen k

The source of the standard chart is its homogeneous-coordinate nonvanishing locus.

@[simp]

theorem TauCeti.ComplexProjectiveSpace.affineChart_target {n : ℕ} (k : Fin (n + 1)) : (affineChart k).target = Set.univ

The standard chart takes values in the whole complex affine space.

@[simp]

theorem TauCeti.ComplexProjectiveSpace.affineChart_apply {n : ℕ} (k : Fin (n + 1)) (p : ComplexProjectiveSpace n) (j : Fin n) : ↑(affineChart k) p j = ratio k (k.succAbove j) p

The standard affine chart reads homogeneous ratios.

@[simp]

theorem TauCeti.ComplexProjectiveSpace.affineChart_symm_apply {n : ℕ} (k : Fin (n + 1)) (z : Fin n → ℂ) : ↑(affineChart k).symm z = affineParam k z

The inverse standard chart inserts the normalizing coordinate one.

theorem TauCeti.ComplexProjectiveSpace.insertNth_affineChart {n : ℕ} (k : Fin (n + 1)) {p : ComplexProjectiveSpace n} (hp : p ∈ affineOpen k) (j : Fin (n + 1)) : k.insertNth 1 (↑(affineChart k) p) j = ratio k j p

On its domain, the standard chart together with the normalizing coordinate one gives all homogeneous ratios.

@[simp]

theorem TauCeti.ComplexProjectiveSpace.affineParam_mem_affineOpen_iff {n : ℕ} (k l : Fin (n + 1)) (z : Fin n → ℂ) : affineParam k z ∈ affineOpen l ↔ k.insertNth 1 z l ≠ 0

On a chart overlap the only restriction is nonvanishing of the new denominator.

@[simp]

theorem TauCeti.ComplexProjectiveSpace.affineChart_transition {n : ℕ} (k l : Fin (n + 1)) (z : Fin n → ℂ) (j : Fin n) : ↑(affineChart l) (↑(affineChart k).symm z) j = k.insertNth 1 z (l.succAbove j) / k.insertNth 1 z l

The transition between standard affine charts is the usual homogeneous-ratio formula.