Proof of Permutations of [n]: Identity, Composition, Inverses, Translations and Transpositions

Each result cited is universally quantified over the data in its own statement.

Preliminaries. The adopted setting extends Sets and Maps: Ordinary Notation by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §base. By Intervals of Natural Numbers §segment and Intervals of Natural Numbers §interval, $[n]=\{k\in\mathbb{N}_{0}:1\le k\le n\}$, a subclass of the set $\mathbb{N}_{0}$ and hence a set by Permutations of a Set and the Set of Permutations of [n] §permutations; $S_{n}$ is a set by the same clause; and every map between sets is a set by Sets and Maps: Ordinary Notation §maps. Hence, by Permutations of a Set and the Set of Permutations of [n] §membership, every $\sigma\in S_{n}$ is a bijective map $\sigma:[n]\to[n]$, and every bijective map $[n]\to[n]$ lies in $S_{n}$. A map $F:A\to B$ has domain $A$ by Functions, Values of a Function, and Functions from One Class to Another §map; so, by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality, two maps $F,G:A\to B$ are equal as soon as $F(u)=G(u)$ for every $u\in A$. We refer to this as (E).

Clause identity. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §identity, $\mathrm{id}_{[n]}$ is a bijective map $[n]\to[n]$, so $\mathrm{id}_{[n]}\in S_{n}$. For $\sigma\in S_{n}$, Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §identity-neutral with $A=B=[n]$ and $F=\sigma$ gives $\sigma\circ\mathrm{id}_{[n]}=\sigma$ and $\mathrm{id}_{[n]}\circ\sigma=\sigma$.

Clause composition. Let $\sigma,\tau\in S_{n}$. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition with $F=\tau$ and $G=\sigma$, $\sigma\circ\tau$ is a map $[n]\to[n]$ with $(\sigma\circ\tau)(u)=\sigma(\tau(u))$ for $u\in[n]$, and it is bijective by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §preservation; so $\sigma\circ\tau\in S_{n}$. Now let $\rho,\sigma,\tau\in S_{n}$. By what was just shown and Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition, $(\rho\circ\sigma)\circ\tau$ and $\rho\circ(\sigma\circ\tau)$ are maps $[n]\to[n]$, and for every $u\in[n]$,

$$((\rho\circ\sigma)\circ\tau)(u)=(\rho\circ\sigma)(\tau(u))=\rho(\sigma(\tau(u)))=\rho((\sigma\circ\tau)(u))=(\rho\circ(\sigma\circ\tau))(u).$$

By (E), $(\rho\circ\sigma)\circ\tau=\rho\circ(\sigma\circ\tau)$.

Clause inverse. Let $\sigma\in S_{n}$. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse, $\sigma^{-1}$ is a bijective map $[n]\to[n]$, so $\sigma^{-1}\in S_{n}$, and $\sigma^{-1}\circ\sigma=\mathrm{id}_{[n]}$ and $\sigma\circ\sigma^{-1}=\mathrm{id}_{[n]}$. Applying Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse-criterion to $F=\sigma^{-1}$ and $G=\sigma$, which are maps $[n]\to[n]$ with $G\circ F=\sigma\circ\sigma^{-1}=\mathrm{id}_{[n]}$ and $F\circ G=\sigma^{-1}\circ\sigma=\mathrm{id}_{[n]}$, gives $G=F^{-1}$, that is, $(\sigma^{-1})^{-1}=\sigma$.

Clause translation. Fix $\tau\in S_{n}$. For a set variable $\sigma$, the expression $\sigma\circ\tau$ is the class abstraction of Relations, Domain, Range, Inverse and Composition §composition, with $\tau$ as parameter, whose formula quantifies over set variables only, the ordered pair being a defined set symbol used properly. For $\sigma\in S_{n}$, $\sigma\circ\tau$ is a map $[n]\to[n]$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition, hence a set by Sets and Maps: Ordinary Notation §maps, and the elimination of a formula $v=\sigma\circ\tau$, as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §class-terms, is the formula $\forall w\,(w\in v\Leftrightarrow\psi(w,\sigma,\tau))$ of Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §class-terms, with $\psi$ the formula of that class abstraction; it applies no quantifier to a class variable, so it is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure. The same holds for $v=\tau\circ\sigma$. By the clause composition, $\sigma\circ\tau\in S_{n}$ and $\tau\circ\sigma\in S_{n}$ for every $\sigma\in S_{n}$. Hence Maps and Relations Given by Formulas §map, with $a=b=S_{n}$ and $t(\sigma)=\sigma\circ\tau$, respectively $t(\sigma)=\tau\circ\sigma$, gives exactly one map $R_{\tau}:S_{n}\to S_{n}$ with $R_{\tau}(\sigma)=\sigma\circ\tau$, and exactly one map $L_{\tau}:S_{n}\to S_{n}$ with $L_{\tau}(\sigma)=\tau\circ\sigma$, for every $\sigma\in S_{n}$.

By the clause inverse, $\tau^{-1}\in S_{n}$, so $R_{\tau^{-1}}$ and $L_{\tau^{-1}}$ exist as well. Let $\sigma\in S_{n}$. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition, the associativity in the clause composition, the clause inverse and the clause identity,

