Associahedron

Stream: maths

[Yaël Dillies]

I was talking with somene about the dreaded infinity categories and how we couldn't even define the association rules. So we started talking about associahedrons. Does anybody know a way to characterize the faces (of all dimensions!) of the n-th associahedron? We thought hard about it and I came up with the idea that each face was corresponding to an invariant part of the binary trees/parenthezations, and then came across this image on Wikipedia.
For now, I figured out it would be quite a good exercise to even define the Tamari lattice.

[Scott Morrison]

I think the simplest characterisation of the faces of the n-th associahedron is as rooted "planar" trees with n leaves (not necessarily binary). The dimension of the face is the N-#vertices for some straightforward N(n). Containment of faces is given by the (transitive closure) of contraction of internal edges.

[Scott Morrison]

e.g. (ignore the text labels)
A4-faces.png

[Scott Morrison]

(The labels are showing you the terms appearing in $d m_4$ in an A_infty algebra.)

[Yaël Dillies]

Ohohoh! Very interesting! So you're saying the faces are identifiable with rooted trees? What do you mean by planar here?

[Adam Topaz]

I remember some talk a while back about formalizing operads. Did anything happen with that?

[Scott Morrison]

Just look at the picture. There's a linear order on the children of each vertex.

[Scott Morrison]

And I guess you need to say every non-leaf vertex has at least 2 children.

[Kyle Miller]

(deleted)

[Scott Morrison]

Does

inductive face : Type
| leaf : face
| fork : face → face → face
| cons : face → face → face

namespace face

def children : face → list face
| leaf := []
| (fork a b) := [a, b]
| (cons a b) := a :: children b

end face

Do it?

[Scott Morrison]

fork is for a 2-child vertex, then you use cons to add more children?

[Yaël Dillies]

Okay, I see.

[Yaël Dillies]

And contraction is replacing fork by cons, right?

[Scott Morrison]

No, it's more complicated, you need to do something with conss as well.

[Scott Morrison]

It might be easier to define boundary rather than coboundary.

[Scott Morrison]

i.e. all the ways to uncontract an edge

[Scott Morrison]

but I guess we want both anyway

[Yaël Dillies]

Okay okay

[Kyle Miller]

Is there a moduli space of metric planar rooted trees, where each edge has an associated positive length? It seems like you can set it up so that edge contraction is a limit of shrinking an edge's length. Can this (or rather some subspace) map cleanly onto the associahedron as a geometric object? I'd expect the subspace where the edges incident to the leaves are all unit length would work, but it seems like it gives a dual cell structure. (A tree with n internal vertices is contained in a cell of dimension n.)

[Scott Morrison]

The following code is possibly correct. At least it seems to get the number and sizes of faces correct:

import data.pnat.basic

namespace list

def splits {α : Type*} : list α → list (list α × list α)
| [] := [([], [])]
| (a :: L) := ([], a :: L) :: (splits L).map (λ p, (a :: p.1, p.2))

/-- Give all ways of decomposing a list into a prefix, a singleton, and a suffix. -/
def prefix_singleton_suffix {α : Type*} : list α → list (list α × α × list α)
| [] := []
| [a] := [([], a, [])]
| (a :: L) := ([], a, L) :: (prefix_singleton_suffix L).map (λ p, (a :: p.1, p.2))

end list

inductive face : Type
| leaf : face
| fork : face → face → face
| cons : face → face → face

namespace face

def of : list face → face
| [] := leaf
| (a :: [])  := a
| (a :: b :: []) := fork a b
| (a :: b :: L) := cons a (of (b :: L))

def children : face → list face
| leaf := []
| (fork a b) := [a, b]
| (cons a b) := a :: children b

lemma children_of (L : list face) (h : L.length ≠ 1) : (of L).children = L :=
sorry

def top : ℕ+ → face
| ⟨0, _⟩ := sorry
| ⟨1, _⟩ := leaf
| ⟨2, _⟩ := fork leaf leaf
| ⟨n+3, _⟩ := cons leaf (top ⟨n+2, sorry⟩)

def leaves : face → ℕ+
| leaf := 1
| (fork a b) := leaves a + leaves b
| (cons a b) := leaves a + leaves b

def depth : face → ℕ
| leaf := 0
| (fork a b) := max (depth a) (depth b) + 1
| (cons a b) := max (depth a + 1) (depth b)

