La definizione di strutture algebriche in Lean non si limita alla mera codifica degli oggetti matematici. È un procedimento raffinato che rende trasparenti le relazioni astratte attraverso un sistema di notazione coerente, un meccanismo di inferenza implicita e una tipizzazione altamente modulare. Per esempio, l’oggetto Equiv α β rappresenta una biiezione tra due tipi α e β. La sua struttura include non solo la funzione diretta e inversa (toFun, invFun), ma anche le proprietà che ne certificano la mutua invertibilità. La notazione α ' β è impiegata in Mathlib per rappresentare il tipo delle equivalenze, che, tramite coercione, può essere utilizzato direttamente come una funzione.

Questa struttura ammette un’identità Equiv.refl, una simmetria Equiv.symm, e una composizione Equiv.trans, rendendo manifesta la natura di relazione di equivalenza. La composizione di equivalenze, in particolare, segue l’ordine inverso nel quale vengono applicate le funzioni, e questo è coerente con l’interpretazione usuale della composizione funzionale: (f.trans g) x = g (f x).

Mathlib generalizza ulteriormente queste costruzioni definendo Equiv.Perm α, il tipo delle permutazioni su α, ovvero delle biiezioni da α in sé stesso. Questo tipo forma un gruppo sotto la composizione, e tale struttura è formalmente codificata come Group1 (Equiv.Perm α), dove le operazioni mul, one, inv sono definite come Equiv.trans, Equiv.refl e Equiv.symm, rispettivamente. L’associatività, la proprietà dell’identità, l’inverso a sinistra e a destra sono dedotte da lemmi interni come Equiv.trans_assoc, Equiv.trans_refl, Equiv.refl_trans, Equiv.self_trans_symm.

In matematica informale possiamo adottare notazioni differenti per gruppi distinti — moltiplicativa, additiva, funzionale — ma in Lean, la notazione è legata direttamente alla struttura dichiarata. La struttura Group ha come campi mul, one, inv; l’alternativa additiva AddGroup li chiama add, zero, neg. Questo consente a Lean di distinguere istanze diverse di strutture simili e di associare correttamente le notazioni e le proprietà dedotte.

Per esempio, definendo il tipo Point con coordinate cartesiane, possiamo dotarlo di una struttura di gruppo additivo (AddGroup1) definendo l’addizione vettoriale, l’inverso e l’elemento neutro. Ma perché tutto il sistema notazionale e deduttivo funzioni correttamente — come accade per Equiv.Perm α — è necessario associare alla struttura non solo le operazioni ma anche le istanze implicite tramite meccanismi più profondi.

La chiave di tutto è la combinazione tra tre strumenti potenti: l’uso della logica strutturale, gli argomenti impliciti, e l’inferenza di tipo basata sulle classi. Ogni definizione o teorema generico comincia specificando un tipo e la sua struttura, ma questi parametri vengono omessi esplicitamente grazie alla notazione {...} o [...], che permette a Lean di riempirli automaticamente tramite deduzione.

Quando un’espressione come f * g viene digitata, Lean deve dedurre non solo che f e g sono elementi di un gruppo, ma anche quale sia la struttura di gruppo che regola la moltiplicazione. Questo è reso possibile dalla registrazione preventiva dell’informazione strutturale come istanza di una "type class", che Lean può recuperare dinamicamente in base al contesto. La notazione [Group G] dice a Lean di sintetizzare automaticamente l’istanza, e grazie a questo meccanismo possiamo scrivere espressioni generiche come f * g * g⁻¹ = f, valide per ogni gruppo, senza dover specificare nulla oltre agli elementi coinvolti.

Questo approccio si estende oltre i gruppi. In Lean, anche la continuità di una funzione tra spazi topologici è gestita in modo simile: scrivere Continuous f impone a Lean di recuperare automaticamente le topologie sui domini e codomini tramite inferenza sulle type class. È un’architettura concettualmente elegante e funzionalmente potente che consente la formalizzazione modulare e riusabile della matematica.

È importante comprendere che l’adozione della notazione e l’inferenza implicita non sono semplici comodità sintattiche: rappresentano una filosofia della formalizzazione che considera la matematica come una struttura coesa di relazioni, non un insieme di simboli arbitrari. Il fatto che si possa definire un unico teorema sul gruppo astratto, e applicarlo tanto alle permutazioni quanto agli spazi topologici, esprime la profondità di questa astrazione.

Come si costruiscono combinazioni lineari e si definisce la dimensione in matematica formalizzata?

Nel contesto della matematica formalizzata, e in particolare nell’uso della libreria Mathlib di Lean, la costruzione delle combinazioni lineari e la definizione della dimensione di uno spazio vettoriale assumono una forma più astratta e strutturata rispetto alla pratica matematica usuale. Si utilizzano strumenti specifici come Finsupp.linearCombination, che permette di costruire combinazioni lineari a partire da una funzione a supporto finito.

Dato un insieme indicizzato ι, un campo K, e uno spazio vettoriale V su K, se abbiamo una funzione a supporto finito c : ι →₀ K e una funzione arbitraria f : ι → V, allora Finsupp.linearCombination K f c restituisce la somma ∑ c i · f i calcolata su tutti gli elementi nel supporto di c. Questa somma può essere estesa a un qualsiasi insieme finito s che contenga il supporto di c, rendendo il meccanismo estremamente flessibile per costruzioni basate su basi.

Questa costruzione si collega direttamente alla rappresentazione dei vettori in una base. Se B è una base dello spazio V, allora per ogni vettore v in V si ha l’identità Finsupp.linearCombination K B (B.repr v) = v, che evidenzia come la funzione repr associ ad ogni vettore la sua rappresentazione come combinazione lineare dei vettori di base, e linearCombination ricostruisca il vettore a partire da tale rappresentazione.

La funzione Finsupp.linearCombination K f non è solo una funzione da ι →₀ K a V, ma è un'applicazione lineare K-lineare, cioè un elemento di (ι →₀ K) →ₗ[K] V. Questo è cruciale perché ci permette di trattare linearCombination come un oggetto matematicamente ben strutturato, parte integrante dell'algebra delle applicazioni lineari.

La formalizzazione continua con il concetto di Basis.constr, che stabilisce un isomorfismo lineare tra le funzioni ι → W e le applicazioni lineari V →ₗ[K] W, dove W è un altro spazio vettoriale su K. La costruzione B.constr K u definisce un’applicazione lineare che mappa ciascun vettore di base B i su u i. Questo mostra in modo esplicito come le basi servano da ponte per costruire e comprendere le applicazioni lineari: ogni applicazione è determinata interamente dai suoi valori sui vettori di base.

Quando sia lo spazio di partenza che quello di arrivo sono dotati di basi, le applicazioni lineari tra di essi possono essere rappresentate come matrici. Questo avviene tramite l'isomorfismo toMatrix B B', che associa ad ogni mappa lineare una matrice in Matrix ι' ι K. L’azione della mappa lineare su un vettore v può quindi essere interpretata come la moltiplicazione della matrice toMatrix B B' φ per la rappresentazione B.repr v. La composizione di mappe lineari si riflette nella moltiplicazione di matrici, e le determinanti delle matrici associate a endomorfismi restano invarianti al cambio di base, purché le basi siano indicizzate dallo stesso insieme.

La definizione della dimensione di uno spazio vettoriale V su un campo `K

Come EtherNet/IP e Modbus Rivoluzionano l'Automazione Industriale
Come la Razza e la Luce Trasformano il Dramma: Il Conflitto nel Mondo di Titus Andronicus e Coriolano
Come si definisce un complesso filtrato di catene poset e la sua struttura?