The quotient topology on projective space

Category: 1-Mathlib (CSD-free Mathlib upstream candidates).

ℙ K V is the quotient of the nonzero vectors {v : V // v ≠ 0} by the action of Kˣ. When V carries a topology we give ℙ K V the quotient topology, and we show that the quotient map Projectivization.mk' is an open quotient map as soon as scalar multiplication by units of K is continuous on V.

Main results

• Projectivization.instTopologicalSpace: the quotient topology on ℙ K V.
• Projectivization.isQuotientMap_mk', Projectivization.continuous_mk': mk' K : {v : V // v ≠ 0} → ℙ K V is a quotient map, in particular continuous.
• Projectivization.isOpenQuotientMap_mk': mk' K is an open quotient map when Kˣ acts continuously on V.
• Projectivization.continuous_iff: a map out of ℙ K V is continuous iff its composite with mk' K is.

Beyond the upstream text, and staying here:

• Projectivization.continuous_lift: a scale-invariant continuous function on the nonzero subtype descends continuously, the topological companion of lift_measurable.
• Projectivization.mapOfInjective_continuous, Projectivization.mapEquiv and its lemmas: continuity of the map induced by an injective linear map, and the LinearEquiv action.
• Projectivization.instT2Space, Projectivization.instCompactSpace: ℙ K V is compact Hausdorff for [RCLike K] and finite-dimensional normed V.
• Projectivization.connectedSpace_of_isConnected_nonzero: connectedness from connectedness of the nonzero vectors.

Provenance

Staged as upstream Mathlib material. The first section below is the Mathlib pull-request text verbatim (Mathlib/LinearAlgebra/Projectivization/Topology.lean, six declarations), so that this repository and the pull request are the same code and any drift between them is visible. Two divergences, both forced by this repository's Mathlib pin and neither touching a statement: the module-system header and this docstring, which the lints here require; and isOpenMap_mk' spelling the coinducing step isQuotientMap_mk'.isCoinducing.isOpen_preimage, since IsQuotientMap.isOpen_preimage postdates the pin. The remaining sections are this repository's own and are the second pull request's material (Hausdorffness, compactness) or stay here.

The Kˣ-action on {v : V // v ≠ 0} is Mathlib's, through Units.nonZeroSubMul; the continuity instance it needs is staged in CsdLean4/Mathlib/Topology/Algebra/MulAction.lean. Until 2026-09-19 this file carried its own scaleNonzero / scaleNonzeroHomeo reimplementation of that action and its own saturation lemma, 461 lines against the 82 of the pull request.

Tags

projectivization, projective space, quotient topology

The upstream text

Everything between here and the end of this section is the Mathlib pull request verbatim. It is wrapped in a section of its own so that its variable lines stop where the pull request file stops, and do not reach the material this repository keeps below.

theorem Projectivization.mk'_eq_mk'_iff {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v w : { v : V // v ≠ 0 }) : mk' K v = mk' K w ↔ ∃ (a : Kˣ), a • w = v

Two nonzero vectors have the same image in ℙ K V iff one is a unit multiple of the other, for the action of Kˣ on {v : V // v ≠ 0}.

theorem Projectivization.preimage_image_mk' {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (U : Set { v : V // v ≠ 0 }) : mk' K ⁻¹' mk' K '' U = ⋃ (a : Kˣ), (fun (x : { v : V // v ≠ 0 }) => a • x) '' U

The saturation of a set of nonzero vectors under mk' is the union of its translates by the units of K.

@[instance_reducible]

instance Projectivization.instTopologicalSpace {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] [TopologicalSpace V] : TopologicalSpace (Projectivization K V)

The quotient topology on ℙ K V, coinduced by Projectivization.mk'.

Equations

• Projectivization.instTopologicalSpace = { IsOpen := Projectivization.instTopologicalSpace._aux_1, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

theorem Projectivization.isQuotientMap_mk' {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] [TopologicalSpace V] : Topology.IsQuotientMap (mk' K)

theorem Projectivization.continuous_mk' {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] [TopologicalSpace V] : Continuous (mk' K)

theorem Projectivization.continuous_iff {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] [TopologicalSpace V] {α : Type u_3} [TopologicalSpace α] {f : Projectivization K V → α} : Continuous f ↔ Continuous (f ∘ mk' K)

theorem Projectivization.isOpenMap_mk' {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] [TopologicalSpace V] [ContinuousConstSMul Kˣ V] : IsOpenMap (mk' K)

theorem Projectivization.isOpenQuotientMap_mk' {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] [TopologicalSpace V] [ContinuousConstSMul Kˣ V] : IsOpenQuotientMap (mk' K)

Continuity descent

Companion to the lift_measurable / measurable_iff_measurable_comp_mk' pair in MeasureSpace.lean: a scale-invariant continuous function on the nonzero subtype descends to a continuous function on ℙ K V.

theorem Projectivization.continuous_lift {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] [TopologicalSpace V] {α : Type u_3} [TopologicalSpace α] (f : { v : V // v ≠ 0 } → α) (hf : ∀ (a b : { v : V // v ≠ 0 }) (t : K), ↑a = t • ↑b → f a = f b) (hf_cont : Continuous f) : Continuous (Projectivization.lift f hf)

A scale-invariant continuous function on the nonzero subtype descends to a continuous function on ℙ K V. Topological companion to lift_measurable in MeasureSpace.lean.

Continuity of Projectivization.map

A continuous injective linear map between modules descends to a continuous map between projectivizations. Builds on continuous_iff above via the standard mk' quotient-map characterisation of continuity.

theorem Projectivization.mapOfInjective_continuous {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] (f : V →ₗ[K] W) (hf : Function.Injective ⇑f) (hf_cont : Continuous ⇑f) : Continuous (map f hf)

A continuous injective linear map descends to a continuous map on projectivizations.

LinearEquiv action on projectivization

A linear self-equivalence e : V ≃ₗ[K] V induces a self-map mapEquiv e : ℙ K V → ℙ K V via Projectivization.map and the canonical injectivity of an equivalence. The construction respects the group structure of V ≃ₗ[K] V via Projectivization.map_id and Projectivization.map_comp.

def Projectivization.mapEquiv {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (e : V ≃ₗ[K] V) : Projectivization K V → Projectivization K V

A linear self-equivalence induces a self-map of the projectivization.

Equations

• Projectivization.mapEquiv e = Projectivization.map ↑e ⋯

@[simp]

theorem Projectivization.mapEquiv_refl {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] : mapEquiv (LinearEquiv.refl K V) = id

@[simp]

theorem Projectivization.mapEquiv_one {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] : mapEquiv 1 = id

The induced map of the identity equivalence is the identity. Syntactic alias for mapEquiv_refl under the Group notation 1 for LinearEquiv.refl (definitionally equal via LinearEquiv.one_eq_refl).

theorem Projectivization.mapEquiv_mul {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (e₁ e₂ : V ≃ₗ[K] V) : mapEquiv (e₁ * e₂) = mapEquiv e₁ ∘ mapEquiv e₂

The induced map of a product of linear self-equivalences equals the composition of the induced maps. Discharged via Projectivization.map_comp applied to the toLinearMap composition: (e₁ * e₂).toLinearMap = e₁.toLinearMap.comp e₂.toLinearMap (= * in the linear-endomorphism ring; both equal by rfl via LinearEquiv.coe_toLinearMap_mul + LinearMap.mul_eq_comp).

@[simp]

theorem Projectivization.mapEquiv_smul_eq {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (e : V ≃ₗ[K] V) (p : Projectivization K V) : e • p = mapEquiv e p

The action of V ≃ₗ[K] V on ℙ K V is Mathlib's Projectivization.instMulAction (Mathlib/LinearAlgebra/Projectivization/Action.lean: any group acting K-linearly on V acts on ℙ K V), specialised to G := V ≃ₗ[K] V through LinearEquiv.applyDistribMulAction; on representatives it is mapEquiv. Until 2026-09-16 this file declared its own instance under the same auto-generated name, which made the two files impossible to import together.

theorem Projectivization.mapEquiv_continuous {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] [TopologicalSpace V] (e : V ≃ₗ[K] V) (he : Continuous ⇑e) : Continuous (mapEquiv e)

The mapEquiv of a continuous linear equivalence is continuous.

Hausdorffness and compactness under normed finite-dim hypotheses

Under [RCLike K] (so K ∈ {ℝ, ℂ} with the usual analytic structure) and [NormedAddCommGroup V] [NormedSpace K V] [FiniteDimensional K V], the projectivization ℙ K V is a compact Hausdorff space.

The hypothesis pattern can be relaxed to [NontriviallyNormedField K]

• [LocallyCompactSpace K] + [NormedAlgebra ℝ K] (sufficient for the unit-sphere normalisation argument), but the RCLike form covers the case of interest (K = ℂ) with strictly less typeclass friction.

theorem Projectivization.isClosed_collinearity_relation {K : Type u_1} {V : Type u_2} [RCLike K] [NormedAddCommGroup V] [NormedSpace K V] : IsClosed {p : { v : V // v ≠ 0 } × { v : V // v ≠ 0 } | mk' K p.1 = mk' K p.2}

The K-collinearity relation on the nonzero subtype is closed.

Two nonzero vectors v, w represent the same projective point iff their pair is linearly dependent (mk_eq_mk_iff' + LinearIndependent.pair_iff'), and the set of linearly dependent pairs is the complement of an open set via isOpen_setOfPred_linearIndependent.

instance Projectivization.instT2Space {K : Type u_1} {V : Type u_2} [RCLike K] [NormedAddCommGroup V] [NormedSpace K V] : T2Space (Projectivization K V)

ℙ K V is Hausdorff under finite-dimensional normed hypotheses on V. Routes through the open-quotient-map criterion t2Space_iff_of_isOpenQuotientMap plus isClosed_collinearity_relation.

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

ℙ K V is compact under finite-dimensional normed hypotheses on V. The unit sphere Metric.sphere (0 : V) 1 is compact as a subtype (Heine-Borel in finite-dim normed; FiniteDimensional.proper_rclike + Metric.sphere.compactSpace), and the corestriction of mk K to the sphere is a continuous surjection from sphere to ℙ K V (every projective point has a unit-norm representative obtained by normalising p.rep).

theorem Projectivization.mapEquiv_continuous_of_finiteDim {K : Type u_1} {V : Type u_2} [RCLike K] [NormedAddCommGroup V] [NormedSpace K V] [FiniteDimensional K V] (e : V ≃ₗ[K] V) : Continuous (mapEquiv e)

In finite-dim normed setting over RCLike, every linear self-equivalence of V is continuous (Banach), so its induced projectivization map is continuous for free.

instance Projectivization.instContinuousConstSMul {K : Type u_1} {V : Type u_2} [RCLike K] [NormedAddCommGroup V] [NormedSpace K V] [FiniteDimensional K V] : ContinuousConstSMul (V ≃ₗ[K] V) (Projectivization K V)

Each individual (V ≃ₗ[K] V)-action on ℙ K V is continuous in the finite-dim normed setting. This is ContinuousConstSMul, which captures continuity in the action argument for every fixed group element. Joint continuity in both arguments (ContinuousSMul) is a strictly stronger statement requiring a topology on V ≃ₗ[K] V itself; deferred.

Connectedness

The projectivization of a module whose nonzero vectors form a connected set is itself connected: it is the continuous image of {v // v ≠ 0} under mk'. Downstream, for an RCLike field and real rank > 1, the nonzero set is connected because the complement of a point in a real normed space of rank > 1 is connected (isConnected_compl_singleton_of_one_lt_rank).

theorem Projectivization.mk'_surjective {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] : Function.Surjective (mk' K)

The canonical surjection mk' is surjective onto the projectivization.

theorem Projectivization.connectedSpace_of_isConnected_nonzero {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] [TopologicalSpace V] (h : IsConnected {v : V | v ≠ 0}) : ConnectedSpace (Projectivization K V)

If the nonzero vectors form a connected set, the projectivization is a connected space.