/-- For a face with n children, choose between 2 and n-1 contiguous children,
and combine those as a single child. -/
-- TODO define this on the constructors?
def uncontract (f : face) : list face :=
do (P, QR) ← f.children.splits,
   (Q, R) ← QR.splits,
   guard (2 ≤ Q.length ∧ Q.length < f.children.length),
   return $ of (P ++ [of Q] ++ R)

def map (f : face) (g : face → list face) : list face :=
do (P, a, R) ← f.children.prefix_singleton_suffix,
   q ← g a,
   return $ of (P ++ [q] ++ R)

def boundary (f : face) : list face :=
uncontract f ++ f.map uncontract

-- The n=5 associahedron has 9 faces:
#eval ((top 5).boundary).length

-- Of those faces, 3 are squares and 6 are pentagons:
#eval ((top 5).boundary).map (λ f : face, f.boundary.length)

-- The n=6 associahedron has 14 faces:
#eval ((top 6).boundary).length

-- Those faces themselves have either 7 or 9 faces:
-- https://www.shapeways.com/product/YAHGXP2QS/associahedron-k-6
#eval ((top 6).boundary).map (λ f : face, f.boundary.length)

end face

It is a bit hacky.

[Kyle Miller]

Dual to the tree characterization for faces is a characterization in terms of arcs in a disk between labeled points:

structure arc (n : ℕ) :=
(a b : fin (n + 1))
(le : (a:ℕ) + 2 ≤ b)

/-- whether the interiors of the arcs must intersect --/
def arc.interlaces {n : ℕ} (p q : arc n) : Prop :=
(p.a < q.a ∧ p.b < q.b) ∨ (q.a < p.a ∧ q.b < p.b)

structure face (n : ℕ) :=
(arcs : finset (arc n))
(disj : arcs.val.pairwise (λ (p q : arc n), ¬ p.interlaces q))

This illustrates the correspondence between a tree and this face structure for a four-leafed tree:

image.png

Edge contraction corresponds to deleting an arc from the arcs set.

(Edit: That (0,5) edge seems unnecessary -- it probably should be excluded in the definition.)

[Scott Morrison]

In what form should the associahedron first enter mathlib.

1. just as a combinatorial object (a simplicial complex?)
2. the definition of an A_infty algebra?

[Yaël Dillies]

Oh wow! I tried but failed to have working code.

[Scott Morrison]

I was wondering if it makes sense to provide the definition of an abstract polytope, and then the associahedra as examples.

[Yaël Dillies]

I don't know what a A_infty algebra is, so I was envisioning defining it as an abstract polytopial complex. Certainly not as a simplicial complex in the way I'm defining them in #9762 because that assumes a geometrical embedding.

[Yaël Dillies]

What's your definition of an abstract polytope?

[Scott Morrison]

https://en.wikipedia.org/wiki/Abstract_polytope seems good. :-) There's some basic order theory about chains and flags that I suspect we don't quite have.

[Scott Morrison]

We would need flag in an arbitrary partial_order, defined as a maximal chain.

[Scott Morrison]

And rank x as the length of the longest chain ending at x.

[Yaël Dillies]

What about docs#zorn.is_max_chain ?

[Yaël Dillies]

Btw I'm all for splitting the chain stuff from order.zorn

[Scott Morrison]

Yes, that should be factored out a bit.

[Scott Morrison]

I guess we also need incident as the relation x \le y \or y \le x, and connected as the transitive closure of incident.

[Yaël Dillies]

That doesn't work. Everything is connected through bot.

[Scott Morrison]

Oops!

[Scott Morrison]

hmm, I guess you restrict incident to the "proper" (i.e. neither top nor bot) elements and take transitive closure there

[Yaël Dillies]

Yeah, that's what wikipedia does. A bit hacky, isn't it?

[Scott Morrison]

None of this is particularly important, but I do love associahedra. :-)

[Yaël Dillies]

I too :heart_eyes:

[Scott Morrison]

I have to head off now, but I'll think about it some more at some point!

[Yaël Dillies]

Okay! I can try working on the definition of an abstract polytope.

[Dima Pasechnik]

combinatorics ppl like me would says that associahedrons are just secondary polytopes of convex n-gons. So, everything is convex, unlike for abstract polytopes, which need not be realizible as convex polytopes.

[Scott Morrison]

While "concrete"/"geometric" polytopes are "better", and in the end we want them, I suspect it's going to be easier to start with something that involves no geometry. The secondary polytope construction immediately requires us to think about volumes, doesn't it?

[Reid Barton]

Scott Morrison said:

In what form should the associahedron first enter mathlib.

