One-point views of optional values

Posits and quires both have a partial exact semantics toRat? : Model → Option Rat whose none case is the unique NaR word. Their intentional one-point projections send some x to the point x and none to the added point of OnePoint. This module defines that map once, as Option.toOnePoint, and proves the characterisations that the posit and quire projective views instantiate.

def Option.toOnePoint {K : Type u_1} : Option K → OnePoint K

Send some x to the point x of the one-point compactification and none to the added point.

@[simp]

theorem Option.toOnePoint_some {K : Type u_1} (x : K) : (some x).toOnePoint = ↑x

some x maps to the finite point x of the one-point compactification.

@[simp]

theorem Option.toOnePoint_none {K : Type u_1} : none.toOnePoint = OnePoint.infty

none maps to the point at infinity.

theorem Option.toOnePoint_eq_coe_iff {K : Type u_1} (option : Option K) (x : K) : option.toOnePoint = ↑x ↔ option = some x

The one-point view is a finite point exactly when the option holds that value.

theorem Option.toOnePoint_eq_infty_iff {K : Type u_1} (option : Option K) : option.toOnePoint = OnePoint.infty ↔ option = none

The one-point view is the added point exactly when the option is none.

theorem Option.toOnePoint_map_eq_coe_iff {K : Type u_1} {L : Type u_2} {f : K → L} (hf : Function.Injective f) (option : Option K) (x : K) : (Option.map f option).toOnePoint = ↑(f x) ↔ option = some x

Mapping through an injective function before the one-point view preserves finite points.

theorem Option.toOnePoint_map_eq_infty_iff {K : Type u_1} {L : Type u_2} (f : K → L) (option : Option K) : (Option.map f option).toOnePoint = OnePoint.infty ↔ option = none

Mapping before the one-point view does not change which options reach the added point.

theorem OnePoint.equivProjectivization_eq_iff (K : Type u_1) [DivisionRing K] [DecidableEq K] (left right : OnePoint K) : (equivProjectivization K) left = (equivProjectivization K) right ↔ left = right

The projective-line equivalence reflects equality of one-point values.