Complex projective space as a quotient of an odd sphere

Complex projective n-space CPⁿ is modelled as the quotient of the unit sphere S²ⁿ⁺¹ of EuclideanSpace ℂ (Fin (n + 1)) by the action of the unit complex numbers S¹ ⊆ ℂ by scalar multiplication: two unit vectors define the same point exactly when one is a unit complex multiple of the other (TauCeti.ComplexProjectiveSpace.mk_eq_mk_iff). Every complex line through the origin meets the unit sphere in exactly one such orbit, so this models the space of complex lines in ℂⁿ⁺¹.

The circle is compact, so its action on the sphere is proper (TauCeti.properSMul_of_compactSpace) and the quotient is Hausdorff. It is compact and path connected as a continuous image of the sphere, and the projection is an open quotient map.

Main declarations

• TauCeti.ComplexProjectiveSpace: complex projective n-space as a circle quotient of S²ⁿ⁺¹.
• TauCeti.ComplexProjectiveSpace.mk: the projection from the unit sphere.
• TauCeti.ComplexProjectiveSpace.lift: functions on the sphere invariant under unit complex scalars descend to CPⁿ.
• TauCeti.ComplexProjectiveSpace.mk_eq_mk_iff: two unit vectors define the same point exactly when they differ by a unit complex scalar.
• TauCeti.ComplexProjectiveSpace.isOpenQuotientMap_mk: the projection is an open quotient map.
• TauCeti.ComplexProjectiveSpace.instT2Space, instCompactSpace, instPathConnectedSpace: CPⁿ is a compact, path-connected Hausdorff space.
• TauCeti.ComplexProjectiveSpace.instSubsingletonZero: CP⁰ is a point.

References

• A. Hatcher, Algebraic Topology, Chapter 0, Example 0.6.
• The quotient model and its API adapt Tau Ceti's real projective space in TauCeti/AlgebraicTopology/UniversalCover/RealProjective/Basic.lean.

def TauCeti.ComplexProjectiveSpace (n : ℕ) : Type

Complex projective n-space, modelled as the orbit quotient of the unit sphere of EuclideanSpace ℂ (Fin (n + 1)) under scalar multiplication by unit complex numbers.

@[instance_reducible]

instance TauCeti.ComplexProjectiveSpace.instTopologicalSpace (n : ℕ) : TopologicalSpace (ComplexProjectiveSpace n)

The quotient topology on complex projective space.

instance TauCeti.ComplexProjectiveSpace.instCompactSpace (n : ℕ) : CompactSpace (ComplexProjectiveSpace n)

Complex projective space is compact as a quotient of the compact unit sphere.

instance TauCeti.ComplexProjectiveSpace.instT2Space (n : ℕ) : T2Space (ComplexProjectiveSpace n)

Complex projective space is Hausdorff: the compact circle acts properly on the unit sphere.

noncomputable def TauCeti.ComplexProjectiveSpace.mk (n : ℕ) : ↑(Metric.sphere 0 1) → ComplexProjectiveSpace n

The projection from the unit sphere onto complex projective space.

theorem TauCeti.ComplexProjectiveSpace.mk_surjective (n : ℕ) : Function.Surjective (mk n)

Every point of complex projective space has a unit-vector representative.

theorem TauCeti.ComplexProjectiveSpace.inductionOn (n : ℕ) {motive : ComplexProjectiveSpace n → Prop} (x : ComplexProjectiveSpace n) (h : ∀ (y : ↑(Metric.sphere 0 1)), motive (mk n y)) : motive x

To prove a property of every point of complex projective space, it suffices to prove it on the image of every unit vector.

@[simp]

theorem TauCeti.ComplexProjectiveSpace.mk_eq_mk_iff (n : ℕ) (x y : ↑(Metric.sphere 0 1)) : mk n x = mk n y ↔ ∃ (c : ↑(Metric.sphere 0 1)), c • y = x

Two unit vectors define the same point of complex projective space exactly when they differ by a unit complex scalar.

@[simp]

theorem TauCeti.ComplexProjectiveSpace.mk_smul (n : ℕ) (c : ↑(Metric.sphere 0 1)) (x : ↑(Metric.sphere 0 1)) : mk n (c • x) = mk n x

Unit complex multiples of a unit vector define the same point of complex projective space.

noncomputable def TauCeti.ComplexProjectiveSpace.lift (n : ℕ) {α : Sort u_1} (f : ↑(Metric.sphere 0 1) → α) (h : ∀ (c : ↑(Metric.sphere 0 1)) (x : ↑(Metric.sphere 0 1)), f (c • x) = f x) : ComplexProjectiveSpace n → α

A function on the unit sphere invariant under unit complex scalars descends to complex projective space.

@[simp]

theorem TauCeti.ComplexProjectiveSpace.lift_mk (n : ℕ) {α : Sort u_1} (f : ↑(Metric.sphere 0 1) → α) (h : ∀ (c : ↑(Metric.sphere 0 1)) (x : ↑(Metric.sphere 0 1)), f (c • x) = f x) (x : ↑(Metric.sphere 0 1)) : ComplexProjectiveSpace.lift n f h (mk n x) = f x

Lifting an invariant function and applying it to a representative recovers the function.

theorem TauCeti.ComplexProjectiveSpace.isOpenQuotientMap_mk (n : ℕ) : IsOpenQuotientMap (mk n)

The projection from the unit sphere onto complex projective space is an open quotient map.

theorem TauCeti.ComplexProjectiveSpace.continuous_mk (n : ℕ) : Continuous (mk n)

The projection from the unit sphere onto complex projective space is continuous.

theorem TauCeti.ComplexProjectiveSpace.continuousAt_lift (n : ℕ) {α : Type u_1} [TopologicalSpace α] {f : ↑(Metric.sphere 0 1) → α} (h : ∀ (c : ↑(Metric.sphere 0 1)) (x : ↑(Metric.sphere 0 1)), f (c • x) = f x) {x : ↑(Metric.sphere 0 1)} (hf : ContinuousAt f x) : ContinuousAt (ComplexProjectiveSpace.lift n f h) (mk n x)

The lift of an invariant function is continuous at the class of every unit vector at which the function is continuous, because the projection is an open quotient map.

instance TauCeti.ComplexProjectiveSpace.instNonempty (n : ℕ) : Nonempty (ComplexProjectiveSpace n)

Complex projective space is nonempty.

instance TauCeti.ComplexProjectiveSpace.instSubsingletonZero : Subsingleton (ComplexProjectiveSpace 0)

Complex projective 0-space is a point: two unit vectors of ℂ¹ differ by a unit scalar.

instance TauCeti.ComplexProjectiveSpace.instPathConnectedSpace (n : ℕ) : PathConnectedSpace (ComplexProjectiveSpace n)

Complex projective space is path connected, as a continuous image of the unit sphere of the real vector space underlying ℂⁿ⁺¹, of real dimension 2n + 2 > 1.