Physlib.Mathematics.Fin.Involutions

There is an equivalence (bijection) between the set of involutions on $\text{Fin}(n+1)$ and the set of pairs $(f, i)$, where $f$ is an involution on $\text{Fin } n$ and $i$ is an element of $\text{Option}(\text{Fin } n)$ satisfying the condition that if $i$ is $\text{some } j \in \text{Fin } n$, then $j$ must be a fixed point of $f$ (i.e., $f(j) = j$). Under this mapping, an involution $g$ on $\text{Fin}(n+1)$ is decomposed based on the image of $0$: 1. If $g(0) = 0$, then $i = \text{none}$ and $f$ is the restriction of $g$ to $\{1, \dots, n\}$. 2. If $g(0) = k+1$ (and thus $g(k+1) = 0$ by involutivity), then $i = \text{some } k$ and $f$ is the involution on $\text{Fin } n$ where $k$ is treated as a fixed point.

Let $n$ be a natural number. Let $\text{Inv}(n)$ be the set of involutions on $\text{Fin } n = \{0, 1, \dots, n-1\}$, which are functions $f$ such that $f(f(x)) = x$ for all $x$. Consider the set of pairs $(f, i)$ such that $f \in \text{Inv}(n)$ and $i$ is either an element of $\text{Fin } n$ that is a fixed point of $f$ (i.e., $f(i) = i$) or $i = \text{none}$. For any two such pairs $f_1 = (f, i)$ and $f_2 = (g, j)$, if $f = g$ and $i = j$, then $f_1 = f_2$.

Given a natural number $n$ and an involution $f: \text{Fin } n \to \text{Fin } n$, let $S = \{i \in \text{Fin } n \mid f(i) = i\}$ be the set of fixed points of $f$. This definition provides an equivalence between the set of optional fixed points of $f$ (which contains either a value `none` or a value `some i` where $i$ is a fixed point of $f$) and the set $\text{Option}(\text{Fin } |S|)$.

Let $n$ be a natural number and $f: \text{Fin}(n+1) \to \text{Fin}(n+1)$ be an involution. Let $(f', i)$ be the pair obtained by decomposing $f$ via the equivalence `involutionCons`, where $f'$ is an involution on $\text{Fin } n$ and $i$ is an optional fixed point of $f'$. If the mapping of this optional fixed point $i$ under `involutionAddEquiv` (with respect to $f'$) results in `none`, then $f(0) = 0$.

Let $n$ be a natural number and let $f_1, f_2: \text{Fin } n \to \text{Fin } n$ be two involutions. Suppose $f_1 = f_2$. Let $S_1$ and $S_2$ be the sets of fixed points of $f_1$ and $f_2$ respectively. The theorem states that the equivalence $\text{involutionAddEquiv } f_1$—which identifies the optional fixed points of $f_1$ (the set of $i \in \text{Option}(\text{Fin } n)$ such that if $i = \text{some } x$, then $f_1(x) = x$) with the set $\text{Option}(\text{Fin } |S_1|)$—is equal to the composition of: 1. The equivalence between the optional fixed points of $f_1$ and those of $f_2$ induced by the equality $f_1 = f_2$. 2. The equivalence $\text{involutionAddEquiv } f_2$ mapping the optional fixed points of $f_2$ to $\text{Option}(\text{Fin } |S_2|)$. 3. The equivalence between $\text{Option}(\text{Fin } |S_2|)$ and $\text{Option}(\text{Fin } |S_1|)$ induced by the equality of the number of fixed points $|S_1| = |S_2|$.

Let $m$ be a natural number and let $f_1, f_2: \text{Fin } m \to \text{Fin } m$ be two involutions. Suppose $f_1 = f_2$. Let $N$ be a natural number such that $N$ is the cardinality of the set of fixed points of $f_1$ (and thus also of $f_2$). For any $n \in \text{Option}(\text{Fin } N)$, the inverse of the equivalence `involutionAddEquiv` (which relates optional fixed points to the set $\text{Option}(\text{Fin } N)$) applied to $n$ for the involution $f_1$ is heterogeneously equal to the inverse of the equivalence applied to $n$ for $f_2$.

Let $n$ be a natural number and let $f$ be an involution on the set $\text{Fin}(n+1) = \{0, 1, \dots, n\}$. Let $(f', i)$ be the decomposition of $f$ into an involution $f'$ on $\text{Fin } n$ and an optional fixed point $i$ provided by the equivalence `involutionCons`. Suppose that the mapping of this decomposition under `involutionAddEquiv` results in `none` (which occurs when $f(0) = 0$ and $i = \text{none}$). Then, for any element $x \in \text{Fin } n$, the successor $x+1$ is a fixed point of $f$ (i.e., $f(x+1) = x+1$) if and only if $x$ is a fixed point of $f'$ (i.e., $f'(x) = x$).

