Representing $\Bbb RP^2$ in Lean: building a type representing a particular set

Question

I need to work with the set of all lines in the Cartesian plane. For my context, the natural way to think of this is that a line can be described by an equation $Ax + By + C = 0$, where $A$ and $B$ cannot both be zero. So a natural representation is as triples $(A,B,C)$ where $A$ and $B$ are not both zero. But the lines characterized by $(A,B,C)$ and by $(7A, 7B, 7C)$ are the same, so I need a quotient. To be explicit, I want to look at the set $Y$ defined by \begin{align} X &= \Bbb R^2 - \{(0,0)\}\\ Y &= X \times \Bbb R \end{align} and the equivalence relation on $Y$ where $((A,B), C) \sim ((P, Q), R)$ if and only if there's a real number $k$ such that $P = kA, Q = kB, R = kC$. Equally good would be to say that $$ Y = \Bbb R^3 - \{(0,0,C) \mid C \in \Bbb R \}, $$ but that seemed as if it might be more difficult to express in Lean.

Those who like geometry will recognize that my set $Y$ is just $\Bbb RP^2$ minus one point, i.e., it's topologically a Mobius band (with "open" edges).

Once I have a description of $Y$, preferably as a type, I can write down the equivalence relation and prove it's an equivalence and even construct the quotient.

Can someone point me in the right direction to defining $Y$ (or even $X$) as a type? (As you may have guessed, I'm a beginner at Lean.)

Answer 1

Let me answer your immediate question first with the following code snippet (which relies on mathlib):

import data.real.basic
import data.matrix.notation

def X := { v : fin 2 → ℝ // v ≠ 0 }

-- The first def for `Y`.
def Y := X × ℝ

-- The second def for `Y`.
def Y' := { v : fin 3 → ℝ // v 0 ≠ 0 ∨ v 1 ≠ 0 }

-- Alternative for `Y'`, using matrix notation:
def Y'' := { v : fin 3 → ℝ // ∀ c : ℝ, v ≠ ![0,0,c] }

Since projective spaces are interesting objects as well, I think it would be worthwhile to first define $\mathbb{RP}^2$, or more generally, $\mathbb{P}^n(k)$, where $k$ is any field, or even better, $\mathbb{P}_k(V)$, the projectivization of the $k$-vector space $V$. Once projective spaces are defined as a type, the next steps would be to build up the API to make them usable! Finally, remove a point from $\mathbb{P}_{\mathbb{R}}(\mathbb{R}^3)$ to obtain your desired object.

For the initial definition of $\mathbb{P}_k(V)$, I see essentially two ways to do this:

1. Consider the type of all one-dimensional subspaces of $V$.
2. Take a quotient of $V \smallsetminus \{0\}$ by the equivalence relation given by multiplication by elements of $k^\times$.

The first approach could be defined as

import linear_algebra.finite_dimensional

variables (k V : Type*) [field k] [add_comm_group V] [module k V]

-- Note that an infinite dimensional space has `finrank = 0`, by convention.
def projectivization := { M : submodule k V // finite_dimensional.finrank k M = 1 }

while the second can be defined as follows (modulo the missing proof):

import linear_algebra.finite_dimensional

variables (k V : Type*) [field k] [add_comm_group V] [module k V]

-- Since `y` is nonzero by assumption, `c • (x : V) = y` will force `c ≠ 0` as well.
def projectivization.setoid : setoid { v : V // v ≠ 0 } := 
{ r := λ x y, ∃ c : k, c • (x : V) = y,
  iseqv := sorry }

def projectivization := quotient (projectivization.setoid k V)

Note that both of these code snippets rely on mathlib, and, of course, one could easily change the implementations (e.g. replacing the finrank condition by an equivalent Prop.

I hope these are useful to get started, and additional help is always available on the Lean zulip.