4

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?

Tim Campion
  • 60,951
  • 1
    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. – David Roberts Mar 16 '22 at 15:23
  • 1
    @DavidRoberts Not if we're talking about automorphisms of finite sets. Finite sets have decidable equality, hence so do their permutations. – Mike Shulman Mar 16 '22 at 15:27
  • @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. – David Roberts Mar 16 '22 at 15:32
  • Yes, certainly, if you talk about K-finite sets rather than (as in this question) B-finite ones, all bets are off. – Mike Shulman Mar 16 '22 at 17:26
  • 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. – Paul Taylor Mar 16 '22 at 21:08
  • @PaulTaylor Ah, that's a good point... I guess that means that step in the proof would also be non-constructive beyond the cardinal-finite case? – Tim Campion Mar 16 '22 at 21:10

1 Answers1

4

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.)

Mike Shulman
  • 65,064
  • 1
    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? – Tim Campion Mar 16 '22 at 15:38
  • 1
    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? – მამუკა ჯიბლაძე Mar 16 '22 at 15:41
  • 4
    @მამუკაჯიბლაძე 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 – daniel gratzer Mar 16 '22 at 16:06
  • The cardinality of a finite set is also uniquely determined, so yes, we can induct on it. (-: – Mike Shulman Mar 16 '22 at 17:27
  • 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. – Mike Shulman Mar 16 '22 at 17:45
  • @MikeShulman : am I understanding correctly that you're saying: in the slices where $X$ is cardinal-finite, it might as well be $[n]$, and then for these ones the proof that the sign is unique just goes through because it has decidable equality ("the logic might as well be Boolean"), and therefore the sign morphisms glue along the slices ? – Maxime Ramzi Mar 16 '22 at 18:49
  • @MaximeRamzi Yes, that would be the way to compile it out into category-theoretic language. But that compilation is done for us by the general interpretation of type theory into a topos, so we don't have to do it manually every time. – Mike Shulman Mar 16 '22 at 19:13
  • @MikeShulman : sure, I said it that way mostly because I'm not sure how cardinals work in the internal logic of a topos – Maxime Ramzi Mar 16 '22 at 19:18
  • (1) In the topos $Set / \mathbb N$, a locally finite object (which apparently is more standardly called a "decidably K-finite" object) is a sequence of finite sets, but with no uniform bound on their cardinality. How does one induct on cardinality in a setting like this? (2) In your alternative argument, it seems to me that if there is a merely existent isomorphism from $X$ to a cardinal, then when we transfer a generating set across we will eventually get only a merely existent equality between two sign homomorphisms -- do we now appeal to truncatedness of $X$ to get an explicit equality? – Tim Campion Mar 16 '22 at 21:25
  • (1) I'm not sure exactly what you're asking. If you're concerned about whether the proof works, then you need to trust the internal logic: we have a theorem that we can interpret type theory in any topos, including $\rm Set/\mathbb{N}$, and we don't need to delve into any of the details of any particular model in order to conclude that an internally valid argument works in every model. – Mike Shulman Mar 16 '22 at 21:34
  • If you're instead curious how this interpretation ends up working in $\rm Set/\mathbb{N}$ -- or more generally $\rm Set/X$ for any set $X$ -- the answer is roughly that you end up doing induction separately over each finite set indexed by each element of $X$. – Mike Shulman Mar 16 '22 at 21:36
  • (2) Yes, truncatedness -- but not of $X$, rather of the codomain of the sign homomorphism, namely $Z_2$. – Mike Shulman Mar 16 '22 at 21:36
  • @DanielGratzer Of course, yes, thanks, should figure this out myself. The whole point of constructive existence is that it means exhibiting an actual term explicitly. – მამუკა ჯიბლაძე Mar 17 '22 at 07:56