For a natural number $n$, let $S$ be the set of fixed-point-free involutions on the finite set $\text{Fin}(n+1) = \{0, 1, \dots, n\}$, which are functions $f: \text{Fin}(n+1) \to \text{Fin}(n+1)$ satisfying $f(f(i)) = i$ and $f(i) \neq i$ for all $i$. This equivalence states that $S$ is in one-to-one correspondence with the disjoint union (sigma-type) over $k \in \{0, 1, \dots, n-1\}$ of the sets of fixed-point-free involutions $f$ such that $f(0) = k+1$. In other words, fixed-point-free involutions of $\text{Fin}(n+1)$ can be uniquely partitioned based on the image of $0$.

Given $n \in \mathbb{N}$, an element $k \in \text{Fin } n$, and a permutation $e$ of $\text{Fin}(n+1)$, there exists an equivalence between the set of fixed-point-free involutions $f$ on $\text{Fin}(n+1)$ such that $f(0) = k+1$ and the set of functions $f$ on $\text{Fin}(n+1)$ such that the conjugate $e^{-1} \circ f \circ e$ is a fixed-point-free involution satisfying $(e^{-1} \circ f \circ e)(0) = k+1$.

Given a natural number $n$, a value $k \in \{0, \dots, n-1\}$, and a permutation $e$ of the set $\{0, 1, \dots, n\}$, there is an equivalence between: 1. The set of functions $f: \{0, \dots, n\} \to \{0, \dots, n\}$ such that the conjugate function $e^{-1} \circ f \circ e$ is an involution with no fixed points (i.e., $(e^{-1} \circ f \circ e) \circ (e^{-1} \circ f \circ e) = \text{id}$ and $(e^{-1} \circ f \circ e)(i) \neq i$ for all $i$) satisfying the condition $(e^{-1} \circ f \circ e)(0) = k+1$. 2. The set of functions $f: \{0, \dots, n\} \to \{0, \dots, n\}$ such that $f$ itself is an involution with no fixed points satisfying the same condition $(e^{-1} \circ f \circ e)(0) = k+1$. This equivalence holds because a function $f$ is a fixed-point free involution if and only if its conjugate $e^{-1} \circ f \circ e$ is also a fixed-point free involution.

Given a natural number $n$, an index $k \in \{0, \dots, n-1\}$, and a permutation $e$ of the set $\{0, \dots, n\}$, there is an equivalence between: 1. The set of functions $f: \{0, \dots, n\} \to \{0, \dots, n\}$ that are involutions ($f \circ f = \text{id}$), have no fixed points ($f(i) \neq i$ for all $i$), and satisfy $(e^{-1} \circ f \circ e)(0) = k+1$. 2. The set of functions $f: \{0, \dots, n\} \to \{0, \dots, n\}$ that are involutions, have no fixed points, and satisfy $f(e(0)) = e(k+1)$. This equivalence arises because the condition $(e^{-1} \circ f \circ e)(0) = k+1$ is mathematically equivalent to $f(e(0)) = e(k+1)$.

For any natural number $n$ and any element $k \in \{0, \dots, n\}$, there is an equivalence between the set of fixed-point-free involutions $f$ on the set $\text{Fin}(n+2) = \{0, 1, \dots, n+1\}$ that satisfy $f(0) = k+1$ and the set of fixed-point-free involutions on the same set that satisfy $f(0) = 1$. Here, an involution is a function such that $f(f(i)) = i$ for all $i$, and being fixed-point-free means $f(i) \neq i$ for all $i$.

For any natural number $n$, the set of fixed-point-free involutions $f: \text{Fin}(n+2) \to \text{Fin}(n+2)$ satisfying the condition $f(0) = 1$ is equivalent (in one-to-one correspondence) to the set of fixed-point-free involutions $g: \text{Fin}(n) \to \text{Fin}(n)$. Here, $\text{Fin}(k)$ denotes the set of natural numbers $\{0, 1, \dots, k-1\}$, and an involution is a function such that $f(f(i)) = i$ for all $i$. The condition $f(0) = 1$ implies $f(1) = 0$ for such involutions, and the remaining $n$ elements are mapped to each other via a fixed-point-free involution on a set of size $n$.

