Perfect matchings of a finite type

A perfect matching of a type α is a permutation of α that is an involution without fixed points; equivalently, it partitions α into the unordered pairs {a, f a}. This file defines perfect matchings, transports them along an equivalence of the underlying types, reconnects two of their arcs, shows that a perfect matching restricted to the complement of one of its arcs is again a perfect matching, and counts the perfect matchings of a finite type: a type of cardinality 2 * m has (2 * m - 1)‼ of them, and a type of odd cardinality has none. Finally it records the parity consequences of being a product of m disjoint transpositions: the sign of a perfect matching, and the evenness of the number of orbits of a product of two perfect matchings.

The counting theorem is the combinatorial content behind the dimension of the Brauer algebra; see TauCeti/Combinatorics/Brauer/Diagram.lean.

Main definitions

• TauCeti.IsPerfectMatching f: the permutation f is an involution with no fixed point.
• TauCeti.PerfectMatching α: the type of perfect matchings of α.
• TauCeti.PerfectMatching.congr: transporting a perfect matching along an equivalence.
• TauCeti.PerfectMatching.reconnect: cutting two arcs and joining their ends the other way.
• TauCeti.PerfectMatching.restrict: the perfect matching induced on the complement of an arc.
• TauCeti.PerfectMatching.extend: the perfect matching obtained by adjoining an arc.
• TauCeti.PerfectMatching.fiberEquiv: the two constructions above are mutually inverse.

Main results

• TauCeti.PerfectMatching.ext_of_eqOn: two perfect matchings agreeing on a set containing a partner of every point are equal.
• TauCeti.even_card_of_nonempty_perfectMatching: a matched type has even cardinality.
• TauCeti.card_perfectMatching: a type of cardinality 2 * m has (2 * m - 1)‼ perfect matchings.
• TauCeti.IsPerfectMatching.sign_eq: a perfect matching of a type of cardinality 2 * m has sign (-1) ^ m.
• TauCeti.IsPerfectMatching.two_mul_orbitCount: a perfect matching has half as many orbits as points.
• TauCeti.IsPerfectMatching.even_orbitCount_mul: the product of two perfect matchings has an even number of orbits.

References

• Schur--Weyl roadmap, Layer 9.

def TauCeti.IsPerfectMatching {α : Type u} (f : Equiv.Perm α) : Prop

A permutation of α is a perfect matching when it is an involution with no fixed point, so that it pairs off the elements of α.

Equations

• TauCeti.IsPerfectMatching f = ((∀ (a : α), f (f a) = a) ∧ ∀ (a : α), f a ≠ a)

theorem TauCeti.isPerfectMatching_iff {α : Type u} {f : Equiv.Perm α} : IsPerfectMatching f ↔ (∀ (a : α), f (f a) = a) ∧ ∀ (a : α), f a ≠ a

A permutation is a perfect matching exactly when it is an involution with no fixed point.

@[simp]

theorem TauCeti.IsPerfectMatching.apply_apply {α : Type u} {f : Equiv.Perm α} (hf : IsPerfectMatching f) (a : α) : f (f a) = a

A perfect matching is an involution.

@[simp]

theorem TauCeti.IsPerfectMatching.apply_ne {α : Type u} {f : Equiv.Perm α} (hf : IsPerfectMatching f) (a : α) : f a ≠ a

A perfect matching moves every point.

@[instance_reducible]

instance TauCeti.instDecidableIsPerfectMatching {α : Type u} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) : Decidable (IsPerfectMatching f)

Equations

• TauCeti.instDecidableIsPerfectMatching f = { decide := decide (∀ (a : α), f (f a) = a) && decide (∀ (a : α), f a ≠ a), reflects_decide := ⋯ }

def TauCeti.PerfectMatching (α : Type u) : Type u

The type of perfect matchings of α, a subtype of Equiv.Perm α so that the finiteness and decidability instances of permutations carry over unchanged.

Equations

