Repository navigation
Conversation
|
Thank you for the PR! I will review it in the next days. But I will already submit a few quick comments in a moment. |
| - property: effective congruences | ||
| proof: The midpoint argument for <a href="/category/Ban">$\Ban$</a> works here, except that we skip the step of showing $R$ is closed. |
There was a problem hiding this comment.
When refering to other proofs, use labels and references.
Have a look how this is done e.g. in Mon.yaml with the property "regular subobject classifier" and the file CMon.yaml that references this proof.
The same remark applies to other proofs here that refer to Ban.
| - property: regular quotient object classifier | ||
| proof: >- | ||
| $\IC$ with its usual norm has exactly two regular quotients, $\{0\}$ and $\IC$. If an object $\Psi$ classified regular quotients, then $\Hom(\Psi, \IC)$ would have cardinality $2$. But this is impossible: if it contains $f \neq 0$, then it contains the distinct elements $0,f/2,f$. |
There was a problem hiding this comment.
For some proofs you refer to Ban because they are the same, but for some you repeat the argument, even though it is very similar. Why?
There was a problem hiding this comment.
sorry this was referring to the proof of regular subobject classifier
There was a problem hiding this comment.
Maybe Ban should be added as a related category, in both directions.
|
|
||
| satisfied_properties: | ||
| - property: locally small | ||
| proof: The forgetful functor to $\Vect_{\IC}$ is faithful, and $\Vect_{\IC}$ is locally small. |
There was a problem hiding this comment.
Having a faithful functor to a locally small category only settles locally essentially small.
Of course, this property is trivial nonetheless. I would phrase it like:
There is a forgetful functor $\SemiNormVect \to \Vect$ and $\Vect$ is locally small.
| name: category of semi-normed vector spaces with linear contractions | ||
| notation: $\SemiNormVect$ | ||
| objects: semi-normed vector spaces over $\IC$ | ||
| morphisms: linear maps $f$ satisfying $|f(x)| \leq |x|$ for every $x$ |
There was a problem hiding this comment.
| morphisms: linear maps $f$ satisfying $|f(x)| \leq |x|$ for every $x$ | |
| morphisms: linear contractions, i.e. linear maps $f$ satisfying $|f(x)| \leq |x|$ for every $x$ |
| proof: >- | ||
| The forgetful functor to vector spaces preserves finite limits and filtered colimits. We just need to show that the semi-norms agree. The case of empty limits is trivial. Now consider filtered diagrams $(X_i)$ and $(Y_i)$ with the same index category. | ||
|
|
||
| For equalizers, consider maps $f_i, g_i : X_i \to Y_i$ with equalizers $E_i\subseteq X_i$, and an element $x\in\colim_i E_i$. So $|x|$ is the infimum of $|x_i|_{X_i}$ taken over its representatives $x_i\in X_i$ such that $f_i(x_i)=g_i(x_i)$. Since the diagram is filtered, this is the same as the infimum over all representatives, which gives the semi-norm in $\colim_i X_i$. Hence the semi-norm agrees with that of the equalizer of $\colim_i f_i$ and $\colim_i g_i$. |
There was a problem hiding this comment.
for parallel arrows always use \rightrightarrows
2 participants
This adds SemiNormVect (no NormVect yet). All properties are decided.