Definition df-swapf 49222

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

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

tpos I depends on more mathbox theorems, and thus are not adopted here. See dfswapf2 49223 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 49221	. 2 class swapF
2		vc	. . 3 setvar 𝑐
3		vd	. . 3 setvar 𝑑
4		cvv 3444	. . 3 class V
5		vs	. . . 4 setvar 𝑠
6	2	cv 1539	. . . . 5 class 𝑐
7	3	cv 1539	. . . . 5 class 𝑑
8		cxpc 18105	. . . . 5 class ×c
9	6, 7, 8	co 7369	. . . 4 class (𝑐 ×c 𝑑)
10		vb	. . . . 5 setvar 𝑏
11	5	cv 1539	. . . . . 6 class 𝑠
12		cbs 17155	. . . . . 6 class Base
13	11, 12	cfv 6499	. . . . 5 class (Base‘𝑠)
14		vh	. . . . . 6 setvar ℎ
15		chom 17207	. . . . . . 7 class Hom
16	11, 15	cfv 6499	. . . . . 6 class (Hom ‘𝑠)
17		vx	. . . . . . . 8 setvar 𝑥
18	10	cv 1539	. . . . . . . 8 class 𝑏
19	17	cv 1539	. . . . . . . . . . 11 class 𝑥
20	19	csn 4585	. . . . . . . . . 10 class {𝑥}
21	20	ccnv 5630	. . . . . . . . 9 class ◡{𝑥}
22	21	cuni 4867	. . . . . . . 8 class ∪ ◡{𝑥}
23	17, 18, 22	cmpt 5183	. . . . . . 7 class (𝑥 ∈ 𝑏 ↦ ∪ ◡{𝑥})
24		vu	. . . . . . . 8 setvar 𝑢
25		vv	. . . . . . . 8 setvar 𝑣
26		vf	. . . . . . . . 9 setvar 𝑓
27	24	cv 1539	. . . . . . . . . 10 class 𝑢
28	25	cv 1539	. . . . . . . . . 10 class 𝑣
29	14	cv 1539	. . . . . . . . . 10 class ℎ
30	27, 28, 29	co 7369	. . . . . . . . 9 class (𝑢ℎ𝑣)
31	26	cv 1539	. . . . . . . . . . . 12 class 𝑓
32	31	csn 4585	. . . . . . . . . . 11 class {𝑓}
33	32	ccnv 5630	. . . . . . . . . 10 class ◡{𝑓}
34	33	cuni 4867	. . . . . . . . 9 class ∪ ◡{𝑓}
35	26, 30, 34	cmpt 5183	. . . . . . . 8 class (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓})
36	24, 25, 18, 18, 35	cmpo 7371	. . . . . . 7 class (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓}))
37	23, 36	cop 4591	. . . . . 6 class ⟨(𝑥 ∈ 𝑏 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓}))⟩
38	14, 16, 37	csb 3859	. . . . 5 class ⦋(Hom ‘𝑠) / ℎ⦌⟨(𝑥 ∈ 𝑏 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓}))⟩
39	10, 13, 38	csb 3859	. . . 4 class ⦋(Base‘𝑠) / 𝑏⦌⦋(Hom ‘𝑠) / ℎ⦌⟨(𝑥 ∈ 𝑏 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓}))⟩
40	5, 9, 39	csb 3859	. . 3 class ⦋(𝑐 ×c 𝑑) / 𝑠⦌⦋(Base‘𝑠) / 𝑏⦌⦋(Hom ‘𝑠) / ℎ⦌⟨(𝑥 ∈ 𝑏 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓}))⟩
41	2, 3, 4, 4, 40	cmpo 7371	. 2 class (𝑐 ∈ V, 𝑑 ∈ V ↦ ⦋(𝑐 ×c 𝑑) / 𝑠⦌⦋(Base‘𝑠) / 𝑏⦌⦋(Hom ‘𝑠) / ℎ⦌⟨(𝑥 ∈ 𝑏 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓}))⟩)
42	1, 41	wceq 1540	1 wff swapF = (𝑐 ∈ V, 𝑑 ∈ V ↦ ⦋(𝑐 ×c 𝑑) / 𝑠⦌⦋(Base‘𝑠) / 𝑏⦌⦋(Hom ‘𝑠) / ℎ⦌⟨(𝑥 ∈ 𝑏 ↦ ∪ ◡{𝑥}), (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (𝑓 ∈ (𝑢ℎ𝑣) ↦ ∪ ◡{𝑓}))⟩)

This definition is referenced by:  dfswapf2  49223  swapfval  49224