• TauCeti.PerfectMatching α = { f : Equiv.Perm α // TauCeti.IsPerfectMatching f }

@[instance_reducible]

instance TauCeti.PerfectMatching.instFintypeOfDecidableEq {α : Type u} [DecidableEq α] [Fintype α] : Fintype (PerfectMatching α)

Equations

• TauCeti.PerfectMatching.instFintypeOfDecidableEq = { elems := TauCeti.PerfectMatching.instFintypeOfDecidableEq._aux_1, complete := ⋯ }

@[instance_reducible]

instance TauCeti.PerfectMatching.instDecidableEqOfFintype {α : Type u} [DecidableEq α] [Fintype α] : DecidableEq (PerfectMatching α)

Equations

• TauCeti.PerfectMatching.instDecidableEqOfFintype = TauCeti.PerfectMatching.instDecidableEqOfFintype._aux_1

def TauCeti.PerfectMatching.mk {α : Type u} (f : Equiv.Perm α) (hinv : ∀ (a : α), f (f a) = a) (hne : ∀ (a : α), f a ≠ a) : PerfectMatching α

Bundle a permutation that is an involution with no fixed point as a perfect matching.

Equations

• TauCeti.PerfectMatching.mk f hinv hne = ⟨f, ⋯⟩

@[simp]

theorem TauCeti.PerfectMatching.val_mk {α : Type u} (f : Equiv.Perm α) (hinv : ∀ (a : α), f (f a) = a) (hne : ∀ (a : α), f a ≠ a) : ↑(mk f hinv hne) = f

@[simp]

theorem TauCeti.PerfectMatching.apply_apply {α : Type u} (D : PerfectMatching α) (x : α) : ↑D (↑D x) = x

A perfect matching is an involution.

@[simp]

theorem TauCeti.PerfectMatching.apply_ne {α : Type u} (D : PerfectMatching α) (x : α) : ↑D x ≠ x

A perfect matching moves every point.

theorem TauCeti.PerfectMatching.apply_eq_of_apply_eq {α : Type u} (D : PerfectMatching α) {x y : α} (h : ↑D x = y) : ↑D y = x

The two ends of an arc determine each other.

theorem TauCeti.PerfectMatching.ext_of_eqOn {α : Type u} {D D' : PerfectMatching α} {s : Set α} (hs : ∀ a ∉ s, ↑D a ∈ s) (h : Set.EqOn (⇑↑D) (⇑↑D') s) : D = D'

Two perfect matchings are equal as soon as they agree on a set s containing the partner, under the first matching, of every point outside s. For instance s may be the set of half-edges pointing away from their crossing in an oriented diagram, since every arc has one end there.

theorem TauCeti.PerfectMatching.apply_ne_and_ne_iff {α : Type u} {a b : α} {D : PerfectMatching α} (hab : ↑D a = b) (x : α) : ↑D x ≠ a ∧ ↑D x ≠ b ↔ x ≠ a ∧ x ≠ b

A perfect matching that joins a to b preserves the complement of {a, b}.

