Come si dimostra l’iniettività e suriettività nella costruzione della funzione di Schröder-Bernstein?

La dimostrazione della funzione di Schröder-Bernstein si fonda su due proprietà cruciali: l’iniettività e la suriettività della funzione costruita sbFun f g, che unisce due funzioni iniettive f e g tra insiemi α e β. Per comprenderne la natura, consideriamo innanzitutto l’insieme A, definito come una unione crescente di insiemi sbAux f g n, e la funzione h, che coincide con f su A e con l’inversa di g fuori da A.

Rimane il caso in cui entrambi gli elementi siano fuori da A. Qui la funzione h coincide con g⁻¹, e quindi h(x₁) = h(x₂) implica g⁻¹(x₁) = g⁻¹(x₂). Applicando g ad entrambi i membri si conclude che x₁ = x₂, consolidando l’iniettività di h.

Un aspetto importante nella formalizzazione di questa dimostrazione in Lean è l’uso di tattiche specifiche. La tattica set consente di abbreviare espressioni complesse con nomi definiti, come A per sbSet f g e h per sbFun f g, rendendo il codice più leggibile. Tuttavia, ciò richiede spesso di espandere esplicitamente tali definizioni con regole di riscrittura per facilitare manipolazioni successive. Di particolare rilevanza è la tattica wlog (without loss of generality), che incapsula il ragionamento di simmetria, consentendo di ridurre i casi da analizzare.

Per quanto riguarda la suriettività, il ragionamento si concentra sull’elemento arbitrario y ∈ β. Si considerano due casi in base alla posizione di g(y) rispetto all’insieme A. Se g(y) ∈ A, allora, poiché A è costruito come un’unione crescente di sbAux, g(y) appartiene a qualche “anello” Sn+1, il quale, per definizione, è immagine di un elemento f(x) con x in Sn. L’iniettività di g permette di risalire a f(x) = y. Nel caso opposto, se g(y) è fuori da A, si dimostra immediatamente che h(g(y)) = y, concludendo la suriettività.

La costruzione complessiva della funzione h, detta sbFun f g, soddisfa quindi sia l’iniettività che la suriettività, mostrando l’esistenza di una biiezione tra α e β a partire da due funzioni iniettive tra i due insiemi, in accordo con il teorema di Schröder-Bernstein.

È fondamentale notare che, nella dimostrazione, l’uso di funzioni inverse parziali (invFun g x) e le proprietà di iniettività garantiscono l’unicità e l’esistenza degli elementi richiesti, elementi che emergono naturalmente dal formalismo usato in Lean. La correttezza del ragionamento dipende strettamente dal modo in cui sono definiti gli insiemi A e gli anelli sbAux, e dal trattamento accurato dei casi limite.

Oltre al testo formale, è importante che il lettore comprenda la filosofia sottesa: la funzione sbFun costruisce una biiezione combinando l’azione di f su una parte dell’insieme e l’azione inversa di g sull’altra, modulando queste due parti tramite l’insieme A, che isola gli elementi raggiunti da f ma non da g. Questo ragionamento è un esempio emblematico di come strutture matematiche complesse possano essere costruite da componenti più semplici, sfruttando proprietà di iniettività e suriettività.

L’approccio utilizzato enfatizza la capacità di scomporre insiemi e funzioni in componenti gestibili, facilitando non solo la dimostrazione formale, ma anche una comprensione concettuale più profonda del teorema. È altresì essenziale considerare che, nel contesto di Lean, le definizioni devono essere date in modo che la macchina possa manipolarle efficacemente, riflettendo il delicato equilibrio tra astrazione matematica e formalizzazione computazionale.

Quali proprietà definiscono il dominio euclideo nei numeri gaussiani?

Partendo da questa e da altre proprietà analoghe, si può costruire formalmente l’istanza dei numeri gaussiani come dominio euclideo, utilizzando le funzioni quoziente e resto definite opportunamente. La definizione di dominio euclideo adottata in questo contesto è più generale di quella standard: si basa su una misura ben fondata, cioè una funzione che assegna a ogni elemento un numero naturale in modo tale che ogni catena decrescente di elementi termini necessariamente. La norma, composita con l’assoluto naturale, rappresenta un esempio di tale misura. Due teoremi fondamentali che supportano questa costruzione sono quelli che garantiscono la diminuzione della norma del resto e la non diminuzione della norma del prodotto, fornendo così gli strumenti essenziali per il controllo degli algoritmi di divisione e resto.

Un risultato immediato di questa struttura è la coincidenza, nei numeri gaussiani, dei concetti di elemento primo e elemento irriducibile. Questa equivalenza è significativa perché, in molti anelli, questi concetti possono divergere. Nei numeri gaussiani, invece, ogni elemento irriducibile è anche primo, un fatto che facilita enormemente lo studio della fattorizzazione e la comprensione della struttura aritmetica di questo anello.

Passando a un livello più astratto, si osserva come la costruzione delle strutture algebriche in sistemi formali come Lean si basi su una gerarchia di classi. Alla base si trovano classi che semplicemente trasportano dati, come l’elemento neutro uno, senza alcuna proprietà associata. Ad esempio, la classe One1 definisce un tipo dotato di un elemento "uno", ma non impone alcuna legge su di esso. Questo approccio permette una grande modularità e flessibilità nella definizione di strutture più complesse.

L’uso di classi consente inoltre di sfruttare la risoluzione automatica delle istanze, facilitando così l’assemblaggio di strutture più complesse a partire da quelle più semplici. Ad esempio, la classe Semigroup definisce una struttura dotata di un’operazione binaria (denominata qui "diamond") che soddisfa la proprietà associativa. Questo è il passo iniziale verso strutture più ricche come anelli e campi, che si ottengono estendendo gerarchicamente le definizioni di base.

Oltre alla mera definizione tecnica, è importante cogliere che l’approccio attraverso le norme e la struttura dei numeri gaussiani offre una finestra sul modo in cui le proprietà algebriche e aritmetiche possono essere sistematizzate e formalizzate in modo rigoroso. La misura ben fondata della norma consente infatti di garantire la terminazione di processi di divisione e fattorizzazione, un aspetto fondamentale per dimostrare proprietà come la primalità o irriducibilità.

Infine, per una comprensione profonda di questi argomenti, è indispensabile considerare come le strutture algebriche si intreccino con concetti computazionali di efficienza e terminazione. La formalizzazione delle gerarchie di classi e l’uso di funzioni misura permettono non solo di ragionare sulle proprietà matematiche astratte, ma anche di implementare algoritmi certi e verificabili che riflettano fedelmente tali proprietà.