A metric on projectivization: the projection embedding

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate — there is no MetricSpace on Projectivization anywhere in Mathlib today, only the staged topology).

Over an RCLike field with an inner product, each projective point p : ℙ K V determines the rank-one orthogonal projection onto its line, rankOneProj v = (‖v‖²)⁻¹ • ⟪v, ·⟫ • v — scale-invariant in v, so it descends to toProjCLM : ℙ K V → (V →L[K] V). This map is injective and continuous off the (staged) quotient topology; since ℙ K V is compact (finite dimension) and the operator space is Hausdorff, it is a closed embedding, and the operator-norm distance pulls back to a MetricSpace instance on ℙ K V whose topology is definitionally the existing quotient topology (Topology.IsEmbedding.comapMetricSpace, which replaceTopologys). The distance is

dist p q = ‖toProjCLM p − toProjCLM q‖ (Projectivization.dist_eq),

the gap metric between the lines — the standard operator-theoretic metrisation of the Fubini–Study topology.

Main declarations

• Projectivization.rankOneProj — the rank-one projection onto a vector's line, with rankOneProj_smul (scale invariance) and rankOneProj_self_apply (idempotence anchor).
• Projectivization.toProjCLM — the descended projection map on ℙ K V; toProjCLM_mk, continuous_toProjCLM, injective_toProjCLM.
• Projectivization.isClosedEmbedding_toProjCLM — compact-to-Hausdorff closed embedding.
• Projectivization.instMetricSpace — the pulled-back metric, topology-compatible by construction; Projectivization.dist_eq — the distance formula.

Downstream (this repo)

The quantified ε-ball forms of the C2 support arc (specs/BACKLOG.md Q28: "every ε-ball around a product ray", "states closer than 2ε have overlapping ε-preparations") become statable; the topological forms already landed. See MATHLIB-GAPS.md (the FS-metric row this closes) and specs/mathlib-gaps-plan.md (MG-1).

The rank-one projection onto a line

noncomputable def Projectivization.rankOneProj {K : Type u_1} {V : Type u_2} [RCLike K] [NormedAddCommGroup V] [InnerProductSpace K V] (v : V) : V →L[K] V

The rank-one projection onto the line of v: x ↦ (‖v‖²)⁻¹ ⟪v, x⟫ • v. For unit v this is the orthogonal projection onto span {v}; the normalisation makes it scale-invariant (rankOneProj_smul), which is what lets it descend to the projectivization.

Equations

• Projectivization.rankOneProj v = (↑‖v‖ ^ 2)⁻¹ • ((innerSL K) v).smulRight v

theorem Projectivization.rankOneProj_apply {K : Type u_1} {V : Type u_2} [RCLike K] [NormedAddCommGroup V] [InnerProductSpace K V] (v x : V) : (rankOneProj v) x = ((↑‖v‖ ^ 2)⁻¹ * inner K v x) • v

theorem Projectivization.normSq_coe_ne_zero {K : Type u_1} {V : Type u_2} [RCLike K] [NormedAddCommGroup V] {v : V} (hv : v ≠ 0) : ↑‖v‖ ^ 2 ≠ 0

The square of a nonzero vector's norm, coerced, is nonzero.

theorem Projectivization.rankOneProj_self_apply {K : Type u_1} {V : Type u_2} [RCLike K] [NormedAddCommGroup V] [InnerProductSpace K V] {v : V} (hv : v ≠ 0) : (rankOneProj v) v = v

The projection fixes its own line: rankOneProj v v = v.

theorem Projectivization.rankOneProj_smul {K : Type u_1} {V : Type u_2} [RCLike K] [NormedAddCommGroup V] [InnerProductSpace K V] (t : K) {v : V} (ht : t ≠ 0) (hv : v ≠ 0) : rankOneProj (t • v) = rankOneProj v

Scale invariance: the projection depends only on the line.

The descended projection map on ℙ K V

theorem Projectivization.rankOneProj_lift_aux {K : Type u_1} {V : Type u_2} [RCLike K] [NormedAddCommGroup V] [InnerProductSpace K V] (a b : { v : V // v ≠ 0 }) (t : K) (hab : ↑a = t • ↑b) : rankOneProj ↑a = rankOneProj ↑b

Scale invariance, in the exact shape Projectivization.lift consumes.

noncomputable def Projectivization.toProjCLM {K : Type u_1} {V : Type u_2} [RCLike K] [NormedAddCommGroup V] [InnerProductSpace K V] : Projectivization K V → V →L[K] V

The projection embedding of projective space into the operator space: a projective point goes to the rank-one projection onto its line.

Equations

• Projectivization.toProjCLM = Projectivization.lift (fun (v : { v : V // v ≠ 0 }) => Projectivization.rankOneProj ↑v) ⋯

@[simp]

theorem Projectivization.toProjCLM_mk {K : Type u_1} {V : Type u_2} [RCLike K] [NormedAddCommGroup V] [InnerProductSpace K V] (v : V) (hv : v ≠ 0) : (mk K v hv).toProjCLM = rankOneProj v

theorem Projectivization.continuous_toProjCLM {K : Type u_1} {V : Type u_2} [RCLike K] [NormedAddCommGroup V] [InnerProductSpace K V] : Continuous toProjCLM

The projection map is continuous off the quotient topology: the representative-level map is continuous (the bounded-bilinear smulRight composed with the continuous innerSL, scaled by the nonvanishing inverse norm-square), and the staged continuous_lift descends it.

theorem Projectivization.injective_toProjCLM {K : Type u_1} {V : Type u_2} [RCLike K] [NormedAddCommGroup V] [InnerProductSpace K V] : Function.Injective toProjCLM

Injectivity: distinct lines have distinct projections. Applying the equal projections to a representative of the second line, the first projection fixes it, so the representatives are collinear.

The metric

theorem Projectivization.isClosedEmbedding_toProjCLM {K : Type u_1} {V : Type u_2} [RCLike K] [NormedAddCommGroup V] [InnerProductSpace K V] [FiniteDimensional K V] : Topology.IsClosedEmbedding toProjCLM

The projection embedding is a closed embedding: continuous and injective from the compact ℙ K V (staged instCompactSpace) into the Hausdorff operator space.

@[instance_reducible]

noncomputable instance Projectivization.instMetricSpace {K : Type u_1} {V : Type u_2} [RCLike K] [NormedAddCommGroup V] [InnerProductSpace K V] [FiniteDimensional K V] : MetricSpace (Projectivization K V)

The metric on projectivization: the operator-norm distance between the lines' projections, pulled back through the closed embedding. comapMetricSpace installs the metric with replaceTopology, so the metric topology is definitionally the staged quotient topology — no diamond with instTopologicalSpace.

Equations

• Projectivization.instMetricSpace = Topology.IsEmbedding.comapMetricSpace Projectivization.toProjCLM ⋯

theorem Projectivization.dist_eq {K : Type u_1} {V : Type u_2} [RCLike K] [NormedAddCommGroup V] [InnerProductSpace K V] [FiniteDimensional K V] (p q : Projectivization K V) : dist p q = ‖p.toProjCLM - q.toProjCLM‖

The distance formula: the gap between the lines, as the operator-norm distance of their projections.