For any natural number $n$ and any element $k \in \{0, \dots, n\}$ (represented as $k \in \text{Fin}(n+1)$), there exists a one-to-one correspondence between the set of fixed-point-free involutions $f: \text{Fin}(n+2) \to \text{Fin}(n+2)$ satisfying $f(0) = k+1$ and the set of fixed-point-free involutions $g: \text{Fin}(n) \to \text{Fin}(n)$. Here, $\text{Fin}(m)$ denotes the set of natural numbers $\{0, 1, \dots, m-1\}$, an involution is a function such that $f(f(i)) = i$ for all $i$, and being fixed-point-free means $f(i) \neq i$ for all $i$.

For any natural number $n$, there exists an equivalence between the set of fixed-point-free involutions on $\text{Fin}(n+2) = \{0, 1, \dots, n+1\}$ and the disjoint union (sigma type) of $n+1$ copies of the set of fixed-point-free involutions on $\text{Fin}(n) = \{0, 1, \dots, n-1\}$. Here, an involution is a function $f$ such that $f(f(i)) = i$ for all $i$, and it is fixed-point-free if $f(i) \neq i$ for all $i$. The correspondence is given by: \[ \{ f : \text{Fin}(n+2) \to \text{Fin}(n+2) \mid f \circ f = \text{id}, \forall i, f(i) \neq i \} \simeq \sum_{k \in \text{Fin}(n+1)} \{ g : \text{Fin}(n) \to \text{Fin}(n) \mid g \circ g = \text{id}, \forall i, g(i) \neq i \} \] This equivalence arises because any fixed-point-free involution on $n+2$ elements must map $0$ to some element $j \in \{1, \dots, n+1\}$. There are $n+1$ such choices for $j$, and for each choice, the remaining $n$ elements must be permuted by a fixed-point-free involution.

For any natural number $n$, there exists an equivalence (bijection) between the set of fixed-point-free involutions on $\text{Fin}(n+2) = \{0, 1, \dots, n+1\}$ and the Cartesian product of $\text{Fin}(n+1) = \{0, 1, \dots, n\}$ and the set of fixed-point-free involutions on $\text{Fin}(n) = \{0, 1, \dots, n-1\}$. An involution is a function $f$ such that $f \circ f = \text{id}$, and it is fixed-point-free if $f(i) \neq i$ for all $i$. This equivalence represents the fact that any fixed-point-free involution of $n+2$ elements can be decomposed into the choice of which element $0$ is mapped to (one of $n+1$ possibilities) and a fixed-point-free involution on the remaining $n$ elements.

For any natural number $n$, the set of functions $f: \{0, 1, \dots, n-1\} \to \{0, 1, \dots, n-1\}$ that are involutions (i.e., $f(f(i)) = i$ for all $i$) and have no fixed points (i.e., $f(i) \neq i$ for all $i$) is finite.

For any natural number $n$, the cardinality of the set of fixed-point-free involutions on $\text{Fin}(n+2)$ is equal to $(n+1)$ times the cardinality of the set of fixed-point-free involutions on $\text{Fin}(n)$. An involution $f$ is a function such that $f(f(i)) = i$ for all $i$, and it is fixed-point-free if $f(i) \neq i$ for all $i$.

For any natural number $n$, the cardinality of the set of fixed-point-free involutions on the set $\text{Fin}(2n) = \{0, 1, \dots, 2n-1\}$ is equal to the double factorial $(2n - 1)!!$. An involution $f$ is a function such that $f(f(i)) = i$ for all $i$, and it is fixed-point-free if $f(i) \neq i$ for all $i$.

For any natural number $n$, the cardinality of the set of fixed-point-free involutions on the set $\text{Fin}(2n+1) = \{0, 1, \dots, 2n\}$ is $0$. An involution $f$ is a function such that $f(f(i)) = i$ for all $i$, and it is fixed-point-free if $f(i) \neq i$ for all $i$.

For any even natural number $n$, the cardinality of the set of fixed-point-free involutions on the set $\text{Fin}(n) = \{0, 1, \dots, n-1\}$ is equal to the double factorial $(n - 1)!!$. A function $f: \text{Fin}(n) \to \text{Fin}(n)$ is an involution if $f(f(i)) = i$ for all $i$, and it is fixed-point-free if $f(i) \neq i$ for all $i$.

For any odd natural number $n$, the cardinality of the set of fixed-point-free involutions on the set $\text{Fin}(n) = \{0, 1, \dots, n-1\}$ is $0$. An involution $f$ is a function such that $f(f(i)) = i$ for all $i \in \text{Fin}(n)$, and it is fixed-point-free if $f(i) \neq i$ for all $i \in \text{Fin}(n)$.