Definition. Nominal Sets as Day Quotients

In the Schanuel topos, the underlying category for Day convolution is 𝐢=𝕀op, where 𝕀 is the category of finite sets and injections.

Given a nominal set 𝑋, its presheaf action describes elements supported by 𝑑:

𝑋(𝑑)={π‘₯βˆˆπ‘‹|π—Œπ—Žπ—‰π—‰(π‘₯)βŠ†π‘‘}

Instead of taking 𝑋 a priori as a presheaf, we can view it as a finitely- supported 𝖯𝖾𝗋𝗆(𝔸)-set. We can restrict our attention to the groupoid core 𝐺=π–Όπ—ˆπ—‹π–Ύ(𝕀), asking for the support to be exactly the input:

𝑋𝑠={π‘₯βˆˆπ‘‹|π—Œπ—Žπ—‰π—‰(π‘₯)=𝑠}

This family 𝑋‒:πΊβ†’π’πžπ­ is functorial on finite sets and bijections.

By extending this functor along the inclusions described in Quotient Coincidence, we can extend 𝑋‒ to both a presheaf π—†π—„π–―π—Œπ—(𝑋‒) and a copresheaf π—†π—„π–’π—ˆπ—‰π—Œπ—(𝑋‒) on 𝐢. This suggests the equivalence:

π—†π—„π–―π—Œπ—(𝑋‒)βŠΈπ‘Œβ‰…π·π—†π—„π–’π—ˆπ—‰π—Œπ—(𝑋‒)π‘Œ

I suspect this allows us to describe name abstraction [𝑋]π‘Œ [1] β€”which ordinarily looks like an operation on two presheaves of the same varianceβ€”as the quotient of π‘Œ by the induced copresheaf π—†π—„π–’π—ˆπ—‰π—Œπ—(𝑋‒).

Concretely, [𝑋]π‘Œ is usually given by the quotient of the product by an equivalence relation:

[𝑋]π‘Œβ‰…π‘‹Γ—π‘ŒβˆΌ

where (π‘₯,𝑦)∼(πœ‹π‘₯,πœ‹π‘¦) for permutations πœ‹ fixing π—Œπ—Žπ—‰π—‰(𝑦)βˆ’π—Œπ—Žπ—‰π—‰(π‘₯).

On the other hand, the Day quotient computes to a coend:

(π·π—†π—„π–’π—ˆπ—‰π—Œπ—(𝑋‒)π‘Œ)(𝑐)=βˆ«π‘ π‘‹π‘ Γ—π‘Œ(π‘ βŠŽπ‘)

A priori, a coend over 𝑠 of the product π‘‹π‘ Γ—π‘Œ(π‘ βŠŽπ‘) is expressed as the quotient of a set of triples by an equivalence relation β‰ˆ:

{(𝑠,π‘₯,𝑦)|𝑠=π—Œπ—Žπ—‰π—‰(π‘₯),π—Œπ—Žπ—‰π—‰(𝑦)βŠ†π‘ βŠŽπ‘}/β‰ˆ

However, because the comprehension formula fixes 𝑠=π—Œπ—Žπ—‰π—‰(π‘₯), we reduce to a quotient of pairs:

{(π‘₯,𝑦)|π—Œπ—Žπ—‰π—‰(𝑦)βŠ†π—Œπ—Žπ—‰π—‰(π‘₯)βŠŽπ‘}/β‰ˆ

I suspect that this quotient will equate to the one given by [𝑋]π‘Œ, thus resolving the apparent issues with variance. I further suspect that one will need the sheaf condition (pullback-preservation) of nominal sets to establish this equivalence.

References

Generalised Name Abstraction for Nominal Sets β†—
nominal-sets-quotient definition entries/parsing/nominal-sets-quotient.hel