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: fields and projective planes

Hugo Jenkins (Sep 24 2021 at 04:27):

I am fascinated by the rough idea, seemingly underlying a lot of what I've read so far (although maybe I misunderstand) that in categorical logic we can produce a category like the syntactic category $\mathcal{C}_{T}$ of a theory $T$, which serves as a sort of ``neutral/universal description'' of the algebraic/syntactic object $T$. I've been led to believe that via this, an equivalence of categories can sometimes be made to explain the existence of constructions which pass between different forms of essentially equivalent data.

Specifically, in the notes I've been reading, it is remarked that there are mutually inverse constructions which, given a field $k$, yield the projective plane $P^{2}(k)$, and given an abstract projective plane $S$ satisfying some conditions automatic for $P^2$ (the Pappus Hexagon Theorem) yield a field $k(S)$.

(1) Can anyone suggest a source for the precise latter construction (``coordinatization'')?

(2) Is there a way I can really see an equivalence of categories $\mathcal{C}_{T}\cong \mathcal{C}_{T'}$, where $\mathcal{C}_{T}$, $\mathcal{C}_{T'}$ are the syntactic pretopoi of appropriate first-order theories $T$ and $T'$ of fields and Pappian projective planes? This would be really cool. How?

(3) If the answer to (2) is yes, are there any more examples we can compute of this phenomenon?

