Boundary cycles of one-vertex chord diagrams

A one-vertex chord diagram is a disc with m untwisted bands attached along its boundary. Its n attaching points are numbered 0, …, n - 1 counterclockwise around the boundary circle, so that turning to the next point is finRotate n, and the bands form a matching of these points, an involution σ of Fin n joining the two ends a, σ a of each band; fixed points of σ are unused marked points of the circle, which subdivide it without changing anything. The boundary of the resulting ribbon surface is traversed by finRotate n * σ: cross the band at the current point, then turn to the next point. Its cycles are the boundary cycles of the diagram.

This file proves the boundary-count criterion for planarity of such a diagram. The diagram has m = n - orbitCount σ bands, and

• it has at most m + 1 boundary cycles: adding one band raises the count by at most one (Equiv.Perm.orbitCount_finRotate_mul_add_orbitCount_le);
• two interleaved bands have a single boundary cycle (TauCeti.orbitCount_finRotate_mul_swap_mul_swap), so a diagram containing an interleaved pair has at most m - 1 boundary cycles (TauCeti.orbitCount_finRotate_mul_add_orbitCount_add_two_le);
• it has exactly m + 1 boundary cycles if and only if no two bands interleave (Function.Involutive.orbitCount_finRotate_mul_add_orbitCount_eq_iff). For the converse, a noncrossing matching has an innermost band, whose two ends are joined by a boundary arc containing no other band (Equiv.Perm.IsNoncrossingMatching.exists_forall_apply_eq_self); deleting it removes exactly one boundary cycle, and the remaining bands are again noncrossing.

Equivalently, the closed surface obtained by capping the boundary cycles has Euler characteristic 1 - m + #boundary cycles, and the diagram is a sphere, that is, planar, exactly when its bands do not interleave. One-vertex ribbon graphs arise by contracting a spanning tree of a connected ribbon graph, such as the underlying graph of a link diagram, and this criterion is the noncrossing consequence of planarity in that one-vertex case. For perfect matchings of Fin (2 * m), where every boundary point is the end of a band, the criterion reads orbitCount (finRotate (2 * m) * σ) = m + 1 (TauCeti.IsPerfectMatching.orbitCount_finRotate_mul_eq_iff).

Main definitions

• Equiv.Perm.IsNoncrossingMatching σ: no two chords {a, σ a} and {b, σ b} of σ interleave.

Main results

• Function.Involutive.isNoncrossingMatching_iff: an involution is a noncrossing matching exactly when its orbit partition is a noncrossing partition.
• Equiv.Perm.IsNoncrossingMatching.apply_mem_Ioo: the chords of a noncrossing involution are nested.
• Equiv.Perm.IsNoncrossingMatching.apply_mem_uIoo_iff, Equiv.Perm.isNoncrossingMatching_of_forall_apply_mem_uIoo: an involution is a noncrossing matching exactly when no chord separates a point from its partner.
• Equiv.Perm.IsNoncrossingMatching.of_semiconj: restricting a noncrossing matching along an order embedding gives a noncrossing matching.
• Equiv.Perm.IsNoncrossingMatching.card_filter_lt_apply_modEq: for a noncrossing perfect matching and a union s of its chords, the two ends of a chord outside s are preceded by the same number of points of s, modulo 2.
• Equiv.Perm.orbitCount_finRotate_mul_add_orbitCount_le: the boundary-count bound.
• TauCeti.orbitCount_finRotate_mul_swap_mul_swap: two interleaved bands have one boundary cycle.
• TauCeti.orbitCount_finRotate_mul_add_orbitCount_add_two_le: an interleaved pair of bands loses two boundary cycles from the bound.
• Equiv.Perm.IsNoncrossingMatching.orbitCount_finRotate_mul_add_orbitCount, Function.Involutive.orbitCount_finRotate_mul_add_orbitCount_eq_iff: the bound is attained exactly by the noncrossing matchings.
• Function.Involutive.isNoncrossingMatching_permCongr_finRotate_iff, Function.Involutive.isNoncrossingMatching_permCongr_revPerm_iff: the noncrossing condition is invariant under rotating and reflecting the boundary circle.
• TauCeti.IsPerfectMatching.orbitCount_finRotate_mul_le, TauCeti.IsPerfectMatching.orbitCount_finRotate_mul_eq_iff: the same for perfect matchings.

