3
$\begingroup$

I’ve had trouble finding a well-established term for the following very obvious and elementary construction on strict partial orders (i.e. transitive, irreflexive relations):

Given two strict partial orders $(X,<_X)$, $(Y,<_Y)$, there is a strict partial order on $X \times Y$ where $(x,y) < (x',y')$ just if one of the following cases holds:

  • $x<x'$ and $y<y'$;
  • $x=x'$ and $y<y'$;
  • $x<x'$ and $y=y'$.

This corresponds clearly to the direct product of the (non-strict) partial orders $\leq_X$, $\leq_Y$ corresponding to $<_X$, $<_Y$. However, it’s not their direct/cartesian product as strict partial orders — or at least, it would be misleading to call it either of those, since those have another more obvious meaning. But presumably many other people must have had cause to make use of this product at some point or another. Does it have a well-established name?

Improve this question
$\endgroup$
1
  • 1
    $\begingroup$ It corresponds to the strong product of graphs, but this is perhaps only tangentially relevant, since the strong product is mostly used in the context of undirected graphs. $\endgroup$
    – Tobias Fritz
    Commented Jun 26, 2018 at 8:44

2 Answers 2

Reset to default
3
$\begingroup$

If one takes the reflexive order relation as fundamental, then this is just the strict product order.

It is good practice to take the reflexive order relation as the primary relation, since in the context of pre-orders, one can define the strict order $<$ from the reflexive order $\leq$, but not necessarily conversely, since there are strict orders $<$ that arise from more than one pre-order.

Thus, one understands an "order" to be the reflexive relation, which comes along with its defined strict relation. With two such orders, then one has the (reflexive) product order relation, and your relation is the strict order arising from that product order.

So I would just call it the strict product order, meaning the strict order notion arising from the (reflexive) product order.

As you note, this is not the product of the strict orders, and I view this simply as one more reason that we don't want the strict orders to be the primary order notion.

Improve this answer
$\endgroup$
5
  • 2
    $\begingroup$ Like you, I usually prefer to take the reflexive orders as fundamental. However, I need this operation in a context where it’s much more natural to consider the non-strict order as fundamental (specifically: constructive well-orderings), hence asking this question. $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Mar 27, 2018 at 22:31
  • 1
    $\begingroup$ With well-orders, then the term "product order" means something else, since one wants $\alpha\cdot\beta$ to mean $\beta$ copies of $\alpha$, using the lexical order, so as to get the product itself as a well order. But of course your order is not generally a well-order, even when both factors are. $\endgroup$
    – Joel David Hamkins
    Commented Mar 27, 2018 at 22:36
  • $\begingroup$ Sorry, when I wrote “well-orderings” I should have written “well-founded (strict) partial orderings”, where “well-founded” is defined in the constructively most useful sense: “satisfying the well-founded induction principle”. While this product doesn’t preserve totalness of the order, as you point out, it does preserve transitivity and well-foundedness (which can be seen since it embeds into the lex product). $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Mar 27, 2018 at 22:42
  • $\begingroup$ I see. In that context, I would still call it the product order, but I would perhaps emphasize that it suffices to descend in only one coordinate. But since you are in a constructive logic context, I would worry that somehow I have made a fundamental mistake in how the strict orders are related to the reflexive orders, since equality can be weird constructively. And so perhaps you shouldn't listen to me. $\endgroup$
    – Joel David Hamkins
    Commented Mar 27, 2018 at 22:48
  • 1
    $\begingroup$ It's not unheard-of in constructive mathematics to refer to a construction that operates on a "strong complement" by the same name as the corresponding classical operation. For instance, one talks about the "quotient" of a group by an anti-subgroup or a ring by an anti-ideal. Sometimes one adds "strong", e.g. a "strongly extensional" function is one that reflects apartness. Using irreflexive relations rather than reflexive ones is somewhat similar, though not the same (your motivating definition "x<=y iff (x<y or x=y)" is not a complement), so you could say "product" or "strong product". $\endgroup$
    – Mike Shulman
    Commented Jul 26, 2018 at 17:00
1
$\begingroup$

I believe that Paul Taylor calls this the "interleaved product" in his book Practical Foundations of Mathematics.

Improve this answer
$\endgroup$
3
  • $\begingroup$ Thankyou! Yes: a quick check in my copy confirms that, named in Proposition 2.6.9. I’ll wait a little in case anyone reports other terms (since Taylor’s terminology is often idiosyncratic), but if not, this sounds like a good option. $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Mar 27, 2018 at 23:40
  • 1
    $\begingroup$ I don't understand in what sense this product is "interleaved", can anyone explain? $\endgroup$
    – Mike Shulman
    Commented Jul 26, 2018 at 17:00
  • $\begingroup$ @MikeShulman: yes, I also find this name bafflingly unmotivated. $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Feb 5, 2019 at 11:36

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .