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

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.)

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.

• Thanks. The first part of your answer is what I really needed; generalizing here makes it less useful, because this comes up in mimicking a development of projective geometry that only discusses $RP^2$ and $RP^3$ as examples, and doesn't have linear algebra as a prerequisite so much as a co-requisite. But the generalization is also interesting to me, so thanks for giving it!
– John
Feb 12, 2022 at 22:13