Definition df-swapf 50367

Description: Define the swap functor from (𝐶 ×_c 𝐷) to (𝐷 ×_c 𝐶) by swapping all objects (swapf1 50379) and morphisms (swapf2 50381) .

Such functor is called a "swap functor" in https://arxiv.org/pdf/2302.07810 50381 or a "twist functor" in https://arxiv.org/pdf/2508.01886 50381, the latter of which finds its counterpart as "twisting map" in https://arxiv.org/pdf/2411.04102 50381 for tensor product of algebras. The "swap functor" or "twisting map" is often denoted as a small tau 𝜏 in literature. However, the term "twist functor" is defined differently in https://arxiv.org/pdf/1208.4046 50381 and thus not adopted here.

tpos I depends on more mathbox theorems, and thus are not adopted here. See dfswapf2 50368 for an alternate definition.

(Contributed by Zhi Wang, 7-Oct-2025.)

Assertion

Ref	Expression
df-swapf	⊢ swapF = (𝑐 ∈ V, 𝑑 ∈ V ↦ ⦋(𝑐 ×c 𝑑) / 𝑠⦌⦋(Base‘𝑠) / 𝑏⦌⦋(Hom ‘𝑠) / ℎ⦌⟨(𝑥 ∈ 𝑏 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓}))⟩)

Distinct variable group:   𝑏,𝑐,𝑑,ℎ,𝑠,𝑢,𝑣,𝑥,𝑓

Detailed syntax breakdown of Definition df-swapf

Step	Hyp	Ref	Expression
1		cswapf 50366	. 2 class swapF
2		vc	. . 3 setvar 𝑐
3		vd	. . 3 setvar 𝑑
4		cvv 3451	. . 3 class V
5		vs	. . . 4 setvar 𝑠
6	2	cv 1569	. . . . 5 class 𝑐
7	3	cv 1569	. . . . 5 class 𝑑
8		cxpc 18342	. . . . 5 class ×c
9	6, 7, 8	co 7420	. . . 4 class (𝑐 ×c 𝑑)
10		vb	. . . . 5 setvar 𝑏
11	5	cv 1569	. . . . . 6 class 𝑠
12		cbs 17387	. . . . . 6 class Base
13	11, 12	cfv 6538	. . . . 5 class (Base‘𝑠)
14		vh	. . . . . 6 setvar ℎ
15		chom 17439	. . . . . . 7 class Hom
16	11, 15	cfv 6538	. . . . . 6 class (Hom ‘𝑠)
17		vx	. . . . . . . 8 setvar 𝑥
18	10	cv 1569	. . . . . . . 8 class 𝑏
19	17	cv 1569	. . . . . . . . . . 11 class 𝑥
20	19	csn 4584	. . . . . . . . . 10 class {𝑥}
21	20	ccnv 5650	. . . . . . . . 9 class ◡{𝑥}
22	21	cuni 4867	. . . . . . . 8 class ∪ ◡{𝑥}
23	17, 18, 22	cmpt 5186	. . . . . . 7 class (𝑥 ∈ 𝑏 ↦ ∪ ◡{𝑥})
24		vu	. . . . . . . 8 setvar 𝑢
25		vv	. . . . . . . 8 setvar 𝑣
26		vf	. . . . . . . . 9 setvar 𝑓
27	24	cv 1569	. . . . . . . . . 10 class 𝑢
28	25	cv 1569	. . . . . . . . . 10 class 𝑣
29	14	cv 1569	. . . . . . . . . 10 class ℎ
30	27, 28, 29	co 7420	. . . . . . . . 9 class (𝑢ℎ𝑣)
31	26	cv 1569	. . . . . . . . . . . 12 class 𝑓
32	31	csn 4584	. . . . . . . . . . 11 class {𝑓}
33	32	ccnv 5650	. . . . . . . . . 10 class ◡{𝑓}
34	33	cuni 4867	. . . . . . . . 9 class ∪ ◡{𝑓}
35	26, 30, 34	cmpt 5186	. . . . . . . 8 class (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓})
36	24, 25, 18, 18, 35	cmpo 7422	. . . . . . 7 class (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓}))
37	23, 36	cop 4590	. . . . . 6 class ⟨(𝑥 ∈ 𝑏 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓}))⟩
38	14, 16, 37	csb 3847	. . . . 5 class ⦋(Hom ‘𝑠) / ℎ⦌⟨(𝑥 ∈ 𝑏 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓}))⟩
39	10, 13, 38	csb 3847	. . . 4 class ⦋(Base‘𝑠) / 𝑏⦌⦋(Hom ‘𝑠) / ℎ⦌⟨(𝑥 ∈ 𝑏 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓}))⟩
40	5, 9, 39	csb 3847	. . 3 class ⦋(𝑐 ×c 𝑑) / 𝑠⦌⦋(Base‘𝑠) / 𝑏⦌⦋(Hom ‘𝑠) / ℎ⦌⟨(𝑥 ∈ 𝑏 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓}))⟩
41	2, 3, 4, 4, 40	cmpo 7422	. 2 class (𝑐 ∈ V, 𝑑 ∈ V ↦ ⦋(𝑐 ×c 𝑑) / 𝑠⦌⦋(Base‘𝑠) / 𝑏⦌⦋(Hom ‘𝑠) / ℎ⦌⟨(𝑥 ∈ 𝑏 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓}))⟩)
42	1, 41	wceq 1570	1 wff swapF = (𝑐 ∈ V, 𝑑 ∈ V ↦ ⦋(𝑐 ×c 𝑑) / 𝑠⦌⦋(Base‘𝑠) / 𝑏⦌⦋(Hom ‘𝑠) / ℎ⦌⟨(𝑥 ∈ 𝑏 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓}))⟩)

This definition is used by:  dfswapf2  50368  swapfval  50369