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 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.
• Projectivization.continuous_mk, Projectivization.continuous_map: Projectivization.mk and Projectivization.map are continuous.

@[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.continuous_mk {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] [TopologicalSpace V] {α : Type u_3} [TopologicalSpace α] {f : α → V} (hf : Continuous f) (hf₀ : ∀ (x : α), f x ≠ 0) : Continuous fun (x : α) => mk K (f x) ⋯

Projectivization.mk is continuous in the vector, as long as the vector stays nonzero.

theorem Projectivization.continuous_map {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] [TopologicalSpace V] {L : Type u_4} {W : Type u_5} [DivisionRing L] [AddCommGroup W] [Module L W] [TopologicalSpace W] {σ : K →+* L} {f : V →ₛₗ[σ] W} (hf : Function.Injective ⇑f) (hfc : Continuous ⇑f) : Continuous (map f hf)

An injective continuous semilinear map induces a continuous map on projective spaces.

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)