1. just as a combinatorial object (a simplicial complex?)
2. the definition of an A_infty algebra?

I would understand an A_infty algebra to be an algebra over an operad (that is a cofibrant replacement of the Assoc operad), so 1 and 2 are kind of the same thing

[Scott Morrison]

If only Lean felt that way. :-)

[Reid Barton]

Right, a better thing to say would be I think it makes sense for it to start out as some combinatorial structure/polytope, then the plan is to realize it as a space/chain complex, and at some point along the way it will gain an operad structure

[Dima Pasechnik]

Yes, one would need convex polytopes, their triangulations, and volumes (of simplices, to begin with - but well, it's just a determinant ;-)). This would be a very useful project, IMHO, I don't know how hard.

[Yaël Dillies]

See branch#sperner-again for a start :wink:

[Dima Pasechnik]

Does https://github.com/leanprover-community/mathlib/tree/sperner-again let one talk about convex hulls of finitely many points? How about facets (and, maybe dual polytopes)?

[Yaël Dillies]

You can already talk about convex hulls of finitely many points. Do you mean bundled as polytopes? If so, yes, although the API is currently quite dry: https://github.com/leanprover-community/mathlib/blob/sperner-again/src/combinatorics/simplicial_complex/polyhedron.lean#L375

[Dima Pasechnik]

I mean an alternative definition of polytope, as a bounded set defined by finitely many linear inequalities.

[Dima Pasechnik]

among such systems of inequalies there is (essentially) one canonical, with as few inequalities as possible.

[Dima Pasechnik]

a.k.a. "dual polytope"

[Yaël Dillies]

That's what I'm trying to do at this line: https://github.com/leanprover-community/mathlib/blob/sperner-again/src/combinatorics/simplicial_complex/polyhedron.lean#L466

[Yaël Dillies]

Well, not for the "bounded" part.

[Dima Pasechnik]

unbounded convex polyhedra are a bit too general - anyhow, to have a decomposition theorem for these (any such polyhedron is Minkowski sum of a polytope, a cone, and an affine subspace) you need bounded ones, and cones.

[Yaël Dillies]

We already have cones in mathlib!

[Yaël Dillies]

docs#convex_cone

[Yaël Dillies]

If you have some idea of what to do and in what order, I'm very happy to hear it. I'm pretty interested in convexity.

[Dima Pasechnik]

how hard is to prove in Lean that a finitely generated (pointed) cone has finitely generated dual?

[Yaël Dillies]

@Bhavik Mehta, what do you think? :up:

[Dima Pasechnik]

to this end, I can only think of proving this by showing correctness of an algorithmic procedure which computes the facets.

[Yaël Dillies]

Bhavik has proved Gordan's lemma, if that's related.

[Chris Hughes]

Is any of this related to the simplex algorithm? I proved correctness of that back in 2019 https://github.com/ChrisHughes24/LP/blob/master/src/simplex.lean It never went into mathlib.

[Kevin Buzzard]

Gordan's lemma seems related to me.

[Dima Pasechnik]

well, there is "reverse search", one of procedures to enumerate facets, whch is sort of running simplex method backwards:
https://www.sciencedirect.com/science/article/pii/0166218X9500026N

[Dima Pasechnik]

the simplest "paper" proof I know is in K. Fukuda's lecture notes https://inf.ethz.ch/personal/fukudak/lect/pclect/notes2015/PolyComp2015.pdf - which uses an easy algorithm to eliminate variables in systems of linear inequalities (Fourier-Motzkin elimination).

[Yaël Dillies]

Ahah! linarith is an implementation of Fourier-Motzkin, but we have no formalization per say.

[Dima Pasechnik]

Dima Pasechnik said:

the simplest "paper" proof I know is in K. Fukuda's lecture notes (Theorem 3.10) https://inf.ethz.ch/personal/fukudak/lect/pclect/notes2015/PolyComp2015.pdf - which uses an easy algorithm to eliminate variables in systems of linear inequalities (Fourier-Motzkin elimination).

tl; dr: if $x=R\lambda$, $\lambda\geq 0$ is representing all the vectors in the cone generated by the columns of the matrix $R$, then eliminating $\lambda$'s will leave us with a finite system of linear inequalities on $x$.

[Reid Barton]

I have a formalization of what is basically Fourier-Motzkin elimination in https://github.com/rwbarton/lean-omin/blob/master/src/o_minimal/examples/isolating.lean though it's probably not quite close enough to be useful here without extra work--in any case, it's not very difficult