16 - Kategorien in der Programmierung [ID:10666]
50 von 642 angezeigt

wiederholend die Definition von einem universellen Pfeil angeschrieben.

Dazu hat man also zunächst mal immer ein Funktur fixiert, der ist gegeben.

Und ein universeller Pfeil ist also ein Morphismus und zwar von einem Objekt X in U von A0,

also A0 ist hier ein Objekt in B, X ist in A, mit dieser universellen Eigenschaft.

Also immer dann, wenn ich irgendeinen Morphismus habe aus X nach U von irgendwas,

für alle solchen F, gibt es genau einen Morphismus von A0 nach A, sodass hier dieses Dreieck kommutiert.

Also ich wende den Funktur U auf F quer an und komponiere das hier und dieses Dreieck muss dann kommutieren.

Da war gerade eben auch die Frage, was ist der Zusammenhang zu Komma-Kategorien oder Slyce-Kategorien?

Da ist es eben so, dass diese Definition genau sagt, dass das ATA hier ein Initialobjekt ist in der Slyce-Kategorie von dem Objekt X,

nicht über ein Funktur G, sondern über ein Funktur U in dem Falle.

Weil die Objekte in dieser Slyce-Kategorie, das sind halt genau, wenn man jetzt hier für G, U einsetzt, solche Morphismen hier.

Und dass es hier diesen eindeutigen gibt, dass er also erstmal sagt, das Dreieck hier, es ist ein Morphismus in der Slyce-Kategorie und den gibt es halt eindeutig.

Und damit ist das ATA hier oben als Objekt ein Initialobjekt.

Okay, so, das ist eine ganz sinnvolle und nützliche Beobachtung und die wird auch tatsächlich,

wenn man nachher über Satz über adjungierte Funkturen spricht, nochmal von Interesse sein, denke ich.

Wir hatten mit so einem kleineren Ergebnis Schluss gemacht, nämlich universelle Pfeile versus Hom-Funkturen.

Und da ist es so, dass also ein solcher Funktur, dessen Codomain-Set ist, repräsentierbar ist, wie das heißt.

Also natürlich isomorph zu einem Hom-Funktur, genau dann, wenn er einen universellen Pfeil aus eins hat.

Und das war sozusagen Ende der Beispiele und das nehme ich jetzt hier an der Stelle wieder auf, im Beweis.

Wir hatten nämlich schon angefangen, zunächst mal zu sehen, also wenn man zunächst mal nicht natürlich isomorph ist zu einem Hom-Funktur,

sondern wenn man Hom-Funktur hat, dann hat der einen universellen Pfeil aus eins.

Das ist sozusagen, wie man anfangen muss, das ist quasi das Beispiel, was wir noch hatten beim letzten Mal oder noch nicht ganz hatten.

Das heißt, da gucken wir uns jetzt sozusagen an, also so ein Hom-Funktur, der geht von der Kategorie A nach Z.

Ich wiederhole vielleicht nochmal für alle, die dies noch nicht gesehen haben, was der eigentlich macht.

Also auf Objekten von A liefert der das, was die Notation hier anzeigt, nämlich die Hom-Menge.

Und die schreibe ich immer so, dass ich die Kategorie schreibe und dann in Klammern x, y.

Manche Leute schreiben da auch Hom mit Index A, aber ich finde das zu lang.

Wenn man nur Hom schreibt, weiß man nicht, um welche Kategorie es geht und so ist es eigentlich prima.

Gut, und was macht das mit Morphismen?

Also wenn ich jetzt irgendwas habe, f von y nach y-Strich, dann brauche ich jetzt irgendwas, was zwischen den Hom-Mengen geht.

Also von A x, y, da muss jetzt also dieses A x, f nach A x, y-Strich gehen.

Das sind jetzt zwei Mengen, und hier leben irgendwelche Morphismen drin von der Kategorie A, die von x nach y gehen.

Das sind hier die Elemente dieser Menge.

Und naja, wenn man, also irgendwie zwingt einen die Natur schon, was ganz bestimmtes zu machen.

Ich habe was von x nach y und was von y nach y-Strich und ich muss was von x nach y-Strich geben.

Da ist es irgendwie klar, was man da machen muss, nämlich man muss die komponieren.

Das heißt also, wie erst f und dann h.

Das ist die Aktion von diesem Hom-Mengen auf Morphismen.

Gut, und jetzt will man also einen universellen Pfeil.

Das hatten wir uns auch schon überlegt.

Also wenn wir jetzt die eine elementige Menge hier angucken, eins, und wir möchten so einen universellen Pfeil haben in,

halt wir hatten hier, ja, lass' mal bei x, wie kommt man da zu so einem Element, was irgendwie ganz kanonisch naturgegeben ist?

Na ja, man setzt hier x ein und nimmt die Identität.

Das ist auch wieder irgendwie so was, was hier fällt.

Also das A0 ist sozusagen hier gleich x und das eta, das mappt dieses eine Element, was es da gibt, auf die Identität von dem Objekt x.

Also das x ist Teil des Hom-Punktors, weil das ist hier fest vorgegeben, sozusagen x ist ein A-Objekt hier.

So, soweit so gut. Jetzt wäre noch die Frage, warum ist das jetzt universell?

Das heißt also, gegeben haben wir jetzt, also die universelle Eigenschaft, das muss man noch prüfen.

So, gegeben ist dann also ein f, eine Abbildung, die geht von 1 nach a von x a.

Also das ist ein Element von der rechten Menge da, das heißt, was wir gegeben haben ist eigentlich ein Morphismus von x nach a.

Teil einer Videoserie :

Zugänglich über

Offener Zugang

Dauer

01:34:33 Min

Aufnahmedatum

2017-12-20

Hochgeladen am

2019-04-20 21:09:03

Sprache

de-DE

Die behandelten Themen bauen auf den Stoff von Algebra des Programmierens auf und vertieft diesen. 
Folgende weiterführende Themen werden behandelt:

  • Kategorie der CPOs; insbesondere freie CPOs, Einbettungen/Projektionen, Limes-Kolimes-Koinzidenz

  • Lokal stetige Funktoren und deren kanonische Fixpunkte; Lösung rekursiver Bereichsgleichungen insbesondere Modell des ungetyptes Lambda-Kalküls

  • freie Konstruktionen, universelle Pfeile und adjungierte Funktoren

  • Äquivalenzfunktoren

  • Monaden: Eilenberg-Moore und Kleisli-Kategorien; Freie Monaden; Becks Satz

  • evtl. Distributivgesetze, verallgemeinerte Potenzmengenkonstruktion und abstrakte GSOS-Regeln

  • evtl. Algebren und Monaden für Iteration

Lernziele und Kompetenzen:

 

Fachkompetenz Verstehen Die Studierenden erklären grundlegende Begriffe und Konzepte der Kategorientheorie und beschreiben Beispiele. Sie erklären außerdem grundlegende kategorielle Ergebnisse. Anwenden Die Studierenden wenden kategorientheoretische Konzepte und Ergebnisse an, um semantische Modelle für Programmiersprachen und Spezifikationsformalismen aufzustellen. Analysieren Die Studierenden analysieren kategorientheoretische Beweise, dieskutieren die entsprechende Argumentationen und legen diese schriftlich klar nieder. Lern- bzw. Methodenkompetenz Die Studieren lesen und verstehen Fachliteratur, die die Sprache der Kategorientheorie benutzt.
Sie sind in der Lage entsprechende mathematische Argumentationen nachzuvollziehen, zu erklären und selbst zu führen und schriftlich darzus
Einbetten
Wordpress FAU Plugin
iFrame
Teilen