References

• S. K. Lando, A. K. Zvonkin, Graphs on Surfaces and Their Applications, Encyclopaedia of Mathematical Sciences 141, Springer 2004, §1.3 (rotation systems and their faces) and §3.4 (chord diagrams).
• P. Biane, Some properties of crossings and partitions, Discrete Math. 175 (1997), 41–53 (noncrossing permutations as geodesics to the full cycle).

def Equiv.Perm.IsNoncrossingMatching {α : Type u_1} [LinearOrder α] (σ : Perm α) : Prop

A permutation σ of a linearly ordered type, read as the matching joining each a to σ a, is a noncrossing matching when no two of its chords interleave: there are no a < b < σ a < σ b. For an involution the chords are the pairs {a, σ a} with σ a ≠ a, and the condition says that they are pairwise noninterleaving, so that they can be drawn disjointly inside a disc whose boundary meets them in the order of α. Equivalently, the partition of α into the orbits of the involution is noncrossing in the sense of Finpartition.IsNoncrossing (Function.Involutive.isNoncrossingMatching_iff); the condition is stated directly on the permutation, the form in which chord diagrams arise.

theorem Equiv.Perm.isNoncrossingMatching_iff {α : Type u_1} [LinearOrder α] {σ : Perm α} : σ.IsNoncrossingMatching ↔ ∀ ⦃a b : α⦄, a < b → b < σ a → ¬σ a < σ b

The defining condition of Equiv.Perm.IsNoncrossingMatching.

@[instance_reducible]

instance Equiv.Perm.instDecidableIsNoncrossingMatchingOfFintype {α : Type u_1} [LinearOrder α] [Fintype α] (σ : Perm α) : Decidable σ.IsNoncrossingMatching

theorem Equiv.Perm.not_isNoncrossingMatching_iff {α : Type u_1} [LinearOrder α] {σ : Perm α} : ¬σ.IsNoncrossingMatching ↔ ∃ (a : α) (b : α), a < b ∧ b < σ a ∧ σ a < σ b

A matching fails to be noncrossing exactly when two of its chords interleave.

@[simp]

theorem Equiv.Perm.isNoncrossingMatching_one {α : Type u_1} [LinearOrder α] : IsNoncrossingMatching 1

The empty matching is noncrossing.

theorem Equiv.Perm.IsNoncrossingMatching.of_forall_apply_eq_or {α : Type u_1} [LinearOrder α] {σ τ : Perm α} (hσ : σ.IsNoncrossingMatching) (h : ∀ (x : α), τ x = x ∨ τ x = σ x) : τ.IsNoncrossingMatching

A matching whose chords are chords of a noncrossing matching is noncrossing: if τ agrees with σ away from its fixed points, then τ is noncrossing when σ is.

theorem Equiv.Perm.IsNoncrossingMatching.apply_mem_Ioo {α : Type u_1} [LinearOrder α] {σ : Perm α} (hσ : σ.IsNoncrossingMatching) (hinv : Function.Involutive ⇑σ) {a b : α} (hab : a < b) (hb : b < σ a) : σ b ∈ Set.Ioo a (σ a)

Chords are nested. If the point b lies strictly inside the chord {a, σ a} of a noncrossing involution, with a < σ a, then so does its partner σ b: a chord starting inside another chord ends inside it.

theorem Equiv.Perm.IsNoncrossingMatching.apply_mem_uIoo_iff {α : Type u_1} [LinearOrder α] {σ : Perm α} (hσ : σ.IsNoncrossingMatching) (hinv : Function.Involutive ⇑σ) (a b : α) : σ b ∈ Set.uIoo a (σ a) ↔ b ∈ Set.uIoo a (σ a)

A chord separates no chord. For a noncrossing involution σ, a point lies strictly between the two ends of the chord {a, σ a} exactly when its partner does.

theorem Equiv.Perm.isNoncrossingMatching_of_forall_apply_mem_uIoo {α : Type u_1} [LinearOrder α] {σ : Perm α} (h : ∀ (a b : α), b ∈ Set.uIoo a (σ a) → σ b ∈ Set.uIoo a (σ a)) : σ.IsNoncrossingMatching

