Hvordan defineres grupper i Lean og deres algebraiske strukturer?

I Lean bruger vi de algebraiske strukturer som grupper, til at arbejde med matematiske begreber, der relaterer sig til symmetri og operationer, som er omvendelige. Grupper er fundamentale i mange matematiske områder, og Lean giver os mulighed for at definere disse strukturer og deres egenskaber meget præcist. I Mathlib, som er en samling af Lean-biblioteker, finder vi en omfattende definition af grupper og deres tilknyttede operationer, herunder ækvivalensrelationer, bijektioner og grupper af permutationer.

I Mathlib er begrebet Equiv defineret som ækvivalensrelationer mellem to typer, α og β. Et element af typen Equiv α β er en bijektion, der kan ses som et sæt af fire komponenter: en funktion, der går fra α til β, en invers funktion fra β til α, og to egenskaber der bekræfter, at disse funktioner er hinandens inverse. De to egenskaber er henholdsvis right_inv, som siger, at anvendelsen af den inverse funktion på et element i β giver det oprindelige element, og left_inv, som siger, at anvendelsen af den inverse funktion på et element i α også giver det oprindelige element.

Denne sammensætning kan ses som en multiplikation af bijektionerne, og denne idé udvider sig til at skabe en gruppe med operationen for sammensætning. En gruppe består af en operation, en identitetselement, og et invers element. I tilfældet med permutationer er gruppen defineret ved at anvende sammensætning som den primære operation, identitetselementet som Equiv.refl, og inversen som Equiv.symm. På denne måde kan vi definere en gruppe som permGroup i Lean.

Derudover støtter Mathlib også strukturering af notationen i grupper. I matematik er notationen for grupper ofte uafhængig af den specifikke struktur, men i Lean er notationerne tættere knyttet til den underliggende struktur. For eksempel anvender Lean den samme notation til at repræsentere grupper og deres operationer, uanset hvilken struktur der anvendes. Det betyder, at når vi skriver en operation som mul, one, og inv i forbindelse med en gruppe, så refererer Lean automatisk til de relevante operationer og strukturer uden behov for at skrive alt ud eksplicit.

Desuden er det muligt at definere grupper med additive operationer ved hjælp af en struktur som AddGroup1. Denne struktur anvender addition som den primære operation i stedet for multiplikation, hvilket giver os mulighed for at arbejde med strukturer som additive grupper. Additive grupper benytter sig af operationer som add, zero, og neg, og de kan definere egenskaber som negation og nul.

Når man definerer grupper i Lean, er der en vigtig egenskab ved systemet, som gør det muligt at arbejde med generiske grupper på en fleksibel måde. Lean bruger en kombination af tre elementer: logik, implicitte argumenter og typeklassificering. Dette betyder, at Lean automatisk fylder de nødvendige oplysninger ud, når vi arbejder med grupper, og vi behøver ikke nødvendigvis at skrive alle detaljer ud manuelt. For eksempel kan Lean automatisk finde den relevante funktion, når vi skriver udtryk som f * g, selvom vi ikke eksplicit skriver, at f og g er funktioner.

Ved at udnytte implicitte argumenter og typeklassificering kan Lean nemt håndtere grupper og deres operationer, og denne funktionalitet giver os mulighed for at arbejde med abstrakte matematiske strukturer på en effektiv og fleksibel måde.

For at arbejde med grupper og deres notation i Lean, kræver det en forståelse af både den algebraiske struktur og den måde, hvorpå Lean fortolker disse operationer. Når du definerer en gruppe, skal du være opmærksom på, hvordan notationen og operationerne interagerer med hinanden, og hvordan Lean bruger typeklassificering til at fylde de nødvendige detaljer ud.

Hvordan arbejder man med algebraiske strukturer i Lean: Grupper, Ringe og Moduler

I Lean, et kraftfuldt værktøj til formel matematik, arbejder vi med algebraiske strukturer som grupper, ringe og moduler ved at definere klassehierarkier og relaterede lemmer. Dette gør det muligt at bygge komplekse matematiske objekter på en systematisk måde, hvor hver klasse og instans afhænger af tidligere definerede egenskaber.

En grundlæggende komponent i algebraiske strukturer er grupper, som i Lean kan udvides med flere egenskaber. For eksempel kan vi definere en gruppe Group3, som ikke kun er en monoid, men også har en invers funktion, der tilfredsstiller betingelsen a * a¹ = 1. Denne egenskab kan defineres som en lemma med en simpel etikette for at lette forenkling i senere beregninger, f.eks. ved at bruge attributten [simp] til at forenkle udtryk, der involverer denne inverse funktion.

Når vi arbejder med sådanne strukturer, er det ofte nødvendigt at oversætte mellem forskellige notationer. I Lean kan dette gøres ved hjælp af attributten @[to_additive], der automatisk oversætter fra multiplicativ til additiv notation. Dette sparer tid og sikrer, at alle nødvendige beviser er til stede i begge formater. For eksempel, i en gruppe Group3, kan vi oversætte lemmers beviser fra den multiplicative form til den additive form og samtidig tilføje forenkling ved hjælp af @[to_additive (attr := simp)].

Udvidelsen af grupper til andre algebraiske strukturer fortsætter naturligt til ringe og moduler. I Lean definerer vi for eksempel en ring som en struktur, der kombinerer både en additiv gruppe og et monoid, hvor multiplicationen er distributiv over additionen. For at definere en ringstruktur i Lean, udvider vi både AddGroup3 og Monoid3 for at sikre, at de nødvendige algebraiske egenskaber er til stede. Multiplikationens distributivitet over additionen er en væsentlig del af denne struktur og kan defineres som en regel i vores klasse, f.eks. ved hjælp af left_distrib og right_distrib.

Et andet vigtigt aspekt ved algebraiske strukturer i Lean er håndteringen af moduler. Et modul over en ring er en generalisering af vektorrum, hvor vi arbejder med en skalar multiplikation defineret af elementerne i en ring. Moduler kan defineres ved hjælp af en klasse Module1, som kræver, at både ringen og den additiv kommutative gruppe opfylder visse krav. En væsentlig egenskab ved moduler er, at de tillader skalar multiplikation og addering på en måde, der respekterer strukturen af ringen og gruppen.

I Lean kan vi også definere modulstrukturer på konkrete eksempler som Z, de hele tal, der fungerer som et modul over sig selv, eller et abelsk gruppe, der fungerer som et modul over Z. Dette kræver, at vi definerer, hvordan skalar multiplikation fungerer, f.eks. ved at definere funktioner som nsmul1 for naturlige tal og zsmul1 for hele tal, som specifikt beskriver, hvordan vi multiplicerer et element med en skalar.

Det er vigtigt at bemærke, at mens Lean tilbyder en meget effektiv måde at bygge disse strukturer på, kræver det en vis forståelse af den underliggende matematik og den logiske struktur af de definitioner, vi arbejder med. For eksempel kan det være nødvendigt at definere flere mellemtrin eller beviser for at forstå, hvordan en bestemt modulstruktur fungerer. Når du arbejder med sådanne definitioner, kan det være nyttigt at fokusere på de grundlæggende algebraiske regler, som f.eks. distributiv lov og kommutativitet, som de er fundamentale for at forstå, hvordan de forskellige operationer interagerer.

Ved at udvide disse strukturer kan vi opbygge et hierarki af algebraiske objekter, der gør det muligt at arbejde med et bredt spektrum af matematiske problemer, fra simple grupper og ringe til mere komplekse moduler og deres relationer. Lean giver os værktøjerne til at definere disse objekter på en præcis og formel måde, hvilket muliggør både bevisførelse og beregning i matematik.