Documentation

TauCeti.Combinatorics.Enumerative.InvolutionTransversal

Transversals of a fixed-point-free involution on a finite set #

Let f : α → α map a finite set S to itself, involutively and without fixed points, so that S is partitioned into the two-element orbits {a, f a}. A transversal of f on S is a subset T ⊆ S meeting each orbit exactly once; equivalently, a ∈ T ↔ f a ∉ T for every a ∈ S.

This file introduces TauCeti.IsInvolutionTransversal, provides the two ways of recognising a transversal (by the defining equivalence, or from a covering by T and its image), records the resulting splitting of a product over S, and counts the transversals: there are 2 ^ (#S / 2) of them, one binary choice per orbit.

The counting theorem is the combinatorial half of TauCeti.ncard_setOf_mul_map_eq_prod, where f is the action of a ring endomorphism, acting involutively on a set of primes of a Dedekind domain, and a transversal picks one prime from each conjugate pair.

A fixed-point-free involution of a whole type is a perfect matching in the sense of TauCeti.IsPerfectMatching; the notion here is its relative form, carried by a Finset rather than by a type, which is what the arithmetic application supplies.

The induction used for the count — strip off one orbit, doubling the number of transversals — is the one in exists_transversal_family of the formalization kim-em/erdos-unit-distance, written for Alpöge's disproof of the uniform-constant Erdős unit-distance conjecture, where it is run on ideals of a CM field rather than on an abstract finite set.

Main definitions #

Main results #

source
structure TauCeti.IsInvolutionTransversal {α : Type u_1} (f : α → α) (S T : Finset α) :
Prop

T is a transversal of the involution f on the finite set S: a subset of S containing exactly one of a and f a for every a ∈ S.

  • subset : T ⊆ S

    A transversal is a subset of the set it is a transversal of.

  • mem_iff_notMem (a : α) : a ∈ S → (a ∈ T ↔ f a ∉ T)

    A transversal contains exactly one element of each orbit.

Instances For
    source
    theorem TauCeti.IsInvolutionTransversal.map_notMem_of_mem {α : Type u_1} {f : α → α} {S T : Finset α} (hT : IsInvolutionTransversal f S T) {a : α} (ha : a ∈ S) (haT : a ∈ T) :
    f a ∉ T

    A transversal omits the partner of each of its elements.

    source
    theorem TauCeti.IsInvolutionTransversal.map_mem_of_notMem {α : Type u_1} {f : α → α} {S T : Finset α} (hT : IsInvolutionTransversal f S T) {a : α} (ha : a ∈ S) (haT : a ∉ T) :
    f a ∈ T

    A transversal contains the partner of each element of S it omits.

    source
    theorem TauCeti.isInvolutionTransversal_of_cover {α : Type u_1} {f : α → α} {S T : Finset α} (hinvol : ∀ a ∈ S, f (f a) = a) (hsub : T ⊆ S) (hdisj : ∀ a ∈ T, f a ∉ T) (hcover : ∀ a ∈ S, a ∈ T ∨ ∃ b ∈ T, f b = a) :
    IsInvolutionTransversal f S T

    A subset of S disjoint from its image and covering S together with it is a transversal.

    source
    theorem TauCeti.IsInvolutionTransversal.prod_mul_prod_comp {α : Type u_1} {f : α → α} {S T : Finset α} (hT : IsInvolutionTransversal f S T) {M : Type u_2} [CommMonoid M] (g : α → M) (hmaps : ∀ a ∈ S, f a ∈ S) (hinvol : ∀ a ∈ S, f (f a) = a) :
    (∏ a ∈ T, g a) * ∏ a ∈ T, g (f a) = ∏ a ∈ S, g a

    A transversal of f on S splits a product over S: the factors indexed by T and the factors indexed by its f-image together exhaust S.

    source
    theorem TauCeti.finite_setOf_isInvolutionTransversal {α : Type u_1} (f : α → α) (S : Finset α) :
    {T : Finset α | IsInvolutionTransversal f S T}.Finite

    There are only finitely many transversals, since each is a subset of S.

    source
    theorem TauCeti.ncard_setOf_isInvolutionTransversal {α : Type u_1} {f : α → α} {S : Finset α} (hmaps : ∀ a ∈ S, f a ∈ S) (hinvol : ∀ a ∈ S, f (f a) = a) (hfree : ∀ a ∈ S, f a ≠ a) :
    {T : Finset α | IsInvolutionTransversal f S T}.ncard = 2 ^ (S.card / 2)

    The transversal count. A fixed-point-free involution of a finite set S has exactly 2 ^ (#S / 2) transversals: one binary choice per orbit.