Points at infinity on affine spaces?

Stream: Is there code for X?

[E M]

Is there anything in Mathlib that allows to add points at infinity to an affine space?

The usual construction seems to be to perform an homogeneization/linearization (representing the affine space as P0 + v, then embedding it in R (+) AffineSpace as (1, p) with vectors being (0, p)) and then perform a projectivization (so that the result only consists of the original affine space plus the quotiented vectors representing points at infinity).

Mathlib has the projectivization, but I can't find either the homogenization or the alternative approach of representing the construction as an inductive (either points or vectors quotiented by smul) other than just using a direct sum with no dedicated API.

[Scott Carnahan]

If you view points at infinity as lines up to parallel equivalence, there is some helpful API near the bottom of LinearAlgebra.AffineSpace.AffineSubspace, e.g., docs#AffineSubspace.affineSpan_pair_parallel_iff_vectorSpan_eq

[Bjørn Kjos-Hanssen]

Maybe tangentially related, this constructs a set-theoretic equivalence betweenOnePoint K (in other words K with infinity added) and the projectivization ℙ K (Fin 2 → K)for an arbitrary field K. I also have a proof that this equivalence is a homeomorphism in the case K=ℝ.

[Yao Liu]

I also wondered how much synthetic projective geometry exists, and it appears not much. I mean, axioms of projective plane or n-space with incidence relations on the points, lines, etc., not as projectivization over some field. I thought Fomin's recent work, Incidences and Tiling, would be a nice formalization project.

[Johan Commelin]

cc @Thomas Browning, who did work on this

[Thomas Browning]

Abstract incidence relations (configurations of points and lines) are defined in this file: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/Configuration.html

This PR adds finite projective planes over fields: #16684

[Thomas Browning]

It would be nice to be able to talk about Desarguesian planes (for instance).

[Johan Commelin]

Nice! I just kicked #16684 on the queue