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: theory: philosophy

Topic: The generic triangle


view this post on Zulip John Baez (Oct 03 2024 at 15:55):

On Mathstodon, Boarders wrote:

Platonism vs nominalism: an old fashioned debate in philosophy is that of universals - talking of triangle as a property commits oneself to the existence of the abstract concept of triangle or perhaps a “generic triangle”.

In this case, we can, to some extent, resolve the question mathematically in a precise way - there is a mathematical object called the moduli stack of triangles, the generic triangle is the generic point of this moduli stack. We can answer various precise questions about this generic triangle such as what automorphism group it has etc. It also specializes to various more particular triangles with a precise notion of specialize due to algebraic geometers. It seems to me this is a better formal apparatus for thinking about mathematical universals than any kind of vague waffle available, but the idea has not managed to escape the purview of mathematicians.

view this post on Zulip David Corfield (Oct 03 2024 at 16:48):

There's a huge industry in philosophy in working out what's meant by when we say "Let nn be a natural number". A common position has it that nn refers to an "arbitrary natural number" which is a different thing from the individual natural numbers and has only generic properties.

Andrej Bauer at his curtest on the subject here:

What I am saying is that "a free variable is a projection" is a great deal better at explaining various perceived mysteries about free variables than fancy words from philosophy books. But your mileage may vary.

A two-pronged attack with Egbert Rijke writing:

The generalised elements of an object AA are morphism into AA. Under this point of view, the generic element of AA is the identity morphism on AA.

view this post on Zulip John Onstead (Oct 04 2024 at 02:43):

Category theory actually gives us the most powerful ever version of finding "the generic X". This process is known as "externalization" and it involves going from a specific instance of X to viewing it as a functor out of a particular category, known as the "generic X" or "walking X". In a sense, the "walking X" is the platonic ideal of X, the archetypal or prototypical X. Making statements about the walking X then you can specialize to all instances of X across mathematics. There's many examples ranging from the "walking morphism" A -> B which is the archetypal morphism, to the Lawvere theory of groups which is the archetypal group object. This is also related to the notion of classifying object, which is the formal dual of the walking object since every morphism into it represents an instance of X.

view this post on Zulip Julius Hamilton (Nov 16 2024 at 16:47):

That’s interesting. I feel like I’m often attracted to “maximum generality”, but I feel like quite a few people caution one that this is sort of a fool’s errand. I feel like I’ve heard quite a few people mention that there is no “single best generalization” of certain ideas; that the purpose of abstraction is to focus on what specifically is relevant to some task at hand; that mathematics has a kind of relativism where we can model structures in different languages but not claim one is more central than any other.

view this post on Zulip Mike Shulman (Nov 16 2024 at 17:01):

"Generic" is different from "maximum generality".

view this post on Zulip John Baez (Nov 17 2024 at 00:26):

Yes, the "generic X" is a perfectly well-defined thing, unique up to equivalence, after we've chosen X (the "theory") and the context in which to work with X (the "doctrine"). If you seek greater generality, you will tend to keep fiddling around with the doctrine and the theory.

(I'm not very attracted to maximum generality: I mainly want to understand things and also use math to help the world. Often these quests are aided by increasing generality - but also very often it's important to decrease generality and think very hard about a specific example! As Polya said: "if there's a question you can't solve, there's probably an easier question you can solve" - so switch to that and see if it helps. Often to find a good easier question you should decrease the level of generality. It's better to add extra assumptions than sit there stuck.)

view this post on Zulip Joe Moeller (Nov 19 2024 at 22:47):

I think there's a pretty straightforward analogy that's helpful here: abstraction is like elevation. When you realize two concrete facts are examples of one abstract fact, you've put two sticks together and you're standing at their apex. This abstract point could be stregthened by supporting it with further struts on the ground: examples. The higher you are, the more you could see (if you dare to look down). So a naively appealing idea is to just build straight upwards, so you could see everything. That's not likely to produce a very stable structure, and if other structures haven't been built in the surrounding areas, you'll likely stop being able to make out any details on the ground anyway. Obviously sometimes it pays to be daring and build upwards a bit.

view this post on Zulip Kevin Carlson (Nov 19 2024 at 22:49):

Great metaphor!

view this post on Zulip Julius Hamilton (Nov 25 2024 at 16:31):

David Corfield said:

What I am saying is that "a free variable is a projection"…

The generalised elements of an object AA are morphisms into AA. Under this point of view, the generic element of AA is the identity morphism on AA.

Why is a free variable a projection?

view this post on Zulip Julius Hamilton (Nov 25 2024 at 16:33):

John Baez said:

As Polya said: "if there's a question you can't solve, there's probably an easier question you can solve" - so switch to that and see if it helps. Often to find a good easier question you should decrease the level of generality. It's better to add extra assumptions than sit there stuck.)

That is an idea I will definitely explore.

view this post on Zulip Ryan Wisnesky (Nov 25 2024 at 16:55):

if you look at a term in context, say, x:Nat, y:String |- x:Nat, then the categorical semantics is a morphism Nat*String->Nat, that is in fact the first projection of the context (the variable x). Whereas if you had x:Nat, y:String |- 5:Nat, you'd have a constant morphism, not a projection.

view this post on Zulip David Corfield (Nov 26 2024 at 08:01):

Right, so when you say 'Let x be a natural number,...', you are working in a context x:Nat...x: Nat \vdash .... Say you want to establish some property of a number in general, and you arrive at x:Natp:P(x)x: Nat \vdash p: P(x). This corresponds to a morphism in the slice over NatNat, p:NatPp: Nat \to P, respecting the maps down to NatNat. If PP is a proposition, this will only be possible if PP holds for all x:Natx: Nat.