A permutation is a noncrossing matching when the partner of every point strictly between the two ends of a chord {a, σ a} lies strictly between them too.

theorem Equiv.Perm.IsNoncrossingMatching.of_semiconj {α : Type u_1} [LinearOrder α] {σ : Perm α} {β : Type u_2} [LinearOrder β] {τ : Perm β} {e : β → α} (hσ : σ.IsNoncrossingMatching) (he : StrictMono e) (h : Function.Semiconj e ⇑τ ⇑σ) : τ.IsNoncrossingMatching

Restriction along an order embedding. If a strictly monotone map e intertwines τ with a noncrossing matching σ, then τ is a noncrossing matching: its chords are chords of σ, relabelled in an order-preserving way.

theorem Equiv.Perm.IsNoncrossingMatching.card_filter_lt_apply_modEq {α : Type u_1} [LinearOrder α] {σ : Perm α} (hσ : σ.IsNoncrossingMatching) (hm : TauCeti.IsPerfectMatching σ) {s : Finset α} (hs : ∀ x ∈ s, σ x ∈ s) {a : α} (ha : a ∉ s) : {x ∈ s | x < σ a}.card ≡ {x ∈ s | x < a}.card [MOD 2]

Parity across a chord. Let σ be a noncrossing perfect matching and s a finite set closed under σ, that is, a union of chords. A point a outside s and its partner σ a are preceded by the same number of points of s, modulo 2: the points of s lying between them are matched among themselves.

theorem Equiv.Perm.IsNoncrossingMatching.permCongr_revPerm {n : ℕ} {σ : Perm (Fin n)} (hσ : σ.IsNoncrossingMatching) (hinv : Function.Involutive ⇑σ) : ((permCongr Fin.revPerm) σ).IsNoncrossingMatching

Reflecting a noncrossing involution of Fin n in the order reversal Fin.rev, so that the chord {a, σ a} becomes {rev a, rev (σ a)}, gives a noncrossing involution.

theorem Function.Involutive.isNoncrossingMatching_permCongr_revPerm_iff {n : ℕ} {σ : Equiv.Perm (Fin n)} (hinv : Involutive ⇑σ) : ((Equiv.permCongr Fin.revPerm) σ).IsNoncrossingMatching ↔ σ.IsNoncrossingMatching

Noninterleaving is invariant under reflection. An involution of Fin n is noncrossing exactly when its reflection in the order reversal Fin.rev is.

theorem Function.Involutive.isNoncrossingMatching_iff {α : Type u_1} [Fintype α] [LinearOrder α] {σ : Equiv.Perm α} [DecidableRel ⇑(Equiv.Perm.SameCycle.setoid σ)] (hinv : Involutive ⇑σ) : σ.IsNoncrossingMatching ↔ (Finpartition.ofSetoid (Equiv.Perm.SameCycle.setoid σ)).IsNoncrossing

An involution of a finite linear order is a noncrossing matching exactly when the partition into its orbits, the pairs {a, σ a} and the fixed points, is a noncrossing partition. Any decidability instance for the orbit relation may be used, for instance a classical one.

Boundary cycles

theorem TauCeti.sameCycle_finRotate_mul_of_forall_apply_eq_self {n : ℕ} {σ : Equiv.Perm (Fin n)} {a c : Fin n} (hac : a ≤ c) (h : ∀ (x : Fin n), a ≤ x → x < c → σ x = x) : (finRotate n * σ).SameCycle a c

If the matching σ fixes a and every point strictly between a and c, then the boundary traversal finRotate n * σ runs along the boundary circle from a to c.

theorem TauCeti.orbitCount_finRotate_mul_swap_mul_swap {n : ℕ} {a b c d : Fin n} (hab : a < b) (hbc : b < c) (hcd : c < d) : orbitCount (finRotate n * Equiv.swap a c * Equiv.swap b d) = 1

Two interleaved bands have one boundary cycle. For boundary points a < b < c < d, the chord diagram with the two bands {a, c} and {b, d} has a single boundary cycle.

