# Trivializations of set-theoretic fiber bundles up to permutations

Let $$A,B$$ be sets with $$|A|=n=k \cdot m$$ and $$|B|=m$$. Let $$\pi: A \twoheadrightarrow B$$ be a surjective map, s.t. $$|\pi^{-1}(b)|=k$$ for all $$b \in B$$. I am basically interested in trivializations $$\alpha: A \cong B \times [k]$$, but only almost. Actually, I would like to identify those $$\alpha$$'s that have the same SET of preimages $$S_{\alpha}=\{\,\alpha^{-1}\left(B\times \{i\}\right) \, | \, i \in [k] \,\}$$.

It's easy to compute the number of trivializations up to this identification. I am actually looking for a nicer set-up, so that the identification is kind of "built-in". I thought about exchanging $$[k]$$ by a multiset with $$k$$ non-distinguishable elements, but I am not sure if this makes sense.. Do you see an elegant (read "categorical"/"natural") way to define trivialitations up to $$S_k$$-action (basically an unordered version of the above)?

• As trivializations, the $\alpha$'s should satisfy $\pi_B \circ \alpha = \pi$ Commented Aug 5 at 18:10

Working in univalent type theory, you could define your type of trivialisations as $$\sum_{(C : BS_k)} \sum_{(\alpha : A \simeq B \times C)} \pi_1 \circ \alpha = \pi$$ where $$BS_k = \sum_{X : \mathcal{U}} \| X \simeq [k] \|$$ is the type of $$k$$-element types. This naturally endows the type of trivialisations $$A \simeq B \times [k]$$ with an action of $$S_k$$. (Alternatively you could just require $$C : \mathcal{U}$$, since the fact that $$C$$ has $$k$$ elements follows from the assumptions. $$\sum_{C : \mathcal{U}} A \simeq B \times C$$ is the type of lenses from $$A$$ to $$B$$.)
• Thx for your answer. I am not sure if I understand this, but a natural $S_k$-action is what I already have. My goal is to find a set-up, where you don't have to mod out this action afterwards to find the desired objects (which are in bijection to trivializations mod $S_k$)... Basically I want an unordered version of the original setup Commented Aug 5 at 19:11
• You get that for free from univalence: a permutation in $S_k$ gives you an identification $[k] = [k]$, which induces an identification between two trivialisations if they only differ by the given permutation. The type above has as many connected components as the number you computed (it is a groupoid, but you can take its set truncation if needed). Commented Aug 5 at 19:24
Naïm Favier gave a nice answer in terms of univalent types. A more "down-to-earth" definition could be the following: A unordered trivialization is an unordered $$k$$-partition $$\{A_1,\dots,A_k\}$$ of $$A$$ s.t. the $$\pi\circ \iota_i:A_i \to B$$ are bijections.