Konstruksjon av relative heltall

I matematikk er konstruksjonen av den abeliske gruppen av relative heltall et standardeksempel på symmetrisering av en kommutativ monoid , i dette tilfellet: monoid av naturlige heltall . ${\ displaystyle (\ mathbb {Z}, +)}$ ${\ displaystyle (\ mathbb {N}, +)}$

Den tilleggsstrukturen til ring og ordrerelasjon blir bare tegnet .

Bygging av settet Z

Vi vet allerede at settet med naturlige heltall, utstyrt med den interne tilleggsloven, er en kommutativ monoid; så vårt mål er ganske enkelt å legge til et motsatt ( symmetrisk element for tillegget) for hvert heltall som ikke er null. Det er ikke snakk om plutselig å legge til et element, det er også nødvendig å definere tillegget. $\ mathbb {N}$

Dette er grunnen til at vi vil starte fra den naive forestillingen om et relativt heltall , som vi antar å være kjent, for å konstruere det tilsvarende matematiske objektet. Hvis vi ønsker å definere med naturlige tall, vil vi se det som , eller som , eller ...; kort sagt, vi vil se det som forskjellen mellom to naturlige tall. Dette utgjør en vanskelighet, fordi vi på den ene siden ser at skrivingen ikke er unik, og på den andre siden at den innebærer en operasjon, subtraksjonen, som ikke alltid har en betydning med de naturlige tallene. $-2$ $0-2$ $5-7$

Vi vil derfor vurdere par av heltall, av formen , og vurdere at paret tilsvarer det naive relative heltallet ; og da vi har sett at det ikke er rimelig å ta relative heltall som et sett, vil vi gruppere parene som tilsvarer det samme naive relative heltallet. $(n_ {1}, n_ {2})$ $(n_ {1}, n_ {2})$ $n_ {1} -n_ {2}$ ${\ displaystyle \ mathbb {N} \ times \ mathbb {N}}$

For dette vil vi sette ut en ekvivalensrelasjon , av: . Intuitivt skriver vi at to par er like hvis vi trekker det andre heltallet fra paret til det første, får vi det samme relative heltallet. Men vi bruker bare summen til å definere , så denne definisjonen bruker ikke et naivt objekt. ${\ displaystyle \ mathbb {N} \ times \ mathbb {N}}$ $R$ $(n_ {1}, n_ {2}) R (n_ {1} ', n_ {2}') \ Leftrightarrow n_ {1} + n_ {2} '= n_ {1}' + n_ {2}$ $R$

Ekvivalensforhold er laget for kvotient ; vi definerer derfor: ${\ displaystyle \ mathbb {Z} = (\ mathbb {N} \ times \ mathbb {N}) / R}$

Definisjon av gruppestrukturen

Vi har nå settet med relative heltall; det gjenstår å definere tillegg på sistnevnte: for det har vi bare definisjonen på heltallene; vi vil derfor først definere en operasjon på par av heltall, og da den vil være kompatibel med relasjonen , vil den gi en operasjon på relative heltall. $R$

Vi definerer summen av to par heltall som følger :; denne operasjonen er kommutativ, assosiativ og av nøytralt element på parene av heltall; det går tydelig over til kvotienten, for å gi en kommutativ monoid struktur, hvis nøytrale er klassen av , bestående av par . $(n_ {1}, n_ {2}) + (n_ {1} ', n_ {2}') = (n_ {1} + n_ {1} ', n_ {2} + n_ {2}')$ $(0,0)$ $\ mathbb {Z}$ $(0,0)$ $(n, n)$

Det gjenstår derfor bare å finne et motsats til enhver relativ helhet; men dette er øyeblikkelig: hvis representerer et relativt heltall i parene av heltall, er lik derfor ekvivalent med . Ekvivalensklassen av er derfor i motsetning til ekvivalensklassen av . $(n_ {1}, n_ {2})$ ${\ displaystyle (n_ {1}, n_ {2}) + (n_ {2}, n_ {1})}$ $(n_ {1} + n_ {2}, n_ {1} + n_ {2})$ $(0,0)$ $(n_ {2}, n_ {1})$ $(n_ {1}, n_ {2})$

Bekreftelse av utvidelsen

Vi vil vise at det er en injiserende monoid morfisme fra i ; på denne måten kan vi se et naturlig heltall som et spesielt tilfelle av et relativt heltall. Nok en gang er det den naive ideen om relative heltall som viser vei. $\ mathbb {N}$ $\ mathbb {Z}$

La være et naturlig tall; vi forbinder det med klassen til paret . Vi ser da at: $ikke$ $(n, 0)$