$$(R_{\tau^{-1}}\circ R_{\tau})(\sigma)=(\sigma\circ\tau)\circ\tau^{-1}=\sigma\circ(\tau\circ\tau^{-1})=\sigma\circ\mathrm{id}_{[n]}=\sigma, \qquad (R_{\tau}\circ R_{\tau^{-1}})(\sigma)=(\sigma\circ\tau^{-1})\circ\tau=\sigma\circ(\tau^{-1}\circ\tau)=\sigma,$$

and likewise

$$(L_{\tau^{-1}}\circ L_{\tau})(\sigma)=\tau^{-1}\circ(\tau\circ\sigma)=(\tau^{-1}\circ\tau)\circ\sigma=\mathrm{id}_{[n]}\circ\sigma=\sigma, \qquad (L_{\tau}\circ L_{\tau^{-1}})(\sigma)=\tau\circ(\tau^{-1}\circ\sigma)=(\tau\circ\tau^{-1})\circ\sigma=\sigma.$$

These composites are maps $S_{n}\to S_{n}$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition, and $\mathrm{id}_{S_{n}}(\sigma)=\sigma$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §identity. By (E), $R_{\tau^{-1}}\circ R_{\tau}=\mathrm{id}_{S_{n}}=R_{\tau}\circ R_{\tau^{-1}}$ and $L_{\tau^{-1}}\circ L_{\tau}=\mathrm{id}_{S_{n}}=L_{\tau}\circ L_{\tau^{-1}}$, so $R_{\tau}$ and $L_{\tau}$ are bijective by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse-criterion.

Clause inversion. For a set variable $\sigma$, $\sigma^{-1}$ is the class abstraction of Relations, Domain, Range, Inverse and Composition §inverse, whose formula quantifies over set variables only. For $\sigma\in S_{n}$, $\sigma^{-1}$ is a map $[n]\to[n]$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse, hence a set by Sets and Maps: Ordinary Notation §maps; as in the clause translation, the elimination of a formula $v=\sigma^{-1}$, as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §class-terms, is the formula of Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §class-terms, which is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure. Since $\sigma^{-1}\in S_{n}$ for every $\sigma\in S_{n}$ by the clause inverse, Maps and Relations Given by Formulas §map with $a=b=S_{n}$ and $t(\sigma)=\sigma^{-1}$ gives exactly one map $J:S_{n}\to S_{n}$ with $J(\sigma)=\sigma^{-1}$ for every $\sigma\in S_{n}$. For $\sigma\in S_{n}$, Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition and the clause inverse give $(J\circ J)(\sigma)=(\sigma^{-1})^{-1}=\sigma=\mathrm{id}_{S_{n}}(\sigma)$, so $J\circ J=\mathrm{id}_{S_{n}}$ by (E), and Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse-criterion with $F=G=J$ shows that $J$ is bijective.

Clause transposition. Let $p,q\in[n]$ with $p\neq q$. Existence. The property $x=p$ of elements $x$ of $[n]$ is expressed by an atomic formula, which is predicative by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §predicative, and the expressions $q$ and $x$ lie in $[n]$ for every $x\in[n]$. By Maps Defined by Cases §cases with $A=B=[n]$ there is a map $g:[n]\to[n]$ with $g(p)=q$ and $g(x)=x$ for every $x\in[n]$ with $x\neq p$. Next, the property $x=q$ is again atomic, $p\in[n]$, and for $x\in[n]$ the expression $g(x)$, the value of Functions, Values of a Function, and Functions from One Class to Another §value, a defined set symbol used properly since $x\in[n]=\operatorname{dom}g$, lies in $[n]$. By Maps Defined by Cases §cases again there is a map $\theta:[n]\to[n]$ with $\theta(q)=p$ and $\theta(x)=g(x)$ for every $x\in[n]$ with $x\neq q$. Then $\theta(q)=p$; $\theta(p)=g(p)=q$ because $p\neq q$; and $\theta(k)=g(k)=k$ for every $k\in[n]$ with $k\neq p$ and $k\neq q$.

Uniqueness. If $\theta':[n]\to[n]$ also has $\theta'(p)=q$, $\theta'(q)=p$ and $\theta'(k)=k$ for every other $k\in[n]$, then $\theta(k)=\theta'(k)$ for every $k\in[n]$, by the three cases $k=p$, $k=q$, and $k\neq p$, $k\neq q$; so $\theta=\theta'$ by (E).

$\theta\circ\theta=\mathrm{id}_{[n]}$ and $\theta\in S_{n}$. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition, $\theta\circ\theta$ is a map $[n]\to[n]$ with $(\theta\circ\theta)(p)=\theta(q)=p$, $(\theta\circ\theta)(q)=\theta(p)=q$, and $(\theta\circ\theta)(k)=\theta(k)=k$ for every other $k\in[n]$. Thus $(\theta\circ\theta)(k)=k=\mathrm{id}_{[n]}(k)$ for every $k\in[n]$, by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §identity, and $\theta\circ\theta=\mathrm{id}_{[n]}$ by (E). Finally Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse-criterion with $F=G=\theta$ shows that $\theta$ is bijective, so $\theta\in S_{n}$ by the preliminaries.