Proof of Inversions of a Permutation Form a Finite Set, and the Sign Map Exists

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

Preliminaries. The adopted setting extends Sets and Maps: Ordinary Notation, The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion, Commutative Rings, Fields and Ordered Fields: Standard Notation and The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness, through the base clauses of the settings it extends, starting from Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces §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 set by Sets and Maps: Ordinary Notation §set-builder, its defining formula being predicative by Commutative Rings, Fields and Ordered Fields: Standard Notation §notation-sources, and finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice §naturals. Write $B=[n]\times[n]$; it is a set by Sets and Maps: Ordinary Notation §sets and finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice §union. Every map between sets is a set by Sets and Maps: Ordinary Notation §maps; $S_{n}$ is a set by Permutations of a Set and the Set of Permutations of [n] §permutations, and 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]$. A map $F:A\to Y$ 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 Y$ are equal as soon as $F(u)=G(u)$ for every $u\in A$; we refer to this as (E). $\mathbb{R}$ is an ordered field by The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness §reals, hence a commutative ring, so by Commutative Rings, Fields and Ordered Fields: Standard Notation §rings its multiplication is an associative and commutative binary operation on the set $\mathbb{R}$ with neutral element $1$, the products over finite sets below are those of Sums and Products over a Finite Set and over an Interval §operation, Sums and Products over a Finite Set and over an Interval §empty and Sums and Products over a Finite Set and over an Interval §subsets, and the empty product is $1$.

Clause inversions. Let $\sigma\in S_{n}$. By Inversions of a Permutation of [n] §inversions, $\mathrm{Inv}(\sigma)$ is a set and a subclass of $[n]\times[n]=B$, so $\mathrm{Inv}(\sigma)\subseteq B$. As $B$ is finite by the preliminaries, $\mathrm{Inv}(\sigma)$ is finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice §subset.