${\ displaystyle 0}$ har for bilde klassen av , derfor av relative heltall; $(0,0)$ ${\ displaystyle 0}$
$n + n '$ , summen av to heltall, har for bildet klassen av , som er summen av klassene av og . $(n + n ', 0)$ $(n, 0)$ $(n ', 0)$

Videre kan vi tydelig se at denne applikasjonen er injiserende, siden det å spørre om klassene av og være like er akkurat det . $(n, 0)$ $(n ', 0)$ $n = n '$

Forenklet skriving av elementene i Z

La oss betegne ( n ; m ) klassen til et par naturlige heltall ( n , m ). Det er en av følgende tre typer:

( d ; 0) hvis n > m med n = m + d og d ikke null
(0; d ) hvis n < m med n + d = m og d ikke null
(0; 0) hvis n = m

Nå er klassesettet ( d ; 0) isomorft til ; vi betegner derfor disse klassene i forenklet form d . $\ mathbb {N}$

På den annen side, for d ikke null, er klassene ( d ; 0) og (0; d ) motsatte. Faktisk ( d ; 0) + (0; d ) = ( d ; d ) = (0; 0). Vi betegner derfor klassene (0; d ) i forenklet form (- d ).

Helheten går deretter tilbake til sin mer klassiske form . $\ mathbb {Z}$ ${\ displaystyle \ mathbb {N} \ cup \ {(- d) \ mid d \ in \ mathbb {N} ^ {*} \}}$

Definisjon av multiplikasjon

Vi kan da definere multiplikasjon som følger: (henter alltid inspirasjon fra analogien med naive relative heltall). $(n_ {1}, n_ {2}) \ times (m_ {1}, m_ {2}) = (n_ {1} m_ {1} + n_ {2} m_ {2}, n_ {1} m_ { 2} + m_ {1} n_ {2})$

Denne operasjonen satt til er assosiativ, kommutativ, har et nøytralt element (1, 0) og er distribuerende for det tidligere definerte tillegget. Videre er det kompatibelt med ekvivalensforholdet. Ved å passere til kvotienten gir det en enhetlig ringstruktur. ${\ displaystyle \ mathbb {N} \ times \ mathbb {N}}$ $\ mathbb {Z}$

Likestillinger

{\ displaystyle (d, 0) \ times (d ', 0) = (dd', 0)}

{\ displaystyle (d, 0) \ times (0, d ') = (0, dd')}

{\ displaystyle (0, d) \ times (0, d ') = (dd', 0)}

tillate skrifter

{\ displaystyle d \ times d '= dd'}

d \ times (-d ') = (- dd')

(-d) \ times (-d ') = dd'

som gjør det mulig å demonstrere at ringen også er intakt.

Definisjon av ordrerelasjonen

Vi kan enkelt sjekke:

{\ displaystyle \ mathbb {N} \ cup (- \ mathbb {N}) = \ mathbb {Z} {\ text {et}} \ mathbb {N} \ cap (- \ mathbb {N}) = \ {0 \}.}

Dette er knyttet til det faktum at en del av stabil ved sum og produkt, tillater oss å vise at binær relasjon på definert ved: $\ mathbb {N}$ $\ mathbb {Z}$ $\ mathbb {Z}$

{\ displaystyle x \ leqslant y \ iff yx \ in \ mathbb {N}}

er en total orden forhold på hvilken strekker seg det av , og at det er kompatibelt med tillegg så vel som multiplikasjon med en positive element . Det kan også trekkes ut fra at en ikke-tom underskjæring (resp. Økt) del har et minimum (resp. A maksimum). $\ mathbb {Z}$ $\ mathbb {N}$ $\ mathbb {Z}$

Alternative konstruksjoner

I teoretisk informatikk brukes andre metoder for å konstruere relative heltall av verktøyene for automatisk å bevise teoremer og omskrive termer . Relative heltall er representert som algebraiske termer konstruert fra noen grunnleggende operasjoner (f.eks. Null , succ , pred ...) og muligens fra naturlige heltall som antas å være tidligere konstruert i henhold til Peano-metoden.

Det er minst ti slike konstruksjoner av relative heltall. Disse konstruksjonene er forskjellige på flere punkter: antall grunnleggende operasjoner som brukes; antallet (vanligvis mellom 0 og 2) og typen argumenter som aksepteres av disse operasjonene; hvorvidt naturlige tall blir brukt som argumenter for noen av disse operasjonene; det faktum at disse operasjonene er gratis eller ikke, det vil si at det samme relative tallet tilsvarer en enkelt eller flere algebraiske termer.

Teknikken med å konstruere relative heltall av symmetrization presentert ovenfor også tilsvarer det spesielle tilfelle hvor det finnes bare ett til og med utgangspunkt operasjon som tar som argumenter to naturlige heltall og og returnerer en relativ heltall (lik ). Denne operasjonen er ikke gratis siden det relative heltallet 0 kan skrives jevnt (0,0), eller til og med (1,1), eller til og med (2,2), etc. Denne konstruksjonsteknikken brukes av bevisassistenten Isabelle / HOL ; mange andre verktøy bruker imidlertid forskjellige konstruksjonsteknikker, spesielt de med gratis konstruktører som er enklere og implementerer mer effektivt i datamaskiner. $(x, y)$ $x$ $y$ $xy$

Bibliografi

(i) Hubert Garavel (2017). “ On the Most Suitable Axiomatization of Signed Integers ” i etterbehandling av 23. internasjonale workshop om algebraisk utviklingsteknikk (WADT'2016) Forelesningsnotater i datalogi 10644 : 120-134 s., Springer ( DOI : 10.1007 / 978-3 -319-72044-9_9 ).

Relaterte artikler