Standard affine charts of projective space

For a division ring K and an index type ι, the projective space ℙ K (ι → K) is covered by the standard affine opens U_i = {[v] | v i ≠ 0}, one for each i : ι. For a field K and ι = Fin (n + 1), the homogeneous ratios [v] ↦ (v (i.succAbove j) / v i)_(j : Fin n) identify U_i with the affine space Fin n → K; the inverse inserts the coordinate 1 in position i, sending z to [Fin.insertNth i 1 z]. The remaining coordinates are enumerated by Fin.succAbove i.

This file records these charts as partial equivalences Projectivization.affineChart i, together with their transition maps: on the overlap of U_i and U_j, the transition from the chart of i to the chart of j divides the homogeneous coordinates Fin.insertNth i 1 z by their j-th entry. These are the algebraic data of the standard atlas of projective space, over an arbitrary field: once projective space carries its quotient topology, they are the charts and rational transition maps from which the smooth structure of real projective space and the complex structure of complex projective space are built.

Main declarations

• Projectivization.affineOpen i: the points whose i-th homogeneous coordinate is nonzero; Projectivization.iUnion_affineOpen says that these sets cover projective space.
• Projectivization.instNontrivial: projective space over at least two coordinates has at least two points.
• Projectivization.affineChart i: the affine chart U_i ≃ Fin n → K by homogeneous ratios.
• Projectivization.affineChart_mk and Projectivization.affineChart_symm_apply: the chart and its inverse in homogeneous coordinates.
• Projectivization.affineChart_symm_zero: the centre of the chart of i is the coordinate point [eᵢ], which lies in no other standard affine open (Projectivization.mk_single_mem_affineOpen_iff).
• Projectivization.affineChart_symm_trans_source and Projectivization.affineChart_symm_trans_apply: the domain and formula of the transition maps.
• Projectivization.affineChart_apply_affineChart_symm: a map of projective spaces given in homogeneous coordinates, read in standard affine charts.

References

• P. Griffiths and J. Harris, Principles of Algebraic Geometry, Chapter 0, §1.

def Projectivization.affineOpen {K : Type u_1} [DivisionRing K] {ι : Type u_2} (i : ι) : Set (Projectivization K (ι → K))

The standard affine open of projective space where the i-th homogeneous coordinate is nonzero.

theorem Projectivization.mem_affineOpen_iff {K : Type u_1} [DivisionRing K] {ι : Type u_2} (i : ι) (x : Projectivization K (ι → K)) : x ∈ affineOpen i ↔ x.rep i ≠ 0

A point lies in the standard affine open of i when the i-th entry of its chosen representative is nonzero; see Projectivization.mk_mem_affineOpen_iff for arbitrary homogeneous coordinates.

@[simp]

theorem Projectivization.mk_mem_affineOpen_iff {K : Type u_1} [DivisionRing K] {ι : Type u_2} (i : ι) (v : ι → K) (hv : v ≠ 0) : mk K v hv ∈ affineOpen i ↔ v i ≠ 0

Membership in a standard affine open does not depend on the chosen homogeneous coordinates.

theorem Projectivization.exists_mem_affineOpen {K : Type u_1} [DivisionRing K] {ι : Type u_2} (x : Projectivization K (ι → K)) : ∃ (i : ι), x ∈ affineOpen i

Every point of projective space lies in some standard affine open.

theorem Projectivization.iUnion_affineOpen {K : Type u_1} [DivisionRing K] {ι : Type u_2} : ⋃ (i : ι), affineOpen i = Set.univ

The standard affine opens cover projective space.

@[simp]

theorem Projectivization.affineOpen_eq_univ {K : Type u_1} [DivisionRing K] {ι : Type u_2} [Subsingleton ι] (i : ι) : affineOpen i = Set.univ

With a single homogeneous coordinate, as for the projective space of dimension zero, the standard affine open is the whole space.

theorem Projectivization.mk_single_mem_affineOpen_iff {K : Type u_1} [DivisionRing K] {ι : Type u_2} [DecidableEq ι] (k i : ι) : mk K (Pi.single k 1) ⋯ ∈ affineOpen i ↔ i = k

The coordinate point [eₖ], the line spanned by the k-th standard basis vector, lies in the standard affine open of i exactly when i = k.

theorem Projectivization.mk_single_injective {K : Type u_1} [DivisionRing K] {ι : Type u_2} [DecidableEq ι] : Function.Injective fun (k : ι) => mk K (Pi.single k 1) ⋯

Distinct standard basis vectors span distinct coordinate points of projective space.

instance Projectivization.instNontrivial {K : Type u_1} [DivisionRing K] {ι : Type u_2} [Nontrivial ι] : Nontrivial (Projectivization K (ι → K))

Projective space over a coordinate space with at least two coordinates has at least two points: the coordinate points of two distinct indices differ.

noncomputable def Projectivization.affineChart {K : Type u_1} [Field K] {n : ℕ} (i : Fin (n + 1)) : PartialEquiv (Projectivization K (Fin (n + 1) → K)) (Fin n → K)

