Come si calcolano le cardinalità nelle strutture finitarie e nelle finset: argomenti di conteggio e applicazioni

Nel contesto della matematica discreta e della combinatoria, la capacità di contare elementi in insiemi finiti, e più specificamente in strutture come i finset o i fintype, rappresenta una competenza fondamentale. Un fintype si può concepire come una struttura algebrica dotata di dati aggiuntivi che ne definiscono la finitezza; la teoria che ne consegue consente di applicare strumenti di conteggio precisi e formali.

Nel trattamento di funzioni iniettive, la cardinalità dell’immagine di un insieme tramite una funzione iniettiva è uguale a quella dell’insieme di partenza: $\#(s.image(f)) = \#s$. Questo fatto consente di trasferire il problema del conteggio da un dominio a un codominio senza perdita di informazioni quantitative.

In contesti più complessi, si considerano funzioni dipendenti, come quelle del tipo $\text{Fin } n \to \alpha$, la cui cardinalità è $\text{card}(\alpha)^n$, o famiglie indicizzate di tipi finiti, per cui la cardinalità del prodotto dipende dal prodotto delle cardinalità dei singoli tipi.

Il calcolo viene formalizzato definendo il triangolo come un’unione disgiunta di righe, ognuna rappresentata come immagine di un insieme più piccolo, con la cardinalità calcolata mediante somme e prodotti di cardinalità di insiemi finiti. In questo modo, la manipolazione delle cardinalità diventa un esercizio di algebra combinatoria rigorosa e ben formalizzata.

Nell’ambito dei grafi bipartiti, si può utilizzare un argomento di doppio conteggio per stimare i vincoli sulle cardinalità dei sottoinsiemi di vertici. Considerando un grafo bipartito con insiemi di vertici $s$ e $t$, e una relazione $r$ che rappresenta gli archi, se ogni vertice di $s$ è collegato ad almeno tre archi, e ogni vertice di $t$ è collegato a uno o nessun arco, si ricava che $3 \times \#s \leq \#t$. Questo risultato si ottiene sommando le cardinalità degli insiemi di vertici e applicando proprietà di disgiunzione e iniezione, sottolineando l’efficacia del conteggio combinatorio nel risolvere problemi di teoria dei grafi.

Oltre al calcolo diretto delle cardinalità, è importante riconoscere come queste tecniche siano strettamente collegate a concetti più ampi come la teoria delle funzioni, la teoria dei grafi e la logica matematica. Il rigore nell’approccio, soprattutto nella formalizzazione con strumenti come Lean, offre una base solida per esplorare teorie più complesse e applicazioni pratiche, dall’analisi algoritmica alla crittografia.

Come vengono rappresentati i sotto-oggetti algebrici in Mathlib?

Nel contesto della libreria Mathlib, i sotto-oggetti di strutture algebriche, come sottogruppi o sottosemigruppi, sono trattati come insiemi dotati di proprietà strutturali aggiuntive. L'approccio adottato è estremamente modulare e riutilizzabile grazie a una raffinata astrazione tramite classi di tipo e coercizioni. L'idea centrale è che un sotto-oggetto può essere rappresentato come un insieme dotato di una certa proprietà chiusa rispetto all'operazione della struttura madre. Questo viene implementato in termini di una funzione da un insieme a una proposizione, cioè come un predicato.

Per evitare la rottura dell’astrazione tra Set X e X → Prop, si utilizza la classe SetLike, che fornisce un modo uniforme per trattare oggetti che possono essere visti come insiemi ma che portano anche ulteriori informazioni strutturali. Invece di incapsulare un'iniezione in un tipo di funzione, la classe incapsula un'iniezione in un tipo Set e definisce le coerzioni e l'istanza di appartenenza corrispondente.

Ad esempio, una struttura Submonoid1 M è definita su un tipo M dotato di struttura di monoide, ed è costituita da un insieme carrier insieme alla proprietà che il prodotto di due elementi e l’elemento neutro appartengono ancora al sottoinsieme. Grazie all’istanza SetLike, possiamo trattare un sotto-monoide N direttamente come un insieme, utilizzando notazioni come 1 ∈ N o f '' N, senza fare riferimento esplicito al campo carrier.

