Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Internal Projective Category?

Alex Kreitzberg (Aug 12 2025 at 19:06):

Is there a nice discussion of how to axiomatize projective geometry in terms of category theory? Here's an approach I've been playing with:

Given formal dots, lines, and planes Given the walking point, walking line, and plane, labeled by $D, L, E$ respectively, it's easy to write

$(l \rightarrow E) \times (l \rightarrow E)\rightarrow (D \rightarrow E)$

For finding an intersection of two lines, and

$(D \rightarrow E) \times (D \rightarrow E) \rightarrow (L \rightarrow E)$

For finding the line between two points.

The way I've written this has problems (For example, what should these mean when the inputed points are the same?)

I think it might be fun to work out the edge cases, but I wanted to ask, is there a nice example/paper of this already being done?

fosco (Aug 12 2025 at 19:08):

https://www.sciencedirect.com/science/article/pii/0022404995001115 not exactly your idea, but worth reading

Alex Kreitzberg (Aug 12 2025 at 19:16):

Thank you! This is an aside, but I just found your book Coend calculus, and I'm excited to work through it!

fosco (Aug 12 2025 at 19:31):

:heart: thank you!

(Also an aside: Sooner or later I have to gather a pdf with all the errata...!)

Kevin Carlson (Aug 12 2025 at 19:40):

I don't understand your typing judgment for "intersection". The type $(L\to E)\times (L\to E)\to (D\to E)$ is the type of functions, given two functions from lines to planes, returning a function from dots to planes. That is not the type of the intersection operator in any reasonable way I can see; I might write it as $L\times L \to D\sqcup \{ !\},$, with the extra value for pairs of lines with no intersection.

Alex Kreitzberg (Aug 12 2025 at 20:07):

I'm thinking of $D$ as terminal or "like a point", and $L$ like the real line without necessarily having an origin, and E as a plane. (And I agree there's a bug, the outputs should have an error term, I left the bug in hoping to keep the question clear)

Here's what I thought one implementation might look like:

$(L \rightarrow E) \times (L \rightarrow E) \rightarrow (D \rightarrow E)$

$(y = m_1x + b_1, y = m_2x + b_2) \mapsto ( \cdot \rightarrow (\frac{b_2 - b_1}{m_1 - m_2}, m_1 \frac{(b_2 - b_1)}{m_1 - m_2} + b_1))$

(This still includes a possible division by zero error)

Kevin Carlson (Aug 12 2025 at 20:07):

How is $y=m_1x+b_1$ supposed to be a term of $L\to E$?

Kevin Carlson (Aug 12 2025 at 20:08):

Ohh, I see, you're saying $L$ is the walking line, not the set of all lines. That's a pretty unusual formulation, but I see where you're going now.

Alex Kreitzberg (Aug 12 2025 at 20:11):

I wrote it as a shorthand for $x \rightarrow (x, m_1x + b_1)$

I'm glad it makes sense! Now I know how to use "walking X" more effectivly.

I'm always nervous to learn that what I'm saying is unusual because I'm worried that means they're hard to use somehow.

Alex Kreitzberg (Aug 12 2025 at 20:26):

I guess the reason I'm using a walking line $L \rightarrow E$, instead of the set of lines $L$, is because I'm trying to encode the line as a sort of map at the level of the category.

Simon Burton (Aug 12 2025 at 23:08):

You could have a look at groupoidification ...

Simon Burton (Aug 12 2025 at 23:16):

Although maybe something closer to what you are asking about: take a category enriched over "distances" (similar to Lawvere's metric spaces) and the objects are the geometric figures of interest, for example flags. The distances here are not just real numbers, but are elements of a Coxeter group, and the composition of morphisms or "distances" is a bit tricky... this is a categorical approach to Buildings...

Alex Kreitzberg (Aug 13 2025 at 06:19):

The groupoidification article was very nice, and I see the connection to projective geometry. I need to think about it a bit and maybe reread it a bit more.

Morgan Rogers (he/him) (Aug 18 2025 at 15:10):

A possible answer can be found in Anders Kock's paper which is better known for the result that the generic model of the theory of local rings is a field.