A product of constant factors. We use the following fact (C): if $D$ is a finite set, $c\in\mathbb{R}$, and $g$ is a map from a set containing $D$ to $\mathbb{R}$ with $g(x)=c$ for every $x\in D$, then $\prod_{x\in D}g(x)=c^{\#D}$. By Sums and Products over a Finite Set and over an Interval §subsets the product is that of the restriction $g|_{D}$, which by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §restriction is a function with domain $D\cap\operatorname{dom}g=D$, as $D\subseteq\operatorname{dom}g$, and with $(g|_{D})(x)=g(x)=c$ for $x\in D$; since $\operatorname{ran}(g|_{D})\subseteq\operatorname{ran}g\subseteq\mathbb{R}$, it is a map $D\to\mathbb{R}$. If $D=\emptyset$, the product is $1$ by Sums and Products over a Finite Set and over an Interval §empty and the preliminaries, $\#D=0$ by Counting: Intervals, Empty Sets and Singletons, Injective Images, Subsets, Unions and Products §empty, and $c^{0}=1$ by Powers with Exponents in the Natural Numbers with Zero §zero. If $D\neq\emptyset$, then by Sums and Products over a Finite Set and over an Interval §operation, with $\#D\in\mathbb{N}$ and a bijection $\varphi$ from $[\#D]$ onto $D$ as provided there, $\prod_{x\in D}g(x)=\prod_{k=1}^{\#D}g|_{D}(\varphi(k))$, which by Iterated Operations: Finite Sums and Finite Products §iterated is the iterated product of the map $k\mapsto g|_{D}(\varphi(k))$ on $[\#D]$. This map has the value $c$ at every $k\in[\#D]$, since $\varphi(k)\in D$, so by (E) it is the map $k\mapsto c$ on $[\#D]$, whose iterated product is $c^{\#D}$ by Powers with Exponents in the Natural Numbers with Zero §power and Iterated Operations: Finite Sums and Finite Products §iterated.

Clause sign-map. The factor map. The product $S_{n}\times B$ is a set by Sets and Maps: Ordinary Notation §sets. Let $\Pi(x)$ be the property of its elements

$$\exists\sigma\,\exists r\,\bigl(x=(\sigma,r)\wedge\sigma\in S_{n}\wedge r\in B\wedge\exists i\,\exists j\,(r=(i,j)\wedge i<j\wedge\sigma(j)<\sigma(i))\bigr),$$

with parameters $S_{n}$, $B$ and the strict order $<$. The last two conjuncts are the defining formula of $\mathrm{Inv}(\sigma)$ in Inversions of a Permutation of [n] §inversions, with $r$ in place of $p$, which is predicative there, with $\sigma$ a set-variable parameter; here $\sigma$ is a bound set variable, so we check $\Pi$ directly: the values $\sigma(i)$ and $\sigma(j)$ are used properly, as the preceding conjuncts give $\sigma\in S_{n}$, so that $\operatorname{dom}\sigma=[n]$ by the preliminaries, and $(i,j)=r\in B$, so that $i,j\in[n]$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership; and the ordered pairs are defined set symbols. The relation notation $\sigma(j)<\sigma(i)$, $i<j$ and the values $\sigma(i)$, $\sigma(j)$ are predicative by Commutative Rings, Fields and Ordered Fields: Standard Notation §notation-sources, and no quantifier is applied to a class variable, so $\Pi$ is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure. The constants $1$ and $-1$ lie in $\mathbb{R}$: $1$ is the unit of the commutative ring $\mathbb{R}$, and $-1\in\mathbb{R}$ is its negative by Negatives, Differences, Reciprocals and Quotients §negative. By Maps Defined by Cases §cases with $A=S_{n}\times B$ and target $\mathbb{R}$, there is a map $f:S_{n}\times B\to\mathbb{R}$ with $f(x)=-1$ if $\Pi(x)$ and $f(x)=1$ otherwise. For $\sigma\in S_{n}$ and $r\in B$: if $r\in\mathrm{Inv}(\sigma)$, then by Inversions of a Permutation of [n] §membership $r=(i,j)$ for some $i,j\in[n]$ with $i<j$ and $\sigma(j)<\sigma(i)$, so $\Pi((\sigma,r))$ holds with the witnesses $\sigma$ and $r$; and if $\Pi((\sigma,r))$ holds with witnesses $\sigma'$ and $r'$, then $(\sigma,r)=(\sigma',r')$ gives $\sigma=\sigma'$ and $r=r'$ by The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic, so $r=(i,j)$ for some $i,j$ with $i<j$ and $\sigma(j)<\sigma(i)$, where $i,j\in[n]$ by $r\in B$ and Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership, and $r\in\mathrm{Inv}(\sigma)$ by Inversions of a Permutation of [n] §membership. Hence $f(\sigma,r)=-1$ if $r\in\mathrm{Inv}(\sigma)$, and $f(\sigma,r)=1$ if $r\in B\setminus\mathrm{Inv}(\sigma)$.

The product map. For $\sigma\in S_{n}$ let $f_{\sigma}:B\to\mathbb{R}$, $r\mapsto f(\sigma,r)$. By Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set §finite-operation, applied to the multiplication of $\mathbb{R}$ (associative, commutative, with neutral element $1$, by the preliminaries), $A=S_{n}$, the finite set $B$ and $f$, there is exactly one map $h:S_{n}\to\mathbb{R}$ with $h(\sigma)=\prod_{r\in B}f_{\sigma}(r)$ for every $\sigma\in S_{n}$.

Its values. Let $\sigma\in S_{n}$, $I=\mathrm{Inv}(\sigma)$ and $C=B\setminus I$. Both are subsets of $B$, hence finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice §subset; $I\cap C=\emptyset$, and $I\cup C=B$ because $I\subseteq B$ by the clause inversions. By Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §disjoint-union, with the products over $I$ and $C$ being those of the restrictions of $f_{\sigma}$ by Sums and Products over a Finite Set and over an Interval §subsets,

$$h(\sigma)=\prod_{r\in B}f_{\sigma}(r)=\Bigl(\prod_{r\in I}f_{\sigma}(r)\Bigr)\Bigl(\prod_{r\in C}f_{\sigma}(r)\Bigr).$$

Since $f_{\sigma}(r)=-1$ for $r\in I$ and $f_{\sigma}(r)=1$ for $r\in C$, (C) gives $\prod_{r\in I}f_{\sigma}(r)=(-1)^{\#I}$ and $\prod_{r\in C}f_{\sigma}(r)=1^{\#C}$, and $1^{\#C}=1$ by Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §product. Therefore $h(\sigma)=(-1)^{\#\mathrm{Inv}(\sigma)}\cdot1=(-1)^{\#\mathrm{Inv}(\sigma)}$.

Existence and uniqueness. The map $s=h:S_{n}\to\mathbb{R}$ has $s(\sigma)=(-1)^{\#\mathrm{Inv}(\sigma)}$ for every $\sigma\in S_{n}$. If $s':S_{n}\to\mathbb{R}$ is another map with this property, then $s(\sigma)=s'(\sigma)$ for every $\sigma\in S_{n}$, so $s=s'$ by (E).