Inversion of a set in a normed division ring

In any division ring, w ↦ q + w⁻¹ inverts the inversion z ↦ (z - q)⁻¹ about q.

For a closed bounded set K and a centre q in a normed division ring, the inversion z ↦ (z - q)⁻¹ maps K \ {q} onto the closed set {w | w ≠ 0 ∧ q + w⁻¹ ∈ K}: the image stays away from 0, and away from 0 it is the preimage of K under the continuous map w ↦ q + w⁻¹. Inverting a set about a point outside its closure gives a bounded set; conversely, inverting a set about a point of its closure that it does not contain gives an unbounded set, and inverting an unbounded set adds 0, the image of infinity, to the closure. Completing the inversion of a set by 0 commutes with closures, and turns an open set with bounded complement into an open set.

Main results

• TauCeti.bijOn_add_inv_image_inv_sub: w ↦ q + w⁻¹ inverts the inversion about q.
• TauCeti.image_inv_sub_eq_preimage_add_inv: the inversion about q maps a set onto its preimage under w ↦ q + w⁻¹.
• TauCeti.isClosed_setOf_ne_zero_and_add_inv_mem: the inversion of a closed bounded set about any centre, with the centre removed, is closed.
• TauCeti.isBounded_image_inv_sub: the inversion of a set about a point outside its closure is bounded.
• TauCeti.not_isBounded_image_sub_inv_of_mem_closure: the inversion of a set about a point of its closure outside the set is unbounded.
• TauCeti.closure_image_inv_sub: the closure of the inversion of an unbounded set is the inverted closure together with 0.
• TauCeti.isOpen_insert_zero_image_inv_sub, TauCeti.closure_insert_zero_image_inv_sub and TauCeti.frontier_insert_zero_image_inv_sub: an open set with bounded complement, inverted about any point and completed by 0, is open; the completed inversion of any set has the completed inverted closure as closure; and for a centre outside the closure of such an open set, the inverted frontier as frontier.
• TauCeti.mapsTo_inv_ball_diff_singleton_compl_closedBall: the inversion maps the punctured ball of radius R⁻¹ about 0 outside the closed ball of radius R.

theorem TauCeti.bijOn_add_inv_image_inv_sub {𝕜 : Type u_1} [DivisionRing 𝕜] {q : 𝕜} (S : Set 𝕜) : Set.BijOn (fun (w : 𝕜) => q + w⁻¹) ((fun (z : 𝕜) => (z - q)⁻¹) '' S) S

The map w ↦ q + w⁻¹ inverts the inversion z ↦ (z - q)⁻¹: it is a bijection from the inverted image of any set S back onto S.

theorem TauCeti.image_inv_sub_eq_preimage_add_inv {𝕜 : Type u_1} [DivisionRing 𝕜] {q : 𝕜} (S : Set 𝕜) : (fun (z : 𝕜) => (z - q)⁻¹) '' S = (fun (w : 𝕜) => q + w⁻¹) ⁻¹' S

The inversion z ↦ (z - q)⁻¹ is a bijection of 𝕜 (sending q to 0⁻¹ = 0) with inverse w ↦ q + w⁻¹, so it maps any set onto the preimage of that set under w ↦ q + w⁻¹.

theorem TauCeti.isClosed_setOf_ne_zero_and_add_inv_mem {𝕜 : Type u_1} [NormedDivisionRing 𝕜] {K : Set 𝕜} (hK : IsClosed K) (hKb : Bornology.IsBounded K) (q : 𝕜) : IsClosed {w : 𝕜 | w ≠ 0 ∧ q + w⁻¹ ∈ K}

The inversion of a closed bounded set is closed. For closed bounded K and any q, the image {w | w ≠ 0 ∧ q + w⁻¹ ∈ K} of K \ {q} under z ↦ (z - q)⁻¹ is closed: it stays away from 0, and away from 0 it is the preimage of K under w ↦ q + w⁻¹.

theorem TauCeti.not_isBounded_image_sub_inv_of_mem_closure {𝕜 : Type u_1} [NormedDivisionRing 𝕜] {s : Set 𝕜} {q : 𝕜} (hq : q ∈ closure s) (hq' : q ∉ s) : ¬Bornology.IsBounded ((fun (z : 𝕜) => (z - q)⁻¹) '' s)

Inverting about a missing point of the closure gives an unbounded set. If q lies in the closure of s but not in s, then the image of s under z ↦ (z - q)⁻¹ is unbounded.

theorem TauCeti.mapsTo_inv_ball_diff_singleton_compl_closedBall {𝕜 : Type u_1} [NormedDivisionRing 𝕜] (R : ℝ) : Set.MapsTo (fun (x : 𝕜) => x⁻¹) (Metric.ball 0 R⁻¹ \ {0}) (Metric.closedBall 0 R)ᶜ

The inversion maps the punctured ball of radius R⁻¹ about 0 into the exterior of the closed ball of radius R.

theorem TauCeti.isBounded_image_inv_sub {𝕜 : Type u_1} [NormedDivisionRing 𝕜] {q : 𝕜} {U : Set 𝕜} (hq : q ∉ closure U) : Bornology.IsBounded ((fun (z : 𝕜) => (z - q)⁻¹) '' U)

Inverting a set U about a point q outside its closure gives a bounded set.

theorem TauCeti.isOpen_insert_zero_image_inv_sub {𝕜 : Type u_1} [NormedDivisionRing 𝕜] {q : 𝕜} {U : Set 𝕜} (hUo : IsOpen U) (hUc : Bornology.IsBounded Uᶜ) : IsOpen (insert 0 ((fun (z : 𝕜) => (z - q)⁻¹) '' U))

Inverting an open set U with bounded complement about any point q, and adding 0, the image of infinity, gives an open set: U contains a neighbourhood of infinity, which the inversion carries onto a punctured neighbourhood of 0.

theorem TauCeti.closure_insert_zero_image_inv_sub {𝕜 : Type u_1} [NormedDivisionRing 𝕜] {q : 𝕜} {U : Set 𝕜} : closure (insert 0 ((fun (z : 𝕜) => (z - q)⁻¹) '' U)) = insert 0 ((fun (z : 𝕜) => (z - q)⁻¹) '' closure U)

Inverting any set U about any point q and adding 0, the image of infinity, commutes with taking closures.

theorem TauCeti.closure_image_inv_sub {𝕜 : Type u_1} [NormedDivisionRing 𝕜] {q : 𝕜} {U : Set 𝕜} (hUb : ¬Bornology.IsBounded U) : closure ((fun (z : 𝕜) => (z - q)⁻¹) '' U) = insert 0 ((fun (z : 𝕜) => (z - q)⁻¹) '' closure U)

Inverting an unbounded set U about any point q, the closure of the image is the image of the closure together with 0, the image of infinity.

theorem TauCeti.frontier_insert_zero_image_inv_sub {𝕜 : Type u_1} [NormedDivisionRing 𝕜] {q : 𝕜} {U : Set 𝕜} (hUo : IsOpen U) (hq : q ∉ closure U) (hUc : Bornology.IsBounded Uᶜ) : frontier (insert 0 ((fun (z : 𝕜) => (z - q)⁻¹) '' U)) = (fun (z : 𝕜) => (z - q)⁻¹) '' frontier U

Inverting an open set U with bounded complement about a point q outside its closure, and adding 0, the image of infinity, the frontier of the resulting open set is the inverted frontier of U.