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, 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.

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.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.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.

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.

@[instance_reducible]

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

Equations

• TauCeti.instDecidableIsPerfectMatching f = TauCeti.instDecidableIsPerfectMatching._aux_1 f

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.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.

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.