Definition df-swapf

Description: Define the swap functor from ( C Xc. D ) to ( D Xc. C ) by swapping all objects ( swapf1 ) and morphisms ( swapf2 ) .

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

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

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

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

Detailed syntax breakdown

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