Un ulteriore passaggio consiste nella coercizione del sotto-monoide a tipo tramite Subtype, che permette di dichiarare variabili del tipo x : N con N : Submonoid1 M, tali che x può essere trattato come un elemento di M e automaticamente sappiamo che x ∈ N. Ciò consente di costruire su N una struttura di monoide coerente, dove le operazioni e le proprietà si ottengono per coercizione e attraverso la lemma SetCoe.ext, che garantisce l'iniettività della coercizione.

Le stesse idee si estendono ad altri sotto-oggetti come sottogruppi o sottoanelli. Per ottenere una maggiore generalizzazione e riutilizzo del codice, si definisce una classe SubmonoidClass1 che accetta come parametro un’istanza SetLike, eliminando la necessità di un campo carrier esplicito. I lemmi che descrivono le proprietà algebriche (come la chiusura rispetto al prodotto o la presenza dell'identità) possono essere scritti direttamente in termini di notazione di appartenenza.

Un aspetto cruciale del trattamento dei sotto-oggetti in Mathlib è che essi formano sempre un reticolo completo. Questo non è solo un dettaglio teorico: è sfruttato attivamente nella libreria. L’intersezione di due sotto-monoidi, ad esempio, non è un semplice lemma, bensì una costruzione di infimo in un reticolo. La struttura di reticolo è resa esplicita tramite un’istanza di Min, che costruisce il sotto-monoide generato dall'intersezione degli insiemi sottostanti, garantendo la presenza dell'identità e la chiusura rispetto al prodotto.

È importante sottolineare che la notazione usata per l’intersezione e l’unione non coincide con quella degli insiemi comuni. In particolare, l’intersezione di due sotto-monoidi è denotata con ⊓ invece di ∩, e la loro unione con ⊔ invece di ∪. Questo perché, mentre l’intersezione di due sotto-oggetti è sempre ancora un sotto-oggetto, l’unione in genere non lo è. N ⊔ P rappresenta il minimo sotto-oggetto che contiene entrambi, e non semplicemente l’unione degli elementi. Questa scelta di notazione garantisce una coerenza concettuale attraverso tutte le strutture algebriche.

Nel caso dei quozienti, viene utilizzata la classe HasQuotient, che introduce una notazione elegante come M ⧸ N. Questo simbolo non è una semplice barra obliqua, ma un carattere Unicode speciale che distingue chiaramente il quoziente dal simbolo di divisione usuale. Ad esempio, nel caso di un monoide commutativo M e un sotto-monoide N, il quoziente M ⧸ N viene definito costruendo una relazione di equivalenza tramite il concetto di Setoid, che stabilisce che due elementi x e y sono equivalenti se esistono w, z in N tali che x * w = y * z.

Questa astrazione non solo permette l’uso di notazioni intuitive, ma evita anche duplicazioni di codice. La struttura del monoide sul quoziente è definita attraverso Quotient.map2 e si avvale delle proprietà algebriche già note del monoide M.

È essenziale capire che queste costruzioni, benché tecnicamente sofisticate, sono progettate per essere trasparenti nell’uso e per permettere una facile estensione ad altre strutture come gruppi, anelli e spazi vettoriali. Le classi come SetLike, SubmonoidClass1 e HasQuotient, insieme alla logica dei reticoli completi, costituiscono un’infrastruttura potente e flessibile per lavorare con sotto-oggetti algebrici in modo modulare, coerente e riutilizzabile.

Un punto importante che il lettore deve comprendere è che questa architettura di Mathlib riflette una profonda separazione tra la semantica degli oggetti algebrici e la loro rappresentazione concreta. Ogni costruzione mira a rendere la matematica astratta facilmente formalizzabile, mantenendo al contempo leggibilità, manutenibilità e rigore. È anche fondamentale notare che le coercizioni e le estensioni di tipo non sono solo comodità sintattiche: esse incarnano una filosofia di programmazione tipica dei sistemi di prova formale, dove ogni lemma e ogni istanza di