Definition df-swapf 49011

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

Such functor is called a "swap functor" in https://arxiv.org/pdf/2302.07810 49025 or a "twist functor" in https://arxiv.org/pdf/2508.01886 49025, the latter of which finds its counterpart as "twisting map" in https://arxiv.org/pdf/2411.04102 49025 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 49025 and thus not adopted here.

tpos I depends on more mathbox theorems, and thus are not adopted here. See dfswapf2 49012 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 49010	. 2 class swapF
2		vc	. . 3 setvar 𝑐
3		vd	. . 3 setvar 𝑑
4		cvv 3463	. . 3 class V
5		vs	. . . 4 setvar 𝑠
6	2	cv 1538	. . . . 5 class 𝑐
7	3	cv 1538	. . . . 5 class 𝑑
8		cxpc 18184	. . . . 5 class ×c
9	6, 7, 8	co 7413	. . . 4 class (𝑐 ×c 𝑑)
10		vb	. . . . 5 setvar 𝑏
11	5	cv 1538	. . . . . 6 class 𝑠
12		cbs 17230	. . . . . 6 class Base
13	11, 12	cfv 6541	. . . . 5 class (Base‘𝑠)
14		vh	. . . . . 6 setvar ℎ
15		chom 17285	. . . . . . 7 class Hom
16	11, 15	cfv 6541	. . . . . 6 class (Hom ‘𝑠)
17		vx	. . . . . . . 8 setvar 𝑥
18	10	cv 1538	. . . . . . . 8 class 𝑏
19	17	cv 1538	. . . . . . . . . . 11 class 𝑥
20	19	csn 4606	. . . . . . . . . 10 class {𝑥}
21	20	ccnv 5664	. . . . . . . . 9 class ◡{𝑥}
22	21	cuni 4887	. . . . . . . 8 class ∪ ◡{𝑥}
23	17, 18, 22	cmpt 5205	. . . . . . 7 class (𝑥 ∈ 𝑏 ↦ ∪ ◡{𝑥})
24		vu	. . . . . . . 8 setvar 𝑢
25		vv	. . . . . . . 8 setvar 𝑣
26		vf	. . . . . . . . 9 setvar 𝑓
27	24	cv 1538	. . . . . . . . . 10 class 𝑢
28	25	cv 1538	. . . . . . . . . 10 class 𝑣
29	14	cv 1538	. . . . . . . . . 10 class ℎ
30	27, 28, 29	co 7413	. . . . . . . . 9 class (𝑢ℎ𝑣)
31	26	cv 1538	. . . . . . . . . . . 12 class 𝑓
32	31	csn 4606	. . . . . . . . . . 11 class {𝑓}
33	32	ccnv 5664	. . . . . . . . . 10 class ◡{𝑓}
34	33	cuni 4887	. . . . . . . . 9 class ∪ ◡{𝑓}
35	26, 30, 34	cmpt 5205	. . . . . . . 8 class (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓})
36	24, 25, 18, 18, 35	cmpo 7415	. . . . . . 7 class (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓}))
37	23, 36	cop 4612	. . . . . 6 class ⟨(𝑥 ∈ 𝑏 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓}))⟩
38	14, 16, 37	csb 3879	. . . . 5 class ⦋(Hom ‘𝑠) / ℎ⦌⟨(𝑥 ∈ 𝑏 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓}))⟩
39	10, 13, 38	csb 3879	. . . 4 class ⦋(Base‘𝑠) / 𝑏⦌⦋(Hom ‘𝑠) / ℎ⦌⟨(𝑥 ∈ 𝑏 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓}))⟩
40	5, 9, 39	csb 3879	. . 3 class ⦋(𝑐 ×c 𝑑) / 𝑠⦌⦋(Base‘𝑠) / 𝑏⦌⦋(Hom ‘𝑠) / ℎ⦌⟨(𝑥 ∈ 𝑏 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓}))⟩
41	2, 3, 4, 4, 40	cmpo 7415	. 2 class (𝑐 ∈ V, 𝑑 ∈ V ↦ ⦋(𝑐 ×c 𝑑) / 𝑠⦌⦋(Base‘𝑠) / 𝑏⦌⦋(Hom ‘𝑠) / ℎ⦌⟨(𝑥 ∈ 𝑏 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓}))⟩)
42	1, 41	wceq 1539	1 wff swapF = (𝑐 ∈ V, 𝑑 ∈ V ↦ ⦋(𝑐 ×c 𝑑) / 𝑠⦌⦋(Base‘𝑠) / 𝑏⦌⦋(Hom ‘𝑠) / ℎ⦌⟨(𝑥 ∈ 𝑏 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓}))⟩)

This definition is referenced by:  dfswapf2  49012  swapfval  49013