Directional words in nomenclature?

Stream: maths

[Jake Levinson]

How should we name lemmas involving relative positions of boxes in a Young diagram? This came up in PR #15822 (discussion with @Eric Wieser @Yaël Dillies @Kyle Miller @Violeta Hernández ).

It's standard to represent Young diagrams as pictures of up- and left-justified boxes, so at least in the literature it's common to find any and all of the below to describe positions:

• directional language (up/down/left/right, above/below, row/column)
• cardinal direction language (northwest, south)
• inequalities (i₁ ≤ i₂ and j₁ ≤ j₂)
  Note that these are "matrix coordinates", so i is the row index and j is the column index.

Mathlib naming conventions might be more in line with saying le, and maybe also using the same adjective for i₁ ≤ i₂ and j₁ ≤ j₂ rather than two or four adjectives.

Thoughts? I'll add my own thoughts below, and eventually we can do a poll.

[Jake Levinson]

My thoughts:
In the stuff I've written on Young tableaux (here), it was very helpful to use directional language because the vertical and horizontal directions have different combinatorial rules (e.g. in a semistandard Young tableau, entries increase weakly along rows, but increase strictly along columns). The directional language made it easier for me to read and write proofs in Lean, just as in real life, where it is ubiquitous in combinatorial arguments about Young tableaux.

My inclination would be to allow one type of directional language. My preference would be the terms listed in the first bullet point above.

An example situation is the following: to place a natural number n in a semistandard Young tableau in position (i, j):

• There must be cells strictly left and strictly above (i, j)
• n must be strictly larger than the entries above (i, j)
• n must be strictly smaller than the entries below (i, j)
• n must be weakly larger than the entries to the left of (i, j)
• n must be weakly smaller than the entries to the right of (i, j).

[Jake Levinson]

These statements are called cell_left, cell_up, up, down, left and right here.

[Violeta Hernández]

I see your point now. I'm fine with directional language as long as it's properly documented.

[Kyle Miller]

My suggestion is that if there's a cell that's the "direct object" of the lemma and a cell that's the "indirect object" (for instance a hypothesis), then we use names like the following for their relationship:

• up, down, left, right
• up_left, down_right, etc. (with up/down first then left/right second, mirroring (i, j) indexing order)
• strict_up, strict_up_right, etc. (for a < relationship)

So the defining lemma of a Young diagram would be mem_of_mem_down_right or even up_left_mem (short for up_left_mem_of_mem).

[Kyle Miller]

The n/s/e/w convention is shorter, but I'm afraid names like lt_strict_e would be more obscure (even to Young diagram enthusiasts) than lt_strict_right

[Jake Levinson]

Kyle Miller said:

My suggestion is that if there's a cell that's the "direct object" of the lemma and a cell that's the "indirect object" (for instance a hypothesis), then we use names like the following for their relationship:

• up, down, left, right
• up_left, down_right, etc. (with up/down first then left/right second, mirroring (i, j) indexing order)
• strict_up, strict_up_right, etc. (for a < relationship)

So the defining lemma of a Young diagram would be mem_of_mem_down_right or even up_left_mem (short for up_left_mem_of_mem).

Yes, I like this. How should we decide between the three names you listed for the defining lemma of a Young diagram? I like up_left_mem since it's short. For semistandard tableaux, the defining lemmas are:

(row_weak : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ →
    entry i j1 ≤ entry i j2)
(col_strict : ∀ {i1 i2 j: ℕ}, i1 < i2 → (i2, j) ∈ μ →
    entry i1 j < entry i2 j)

Are these names OK, or should they become le_of_left and lt_of_up? Or perhaps le_of_left_of_mem and lt_of_up_of_mem? Here also the "real-world" nomenclature is definitely "row-weak" and "column-strict", but I think le_of_left and lt_of_up sound OK.

[Jake Levinson]

Also, the row_weak one illustrates a subtlety involving the assumption j1 < j2. This can actually be relaxed to j1 ≤ j2, and indeed my API declares row_weak' with that assumption. But for proving that a tableau is semistandard, the j1 = j2 case is trivial, so it's nicer to not have it in the definition at all.

I'm a little torn as to whether left should mean weakly or strictly left.

[Kyle Miller]

For the semistandard tableaux, le_of_strict_left and lt_of_strict_up seems like it would match better. Then the primed version you mention could be le_of_left

[Kyle Miller]

Another option is le_of_strict_right_mem and lt_of_strict_down_mem. It's the (i, j2) ∈ μ and (i2, j) ∈ μ hypotheses that are being named.

