Topology on projectivization

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

The quotient topology on Projectivization K V is inherited from instTopologicalSpaceQuotient. Because Projectivization K V is a def (not @[reducible]) over Quotient (projectivizationSetoid K V), typeclass synthesis does not unfold it; this file installs the explicit TopologicalSpace (ℙ K V) instance and develops its consequences:

• Projectivization.continuous_mk': the canonical surjection {v : V // v ≠ 0} → ℙ K V is continuous.
• Projectivization.isOpenMap_mk': the canonical surjection is an open map. Proved directly using mk' ⁻¹' (mk' '' U) = ⋃ a : Kˣ, scaleNonzero a '' U.
• Projectivization.isQuotientMap_mk' and Projectivization.isOpenQuotientMap_mk': combine openness + continuity
  • surjectivity.

For [RCLike K] and finite-dimensional normed V:

• Projectivization.instT2Space: Hausdorffness, via the open-quotient-map criterion t2Space_iff_of_isOpenQuotientMap reduced to closedness of the K-collinearity relation, which in turn follows from isOpen_setOfPred_linearIndependent and LinearIndependent.pair_iff'.
• Projectivization.instCompactSpace: compactness, via continuous surjection from Metric.sphere (0 : V) 1 (compact by Heine-Borel in finite-dim normed).

Provenance

Staged as upstream Mathlib material. All declarations live under namespace Projectivization with no CsdLean4-namespace prefix; the file is intended to land in Mathlib/LinearAlgebra/Projectivization/Topology.lean once usage stabilises. Naming, docstring format, and import discipline track Mathlib idiom.

Tags

projectivization, projective space, quotient topology

@[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 Projectivization K V.

Projectivization is a def over Quotient (projectivizationSetoid K V), so the generic instTopologicalSpaceQuotient does not fire by typeclass synthesis alone. We provide the explicit forwarding instance.

Equations

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

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

The canonical surjection {v : V // v ≠ 0} → ℙ K V is continuous.

def Projectivization.scaleNonzero {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (a : Kˣ) (v : { v : V // v ≠ 0 }) : { v : V // v ≠ 0 }

Scaling by a unit a : Kˣ corestricts to a self-map of the nonzero subtype {v : V // v ≠ 0}.

Equations

• Projectivization.scaleNonzero a v = ⟨↑a • ↑v, ⋯⟩

@[simp]

theorem Projectivization.scaleNonzero_coe {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (a : Kˣ) (v : { v : V // v ≠ 0 }) : ↑(scaleNonzero a v) = ↑a • ↑v

theorem Projectivization.scaleNonzero_mul {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (a b : Kˣ) (v : { v : V // v ≠ 0 }) : scaleNonzero a (scaleNonzero b v) = scaleNonzero (a * b) v

@[simp]

theorem Projectivization.scaleNonzero_one {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : { v : V // v ≠ 0 }) : scaleNonzero 1 v = v

theorem Projectivization.continuous_scaleNonzero {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] [TopologicalSpace V] [ContinuousConstSMul K V] (a : Kˣ) : Continuous (scaleNonzero a)

Scaling by a unit, viewed as a self-map of {v : V // v ≠ 0}, is continuous: it is the corestriction of the continuous map (a : K) • · : V → V along the subtype inclusion.

def Projectivization.scaleNonzeroHomeo {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] [TopologicalSpace V] [ContinuousConstSMul K V] (a : Kˣ) : { v : V // v ≠ 0 } ≃ₜ { v : V // v ≠ 0 }

Scaling by a unit is a homeomorphism of the nonzero subtype, with inverse given by scaling by the inverse unit.

Equations

• One or more equations did not get rendered due to their size.

theorem Projectivization.mk'_preimage_mk'_image {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ˣ), scaleNonzero a '' U

Saturation lemma: pulling the image of a set U ⊆ {v : V // v ≠ 0} back through mk' K recovers the orbit of U under the Kˣ scaling action on the nonzero subtype.

This is the projectivization analogue of MulAction.quotient_preimage_image_eq_union_mul. The projectivization setoid (defined as (MulAction.orbitRel Kˣ V).comap (↑)) gives the same orbit relation on the nonzero subtype as the unit-action; this lemma makes that explicit at the set level.

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)

The canonical surjection {v : V // v ≠ 0} → ℙ K V is an open map.

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

The canonical surjection {v : V // v ≠ 0} → ℙ K V is a quotient map.

Combines openness, continuity, and surjectivity via IsOpenMap.isQuotientMap.

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)

The canonical surjection {v : V // v ≠ 0} → ℙ K V is an open quotient map.

Continuity descent

Companions to the lift_measurable / measurable_iff_measurable_comp_mk' pair in MeasureSpace.lean: a function out of ℙ K V is continuous iff its precomposition with mk' is, and a scale-invariant continuous function on the nonzero subtype descends to a continuous function on ℙ K V.

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

A function out of ℙ K V is continuous iff its precomposition with mk' is continuous. Topological companion to measurable_iff_measurable_comp_mk' in MeasureSpace.lean.

theorem Projectivization.continuous_lift {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] [TopologicalSpace V] [ContinuousConstSMul K 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_lift 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] [ContinuousConstSMul K 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).

@[instance_reducible]

instance Projectivization.instMulAction {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] : MulAction (V ≃ₗ[K] V) (Projectivization K V)

V ≃ₗ[K] V acts on Projectivization K V via mapEquiv.

The group structure on V ≃ₗ[K] V (LinearEquiv.automorphismGroup, with 1 = refl and e₁ * e₂ = e₂.trans e₁) transports to a MulAction on ℙ K V because Projectivization.map_id discharges one_smul and Projectivization.map_comp discharges mul_smul.

Equations

• Projectivization.instMulAction = { smul := Projectivization.mapEquiv, mul_smul := ⋯, one_smul := ⋯ }

@[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

theorem Projectivization.mapEquiv_continuous {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] [TopologicalSpace V] [ContinuousConstSMul K 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 = ℂ for LF4) 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.