The quotient topology on projective space

ℙ K V is the quotient of the nonzero vectors {v : V // v ≠ 0} by the action of Kˣ. When V carries a topology, Mathlib gives ℙ K V the quotient topology (Projectivization.instTopologicalSpace) and shows that the quotient map Projectivization.mk' is an open quotient map as soon as scalar multiplication by units of K is continuous on V (Projectivization.isOpenQuotientMap_mk', in Mathlib/Topology/Algebra/Projectivization).

We prove the separation and compactness properties of this topology which make projective space a compact Hausdorff space, the ambient space of projective algebraic sets. Over a topological field K whose continuous linear forms on V separate points (for instance any normed space over ℝ or ℂ, by the Hahn–Banach theorem), two nonzero vectors span the same line exactly when f v * g w = f w * g v for all continuous linear forms f and g. These are closed conditions, so the relation is closed and ℙ K V is Hausdorff. Over ℝ or ℂ every line meets the unit sphere, so for finite-dimensional V the projective space is a continuous image of a compact sphere and is compact. Second countability passes to ℙ K V along the open quotient map. When V has real dimension greater than one, its nonzero vectors form a path-connected space, so ℙ K V is path-connected; over ℝ or ℂ the only other nonzero case is a real line, whose projectivization is a point. Hence ℙ 𝕜 V is path-connected, and in particular connected, for every nonzero normed space V over ℝ or ℂ.

Finally, over a field with continuous multiplication and inversion, the standard affine charts Projectivization.affineChart i of ℙ K (Fin (n + 1) → K) are homeomorphisms from the open sets U_i = {[v] | v i ≠ 0} onto the affine space Fin n → K. These charts form the standard atlas of projective space.

Main results

• Projectivization.isOpen_linearProjectionDomain: the points where a continuous linear map does not vanish form an open set.
• Projectivization.mk'_eq_mk'_iff_forall_strongDual: when continuous linear forms separate points, two nonzero vectors span the same line iff all the 2 × 2 minors f v * g w - f w * g v vanish.
• Projectivization.instT2Space: ℙ K V is Hausdorff when continuous linear forms separate points.
• Projectivization.instCompactSpace: ℙ 𝕜 V is compact for a finite-dimensional normed space V over ℝ or ℂ.
• Projectivization.instSecondCountableTopology: ℙ K V is second countable when V is.
• Projectivization.pathConnectedSpace_of_one_lt_rank: ℙ K V is path-connected when V has real dimension greater than one, for any division ring K.
• Projectivization.instPathConnectedSpace: ℙ 𝕜 V is path-connected for a nonzero normed space V over ℝ or ℂ.
• Projectivization.isOpen_affineOpen: the standard affine opens are open.
• Projectivization.affineOpenPartialHomeomorph: the standard affine chart as an open partial homeomorphism from U_i onto Fin n → K.
• Projectivization.interAffineOpenHomeomorph: the affine chart identifies the part X ∩ U_i of a set X with its image in Fin n → K.

theorem Projectivization.isOpen_linearProjectionDomain {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] [TopologicalSpace V] {W : Type u_3} [AddCommGroup W] [Module K W] [TopologicalSpace W] [T1Space W] {G : V →ₗ[K] W} (hG : Continuous ⇑G) : IsOpen (linearProjectionDomain G)

The set of points at which a continuous linear map does not vanish, the domain of Projectivization.linearProjection G, is open.

instance Projectivization.instSecondCountableTopology {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] [TopologicalSpace V] [ContinuousConstSMul Kˣ V] [SecondCountableTopology V] : SecondCountableTopology (Projectivization K V)

Projective space is second countable when the vector space is.

theorem Projectivization.mk'_eq_mk'_iff_forall_strongDual {K : Type u_1} {V : Type u_2} [Field K] [TopologicalSpace K] [AddCommGroup V] [Module K V] [TopologicalSpace V] [SeparatingDual K V] (v w : { v : V // v ≠ 0 }) : mk' K v = mk' K w ↔ ∀ (f g : StrongDual K V), f ↑v * g ↑w = f ↑w * g ↑v

When continuous linear forms separate the points of V, two nonzero vectors span the same line iff the 2 × 2 minors f v * g w - f w * g v vanish for all continuous linear forms f and g.

instance Projectivization.instT2Space {K : Type u_1} {V : Type u_2} [Field K] [TopologicalSpace K] [AddCommGroup V] [Module K V] [TopologicalSpace V] [T2Space K] [ContinuousMul K] [ContinuousConstSMul Kˣ V] [SeparatingDual K V] : T2Space (Projectivization K V)

Projective space is Hausdorff over a Hausdorff topological field, when continuous linear forms separate the points of V: the relation of spanning the same line is cut out by the closed conditions f v * g w = f w * g v, and the quotient map is open.

theorem Projectivization.exists_norm_eq_one_mk_eq {𝕜 : Type u_1} {V : Type u_2} [RCLike 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] (x : Projectivization 𝕜 V) : ∃ (v : V) (hv : v ≠ 0), ‖v‖ = 1 ∧ mk 𝕜 v hv = x

Every point of ℙ 𝕜 V is spanned by a unit vector.

instance Projectivization.instCompactSpace {𝕜 : Type u_1} {V : Type u_2} [RCLike 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] : CompactSpace (Projectivization 𝕜 V)

Projective space is compact for a finite-dimensional normed space over ℝ or ℂ: it is the image of the compact unit sphere.

Connectedness

theorem Projectivization.pathConnectedSpace_of_one_lt_rank {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] [TopologicalSpace V] [Module ℝ V] [ContinuousAdd V] [ContinuousSMul ℝ V] (h : 1 < Module.rank ℝ V) : PathConnectedSpace (Projectivization K V)

Projective space is path-connected when V, as a real topological vector space, has dimension greater than one: it is then the continuous image of the path-connected space of nonzero vectors. The division ring K is arbitrary, so this applies equally to real, complex and quaternionic projective spaces.

instance Projectivization.instPathConnectedSpace {𝕜 : Type u_1} {V : Type u_2} [RCLike 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [Nontrivial V] : PathConnectedSpace (Projectivization 𝕜 V)

Projective space is path-connected for a nonzero normed space V over ℝ or ℂ, hence connected. In real dimension greater than one this is pathConnectedSpace_of_one_lt_rank; otherwise V is a line and ℙ 𝕜 V is a single point. In particular ℂℙⁿ and ℝℙⁿ are connected for every n, including the point n = 0.

The standard affine charts

theorem Projectivization.isOpen_affineOpen {K : Type u_1} [DivisionRing K] [TopologicalSpace K] [T1Space K] {ι : Type u_2} (i : ι) : IsOpen (affineOpen i)

The standard affine open of projective space, where a given homogeneous coordinate is nonzero, is open.

theorem Projectivization.continuous_affineChart_symm {K : Type u_1} [Field K] [TopologicalSpace K] {n : ℕ} (i : Fin (n + 1)) : Continuous ↑(affineChart i).symm

The inverse z ↦ [Fin.insertNth i 1 z] of the standard affine chart is continuous.

theorem Projectivization.continuousOn_affineChart {K : Type u_1} [Field K] [TopologicalSpace K] {n : ℕ} [ContinuousMul K] [ContinuousInv₀ K] (i : Fin (n + 1)) : ContinuousOn (↑(affineChart i)) (affineOpen i)

The standard affine chart of projective space is continuous on its domain.

noncomputable def Projectivization.affineOpenPartialHomeomorph {K : Type u_1} [Field K] [TopologicalSpace K] {n : ℕ} [ContinuousMul K] [ContinuousInv₀ K] [T1Space K] (i : Fin (n + 1)) : OpenPartialHomeomorph (Projectivization K (Fin (n + 1) → K)) (Fin n → K)

The standard affine chart of projective space at the coordinate i, as an open partial homeomorphism from the affine open U_i = {[v] | v i ≠ 0} onto Fin n → K.

@[simp]

theorem Projectivization.affineOpenPartialHomeomorph_toPartialEquiv {K : Type u_1} [Field K] [TopologicalSpace K] {n : ℕ} [ContinuousMul K] [ContinuousInv₀ K] [T1Space K] (i : Fin (n + 1)) : (affineOpenPartialHomeomorph i).toPartialEquiv = affineChart i

@[simp]

theorem Projectivization.coe_affineOpenPartialHomeomorph {K : Type u_1} [Field K] [TopologicalSpace K] {n : ℕ} [ContinuousMul K] [ContinuousInv₀ K] [T1Space K] (i : Fin (n + 1)) : ↑(affineOpenPartialHomeomorph i) = ↑(affineChart i)

@[simp]

theorem Projectivization.coe_affineOpenPartialHomeomorph_symm {K : Type u_1} [Field K] [TopologicalSpace K] {n : ℕ} [ContinuousMul K] [ContinuousInv₀ K] [T1Space K] (i : Fin (n + 1)) : ↑(affineOpenPartialHomeomorph i).symm = ↑(affineChart i).symm

noncomputable def Projectivization.interAffineOpenHomeomorph {K : Type u_1} [Field K] [TopologicalSpace K] {n : ℕ} [ContinuousMul K] [ContinuousInv₀ K] [T1Space K] {X : Set (Projectivization K (Fin (n + 1) → K))} {i : Fin (n + 1)} {Z : Set (Fin n → K)} (hZ : ↑(affineChart i) '' (X ∩ affineOpen i) = Z) : ↑(X ∩ affineOpen i) ≃ₜ ↑Z

The affine part of a subset of projective space. The standard affine chart at the coordinate i restricts to a homeomorphism from the part X ∩ U_i of a set X inside the affine open U_i = {[v] | v i ≠ 0} onto its image Z in Fin n → K.

@[simp]

theorem Projectivization.coe_interAffineOpenHomeomorph_apply {K : Type u_1} [Field K] [TopologicalSpace K] {n : ℕ} [ContinuousMul K] [ContinuousInv₀ K] [T1Space K] {X : Set (Projectivization K (Fin (n + 1) → K))} {i : Fin (n + 1)} {Z : Set (Fin n → K)} (hZ : ↑(affineChart i) '' (X ∩ affineOpen i) = Z) (y : ↑(X ∩ affineOpen i)) : ↑((interAffineOpenHomeomorph hZ) y) = ↑(affineChart i) ↑y

The homeomorphism Projectivization.interAffineOpenHomeomorph is the affine chart.

@[simp]

theorem Projectivization.coe_interAffineOpenHomeomorph_symm_apply {K : Type u_1} [Field K] [TopologicalSpace K] {n : ℕ} [ContinuousMul K] [ContinuousInv₀ K] [T1Space K] {X : Set (Projectivization K (Fin (n + 1) → K))} {i : Fin (n + 1)} {Z : Set (Fin n → K)} (hZ : ↑(affineChart i) '' (X ∩ affineOpen i) = Z) (z : ↑Z) : ↑((interAffineOpenHomeomorph hZ).symm z) = ↑(affineChart i).symm ↑z

The inverse of Projectivization.interAffineOpenHomeomorph is the inverse affine chart.