ProjectiveTopology.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Hausdorff projective spaces and topological projective maps

instance OAI.Nagata.W21.projectivizationTopologicalSpace line 18
theorem OAI.Nagata.W21.continuous_projectivization_mk' line 23
theorem OAI.Nagata.W21.isQuotientMap_projectivization_mk' line 28

theorem OAI.Nagata.Workers.W11.projectivization_mk'_eq_iff_minors line 53

Source documentation

Proportionality of nonzero complex vectors is detected by the actual coordinate minors.

theorem projectivization_mk'_eq_iff_minors
    (v w : {x : ι → ℂ // x ≠ 0}) :
    Projectivization.mk' ℂ v = Projectivization.mk' ℂ w ↔
      ∀ i j, v.val i * w.val j = v.val j * w.val i := by
…

theorem OAI.Nagata.Workers.W11.isClosed_projectivization_relation line 82

Source documentation

The relation defining projective points is closed in the product of the actual nonzero-vector spaces.

theorem isClosed_projectivization_relation :
    IsClosed {p : {x : ι → ℂ // x ≠ 0} × {x : ι → ℂ // x ≠ 0} |
      Projectivization.mk' ℂ p.1 = Projectivization.mk' ℂ p.2} := by
…

def OAI.Nagata.Workers.W11.scaleNonzeroVector line 103
Source documentation
Multiplication by a nonzero scalar on actual nonzero vectors.
```
def scaleNonzeroVector (a : ℂˣ) (v : {x : ι → ℂ // x ≠ 0}) :
    {x : ι → ℂ // x ≠ 0} :=
…
```
theorem OAI.Nagata.Workers.W11.continuous_scaleNonzeroVector line 107
theorem OAI.Nagata.Workers.W11.isOpenMap_projectivization_mk' line 113
Source documentation
Saturation of an open set by scalar equivalence is open; hence the genuine projectivization quotient map is an open map.
```
theorem isOpenMap_projectivization_mk' :
    IsOpenMap (Projectivization.mk' ℂ : {x : ι → ℂ // x ≠ 0} →
      Projectivization ℂ (ι → ℂ)) := by
…
```
theorem OAI.Nagata.Workers.W11.isOpenQuotientMap_projectivization_mk' line 137
instance OAI.Nagata.Workers.W11.complexProjectivizationT2Space line 147
Source documentation
The actual projectivization with its canonical complex quotient topology is Hausdorff. In particular this applies to the genuine projective plane with index type Fin 3.
```
instance complexProjectivizationT2Space (ι : Type*) :
    T2Space (Projectivization ℂ (ι → ℂ)) :=
…
```