[Jake Levinson]

Okay, I'm fine with le_of_strict_left and lt_of_strict_up (and the API will also have le_of_left and le_of_up).

A random thought: the direct/indirect nomenclature thing is sort of a mirror of forward vs backward reasoning. To show that entry i j < k, you can either work from (i, j) down and right towards various other cells until you reach a cell that is < k. Or, you can work up-and-right from that last cell, backwards to (i, j). So in most situations it feels pretty symmetric to me to choose between up_left vs down_right in naming. How about if we always use up and left by default, unless the situation clearly calls for down or right?

[Jake Levinson]

(Or vice versa)

[Jake Levinson]

This is similar to always using < instead of >.

[Kyle Miller]

I'd like it if we could figure out how to make this naming scheme work without an up/left default.

Here's how I was thinking about generating these names in particular for ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry i j1 ≤ entry i j2.

• The conclusion is an le, and we take the left-hand-side of it (entry i j1) to be what it's about (the direct object) and the right-hand side to be the indirect object. Then the hypotheses are saying that the direct object is strictly to the left of the indirect object, so it's le_of_strict_left.

• The conclusion is an le. We look in the hypotheses and see that we have (i, j2) is a member of the cell set, and the other hypothesis is that it's to the right of another cell (using the Young diagram axiom implicitly). So le_of_strict_right_mem.

[Jake Levinson]

Hmm right okay. Let me think about which one I like better.

[Jake Levinson]

Suppose we are _replacing_ entry (i, j) of tableau T by val. In this case we already know (i, j) ∈ μ. This situation is basically as follows:

structure ssyt.legal_replacement {μ : young_diagram} (T : ssyt μ) :=
  (i j val : ℕ)
  (cell : (i, j) ∈ μ)
  (left : ∀ {j'}, j' < j → T i j' ≤ val)
  (up : ∀ {i'}, i' < i → T i' j < val)
  (right : ∀ {j'}, j < j' → (i, j') ∈ μ → val ≤ T i j')
  (down : ∀ {i'}, i < i' → (i', j) ∈ μ → val < T i' j)

The naming conventions are a little funny here. I would say (i, j) and val are the "direct object" of the situation, and my inclination was to name these by saying where the other cell is relative to (i, j). Basically "looking outward from (i, j)". But both naming conventions become a little awkward here, I think?

• First naming convention: le_of_strict_left, lt_of_strict_up, le_of_strict_left again, lt_of_strict_up again
• Second naming convention: le_of...?, lt_of...?, le_of_strict_right_mem, lt_of_strict_down_mem.

[Kyle Miller]

Another set of options for these: apply_strict_left_le, apply_strict_up_lt, le_apply_strict_right, lt_apply_strict_down

[Jake Levinson]

Hmm, can you explain what apply means here?

[Kyle Miller]

It's just that T is being applied to a cell position, and apply tends to be how that's rendered. Maybe the matrix library will give other naming ideas like this.

[Jake Levinson]

Another option would be to avoid up/down in favor of col and left/right in favor of row. So e.g. we could have two defining lemmas for Young diagrams, mem_of_row and mem_of_col and for SSYTs, le_of_row and lt_of_col. I'm not sure I like this, just throwing it out there.

[Jake Levinson]

I think my favourites from our conversation are following the "direct object" mode:

lemma young_diagram.up_left_mem
lemma ssyt.le_of_strict_left
lemma ssyt.le_of_left
lemma ssyt.lt_of_strict_up
lemma ssyt.le_of_up

and maybe just treating ssyt.legal_replacement as a rather exceptional case, since it's clear that all four statements are relative to the same central cell.

[Jake Levinson]

Some other definitions:

-- a corner box inside the Young diagram
structure young_diagram.inner_corner (μ : young_diagram) :=
  (i j : ℕ)
  (mem : (i, j) ∈ μ)
  (not_mem_of_strict_right : ∀ {j'}, j < j' → (i, j') ∉ μ)
  (not_mem_of_strict_down : ∀ {i'}, i < i' → (i', j) ∉ μ)

-- a corner box just outside the Young diagram
structure young_diagram.outer_corner (μ : young_diagram) :=
  (i j : ℕ)
  (not_mem : (i, j) ∉ μ)
  (mem_of_strict_left : ∀ {j'}, j' < j → (i, j') ∈ μ)
  (mem_of_strict_up : ∀ {i'}, i' < i → (i', j) ∈ μ)