Discrete Category on Set is Discrete Category

From ProofWiki
Jump to navigation Jump to search


Work In Progress
In particular: Theorem can't be formulated atm, what is up now must move to Definition:Set Category (not to be confused with Definition:Category of Sets)
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by completing it.
To discuss this page in more detail, feel free to use the talk page.
When this work has been completed, you may remove this instance of {{WIP}} from the code.


Theorem

Let $S$ be a set.

Let $\map {\mathbf {Dis} } S$ be the discrete category on $S$.


Then $\map {\mathbf {Dis} } S$ determines a unique (up to isomorphism discrete category $\map {\mathbf {Dis} } S$ whose objects precisely comprise $S$.


This article is complete as far as it goes, but it could do with expansion.
In particular: That is, $\mathbf {Dis}: \mathbf {Set} \to \mathbf {Cat}$ is a functor (with left inverse $\mathbf {ob}$)
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding this information.
To discuss this page in more detail, feel free to use the talk page.
When this work has been completed, you may remove this instance of {{Expand}} from the code.
If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.


Proof


This needs considerable tedious hard slog to complete it.
In particular: Trivial.
To discuss this page in more detail, feel free to use the talk page.
When this work has been completed, you may remove this instance of {{Finish}} from the code.
If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.


$\blacksquare$


Sources

Retrieved from "https://proofwiki.org/w/index.php?title=Discrete_Category_on_Set_is_Discrete_Category&oldid=514218"