Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Define Universal Property for Algebraic Structures #943

Open
felixwellen opened this issue Oct 12, 2022 · 1 comment
Open

Define Universal Property for Algebraic Structures #943

felixwellen opened this issue Oct 12, 2022 · 1 comment
Labels
discuss Should be discussed and possibly assigned in the next meeting new content New mathematical content refactor Refactorings, e.g. renaming, moving, rearranging...

Comments

@felixwellen
Copy link
Collaborator

There are lot's of universal properties in the algebra part of the library and we often use easy consequences of those, e.g. uniqueness of universal things. Unfortunately, it is not possible to use a definition from category theory, since that wouldn't be general enough in terms of universe levels. So it probably makes sense to have a specific definition for algebraic structures. This, however, could mean redefining some category theory with more general universe levels...
@felixwellen felixwellen added new content New mathematical content discuss Should be discussed and possibly assigned in the next meeting refactor Refactorings, e.g. renaming, moving, rearranging... labels Oct 12, 2022
@felixwellen felixwellen mentioned this issue Oct 12, 2022
Merged
@maxsnew
Copy link
Collaborator

maxsnew commented Feb 19, 2023

Why wouldn't the definition from category theory be general enough?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
discuss Should be discussed and possibly assigned in the next meeting new content New mathematical content refactor Refactorings, e.g. renaming, moving, rearranging...
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@maxsnew @felixwellen