(By the way the notes I am talking about are https://www.math.ias.edu/~lurie/278x.html and this is Remark 14 in Lecture 1.)

Mike Shulman (Sep 24 2021 at 04:45):

Note that what Lurie strongly implies (though does not explicitly claim in that remark, as far as I can see) is an equivalence between (1) the theory of fields and (2) the theory of Pappian projective planes equipped with four distinguished points in general position.

David Michael Roberts (Sep 24 2021 at 08:57):

Rey Casse's book Projective Geometry does the most general case of arbitrary projective plane, and also the various nice cases like skew fields and fields

John Baez (Sep 24 2021 at 14:01):

Mike Shulman said:

Note that what Lurie strongly implies (though does not explicitly claim in that remark, as far as I can see) is an equivalence between (1) the theory of fields and (2) the theory of Pappian projective planes equipped with four distinguished points in general position.

But you get isomorphic fields regardless of the choice of these four points, right?

(Of course that fact is not everything you might want, but it's enough for category-theory-insensitive people to stop carrying about the choice of those points.)

John Baez (Sep 24 2021 at 14:03):

(There could be some degenerate Pappian planes where there don't exist 4 points in general position, but I think the usual axioms of projective planes deliberately rule out those degenerate cases.)

Mike Shulman (Sep 24 2021 at 16:17):

Yes, I think that's right: you get isomorphic fields, but the isomorphism may not be unique. And yes, I believe the usual axioms of projective geometry ensure that there exist 4 points in general position -- even the Fano plane has such.

Mike Shulman (Sep 24 2021 at 16:19):

Some other references for introducing coordinates in a projective plane are Seidenberg's Lectures in projective geometry, Beutelspacher and Rosenbaum's Projective geometry, and Hartshorne's Foundations of projective geometry. (A few years ago I taught a course on synthetic projective geometry, so I accumulated some books on my shelf.)

Leopold Schlicht (Sep 24 2021 at 18:13):

Hugo Jenkins said:

(2) Is there a way I can really see an equivalence of categories $\mathcal{C}_{T}\cong \mathcal{C}_{T'}$, where $\mathcal{C}_{T}$, $\mathcal{C}_{T'}$ are the syntactic pretopoi of appropriate first-order theories $T$ and $T'$ of fields and Pappian projective planes? This would be really cool. How?

(3) If the answer to (2) is yes, are there any more examples we can compute of this phenomenon?

I believe in most settings of categorical logic the following are equivalent for any two theories $T$ and $T'$:

1. The syntactic category of $T$ is equivalent to the syntactic category of $T'$.
2. For each (in this case coherent category) $\mathcal C$, the category of $T$-models in $\mathcal C$ is equivalent to the category of $T'$-models in $\mathcal C$ and this equivalence is natural in $\mathcal C$ (in the 2-categorical sense).
3. There is a translation $J$ from $T$ to $T'$ (sending basic types of $T$ to types of $T'$ and function symbols of $T$ to terms of $T'$ such that whenever a formula is provable in $T$ its translation is provable in $T'$, roughly speaking) and a translation $K$ from $T'$ to $T$ such that $J\circ K$ and $K\circ J$ are "isomorphic" to the identity. (To make that precise one needs to define 2-cells between translations.)

The implication "(2) implies (1)" should follow from the 2-categorical Yoneda lemma and the observation that the syntactic category $\mathrm{Syn}(T)$ of $T$ classifies the models of $T$ in the sense that for all (in this case coherent categories) $\mathcal C$, the category $\mathrm{Hom}(\mathrm{Syn}(T),\mathcal C)$ is canonically equivalent to the category of $T$-models in $\mathcal C$. The implication "(1) implies (2)" is trivial.

The equivalence between (1) and (3) should follow from the "fact" that the 2-category of coherent categories is biequivalent to the 2-category of coherent theories, one direction being given on objects by the 2-functor sending a coherent theory to its syntactic category. (Recently I asked hundreds of questions about these correspondences in this stream. From what I've picked up I would be surprised if someone ever wrote down a proof of this "fact". But you can find analogues in Lambek and Scott's Introduction to Higher-Order Categorical Logic for other doctrines.)

It seems to me that in Example 14 Lurie only sketched the verification of (2) in the case $\mathcal C=\mathbf{Set}$.

What would be interesting is to find two translations in the sense of (3) relating the theory of fields with the theory of Pappian projective planes equipped with four distinguished points in general position. Maybe this could answer your question (3) about how to "compute" this phenomenon. What confuses me a bit is that it seems like the translation from the theory of fields to the theory of Pappian projective planes equipped with four distinguished points in general position sketched by Lurie requires "power types", but coherent categories don't have power objects in general (so there shouldn't be power types in the doctrine we are working with).

Mike Shulman (Sep 24 2021 at 19:30):

I think that's all right, but Lurie is working with the more expressive doctrine of pretoposes, a.k.a. coherent logic with coproducts and quotients, rather than coherent categories. In this case the same equivalence holds, but the "syntactic categories" in (1) are the pretopos completions of the ordinary coherent syntactic categories, in (2) we speak about arbitrary pretoposes rather than arbitrary coherent categories, and in (3) the "types" that basic types are allowed to be sent to are generated by coproducts and quotients as well as the other coherent logic operations.

Mike Shulman (Sep 24 2021 at 19:31):

I think this resolves your worry about power types. I presume you are thinking of power types being used in defining the points of the projective plane over a field $k$ to be subsets (linear subspaces) of $k^3$. But we can equivalently define the projective plane to be the quotient of $k^3 \setminus \{0\}$ by scalar multiplication.

Mike Shulman (Sep 24 2021 at 19:33):

But there is some subtlety about constructivity here! There's more than one constructive notion of "field", and so presumably there will be more than one constructive notion of "projective plane". Since synthetic projective geometry uses the notion of "distinct point" a lot, I think probably one will want a constructive version to be equipped with an apartness relation, and so it ought to correspond to a notion of field that has an apartness relation too.

Morgan Rogers (he/him) (Sep 24 2021 at 19:38):

It's also worth noting that there are conservativity results that guarantee that the coherent syntactic categories are equivalent when their extensions to richer categories are equivalent (since we can identify these categories with the "coherent objects" in their extensions), so provided that the theory of fields and the theory of projective planes you look at are both coherent, you can recover the equivalence at that level, even if you obtained it using power types etc!

Mike Shulman (Sep 24 2021 at 19:48):

Ah! I knew there was a reference I wanted to point to, but it took me far too long to find it. It's the thesis of Achilleas Kryftis, A constructive approach to affine and projective planes:

In classical geometric algebra, there have been several treatments of affine and projective planes based on fields. In this thesis we approach affine and projective planes from a constructive point of view and we base our geometry on local rings instead of fields. We start by constructing projective and affine planes over local rings and establishing forms of Desargues' Theorem and Pappus' Theorem which hold for these. From this analysis we derive coherent theories of projective and affine planes. The great Greek mathematicians of the classical period used geometry as the basis for their theory of quantities. The modern version of this idea is the reconstruction of algebra from geometry. We show how we can construct a local ring whenever we are given an affine or a projective plane. This enables us to describe the classifying toposes of our theories of affine and projective planes as extensions of the Zariski topos by certain group actions. Through these descriptions of the classifying toposes, the links between the theories of local rings, affine and projective planes become clear. In particular, the geometric morphisms between these classifying toposes are all induced by group homomorphisms even though they demonstrate complicated constructions in geometry. In this thesis, we also prove results in topos theory which are applied to these geometric morphisms to give Morita equivalences between some further theories.

John Baez (Sep 24 2021 at 19:51):

Hmm, a local ring! Mac Lane and Moerdijk talk about how local rings are the nice topos-theoretic substitute for fields, but I admit I never fully got it.

Can you go from local ring (object) to something like a projective plane (object)? That would be cool. The abstract doesn't quite come out and say so, though it says "the links between the theories of local rings, affine and projective planes become clear".

Mike Shulman (Sep 24 2021 at 19:57):

Can you go from local ring (object) to something like a projective plane (object)?

It's been a while since I read the thesis, but I think the answer is yes, although you have to squint a bit to tell the difference between the resulting "projective plane" and the more ordinary projective plane over the residue field of the local ring. I think he does something like define the apartness relation on the projective plane in terms of invertibility of elements in the local ring. So two points are "not apart" just when some element of the ring is in the maximal ideal, whereas they are only equal if that corresponding element of the ring is zero. So the apartness is not "tight", and if you quotient by the equivalence relation of "non-apartness" you should get the ordinary projective space over the residue field.

However, don't quote me on any of that, at least not without reading the thesis first to check whether it's right!

Hugo Jenkins (Sep 26 2021 at 19:57):

Mike Shulman said:

I think this resolves your worry about power types. I presume you are thinking of power types being used in defining the points of the projective plane over a field $k$ to be subsets (linear subspaces) of $k^3$. But we can equivalently define the projective plane to be the quotient of $k^3 \setminus \{0\}$ by scalar multiplication.

I don’t understand really what quotients or power types are, or how we use them here. What I was imagining was: let the theory of projective planes be that with two sorts, points and lines, and one relation between them, point on line, with appropriate axioms. $T_\text{fields}$ can have one sort and two trinary relations for addition and multiplication. We can make the projective plane theory untyped by having unary predicates for points and lines. Then the syntactic categories as I understand them (categories of formulas and definable maps) seem to be two things we could directly compare.

Hugo Jenkins (Sep 26 2021 at 20:23):

@Leopold Schlicht Intuitively it seems like the equivalence in point 2 should come from the construction I am talking about: models of $T$ (=projective planes) $\leftrightarrow$ models of $T'$ (=fields). In particular this construction hopefully respects elementary embeddings in the two theories, and so is functorial. So is what you're saying essentially that once I understand this construction, I then obtain the equivalence of syntactic categories via the 2-Yoneda lemma?

Leopold Schlicht (Sep 27 2021 at 11:05):

@Hugo Jenkins Here are two ways of showing that $\mathrm{Syn}(T)$ is equivalent to $\mathrm{Syn}(T')$:

1. Prove that for each pretopos $\mathcal C$, the category of models of $T$ in $\mathcal C$ and homomorphisms is equivalent to the category of models of $T'$ in $\mathcal C$ and homomorphisms, and this equivalence is natural in $\mathcal C$. Then apply the 2-categorical Yoneda lemma to conclude that $\mathrm{Syn}(T)$ is equivalent to $\mathrm{Syn}(T')$.
2. Prove that there is an equivalence of ultracategories between the ultracategory of models of $T$ in $\mathbf{Set}$ and the ultracategory of models of $T'$ in $\mathbf{Set}$. Then apply Makkai's conceptual completeness theorem to conclude that $\mathrm{Syn}(T)$ is equivalent to $\mathrm{Syn}(T')$.

I think an equivalence of ultracategories is the same as an equivalence of categories, but note that the ultracategory of models of $T$ in $\mathbf{Set}$ considered in (2) has as morphisms something like elementary embeddings, while the category of models of $T$ in $\mathcal C$ considered in (1) has as morphisms usual homomorphisms between structures.

Lurie seems to be talking about (2) rather than (1), so in this case you don't need the 2-categorical Yoneda lemma.

Mike Shulman (Sep 27 2021 at 13:30):

I think an ultracategory is a category equipped with structure, so an equivalence of ultracategories is an equivalence of categories that preserves that structure.

Leopold Schlicht (Sep 27 2021 at 14:01):

Oh, yes. What I was trying to say was that an equivalence of ultracategories is an ultrafunctor that happens to be an equivalence of categories, i.e., the inverse is automatically an ultrafunctor. At least Lurie seems to suggest that in Lecture 29X:

It follows immediatey from the definitions that an ultrafunctor $F\colon M \to M'$ is invertible (in the 2-category of ultracategories) if and only if it is an equivalence (in particular if $F$ is an equivalence of categories, then a homotopy inverse $F^{−1}$ to $F$ can also be regarded as an ultrafunctor).

Leopold Schlicht (Sep 27 2021 at 14:26):

Morgan Rogers (he/him) said:

It's also worth noting that there are conservativity results that guarantee that the coherent syntactic categories are equivalent when their extensions to richer categories are equivalent (since we can identify these categories with the "coherent objects" in their extensions), so provided that the theory of fields and the theory of projective planes you look at are both coherent, you can recover the equivalence at that level, even if you obtained it using power types etc!

I don't think this is correct. Example 2 in Lecture 7 gives two coherent categories which are not equivalent but whose pretopos completions are equivalent.
But maybe it's true for the completion "pretopos $\to$ coherent topos"? In Lecture 1, there's an equality sign between $\{\text{pretopoi}\}$ and $\{\text{coherent topoi}\}$ in the (commutative?) diagram on page 6.

Mike Shulman (Sep 27 2021 at 16:33):

Leopold Schlicht said:

What I was trying to say was that an equivalence of ultracategories is an ultrafunctor that happens to be an equivalence of categories, i.e., the inverse is automatically an ultrafunctor.

Yes, that's true for nearly all kinds of structured categories.

Leopold Schlicht (Sep 27 2021 at 16:36):

I found out it's Lemma 8.4 in Makkai's Stone Duality for First Order Logic, and the proof needs one whole page, with one large diagram. :grinning_face_with_smiling_eyes:

Mike Shulman (Sep 27 2021 at 16:39):

Leopold Schlicht said:

Morgan Rogers (he/him) said:

It's also worth noting that there are conservativity results that guarantee that the coherent syntactic categories are equivalent when their extensions to richer categories are equivalent (since we can identify these categories with the "coherent objects" in their extensions)...

I don't think this is correct. Example 2 in Lecture 7 gives two coherent categories which are not equivalent but whose pretopos completions are equivalent.
But maybe it's true for the completion "pretopos $\to$ coherent topos"? In Lecture 1, there's an equality sign between $\{\text{pretopoi}\}$ and $\{\text{coherent topoi}\}$ in the (commutative?) diagram on page 6.

I agree. Here's Johnstone in the remarks after D1.4.12 of Sketches of an Elephant:

We define Morita equivalence for regular (resp. coherent, geometric) theories to mean equivalence of [their syntactic exact categories (resp. pretoposes, infinitary pretoposes)] rather than of the syntactic categories themselves. Of course, this is a weaker notion than equivalence of the syntactic categories; but it suffices to ensure that the theories have equivalent model categories in any... topos, which is our main concern. (We shall see in 3.1.12 and 3.3.8 below that the converse is true.)

The reference D3.3.8 shows that the syntactic pretopos of a coherent theory is the category of coherent objects in its classifying topos, in line with what Leopold said. In general, a categorical smallness condition like "coherent object" will automatically be closed under operations like quotients, so it can't detect the difference between a coherent category and its pretopos completion.

Morgan Rogers (he/him) (Sep 28 2021 at 07:42):

You're right, my statement should have been "the coherent syntactic categories are equivalent up to exact completion when their extensions to richer categories are equivalent". Thanks for the corrections :+1:

On the other hand, since no one has actually provided an equivalence and since @Hugo Jenkins' original question appears to be about models of projective planes and fields in the topos of sets, it seems to me more likely that there will be an equivalence of exact completions of the syntactic categories rather than of the syntactic categories themselves.

Mike Shulman (Sep 28 2021 at 15:46):

Yes, this is what I was getting at with my comment

I presume you are thinking of power types being used in defining the points of the projective plane over a field $k$ to be subsets (linear subspaces) of $k^3$. But we can equivalently define the projective plane to be the quotient of $k^3 \setminus \{0\}$ by scalar multiplication.

That is, when formulated using quotients rather than subsets, the "usual construction" of an equivalence should apply directly in the internal language of pretoposes.

Leopold Schlicht (Sep 28 2021 at 17:08):

@Morgan Rogers (he/him) Lurie's notion of "syntactic category" is what you call "exact completion of the syntactic category", and what you call "syntactic category" he calls "weak syntactic category". :grinning_face_with_smiling_eyes:

Morgan Rogers (he/him) (Sep 28 2021 at 17:16):

Is there some good reason for that which I'm not aware of? What fragment of logic is a pretopos the syntactic category of? (I'm only used to dealing with fragments of geometric logic, so this may just be my ignorance)

Mike Shulman (Sep 28 2021 at 17:57):

Pretopoi are the syntactic categories of coherent-logic-with-finite-coproducts-and-quotients. That's not a fragment of geometric logic, or even of possibly-infinitary first-order logic, but it's a "logic" in the generalized sense of a type theory.

Morgan Rogers (he/him) (Sep 28 2021 at 18:11):

So that's kind of a no? In the sense that there is no syntax for this to be the syntactic category of?

Mike Shulman (Sep 28 2021 at 18:24):

Type theory is syntax!

Morgan Rogers (he/him) (Sep 28 2021 at 18:30):

Oops. That explains why the constructions of syntactic categories on the nLab page use completely different notation to what I'm used to from eg. the Elephant...

Morgan Rogers (he/him) (Sep 28 2021 at 18:32):

Thanks for the clarification :sweat_smile: