4
$\begingroup$

Let $X$ be a finite set. I now have a favorite construction of the sign homomorphism $Sym(X) \to C_2$. But perhaps it shouldn't be my favorite construction.

After discussion with the experts, I've learned that Poonen's construction only works constructively if $X$ is assumed to be cardinal-finite in the following sense. I refer to the nlab page for finite object:

Definition: Let $X$ be an object of a topos. Say that $X$ is a finite cardinal if it is a proper initial segment of $\mathbb N$, and cardinal-finite if it is equipped with a bijection to a finite cardinal. (This is the definition under "external version" on the nlab page.)

The reason is that Poonen's construction involves picking out the index-2 subgroup $G < C_2^{\binom{X}{2}}$ defined by $G = \{(x_e)_{e \in \binom{X}{2}} \mid \sum_e x_e = 0\}$. Here $\binom{X}{2}$ is the set of 2-element subsets of $X$. The point is that in order to sum over $\binom{X}{2}$, it needs to be a cardinal-finite set, which in turn basically means that $X$ itself should be cardinal-finite.

Here is an example suggesting that this may not be the optimal generality, pointed out to me by Andrew Swan. Let $G$ be a discrete group, and let $\mathcal E$ be the topos of $G$-sets. Then a cardinal-finite object $X$ in $\mathcal E$ is a finite set equipped with the trivial $G$-action. In this case, $Sym(X)$ is the usual symmetric group on $X$, again equipped with the trivial $G$-action. And indeed, the sign permutation $Sym(X) \to C_2$ is well-defined ($C_2$ is the usual group, with trivial $G$-action). But more generally, if $X$ is any finite set with (possibly nontrivial) $G$-action, then although the $G$-action on $Sym(X)$ is generally nontrivial, via $(g \cdot f)(x) = g \cdot (f(g^{-1} \cdot x))$, it's plain from this formula that each $g \in G$ acts via an even permutation on $Sym(X)$, so that the sign permutation $Sym(X) \to C_2$ is still well-defined! Such an object $X$ is locally cardinal-finite in the following sense:

Definition: Let $X$ be an object of a topos. Say that $X$ is locally cardinal-finite if it becomes cardinal-finite after pullback to some well-supported slice topos. (This is Definition 2.1 on the nlab page above).

This suggests that answer to the following might be yes, even though I don't know a proof:

Question 1: Let $X$ be a locally cardinal-finite object of a topos $\mathcal E$. Then does the internal group object $Sym(X) \in Grp(\mathcal E)$ admit a nontrivial "sign" homomorphism $Sym(X) \to C_2$ in $Grp(\mathcal E)$?

I believe the definition of local cardinal-finiteness is equivalent to saying in the internal logic of $\mathcal E$ that there merely exists a bijection from $X$ to a finite cardinal. So I think the following version of the question is more-or-less equivalent:

Question 2: Work in a constructive metatheory. Let $X$ be a set for which there exists a bijection from $X$ to a finite cardinal. Then does there exist a nontrivial "sign" homomorphism $Sym(X) \to C_2$?

Question 3: Perhaps I haven't identified the right class of "finite" objects to work with for the sign to exist constructively. Is there some other constructive notion of "finiteness" more general than cardinal-finiteness for which the "sign" homomorphism is well-defined?

$\endgroup$
6
  • 1
    $\begingroup$ Another approach to this, which may be obviously false, is to instead replace $C_2$ by the automorphisms of something that's not the booleans $\{\top,\bot\}$... it seems too much to hope for that one could get the automorphisms of some (sub)object of truth values (if not $\Omega$ itself), but it sounds tantalising. I mean, saying a permutation is either even or not even smells very much like a truth value thing that should be altered in the absence of LEM. $G\mathbf{Set}$ is Boolean, after all, which might account for Swan's examle. $\endgroup$
    – David Roberts
    Mar 16, 2022 at 15:23
  • 1
    $\begingroup$ @DavidRoberts Not if we're talking about automorphisms of finite sets. Finite sets have decidable equality, hence so do their permutations. $\endgroup$ Mar 16, 2022 at 15:27
  • $\begingroup$ @MikeShulman I did say it might be obviously false. I'm mildly surprised about the decidable equality, but I presume that might be hiding inside the definition of "finite". My comment is meant to be considered in the light of all the variations, like Kuratowski-finite etc. The sentence "the “internally finite” objects (those that are locally isomorphic to a finite cardinal, as above) can be characterized as the decidable $K$-finite objects." at the nLab makes me think there can be non-decidable $K$-finite objects. But this is not strictly Tim's question, I agree. $\endgroup$
    – David Roberts
    Mar 16, 2022 at 15:32
  • $\begingroup$ Yes, certainly, if you talk about K-finite sets rather than (as in this question) B-finite ones, all bets are off. $\endgroup$ Mar 16, 2022 at 17:26
  • $\begingroup$ What do you mean by "two-element subsets" unless the set has decidable equality? The way to resolve this question would be to ask it in either sheaves on the Möbius strip or anon-decidable quotient of 2. $\endgroup$ Mar 16, 2022 at 21:08

1 Answer 1

4
$\begingroup$

The answer to question 2 as phrased is trivially yes: since there exists such a bijection, choose one, and use it to define a sign homomorphism. But I assume what you meant to ask is, if there exists a bijection from $X$ to a finite cardinal, can we construct a specified sign homomorphism? (In the language of type theory, we're switching from a propositionally truncated $\exists$ to an untruncated $\Sigma$. It's harder to formulate this exactly in first-order logic.) This is what's equivalent to question 1 (the way you phrased question 2 originally would be equivalent to asking whether there is such a sign homomorphism in some well-supported slice).

However, the answer to these questions is also yes, because the sign homomorphism for finite cardinals is unique, and unique objects can always be specified. In the language of type theory, the "type of sign homomorphisms" is always a proposition, so we can eliminate into it out of a propositionally truncated type like "there exists a bijection to a finite cardinal" without needing to truncate it first.

(The standard proof of uniqueness of the sign homomorphism should go through constructively. For instance, since ${\rm Sym}(X)$ is generated by transpositions, and any two transpositions are conjugate, any such homomorphism is determined by a single value, hence there can be at most one nontrivial such.)

$\endgroup$
13
  • 1
    $\begingroup$ Interesting, thanks! If I understand right, your argument relies on being able to prove that if $X$ is locally cardinal-finite, then we can exhibit an equality between any two homomorphisms $Sym(X) \rightrightarrows C_2$. I guess what worries me is that I'm not sure I could prove $Sym(X)$ is generated by transpositions if I only know that $Sym(X)$ is locally cardinal-finite... e.g. we can't argue by induction on the cardinality of $X$, can we? $\endgroup$
    – Tim Campion
    Mar 16, 2022 at 15:38
  • 1
    $\begingroup$ What you say reminds me of my old desire to ask about. I heard from many toposophers the slogan "unique existence implies global existence". But how exactly does this work in Type Theory? Suppose I have two separate proofs: one, that some type is inhabited and another, that it is a subsingleton. It is hard for me to imagine - how can this help to get hold of an explicit term? $\endgroup$ Mar 16, 2022 at 15:41
  • 4
    $\begingroup$ @მამუკაჯიბლაძე while this could probably be a full question, the rough idea is that mere existence has an elimination principle that says you can extend a map $f : (a : A) \to (p : P(a)) \to B(a,p)$ to a map $(x : \exists a : A. P(a)) \to B(x)$ when $f(a, p) = f(a',p')$ for any $a'$ and $p'$. Unique existence precisely asserts that $(a,p) = (a',p')$ for any $(a',p')$ so this additional constraint collapses. To answer your question then, the function for unique choice just works by picking out the term you had to provide to witness inhabitation, and uniqueness ensures that this is well-defined $\endgroup$ Mar 16, 2022 at 16:06
  • $\begingroup$ The cardinality of a finite set is also uniquely determined, so yes, we can induct on it. (-: $\endgroup$ Mar 16, 2022 at 17:27
  • $\begingroup$ Alternatively, we can prove in the obvious way that ${\rm Sym}([n])$ is generated by transpositions for any finite cardinal, and then use the fact that generating sets of groups transfer across isomorphisms. $\endgroup$ Mar 16, 2022 at 17:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.