ZFC pair rename

Stream: maths

[Violeta Hernández]

I want to rename the Kuratowski pair docs#Set.pair to something like Set.kpair, since otherwise there's ambiguity in theorem names between {x, y} and pair x y. Is this ok?

[Violeta Hernández]

@Mario Carneiro

[Mario Carneiro]

IMO the name "pair" is better suited to the ordered pair than the unordered pair

[Mario Carneiro]

and this is a more important distinction than kuratowski pair (unless we want to have other kinds of ordered pair)

[Violeta Hernández]

Well, pair is used for {x, y} elsewhere in mathlib, such as docs#set.pair_comm or docs#set.image_pair

[Violeta Hernández]

To be clear this is entirely a theorem naming issue, I don't plan on adding other kinds of pairs atm

[Violeta Hernández]

I would argue that the Kuratowski ordered pair is somewhat less "fundamental" than the more general unordered pair, hence its renaming.

[Violeta Hernández]

The best alternative I have is to just add tildes on the Kuratowski theorems

[Mario Carneiro]

we don't even have a definition for the unordered pair, so I don't see how that is the case

[Mario Carneiro]

it's just insert insert empty

[Yaël Dillies]

{x, y} is sometimes also called doubleton

[Patrick Johnson]

I'd vote "pair" for ordered and "upair" for unordered.

[Violeta Hernández]

Let me give a concrete example of a name clash.

theorem sUnion_pair (x y : Set.{u}) : ⋃₀ ({x, y} : Set.{u}) = x ∪ y := sorry

theorem sUnion_pair' (x y : Set.{u}) : ⋃₀ (pair x y) = {x, y} := sorry

[Violeta Hernández]

The former matches docs#set.sUnion_pair. The latter is a lemma I need to prove to define the projection functions.

[Violeta Hernández]

If renaming the Kuratowski pair is not an option, then I suggest we use tildes on the Kuratowski lemmas in case of name clashing.

[Violeta Hernández]

Renaming pair throughout Mathlib seems overkill

[Violeta Hernández]

(That said, I could get behind standardizing pair / doubleton)

[Mario Carneiro]

I don't see any reason to rename pair throughout mathlib

[Patrick Johnson]

⋃₀ (pair x y) = {x, y} does not hold for all models of ordered pair and the fact that we use Kuratowski's model seems arbitrary. If you need that specific model to prove something, why not define a new function (for example def kpair x y := pair x y)

[Violeta Hernández]

Patrick Johnson said:

If you need that specific model to prove something, why not define a new function (for example def kpair x y := pair x y)

Why not just rename pair directly?

[Violeta Hernández]

It's not that I want that specific model to prove something, but rather that I am proving something about that specific model, namely that the aforementioned projection functions work.

[Patrick Johnson]

I'm not against renaming pair to kpair, but I think we should have model agnostic definition of ordered pair such as this:

def pair : Set.{u} → Set.{u} → Set.{u} :=
classical.epsilon $ λ f, ∀ a b c d, f a b = f c d ↔ a = c ∧ b = d

[Patrick Johnson]

That's just my opinion. Others may disagree.

[Violeta Hernández]

I don't really see what we would get out of this.

[Violeta Hernández]

Besides, to get things done, we'd still need to prove the existence of such a set function

[Patrick Johnson]

As I said, that's just my opinion. Personally, I dislike the idea of being able to prove statements that are true for some models of ordered pair, but not for the others, as the name pair should not imply any particular model. Just like I would be unhappy if I could prove 5 ∈ 7, since that would reveal the underlying model of natural numbers.

If you want to know what others think, try opening a poll.

[Kevin Buzzard]

I guess there are plenty of examples of people abusing definitional equality in mathlib, and those are also examples of statements which are true for some implementation of a concept but not for others. I'm not expressing an opinion about pair though.

[Mario Carneiro]

This is ZFC we're talking about. It is basically a theorem that every construction exposes implementation details (there are no nontrivial automorphisms of V)

[Antoine Chambert-Loir]

Everytime a French mathematician reads something about "ordered pair", a kitten dies in pain in the heart of their soul… (The French terminology is couple (ordered)/paire (unordered), but we'll have to cope with that.) On the other hand, whatever a pair is, preferably unordered, the other variant should have a clearly distinct name.