Fixpunktsatz von Lawvere

Der Fixpunktsatz von Lawvere, benannt nach dem Mathematiker William Lawvere, ist eine mathematische Aussage aus der Kategorientheorie. Er gibt eine Bedingung, wann Objekte einer Kategorie die Fixpunkteigenschaft erfüllen, und verallgemeinert damit Sätze wie den Satz von Cantor oder den Rekursionssatz.

Aussage

Es sei C {\displaystyle {\mathcal {C}}} eine Kategorie mit endlichen Produkten und Y {\displaystyle Y} ein C {\displaystyle {\mathcal {C}}} -Objekt.

Wenn es ein Objekt A {\displaystyle A} und einen Pfeil g : A × A Y {\displaystyle g\colon A\times A\to Y} mit der Eigenschaft

f : A Y .   c : 1 A .   a : 1 A .   g c , a = f a {\displaystyle \forall f\colon A\to Y.\ \exists c\colon \mathbf {1} \to A.\ \forall a\colon \mathbf {1} \to A.\ g\circ \langle c,a\rangle =f\circ a}

gibt, dann hat Y {\displaystyle Y} die Fixpunkteigenschaft: für jedes t : Y Y {\displaystyle t\colon Y\to Y} gibt es einen „Fixpunkt“, d. h. einen Pfeil y : 1 Y {\displaystyle y\colon \mathbf {1} \to Y} mit t y = y {\displaystyle t\circ y=y} .

Beweis

Es gebe A {\displaystyle A} und g : A × A Y {\displaystyle g\colon A\times A\to Y} mit der geforderten Eigenschaft und t : Y Y {\displaystyle t\colon Y\to Y} sei beliebig. Es gibt dann den speziellen Pfeil f : A Y {\displaystyle f\colon A\to Y} , definiert durch

f = t g i d , i d {\displaystyle f=t\circ g\circ \langle \mathrm {id} ,\mathrm {id} \rangle } .

Für ihn wiederum gibt es ein c : 1 A {\displaystyle c\colon \mathbf {1} \to A} , für das gilt

g c , c = f c = t g i d , i d c = t g c , c {\displaystyle g\circ \langle c,c\rangle =f\circ c=t\circ g\circ \langle \mathrm {id} ,\mathrm {id} \rangle \circ c=t\circ g\circ \langle c,c\rangle } .

Das heißt, g c , c {\displaystyle g\circ \langle c,c\rangle } ist Fixpunkt von t {\displaystyle t} .

Folgerungen

  • Wenn C {\displaystyle {\mathcal {C}}} kartesisch abgeschlossen ist, kann statt g : A × A Y {\displaystyle g\colon A\times A\to Y} dessen transponierte Version g ~ : A Y A {\displaystyle {\tilde {g}}\colon A\to Y^{A}} herangezogen werden. Für diese wird die geforderte „Eigenschaft“ zu einer gewissen Form der Surjektivität, die mittels globalen Elementen definiert ist. Lawvere nennt sie weakly point-surjective. Die Aussage des Satzes ist dann: Wenn es ein weakly point-surjective A Y A {\displaystyle A\to Y^{A}} gibt, haben alle Endomorphismen auf Y {\displaystyle Y} einen Fixpunkt.
  • Im Fall C = S e t {\displaystyle {\mathcal {C}}=\mathbf {Set} } und Y = 2 {\displaystyle Y=\mathbf {2} } erhält man den Satz von Cantor per Kontraposition: Da n o t : 2 2 {\displaystyle \mathrm {not} \colon \mathbf {2} \to \mathbf {2} } keinen Fixpunkt hat, gibt es für keine Menge A {\displaystyle A} eine surjektive Funktion A 2 A = P A {\displaystyle A\to \mathbf {2} ^{A}={\mathcal {P}}A} .

Literatur

  • William Lawvere: Diagonal arguments and cartesian closed categories. In: Lecture Notes in Mathematics, 92. 1969, S. 134–145 (reprint). 
  • Noson S. Yanofsky: A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points. 2003, arxiv:math/0305282. 
V
Kategorientheorie
Einordnung
Typen von Kategorien

dual | diskret | klein | lokal klein | monoidal | symmetrisch monoidal | angereichert | ausgeglichen | erreichbar | vollständig | kovollständig

Typen von Objekten

initial | terminal | null | injektiv | projektiv | Generator | Kogenerator | Pro | Ind | Gruppe | Monoid | exponential | frei | kompakt

Typen von Morphismen

Mono | Epi | Bi | Retraktion | Koretraktion | Injektive Auflösung | Projektive Auflösung

Typen von Funktoren

konstant | voll | treu | volltreu | additiv | exakt | abgeleitet | glatt

Konstruktionen
Limes

Produkt | Differenzkern | Faserprodukt | Ende

Kolimes

Filtrierter Kolimes | Koprodukt | Differenzkokern | Kofaserprodukt

Kan-Erweiterung | Monade | Komonade | Kategorie der Elemente | Kommakategorie | Pfeilkategorie | Homotopie-Kategorie

Resultate

Lemma von Yoneda | Fixpunktsatz von Lawvere | Einbettungssatz von Mitchell

Spezielle Funktoren

Hom-Funktor | Potenzmengenfunktor | Diagonalfunktor | Ext | Tor