def TauCeti.PerfectMatching.restrict {α : Type u} {a b : α} (D : PerfectMatching α) (hab : ↑D a = b) : PerfectMatching { x : α // x ≠ a ∧ x ≠ b }

The perfect matching induced on the complement of the arc joining a to b.

Equations

• D.restrict hab = ⟨(↑D).subtypePerm ⋯, ⋯⟩

@[simp]

theorem TauCeti.PerfectMatching.restrict_apply_coe {α : Type u} {a b : α} (D : PerfectMatching α) (hab : ↑D a = b) (x : { x : α // x ≠ a ∧ x ≠ b }) : ↑(↑(D.restrict hab) x) = ↑D ↑x

def TauCeti.PerfectMatching.extend {α : Type u} {a b : α} [DecidableEq α] (hab : a ≠ b) (E : PerfectMatching { x : α // x ≠ a ∧ x ≠ b }) : PerfectMatching α

The perfect matching of α obtained from a perfect matching of the complement of {a, b} by adjoining the arc joining a to b.

Equations

• TauCeti.PerfectMatching.extend hab E = ⟨TauCeti.PerfectMatching.extendPerm✝ E, ⋯⟩

theorem TauCeti.PerfectMatching.extend_apply_of_mem {α : Type u} {a b : α} [DecidableEq α] (hab : a ≠ b) (E : PerfectMatching { x : α // x ≠ a ∧ x ≠ b }) {x : α} (hx : x ≠ a ∧ x ≠ b) : ↑(extend hab E) x = ↑(↑E ⟨x, hx⟩)

Away from {a, b}, the extended matching acts through E.

@[simp]

theorem TauCeti.PerfectMatching.extend_apply_left {α : Type u} {a b : α} [DecidableEq α] (hab : a ≠ b) (E : PerfectMatching { x : α // x ≠ a ∧ x ≠ b }) : ↑(extend hab E) a = b

Adjoining the arc {a, b} sends a to b.

@[simp]

theorem TauCeti.PerfectMatching.extend_apply_right {α : Type u} {a b : α} [DecidableEq α] (hab : a ≠ b) (E : PerfectMatching { x : α // x ≠ a ∧ x ≠ b }) : ↑(extend hab E) b = a

Adjoining the arc {a, b} sends b to a.

@[simp]

theorem TauCeti.PerfectMatching.restrict_extend {α : Type u} {a b : α} [DecidableEq α] (hab : a ≠ b) (E : PerfectMatching { x : α // x ≠ a ∧ x ≠ b }) : (extend hab E).restrict ⋯ = E

Adjoining an arc and then restricting it away recovers the smaller matching.

@[simp]

theorem TauCeti.PerfectMatching.extend_restrict {α : Type u} {a b : α} [DecidableEq α] (hab : a ≠ b) (D : PerfectMatching α) (h : ↑D a = b) : extend hab (D.restrict h) = D

Restricting away an arc and then adjoining it back recovers the original matching.

def TauCeti.PerfectMatching.fiberEquiv {α : Type u} {a b : α} [DecidableEq α] (hab : a ≠ b) : { D : PerfectMatching α // ↑D a = b } ≃ PerfectMatching { x : α // x ≠ a ∧ x ≠ b }

Restricting away an arc and adjoining it back are mutually inverse: the perfect matchings of α joining a to b are the perfect matchings of the complement of {a, b}.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.PerfectMatching.fiberEquiv_apply {α : Type u} {a b : α} [DecidableEq α] (hab : a ≠ b) (D : { D : PerfectMatching α // ↑D a = b }) : (fiberEquiv hab) D = (↑D).restrict ⋯

The fiber equivalence restricts away the arc joining a to b.

@[simp]

theorem TauCeti.PerfectMatching.fiberEquiv_symm_apply {α : Type u} {a b : α} [DecidableEq α] (hab : a ≠ b) (E : PerfectMatching { x : α // x ≠ a ∧ x ≠ b }) : ↑((fiberEquiv hab).symm E) = extend hab E

The inverse of the fiber equivalence adjoins the arc joining a to b.

theorem TauCeti.PerfectMatching.isPerfectMatching_permCongr {α : Type u} {β : Type v} (e : α ≃ β) {f : Equiv.Perm α} (hf : IsPerfectMatching f) : IsPerfectMatching (e.permCongr f)

Transporting an involution without fixed points along an equivalence leaves it an involution without fixed points.

theorem TauCeti.PerfectMatching.isPerfectMatching_permCongr_iff {α : Type u} {β : Type v} (e : α ≃ β) {f : Equiv.Perm α} : IsPerfectMatching (e.permCongr f) ↔ IsPerfectMatching f

A permutation is a perfect matching exactly when its transport along an equivalence is.

def TauCeti.PerfectMatching.congr {α : Type u} {β : Type v} (e : α ≃ β) : PerfectMatching α ≃ PerfectMatching β

Transporting a perfect matching along an equivalence of the underlying types: the arc joining a to b becomes the arc joining e a to e b.

Equations

• TauCeti.PerfectMatching.congr e = e.permCongr.subtypeEquiv ⋯

@[simp]

theorem TauCeti.PerfectMatching.congr_val {α : Type u} {β : Type v} (e : α ≃ β) (D : PerfectMatching α) : ↑((congr e) D) = e.permCongr ↑D

The involution underlying a transported matching is the transported involution.

theorem TauCeti.PerfectMatching.congr_val_apply {α : Type u} {β : Type v} (e : α ≃ β) (D : PerfectMatching α) (b : β) : ↑((congr e) D) b = e (↑D (e.symm b))

The transported matching matches b with the image of the partner of e.symm b.

theorem TauCeti.PerfectMatching.congr_val_apply_apply {α : Type u} {β : Type v} (e : α ≃ β) (D : PerfectMatching α) (a : α) : ↑((congr e) D) (e a) = e (↑D a)

The transported matching matches e a with the image of the partner of a.

@[simp]

theorem TauCeti.PerfectMatching.congr_refl {α : Type u} (D : PerfectMatching α) : (congr (Equiv.refl α)) D = D

Transporting along the identity equivalence changes nothing.

@[simp]

theorem TauCeti.PerfectMatching.congr_trans {α : Type u} {β : Type v} {γ : Type w} (e : α ≃ β) (e' : β ≃ γ) (D : PerfectMatching α) : (congr e') ((congr e) D) = (congr (e.trans e')) D

Transports compose: transporting along e and then along e' is transporting along e.trans e', both matchings sending c to e' (e (D.val (e.symm (e'.symm c)))).

@[simp]

theorem TauCeti.PerfectMatching.congr_symm {α : Type u} {β : Type v} (e : α ≃ β) : (congr e).symm = congr e.symm

Transporting back along e is transporting along e.symm, since transports compose.

def TauCeti.PerfectMatching.reconnect {α : Type u} [DecidableEq α] (D : PerfectMatching α) (a b : α) : PerfectMatching α

Reconnecting two arcs. Cut the arc of D at a and the arc at b, and join a to b and D.val a to D.val b; every other arc is kept. It is D transported along the transposition of D.val a with b. The arcs at a and b are distinct when b ≠ a and b ≠ D.val a; when b = D.val a the transposition is trivial and the result is D itself.

Equations

• D.reconnect a b = (TauCeti.PerfectMatching.congr (Equiv.swap (↑D a) b)) D

theorem TauCeti.PerfectMatching.reconnect_val {α : Type u} [DecidableEq α] (D : PerfectMatching α) (a b : α) : ↑(D.reconnect a b) = (Equiv.permCongr (Equiv.swap (↑D a) b)) ↑D

The involution underlying a reconnected matching is the old one conjugated by the transposition of D.val a with b.

@[simp]

theorem TauCeti.PerfectMatching.reconnect_partner {α : Type u} [DecidableEq α] (D : PerfectMatching α) (a : α) : D.reconnect a (↑D a) = D

Reconnecting the two ends of one arc leaves the matching unchanged.

@[simp]

theorem TauCeti.PerfectMatching.reconnect_val_self {α : Type u} {a b : α} {D : PerfectMatching α} [DecidableEq α] (hba : b ≠ a) : ↑(D.reconnect a b) a = b

After reconnecting, a is joined to b.

@[simp]

theorem TauCeti.PerfectMatching.reconnect_val_right {α : Type u} {a b : α} {D : PerfectMatching α} [DecidableEq α] (hba : b ≠ a) : ↑(D.reconnect a b) b = a

After reconnecting, b is joined to a.

@[simp]

theorem TauCeti.PerfectMatching.reconnect_val_val_self {α : Type u} {a b : α} {D : PerfectMatching α} [DecidableEq α] (hba : b ≠ a) : ↑(D.reconnect a b) (↑D a) = ↑D b

After reconnecting, the other end D.val a of the first arc is joined to the other end D.val b of the second.

@[simp]

theorem TauCeti.PerfectMatching.reconnect_val_val_right {α : Type u} {a b : α} {D : PerfectMatching α} [DecidableEq α] (hba : b ≠ a) : ↑(D.reconnect a b) (↑D b) = ↑D a

After reconnecting, the other end D.val b of the second arc is joined to the other end D.val a of the first.

@[simp]

theorem TauCeti.PerfectMatching.reconnect_val_of_ne {α : Type u} {a b : α} {D : PerfectMatching α} [DecidableEq α] {x : α} (hxa : x ≠ a) (hxb : x ≠ b) (hxa' : x ≠ ↑D a) (hxb' : x ≠ ↑D b) : ↑(D.reconnect a b) x = ↑D x

Reconnecting keeps every arc that does not end at a or b.

@[simp]

theorem TauCeti.PerfectMatching.reconnect_self {α : Type u} [DecidableEq α] (D : PerfectMatching α) (a : α) : D.reconnect a a = D

Reconnecting an endpoint with itself leaves the matching unchanged.

theorem TauCeti.even_card_of_nonempty_perfectMatching (α : Type u) [Fintype α] (h : Nonempty (PerfectMatching α)) : Even (Fintype.card α)

A type carrying a perfect matching has even cardinality: the arcs pair its elements.

theorem TauCeti.isEmpty_perfectMatching_of_not_even {α : Type u} [Fintype α] (h : ¬Even (Fintype.card α)) : IsEmpty (PerfectMatching α)

A type of odd cardinality carries no perfect matching.

theorem TauCeti.card_perfectMatching (α : Type u) [Fintype α] [DecidableEq α] {m : ℕ} (hcard : Fintype.card α = 2 * m) : Fintype.card (PerfectMatching α) = (2 * m - 1).doubleFactorial

The number of perfect matchings of a finite type. A type with 2 * m elements has exactly (2 * m - 1)‼ = 1 · 3 · 5 ⋯ (2 * m - 1) perfect matchings.

theorem TauCeti.IsPerfectMatching.sign_eq {α : Type u} [Fintype α] [DecidableEq α] {f : Equiv.Perm α} (hf : IsPerfectMatching f) : Equiv.Perm.sign f = (-1) ^ (Fintype.card α / 2)

The sign of a perfect matching. A perfect matching of a finite type is a product of half as many disjoint transpositions as the type has elements.

theorem TauCeti.IsPerfectMatching.even_orbitCount_mul {α : Type u} [Finite α] {f g : Equiv.Perm α} (hf : IsPerfectMatching f) (hg : IsPerfectMatching g) : Even (orbitCount (f * g))

A product of two perfect matchings has an even number of orbits. Both factors have the same sign, so the product is even, while the type has even cardinality; the sign of a permutation is the parity of the number of points minus the number of orbits.

theorem TauCeti.IsPerfectMatching.two_mul_orbitCount {α : Type u} [Finite α] {f : Equiv.Perm α} (hf : IsPerfectMatching f) : 2 * orbitCount f = Nat.card α

A perfect matching has half as many orbits as points: its orbits are its pairs.