{ localUrl: '../page/reals_as_dedekind_cuts_form_a_field.html', arbitalUrl: 'https://arbital.com/p/reals_as_dedekind_cuts_form_a_field', rawJsonUrl: '../raw/53v.json', likeableId: '2954', likeableType: 'page', myLikeValue: '0', likeCount: '1', dislikeCount: '0', likeScore: '1', individualLikes: [ 'JoeZeng' ], pageId: 'reals_as_dedekind_cuts_form_a_field', edit: '4', editSummary: '', prevEdit: '3', currentEdit: '4', wasPublished: 'true', type: 'wiki', title: 'The reals (constructed as Dedekind cuts) form a field', clickbait: 'The reals are an archetypal example of a field, but if we are to construct them from simpler objects, we need to show that our construction does indeed have the right properties.', textLength: '2996', alias: 'reals_as_dedekind_cuts_form_a_field', externalUrl: '', sortChildrenBy: 'likes', hasVote: 'false', voteType: '', votesAnonymous: 'false', editCreatorId: 'DylanHendrickson', editCreatedAt: '2016-07-08 17:20:19', pageCreatorId: 'PatrickStevens', pageCreatedAt: '2016-07-05 22:03:55', seeDomainId: '0', editDomainId: 'AlexeiAndreev', submitToDomainId: '0', isAutosave: 'false', isSnapshot: 'false', isLiveEdit: 'true', isMinorEdit: 'false', indirectTeacher: 'false', todoCount: '9', isEditorComment: 'false', isApprovedComment: 'true', isResolved: 'false', snapshotText: '', anchorContext: '', anchorText: '', anchorOffset: '0', mergedInto: '', isDeleted: 'false', viewCount: '30', text: 'The real numbers, when [50g constructed as Dedekind cuts] over the [4zq rationals], form a [481 field].\n\nWe shall often write the one-sided [dedekind_cut Dedekind cut] $(A, B)$ %%note:Recall: "one-sided" means that $A$ has no greatest element.%% as simply $\\mathbf{A}$ (using bold face for Dedekind cuts); we can do this because if we already know $A$ then $B$ is completely determined.\nThis will make our notation less messy.\n\nThe field structure, together with the [total_order total ordering] on it, is as follows (where we write $\\mathbf{0}$ for the Dedekind cut $(\\{ r \\in \\mathbb{Q} \\mid r < 0\\}, \\{ r \\in \\mathbb{Q} \\mid r \\geq 0 \\})$): \n\n- $(A, B) + (C, D) = (A+C, B+D)$\n- $\\mathbf{A} \\leq \\mathbf{C}$ if and only if everything in $A$ lies in $C$.\n- Multiplication is somewhat complicated.\n - If $\\mathbf{0} \\leq \\mathbf{A}$, then $\\mathbf{A} \\times \\mathbf{C} = \\{ a c \\mid a \\in A, a > 0, c \\in C \\}$. [todo: we've missed out the complement in this notation, and can't put set-builder sets in boldface]\n - If $\\mathbf{A} < \\mathbf{0}$ and $\\mathbf{0} \\leq \\mathbf{C}$, then $\\mathbf{A} \\times \\mathbf{C} = \\{ a c \\mid a \\in A, c \\in C, c > 0 \\}$.\n - If $\\mathbf{A} < \\mathbf{0}$ and $\\mathbf{C} < \\mathbf{0}$, then $\\mathbf{A} \\times \\mathbf{C} = \\{\\} $ [todo: write down the form of the set]\n\nwhere $(A, B)$ is a one-sided [dedekind_cut Dedekind cut] (so that $A$ has no greatest element).\n\n(Here, the "set sum" $A+C$ is defined as "everything that can be made by adding one thing from $A$ to one thing from $C$": namely, $\\{ a+c \\mid a \\in A, c \\in C \\}$ in [-3lj]; and $A \\times C$ is similarly $\\{ a \\times c \\mid a \\in A, c \\in C \\}$.)\n\n# Proof\n\n## Well-definedness\n\nWe need to show firstly that these operations do in fact produce [dedekind_cut Dedekind cuts].\n\n### Addition\nFirstly, we need everything in $A+C$ to be less than everything in $B+D$.\nThis is true: if $a+c \\in A+C$, and $b+d \\in B+D$, then since $a < b$ and $c < d$, we have $a+c < b+d$.\n\nNext, we need $A+C$ and $B+D$ together to contain all the rationals.\nThis is true: [todo: this, it's quite boring]\n\nFinally, we need $(A+C, B+D)$ to be one-sided: that is, $A+C$ needs to have no top element, or equivalently, if $a+c \\in A+C$ then we can find a bigger $a' + c'$ in $A+C$.\nThis is also true: if $a+c$ is an element of $A+C$, then we can find an element $a'$ of $A$ which is bigger than $a$, and an element $c'$ of $C$ which is bigger than $C$ (since both $A$ and $C$ have no top elements, because the respective Dedekind cuts are one-sided); then $a' + c'$ is in $A+C$ and is bigger than $a+c$.\n\n### Multiplication\n[todo: this section]\n\n### Ordering\n[todo: this section]\n\n## Additive [3jb commutative] [3gd group structure]\n\n[todo: identity, associativity, inverse, commutativity]\n\n## [3gq Ring structure]\n\n[todo: multiplicative identity, associativity, distributivity]\n\n## [481 Field structure]\n\n[todo: inverses]\n\n## Ordering on the field\n\n[todo: a <= b implies a+c <= b+c, and 0 <= a, 0 <= b implies 0 <= ab]', 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: [ 'DylanHendrickson', 'PatrickStevens' ], childIds: [], parentIds: [ 'real_number_as_dedekind_cut' ], commentIds: [], questionIds: [], tagIds: [ 'work_in_progress_meta_tag', 'proof_meta_tag' ], relatedIds: [], markIds: [], explanations: [], learnMore: [], requirements: [ { id: '4829', parentId: 'algebraic_field', childId: 'reals_as_dedekind_cuts_form_a_field', type: 'requirement', creatorId: 'PatrickStevens', createdAt: '2016-07-05 18:20:51', level: '1', isStrong: 'false', everPublished: 'true' }, { id: '4830', parentId: 'real_number_as_dedekind_cut', childId: 'reals_as_dedekind_cuts_form_a_field', type: 'requirement', creatorId: 'PatrickStevens', createdAt: '2016-07-05 18:20:57', level: '1', isStrong: 'false', everPublished: 'true' } ], 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: '16235', pageId: 'reals_as_dedekind_cuts_form_a_field', userId: 'DylanHendrickson', edit: '4', type: 'newEdit', createdAt: '2016-07-08 17:20:19', auxPageId: '', oldSettingsValue: '', newSettingsValue: '' }, { likeableId: '0', likeableType: 'changeLog', myLikeValue: '0', likeCount: '0', dislikeCount: '0', likeScore: '0', individualLikes: [], id: '15968', pageId: 'reals_as_dedekind_cuts_form_a_field', userId: 'DylanHendrickson', edit: '3', type: 'newEdit', createdAt: '2016-07-07 14:01:42', auxPageId: '', oldSettingsValue: '', newSettingsValue: '' }, { likeableId: '0', likeableType: 'changeLog', myLikeValue: '0', likeCount: '0', dislikeCount: '0', likeScore: '0', individualLikes: [], id: '15469', pageId: 'reals_as_dedekind_cuts_form_a_field', userId: 'PatrickStevens', edit: '0', type: 'newTag', createdAt: '2016-07-05 22:04:18', auxPageId: 'work_in_progress_meta_tag', oldSettingsValue: '', newSettingsValue: '' }, { likeableId: '0', likeableType: 'changeLog', myLikeValue: '0', likeCount: '0', dislikeCount: '0', likeScore: '0', individualLikes: [], id: '15467', pageId: 'reals_as_dedekind_cuts_form_a_field', userId: 'PatrickStevens', edit: '0', type: 'newRequirement', createdAt: '2016-07-05 22:03:57', auxPageId: 'algebraic_field', oldSettingsValue: '', newSettingsValue: '' }, { likeableId: '0', likeableType: 'changeLog', myLikeValue: '0', likeCount: '0', dislikeCount: '0', likeScore: '0', individualLikes: [], id: '15468', pageId: 'reals_as_dedekind_cuts_form_a_field', userId: 'PatrickStevens', edit: '0', type: 'newRequirement', createdAt: '2016-07-05 22:03:57', auxPageId: 'real_number_as_dedekind_cut', oldSettingsValue: '', newSettingsValue: '' }, { likeableId: '0', likeableType: 'changeLog', myLikeValue: '0', likeCount: '0', dislikeCount: '0', likeScore: '0', individualLikes: [], id: '15465', pageId: 'reals_as_dedekind_cuts_form_a_field', userId: 'PatrickStevens', edit: '0', type: 'newParent', createdAt: '2016-07-05 22:03:56', auxPageId: 'real_number_as_dedekind_cut', oldSettingsValue: '', newSettingsValue: '' }, { likeableId: '0', likeableType: 'changeLog', myLikeValue: '0', likeCount: '0', dislikeCount: '0', likeScore: '0', individualLikes: [], id: '15466', pageId: 'reals_as_dedekind_cuts_form_a_field', userId: 'PatrickStevens', edit: '0', type: 'newTag', createdAt: '2016-07-05 22:03:56', auxPageId: 'proof_meta_tag', oldSettingsValue: '', newSettingsValue: '' }, { likeableId: '0', likeableType: 'changeLog', myLikeValue: '0', likeCount: '0', dislikeCount: '0', likeScore: '0', individualLikes: [], id: '15463', pageId: 'reals_as_dedekind_cuts_form_a_field', userId: 'PatrickStevens', edit: '1', type: 'newEdit', createdAt: '2016-07-05 22:03:55', auxPageId: '', oldSettingsValue: '', newSettingsValue: '' } ], feedSubmissions: [], searchStrings: {}, hasChildren: 'false', hasParents: 'true', redAliases: {}, improvementTagIds: [], nonMetaTagIds: [], todos: [], slowDownMap: 'null', speedUpMap: 'null', arcPageIds: 'null', contentRequests: {} }