{ localUrl: '../page/product_is_unique_up_to_isomorphism.html', arbitalUrl: 'https://arbital.com/p/product_is_unique_up_to_isomorphism', rawJsonUrl: '../raw/60v.json', likeableId: '0', likeableType: 'page', myLikeValue: '0', likeCount: '0', dislikeCount: '0', likeScore: '0', individualLikes: [], pageId: 'product_is_unique_up_to_isomorphism', edit: '2', editSummary: '', prevEdit: '1', currentEdit: '2', wasPublished: 'true', type: 'wiki', title: 'Product is unique up to isomorphism', clickbait: 'If something satisfies the universal property of the product, then it is uniquely specified by that property, up to isomorphism.', textLength: '3749', alias: 'product_is_unique_up_to_isomorphism', externalUrl: '', sortChildrenBy: 'likes', hasVote: 'false', voteType: '', votesAnonymous: 'false', editCreatorId: 'PatrickStevens', editCreatedAt: '2016-08-28 14:53:27', pageCreatorId: 'PatrickStevens', pageCreatedAt: '2016-08-28 14:52:50', seeDomainId: '0', editDomainId: 'AlexeiAndreev', submitToDomainId: '0', isAutosave: 'false', isSnapshot: 'false', isLiveEdit: 'true', isMinorEdit: 'false', indirectTeacher: 'false', todoCount: '0', isEditorComment: 'false', isApprovedComment: 'true', isResolved: 'false', snapshotText: '', anchorContext: '', anchorText: '', anchorOffset: '0', mergedInto: '', isDeleted: 'false', viewCount: '44', text: '[summary: Here, we prove that the [-5zv] characterises objects uniquely up to [4f4]. That is, if two objects both satisfy the universal property of the product of $A$ and $B$, then they are isomorphic objects.]\n\nRecall the [-600] of the [5zv product]:\n\n> Given objects $A$ and $B$, we define the *product* to be the following collection of three objects, if it exists: $$A \\times B \\\\ \\pi_A: A \\times B \\to A \\\\ \\pi_B : A \\times B \\to B$$ with the requirement that for every object $X$ and every pair of maps $f_A: X \\to A, f_B: X \\to B$, there is a *unique* map $f: X \\to A \\times B$ such that $\\pi_A \\circ f = f_A$ and $\\pi_B \\circ f = f_B$.\n\nWe wish to show that if the collections $(R, \\pi_A, \\pi_B)$ and $(S, \\phi_A, \\phi_B)$ satisfy the above condition, then there is an [-4f4] between $R$ and $S$. %%note: I'd write $A \\times_1 B$ and $A \\times_2 B$ instead of $R$ and $S$, except that would be really unwieldy. Just remember that $R$ and $S$ are both standing for products of $A$ and $B$.%%\n\n# Proof\n\nThe proof follows a pattern which is standard for these things.\n\nSince $R$ is a product of $A$ and $B$, we can let $X = S$ in the universal property to obtain:\n\n> For every pair of maps $f_A: S \\to A, f_B: S \\to B$ there is a unique map $f: S \\to R$ such that $\\pi_A \\circ f = f_A$ and $\\pi_B \\circ f = f_B$.\n\nNow let $f_A = \\phi_A, f_B = \\phi_B$:\n\n> There is a unique map $\\phi: S \\to R$ such that $\\pi_A \\circ \\phi = \\phi_A$ and $\\pi_B \\circ \\phi = \\phi_B$.\n\nDoing the same again but swapping $R$ for $S$ and $\\phi$ for $\\pi$ (basically starting over with the line "Since $S$ is a product of $A$ and $B$, we can let $X = R$…"), we obtain:\n\n> There is a unique map $\\pi: R \\to S$ such that $\\phi_A \\circ \\pi = \\pi_A$ and $\\phi_B \\circ \\pi = \\pi_B$.\n\nNow, $\\pi \\circ \\phi: S \\to S$ is a map which we wish to be the identity on $S$; that would get us halfway to the answer, because it would tell us that $\\pi$ is left-inverse to $\\phi$.\n\nBut we can use the universal property of $S$ once more, this time looking at maps into $S$:\n\n> For every pair of maps $f_A: S \\to A, f_B: S \\to B$ there is a unique map $f: S \\to S$ such that $\\phi_A \\circ f = f_A$ and $\\phi_B \\circ f = f_B$.\n\nLetting $f_A = \\phi_A$ and $f_B = \\phi_B$, we obtain:\n\n> There is a unique map $f: S \\to S$ such that $\\phi_A \\circ f = \\phi_A$ and $\\phi_B \\circ f = \\phi_B$.\n\nBut I claim that both the identity $1_S$ and also $\\pi \\circ \\phi$ satisfy the same property as $f$, and hence they're equal by the uniqueness of $f$.\nIndeed, \n\n- $1_S$ certainly satisfies the property, since that would just say that $\\phi_A = \\phi_A$ and $\\phi_B = \\phi_B$;\n- $\\pi \\circ \\phi$ satisfies the property, since we already found that $\\phi_A \\circ \\pi = \\pi_A$ and that $\\phi_B \\circ \\pi = \\pi_B$.\n\nTherefore $\\pi$ is left-inverse to $\\phi$.\n\nNow to complete the proof, we just need to repeat *exactly* the same steps but with $(R, \\pi_A, \\pi_B)$ and $(S, \\phi_A, \\phi_B)$ interchanged throughout.\nThe outcome is that $\\phi$ is left-inverse to $\\pi$.\n\nHence $\\pi$ and $\\phi$ are genuinely inverse to each other, so they are both isomorphisms $R \\to S$ and $S \\to R$ respectively.\n\n# The characterisation is not unique\n\nTo show that we can't do better than "characterised up to isomorphism", we show that the product is not characterised *uniquely*.\nIndeed, if $(A \\times B, \\pi_A, \\pi_B)$ is a product of $A$ and $B$, then so is $(B \\times A, \\pi'_A, \\pi'_B)$, where $\\pi'_A(b, a) = a$ and $\\pi'_B(b, a) = b$.\n(You can check that this does satisfy the universal property for a product of $A$ and $B$.)\n\nNotice, though, that $A \\times B$ and $B \\times A$ are isomorphic as guaranteed by the theorem.\nThe isomorphism is the map $A \\times B \\to B \\times A$ given by $(a,b) \\mapsto (b,a)$.', metaText: '', isTextLoaded: 'true', isSubscribedToDiscussion: 'false', isSubscribedToUser: 'false', isSubscribedAsMaintainer: 'false', discussionSubscriberCount: '1', maintainerCount: '1', userSubscriberCount: '0', lastVisit: '', hasDraft: 'false', votes: [], voteSummary: 'null', muVoteSummary: '0', voteScaling: '0', currentUserVote: '-2', voteCount: '0', lockedVoteType: '', maxEditEver: '0', redLinkCount: '0', lockedBy: '', lockedUntil: '', nextPageId: '', prevPageId: '', usedAsMastery: 'false', proposalEditNum: '0', permissions: { edit: { has: 'false', reason: 'You don't have domain permission to edit this page' }, proposeEdit: { has: 'true', reason: '' }, delete: { has: 'false', reason: 'You don't have domain permission to delete this page' }, comment: { has: 'false', reason: 'You can't comment in this domain because you are not a member' }, proposeComment: { has: 'true', reason: '' } }, summaries: {}, creatorIds: [ 'PatrickStevens' ], childIds: [], parentIds: [ 'product_universal_property' ], commentIds: [], questionIds: [], tagIds: [ 'proof_meta_tag' ], relatedIds: [], markIds: [], explanations: [], learnMore: [], requirements: [], subjects: [], lenses: [], lensParentId: '', pathPages: [], learnMoreTaughtMap: {}, learnMoreCoveredMap: {}, learnMoreRequiredMap: {}, editHistory: {}, domainSubmissions: {}, answers: [], answerCount: '0', commentCount: '0', newCommentCount: '0', linkedMarkCount: '0', changeLogs: [ { likeableId: '0', likeableType: 'changeLog', myLikeValue: '0', likeCount: '0', dislikeCount: '0', likeScore: '0', individualLikes: [], id: '19365', pageId: 'product_is_unique_up_to_isomorphism', userId: 'PatrickStevens', edit: '0', type: 'newTag', createdAt: '2016-08-28 14:54:07', auxPageId: 'proof_meta_tag', oldSettingsValue: '', newSettingsValue: '' }, { likeableId: '0', likeableType: 'changeLog', myLikeValue: '0', likeCount: '0', dislikeCount: '0', likeScore: '0', individualLikes: [], id: '19364', pageId: 'product_is_unique_up_to_isomorphism', userId: 'PatrickStevens', edit: '2', type: 'newEdit', createdAt: '2016-08-28 14:53:27', auxPageId: '', oldSettingsValue: '', newSettingsValue: '' }, { likeableId: '0', likeableType: 'changeLog', myLikeValue: '0', likeCount: '0', dislikeCount: '0', likeScore: '0', individualLikes: [], id: '19363', pageId: 'product_is_unique_up_to_isomorphism', userId: 'PatrickStevens', edit: '0', type: 'newParent', createdAt: '2016-08-28 14:52:51', auxPageId: 'product_universal_property', oldSettingsValue: '', newSettingsValue: '' }, { likeableId: '0', likeableType: 'changeLog', myLikeValue: '0', likeCount: '0', dislikeCount: '0', likeScore: '0', individualLikes: [], id: '19361', pageId: 'product_is_unique_up_to_isomorphism', userId: 'PatrickStevens', edit: '1', type: 'newEdit', createdAt: '2016-08-28 14:52:50', auxPageId: '', oldSettingsValue: '', newSettingsValue: '' } ], feedSubmissions: [], searchStrings: {}, hasChildren: 'false', hasParents: 'true', redAliases: {}, improvementTagIds: [], nonMetaTagIds: [], todos: [], slowDownMap: 'null', speedUpMap: 'null', arcPageIds: 'null', contentRequests: {} }