Inversion on the Riemann sphere (CC5)

Unit: projective-line (docs/design/projective-line.md §3.1). ℙ¹ := OnePoint ℂ.

This file defines inversion : OnePoint ℂ → OnePoint ℂ, the map z ↦ z⁻¹ extended by ∞ ↦ 0 and 0 ↦ ∞, proves it is a continuous involution, and packages it as a self-inverse homeomorphism inversionHomeomorph. The continuity proof is the 𝓝 ∞ filter work referenced by the design's task brief ("verify OnePoint.nhds_infty_eq").

Main declarations: inversion, inversion_involutive, inversion_eq_infty_iff, tendsto_coe_cocompact, tendsto_coe_inv_nhdsNE_zero, continuous_inversion, inversionHomeomorph.

noncomputable def RS.P1.inversion : OnePoint ℂ → OnePoint ℂ

Inversion z ↦ z⁻¹ on the Riemann sphere, with ∞ ↦ 0 and 0 ↦ ∞.

Equations

• RS.P1.inversion p = p.elim ↑0 fun (z : ℂ) => if z = 0 then OnePoint.infty else ↑z⁻¹

@[simp]

theorem RS.P1.inversion_infty : inversion OnePoint.infty = ↑0

@[simp]

theorem RS.P1.inversion_coe_zero : inversion ↑0 = OnePoint.infty

theorem RS.P1.inversion_coe {z : ℂ} (hz : z ≠ 0) : inversion ↑z = ↑z⁻¹

theorem RS.P1.inversion_involutive : Function.Involutive inversion

@[simp]

theorem RS.P1.inversion_inversion (p : OnePoint ℂ) : inversion (inversion p) = p

theorem RS.P1.inversion_eq_infty_iff {p : OnePoint ℂ} : inversion p = OnePoint.infty ↔ p = ↑0

theorem RS.P1.tendsto_coe_cocompact : Filter.Tendsto OnePoint.some (Filter.cocompact ℂ) (nhds OnePoint.infty)

(↑) sends cocompact ℂ to 𝓝 ∞ (mathlib's tendsto_coe_infty re-based off coclosedCompact for downstream convenience).

theorem RS.P1.tendsto_coe_inv_nhdsNE_zero : Filter.Tendsto (fun (z : ℂ) => ↑z⁻¹) (nhdsWithin 0 {0}ᶜ) (nhds OnePoint.infty)

The 𝓝 ∞ filter work, packaged: z ↦ ↑(z⁻¹) blows up at 0.

theorem RS.P1.continuous_inversion : Continuous inversion

noncomputable def RS.P1.inversionHomeomorph : OnePoint ℂ ≃ₜ OnePoint ℂ

Inversion as a self-inverse homeomorphism of the Riemann sphere.

Equations

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

@[simp]

theorem RS.P1.inversionHomeomorph_apply : ⇑inversionHomeomorph = inversion

@[simp]

theorem RS.P1.inversionHomeomorph_symm : inversionHomeomorph.symm = inversionHomeomorph