theorem TauCeti.orbitCount_finRotate_mul_add_orbitCount_add_two_le {n : ℕ} {σ : Equiv.Perm (Fin n)} {a b : Fin n} (hab : a < b) (hb : b < σ a) (hσ : σ a < σ b) : orbitCount (finRotate n * σ) + orbitCount σ + 2 ≤ n + 1

An interleaved pair of bands loses two boundary cycles. If two chords of σ interleave, a < b < σ a < σ b, then the chord diagram of σ, with m = n - orbitCount σ bands, has at most m - 1 boundary cycles: the two interleaved bands have one boundary cycle, and each of the other m - 2 bands raises the count by at most one.

theorem Equiv.Perm.orbitCount_finRotate_mul_add_orbitCount_le {n : ℕ} (σ : Perm (Fin n)) : TauCeti.orbitCount (finRotate n * σ) + TauCeti.orbitCount σ ≤ n + 1

The boundary-count bound. A chord diagram on n boundary points with matching σ has m = n - orbitCount σ bands and at most m + 1 boundary cycles: adding one band raises the number of boundary cycles by at most one.

theorem Equiv.Perm.IsNoncrossingMatching.exists_forall_apply_eq_self {n : ℕ} {σ : Perm (Fin n)} (hσ : σ.IsNoncrossingMatching) (hinv : Function.Involutive ⇑σ) (h1 : σ ≠ 1) : ∃ a < σ a, ∀ (x : Fin n), a < x → x < σ a → σ x = x

A noncrossing involution other than the identity has an innermost chord: a chord {a, σ a} with a < σ a whose arc of the boundary circle from a to σ a contains no end of another chord.

theorem Equiv.Perm.IsNoncrossingMatching.orbitCount_finRotate_mul_add_orbitCount {n : ℕ} [NeZero n] {σ : Perm (Fin n)} (hσ : σ.IsNoncrossingMatching) (hinv : Function.Involutive ⇑σ) : TauCeti.orbitCount (finRotate n * σ) + TauCeti.orbitCount σ = n + 1

A noncrossing matching attains the boundary-count bound. A chord diagram whose m bands do not interleave has exactly m + 1 boundary cycles.

theorem Function.Involutive.orbitCount_finRotate_mul_add_orbitCount_eq_iff {n : ℕ} [NeZero n] {σ : Equiv.Perm (Fin n)} (hinv : Involutive ⇑σ) : TauCeti.orbitCount (finRotate n * σ) + TauCeti.orbitCount σ = n + 1 ↔ σ.IsNoncrossingMatching

The boundary-count criterion for noninterleaving. A chord diagram on a nonempty boundary circle, with matching an involution σ and m = n - orbitCount σ bands, has exactly m + 1 boundary cycles if and only if no two of its bands interleave.

theorem Function.Involutive.isNoncrossingMatching_permCongr_finRotate_iff {n : ℕ} {σ : Equiv.Perm (Fin n)} (hinv : Involutive ⇑σ) : ((Equiv.permCongr (finRotate n)) σ).IsNoncrossingMatching ↔ σ.IsNoncrossingMatching

Noninterleaving is a cyclic condition. An involution of Fin n is noncrossing exactly when its rotation by one step around the boundary circle is, the chord {a, σ a} becoming {finRotate n a, finRotate n (σ a)}. So the noncrossing condition depends only on the cyclic order of the boundary points, not on where the circle is cut open.

theorem TauCeti.IsPerfectMatching.orbitCount_finRotate_mul_le {m : ℕ} {σ : Equiv.Perm (Fin (2 * m))} (hσ : IsPerfectMatching σ) : orbitCount (finRotate (2 * m) * σ) ≤ m + 1

A chord diagram whose 2 * m boundary points are the ends of m bands has at most m + 1 boundary cycles.

theorem TauCeti.IsPerfectMatching.orbitCount_finRotate_mul_eq_iff {m : ℕ} {σ : Equiv.Perm (Fin (2 * m))} [NeZero m] (hσ : IsPerfectMatching σ) : orbitCount (finRotate (2 * m) * σ) = m + 1 ↔ σ.IsNoncrossingMatching

The boundary-count criterion for a perfect matching. A chord diagram whose 2 * m boundary points are the ends of m ≠ 0 bands has m + 1 boundary cycles exactly when no two bands interleave.