Come si comportano immagini e controimmagini rispetto a unione, intersezione e iniezioni nelle funzioni

Nel contesto della teoria degli insiemi e delle funzioni, un ruolo fondamentale è giocato dalle operazioni di immagine e controimmagine di un insieme tramite una funzione. Dato un insieme $s$ di elementi di tipo $\alpha$ e una funzione $f : \alpha \to \beta$, l'immagine $f''s$ è definita come l'insieme di tutti gli elementi $y$ di tipo $\beta$ tali che esiste $x \in s$ con $f(x) = y$. Viceversa, la controimmagine $f^{ -1}(p)$ di un insieme $p \subseteq \beta$ è l'insieme di tutti $x \in \alpha$ per cui $f(x) \in p$.

Queste identità sono conseguenze dirette della natura delle definizioni e possono essere dimostrate tramite argomenti di appartenenza e decomposizione di quantificatori.

Tuttavia, la situazione si complica con le intersezioni di immagini, che in generale soddisfano solo una disuguaglianza:

e non necessariamente l'uguaglianza. Questo accade perché l'immagine può perdere informazioni di unicità, mentre la controimmagine mantiene la struttura della funzione in modo più fedele. La differenza tra immagine e controimmagine si manifesta profondamente in presenza di funzioni iniettive o suriettive, dove si osservano varie inclusioni e uguaglianze che riflettono queste proprietà. Per esempio, se $f$ è iniettiva, allora

mentre se è suriettiva

Questi risultati sono esempi concreti della connessione di Galois tra immagine e controimmagine, che sono funzioni monotone tra insiemi parzialmente ordinati secondo l'inclusione.

Estendendo queste proprietà agli indici arbitrari, si ottengono formule analoghe per unioni e intersezioni indicizzate, ossia:

e analoghe inclusioni per le intersezioni di immagini.

Inoltre, la nozione di iniezione relativa a un sottoinsieme, definita tramite il predicato $\text{InjOn } f \, s$, sottolinea come l'iniettività possa essere considerata localmente su un dominio ristretto, permettendo un trattamento più fine delle funzioni che non sono necessariamente iniettive sull'intero dominio ma lo sono su insiemi di interesse.

La comprensione di queste proprietà è essenziale non solo in ambito teorico, ma anche per formalizzare e automatizzare dimostrazioni matematiche, come nel sistema Lean, dove la manipolazione di immagini e controimmagini, la gestione di quantificatori e l'applicazione di tecniche come il principio del caso ("by_cases") o l'uso di tactiche specifiche sono strumenti fondamentali.

Infine, il lettore dovrebbe avere presente che le operazioni di immagine e controimmagine sono strumenti potenti per studiare la relazione tra domini e codomini, e per gestire problemi di inclusione, uguaglianza e caratterizzazione di insiemi mediante funzioni, e che la familiarità con queste nozioni costituisce una base indispensabile per affrontare questioni avanzate in algebra, analisi e teoria della misura.

Come si definiscono e si manipolano i Finset in Lean?

Gli insiemi finiti possono essere definiti esplicitamente enumerando gli elementi, ad esempio {0, 2, 5} : Finset Nat, e Lean riconosce automaticamente che l’ordine degli elementi e la loro ripetizione non influiscono sull’insieme. Ciò è dimostrato da uguaglianze come {0, 1, 2} = {1, 2, 0} o {x, x} = {x}, ottenute con la strategia decide o tramite riscritture che fanno uso di proprietà di commutatività e idempotenza degli insiemi.

Le operazioni di inserimento (insert) e cancellazione (erase) di un elemento in un finset sono fondamentali e vengono utilizzate spesso nelle dimostrazioni per esprimere proprietà ricorsive o per dimostrare uguaglianze che coinvolgono manipolazioni di insiemi finiti. È importante notare che erase appartiene alla namespace Finset, mentre insert è definito nella root, un dettaglio che può sembrare marginale ma che è essenziale per una corretta organizzazione del codice e l’evitamento di ambiguità.

Per definire sottoinsiemi di un finset mediante proprietà, si utilizza la notazione di insieme con filtro: {x ∈ s | P x} corrisponde al filtro s.filter P. Questo consente di lavorare comodamente con insiemi derivati da condizioni logiche, ad esempio i numeri pari in un intervallo finito, con uguale efficacia sia formale che computazionale.

Lean gestisce anche immagini, prodotti cartesiani e insiemi delle parti (powerset) di finset, fornendo così strumenti robusti per la costruzione di insiemi derivati e strutture più complesse. La definizione di operazioni su finset richiede di rispettare la proprietà di indipendenza dall’ordine degli elementi; per questo si ricorre a operazioni come Finset.fold che applica funzioni associative e commutative per ottenere risultati univoci e ben definiti, come somme o prodotti finiti.

Lean consente anche di lavorare con elementi scelti da un finset non vuoto tramite il principio di scelta classica, oltre a fornire funzioni per trasformare finset in liste con ordine arbitrario degli elementi, mantenendo la corrispondenza tra appartenenza all’insieme e presenza nella lista.

Per insiemi di elementi ordinati linearmente o dotati di struttura reticolare, Lean fornisce funzioni per estrarre minimo, massimo, infimo e supremo, distinguendo tra versioni che richiedono la non-vuotezza dell’insieme (versioni “prime”) e quelle che gestiscono anche insiemi vuoti tramite l’aggiunta di elementi top o bottom. Questa distinzione è fondamentale per garantire la correttezza formale e per evitare ambiguità in caso di insiemi vuoti.

La cardinalità di un finset è ben definita e può essere espressa come somma degli 1 associati a ogni elemento, con proprietà che si riflettono nella corrispondente cardinalità dei fintype, ossia tipi finiti dotati di un universale finset contenente tutti gli elementi. La relazione tra finset e fintype consente di passare agevolmente dalla teoria degli insiemi finiti alla teoria dei tipi, facilitando l’espressione e la dimostrazione di proprietà matematiche.

Infine, ogni finset può essere visto come un sottotipo del tipo di partenza costituito dagli elementi che appartengono all’insieme. Questa visualizzazione facilita l’integrazione tra la teoria degli insiemi e la teoria dei tipi, rendendo possibili dimostrazioni più strutturate e coerenti.