Swap functors, transposed curry functors, post-composition functors, and pre-composition functors #5051
Conversation
… [fix] algebraic scalars map -> algebra scalars map
This reverts commit 5fb5705.
set.mm
Outdated
| FUAUBUCVGFJFVFFUDUEUFTUGUHUJUIUKULT $. | ||
|
|
||
| $( Alternate definition of ` tpos ` . The second half of the right hand | ||
| side could be applied ~ ressn and become ` ( F |`` { (/) } ) ` |
There was a problem hiding this comment.
| side could be applied ~ ressn and become ` ( F |`` { (/) } ) ` | |
| side could apply ~ ressn and become ` ( F |`` { (/) } ) ` |
There was a problem hiding this comment.
| $( The transposition restricted to a converse is the transposition of the | ||
| restricted class, with the empty set removed from the domain. | ||
| (Contributed by Zhi Wang, 6-Oct-2025.) $) | ||
| tposrescnv $p |- ( tpos F |` `' R ) | ||
| = ( F o. ( x e. `' dom ( F |` R ) |-> U. `' { x } ) ) $= |
There was a problem hiding this comment.
(note: the RHS is a more useful form of ( tpos ( F |` R ) ) |` ( _V \ { (/) } ) by df-tpos)
There was a problem hiding this comment.
Added the comment in fd0c62ea8c2fbb634a0dfd59d786a84f8bb05289
| ${ | ||
| elxpcbasex1.t $e |- T = ( C Xc. D ) $. | ||
| elxpcbasex1.b $e |- B = ( Base ` T ) $. | ||
| elxpcbasex1.x $e |- ( ph -> X e. B ) $. | ||
| $( A non-empty base set of the product category indicates the existence of | ||
| the first factor of the product category. (Contributed by Zhi Wang, | ||
| 8-Oct-2025.) $) | ||
| elxpcbasex1 $p |- ( ph -> C e. _V ) $= | ||
| ( c1st cfv cbs cxp wcel eqid xpcbas eqtr4i eleqtrdi xp1st syl elfvexd ) A | ||
| FJKZLCAFCLKZDLKZMZNUBUCNAFBUEIBELKUEHCDEUCUDGUCOUDOPQRFUCUDSTUA $. | ||
|
|
||
| $( A non-empty base set of the product category indicates the existence of | ||
| the second factor of the product category. (Contributed by Zhi Wang, | ||
| 8-Oct-2025.) $) | ||
| elxpcbasex2 $p |- ( ph -> D e. _V ) $= | ||
| ( c2nd cfv cbs cxp wcel eqid xpcbas eqtr4i eleqtrdi xp2nd syl elfvexd ) A | ||
| FJKZLDAFCLKZDLKZMZNUBUDNAFBUEIBELKUEHCDEUCUDGUCOUDOPQRFUCUDSTUA $. | ||
| $} |
There was a problem hiding this comment.
if reldmxpc was proven a la reldmress, then these might be shortenable by elbasov and strov2rcl
| $( The transposed curry functor of a functor ` F : D X. C --> E ` is a | ||
| functor tposcurry ` ( F ) : C --> ( D --> E ) ` . (Contributed by Zhi | ||
| Wang, 9-Oct-2025.) $) |
There was a problem hiding this comment.
note: the intended reading of this is:
...is a functor tposcurry( F ) : C --> ( D --> E )
There was a problem hiding this comment.
Yes. I would like to put tposcurry into the "`" statement but I have not defined it yet. (Maybe will never define it per least definition rule...)
set.mm
Outdated
| WAUSUNZAWFLVNURWGLVTWAUSUNZUTAKVKLVNHWHWIUTAVEVPVFVQIABCDEFJKMNRSVAABCDEF | ||
| JLMNRTVAUTVBVC $. | ||
|
|
||
| $( Alternate proof for ~ swapf2f1oa . (Contributed by Zhi Wang, |
There was a problem hiding this comment.
Note: "Alternate proof of" is more common than "Alternate proof for" (216 vs 11), however, this doesn't error, so I guess it may be fine?
There was a problem hiding this comment.
|| many of the latter of which are mine ||
I am keeping others as is but fixing mine. e4c20f4
4 participants
No description provided.