Come le azioni di gruppo e i quozienti strutturano la teoria dei gruppi in Lean

Nel formalismo Lean, l’azione di un gruppo $G$ su un tipo $X$ è codificata attraverso la classe di tipo $\text{MulAction} \ G \ X$, che permette a Lean di inferire automaticamente la morfismo di azione, evitando di doverlo portare esplicitamente ad ogni passo. Questa struttura definisce l’azione di un elemento $g \in G$ su un elemento $x \in X$, indicata sinteticamente come $g \cdot x$. Analogamente, esiste la versione additiva, $\text{AddAction}$, con la notazione $+_v$, utile ad esempio nella definizione degli spazi affini.

Quando $X$ è finito, questa struttura si traduce in un’equazione chiara per la cardinalità di $X$: essa è la somma delle cardinalità delle orbite. Inoltre, ogni orbita può essere identificata con il quoziente del gruppo $G$ rispetto allo stabilizzatore dell’elemento $x$, cioè $G / \text{stabilizer}(G, x)$, stabilendo così un legame stretto tra la struttura delle orbite e quella dei sottogruppi di $G$.

Si può inoltre costruire un’azione di coniugio di un gruppo sui suoi sottogruppi, che gioca un ruolo cruciale nella teoria dei gruppi normali e nella definizione di quozienti.

Proprio la costruzione dei gruppi quoziente $G / H$, dove $H$ è un sottogruppo normale, è centrale per la teoria. Solo in questo caso $G / H$ può essere dotato in modo univoco di una struttura di gruppo tale che la proiezione $G \to G / H$ sia un morfismo di gruppi. Questa condizione è codificata nel tipo $H.\text{Normal}$, che consente a Lean di inferire la struttura di gruppo sul quoziente. L’importanza di questa costruzione emerge nella proprietà universale dei gruppi quoziente, che consente di fattorizzare ogni morfismo di gruppi $\varphi : G \to M$ la cui nucleo contiene $N$ attraverso il gruppo quoziente $G / N$.

Una sottigliezza tecnica importante è che, sebbene due sottogruppi normali $M$ e $N$ siano uguali, i corrispondenti gruppi quoziente $G / M$ e $G / N$ sono uguali solo fino a isomorfismo, non in senso strettamente definizionale. Tuttavia, la proprietà universale garantisce l’esistenza di un isomorfismo naturale.

È cruciale comprendere che l’intero impianto si basa sull’interazione tra l’azione di un gruppo su un insieme e la struttura interna del gruppo stesso. L’uso delle classi di tipo in Lean consente una gestione elegante e automatizzata delle strutture coinvolte, ma la loro interpretazione richiede una visione profonda delle connessioni tra gruppi, azioni, orbite, stabilizzatori e sottogruppi normali. In particolare, il passo dalla semplice azione alla costruzione dei gruppi quoziente e delle proprietà universali corrispondenti riflette un’armoniosa sintesi tra teoria astratta e formalizzazione computazionale.

Come si definisce e si comprende l’invertibilità delle matrici e la struttura delle basi negli spazi vettoriali

In algebra lineare, la nozione di invertibilità di una matrice è strettamente legata al concetto di determinante. Più precisamente, esiste una funzione generale, chiamata Ring.inverse, che definisce l'inverso in un anello qualsiasi. Nel caso di una matrice $A$, l’inverso $A^{ -1}$ è dato da $\text{Ring.inverse} \, ( \det A ) \cdot \text{adjugate}(A)$. Secondo la regola di Cramer, questa è proprio la definizione dell'inverso di $A$ quando il determinante di $A$ è diverso da zero, ovvero quando $A$ è invertibile. Questa definizione è di fatto utile solo per matrici invertibili, ed esiste una classe di tipo generale, chiamata Invertible, che consente di rappresentare questa proprietà nel sistema formale.

Nell’ambito della formalizzazione matematica, come in Lean, la presenza della classe Invertible permette di automatizzare ragionamenti e dimostrazioni riguardanti matrici invertibili, facilitando l’uso di lemmi come inv_mul_of_invertible. Questo approccio è essenziale non solo per gestire matrici concrete ma anche per lavorare con matrici definite su indici arbitrari, non necessariamente numerici. Ad esempio, per matrici di adiacenza di grafi finiti, le righe e le colonne sono indicizzate dai vertici del grafo stesso, consentendo così una rappresentazione più naturale e flessibile.

Per non perdere i benefici del sistema di classi di tipo, si usa una corrispondenza (equivalenza) tra funzioni e matrici, come nel caso di Matrix.of, che permette di definire matrici in modo funzionale ma mantenendo la struttura algebrica necessaria. Ad esempio, le matrici di Vandermonde possono essere definite tramite funzioni che elevano a potenza i componenti di un vettore, mostrando la flessibilità di questa definizione.

Passando agli spazi vettoriali, la nozione di base è fondamentale. Una base è intuitivamente una famiglia di vettori linearmente indipendenti che generano tutto lo spazio vettoriale, oppure, equivalentemente, una famiglia tale che ogni vettore dello spazio può essere espresso in modo unico come combinazione lineare di vettori della base. Una definizione più astratta e potente, utilizzata nei sistemi formali come Mathlib, vede la base come un’isomorfismo lineare tra lo spazio vettoriale $V$ e una somma diretta di copie del campo base $K$, indicizzate da un insieme $\iota$.

Se la base è finita, la rappresentazione si riduce al caso più familiare delle somme finite di combinazioni lineari. Se la base è infinita, invece, la somma diventa una somma finita implicita a causa del supporto finito. In entrambi i casi, la struttura delle basi permette di definire isomorfismi lineari e di sviluppare una teoria coerente e generale.

Quando l’insieme degli indici $\iota$ è finito, si può usare la base funzionale $\text{Pi.basisFun}$, che rappresenta la base completa dello spazio delle funzioni $\iota \to K$. In tal caso, la distinzione tra somme finite e infinite non si pone, e la rappresentazione è particolarmente semplice.

Un punto cruciale per il lettore è riconoscere che la struttura delle matrici e delle basi non è solo una questione di notazione o di definizione, ma incide profondamente sulla capacità di formalizzare e automatizzare ragionamenti matematici, specialmente in ambienti come Lean. L’interazione tra le classi di tipo per la definizione di invertibilità, la distinzione tra diversi modi di rappresentare matrici come funzioni o oggetti strutturati, e la cura nella definizione delle basi con supporto finito sono tutti elementi essenziali per garantire la robustezza delle costruzioni e la possibilità di ragionare correttamente su spazi di dimensione arbitraria, finita o infinita.