The standard affine chart of projective space at the coordinate i: on the affine open where the i-th homogeneous coordinate is nonzero, it is given by the ratios of the other coordinates to that one, enumerated by Fin.succAbove i. Its inverse sends z to [Fin.insertNth i 1 z].

@[simp]

theorem Projectivization.affineChart_source {K : Type u_1} [Field K] {n : ℕ} (i : Fin (n + 1)) : (affineChart i).source = affineOpen i

@[simp]

theorem Projectivization.affineChart_target {K : Type u_1} [Field K] {n : ℕ} (i : Fin (n + 1)) : (affineChart i).target = Set.univ

@[simp]

theorem Projectivization.affineChart_mk {K : Type u_1} [Field K] {n : ℕ} (i : Fin (n + 1)) (v : Fin (n + 1) → K) (hv : v ≠ 0) : ↑(affineChart i) (mk K v hv) = fun (j : Fin n) => v (i.succAbove j) / v i

The standard affine chart in homogeneous coordinates: the ratios of the other coordinates to the i-th one. Outside the chart domain both sides are 0.

@[simp]

theorem Projectivization.affineChart_symm_apply {K : Type u_1} [Field K] {n : ℕ} (i : Fin (n + 1)) (z : Fin n → K) : ↑(affineChart i).symm z = mk K (i.insertNth 1 z) ⋯

The inverse of the standard affine chart sends z to [Fin.insertNth i 1 z].

theorem Projectivization.affineChart_symm_zero {K : Type u_1} [Field K] {n : ℕ} (i : Fin (n + 1)) : ↑(affineChart i).symm 0 = mk K (Pi.single i 1) ⋯

The centre of the standard affine chart of i is the coordinate point [eᵢ], the line spanned by the i-th standard basis vector.

theorem Projectivization.affineChart_mk_single {K : Type u_1} [Field K] {n : ℕ} (i : Fin (n + 1)) : ↑(affineChart i) (mk K (Pi.single i 1) ⋯) = 0

The standard affine chart of i sends the coordinate point [eᵢ] to its centre 0.

theorem Projectivization.affineChart_symm_trans_source {K : Type u_1} [Field K] {n : ℕ} (i j : Fin (n + 1)) : ((affineChart i).symm.trans (affineChart j)).source = {z : Fin n → K | i.insertNth 1 z j ≠ 0}

The domain of the transition map from the standard affine chart of i to that of j consists of the points whose homogeneous coordinates Fin.insertNth i 1 z have nonzero j-th entry.

theorem Projectivization.affineChart_symm_trans_apply {K : Type u_1} [Field K] {n : ℕ} (i j : Fin (n + 1)) (z : Fin n → K) : ↑((affineChart i).symm.trans (affineChart j)) z = fun (k : Fin n) => i.insertNth 1 z (j.succAbove k) / i.insertNth 1 z j

The transition map from the standard affine chart of i to that of j divides the homogeneous coordinates Fin.insertNth i 1 z by their j-th entry.

theorem Projectivization.affineChart_apply_affineChart_symm {K : Type u_1} [Field K] {n m : ℕ} {f : Projectivization K (Fin (m + 1) → K) → Projectivization K (Fin (n + 1) → K)} {F : (Fin (m + 1) → K) → Fin (n + 1) → K} (i : Fin (m + 1)) (j : Fin (n + 1)) (z : Fin m → K) (hF : F (i.insertNth 1 z) ≠ 0) (hf : f (mk K (i.insertNth 1 z) ⋯) = mk K (F (i.insertNth 1 z)) hF) : ↑(affineChart j) (f (↑(affineChart i).symm z)) = fun (k : Fin n) => F (i.insertNth 1 z) (j.succAbove k) / F (i.insertNth 1 z) j

A map f of projective spaces sending [w] to [F w] for w = Fin.insertNth i 1 z, read in the standard affine charts at i and j: it sends z to the homogeneous ratios of F w with respect to its j-th coordinate. Outside the domain of the chart at j both sides are 0.

theorem Projectivization.apply_affineChart_symm_mem_affineOpen_iff {K : Type u_1} [Field K] {n m : ℕ} {f : Projectivization K (Fin (m + 1) → K) → Projectivization K (Fin (n + 1) → K)} {F : (Fin (m + 1) → K) → Fin (n + 1) → K} (i : Fin (m + 1)) (j : Fin (n + 1)) (z : Fin m → K) (hF : F (i.insertNth 1 z) ≠ 0) (hf : f (mk K (i.insertNth 1 z) ⋯) = mk K (F (i.insertNth 1 z)) hF) : f (↑(affineChart i).symm z) ∈ affineOpen j ↔ F (i.insertNth 1 z) j ≠ 0

The image of the point [w], for w = Fin.insertNth i 1 z, under a map f of projective spaces sending it to [F w] lies in the standard affine open at j exactly when the j-th coordinate of F w is nonzero.