Welcome and we have one more of the housework left over, so to speak, half done, last time.
I said, you shouldn't explain that in the last five minutes, then I overdid it.
I would then get back to the point, so the thing with the proof details of the Limites,
and then hand it over to you for what was missing, namely universal property.
And then we close the door.
So, we want to come up front? Okay.
I don't know, double-wasted Limites.
Okay.
So.
So, last time we had shown that this equalizer E is a cone,
and now we want to show that it's the universal cone, in other words, the Limit.
So, we are going to say that suppose there is another cone,
which is going to be an object C with his morphism little c.
First of all, it's a cone on D, so you have a family of morphisms.
Yes, I'm getting there. I will make that same mistake.
And I want to, I've defined it like this so that we have now, this morphism here is from C to this product,
but the actual cone is from C to the diagram down here,
and the morphism for that is going to be a morphism C i, which is one of these,
with the projection here, but I've put them the wrong way around.
So, C i equals the projection of i with C.
So, this is our cone here with all the C i's.
C i's are given, and the C is the one that you get by taking the family of all C i's and taking the induced one.
So, you get one of the cones, and you get, this is the family of every D of i, or C of every D of i.
Yes, so now, so now what I want to show is that this C here, up here, must equalize these two.
So, by showing that, we show that C is an equalizer, and therefore there must be unique morphism between C and A.
So, we have that this here commutes, so we can use that to have, let me see, sorry, I'm trying to get my, so.
So.
There's still something missing that you probably will need now, and that's the definition of phi.
Because the square, the right hand's lower square, that's the definition of psi.
Oh, yeah.
I guess, and so the only thing that's missing is the, how phi is defined when you project to dj, and I think it maybe doesn't quite fit in the diagram,
or you draw an arrow around from the product of the i.
So, from here to here, you mean?
Right, on the outside of the square, if you want to put this on a one diagram.
So, this one.
Right, so there's something there, and that's the definition of phi, which.
So, that is.
So, that would be that where the ketamine of alpha is dj.
Right, exactly.
Yeah.
So, yes, we've got that, and we've got that psi, we've got also a definition of psi over here,
which is the projection of alpha with psi equals the diagonal version of alpha times the projection of the domain of alpha.
Okay, now we can use these two, and we want to find out what projection of alpha, phi, and the family of ci, which is c.
Well, this would be the projection of the codomain of alpha times the family of ci from our definition here,
and well, that would just be cj here.
And we also have the projection of alpha, psi, and the family ci equals, using this definition over here,
the diagonal alpha projection of the domain of alpha this time times the family ci,
which would be equal to the domain of times this.
Okay, and this shows us that...
Sorry, just a second.
Presenters
Zugänglich über
Offener Zugang
Dauer
01:37:02 Min
Aufnahmedatum
2017-11-20
Hochgeladen am
2019-04-20 10:59: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