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


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

  • $\begingroup$ 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! $\endgroup$
    – John
    Feb 12, 2022 at 22:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.