39,020 reputation
246117
bio website
location
age
visits member for 3 years, 11 months
seen 6 hours ago

Jan
10
comment Why are only the first four alternating groups are non-simple?
It's too simple to be simple.
Jan
10
comment sSet is a model for Martin-lof type theory
I don't know. As I understand it, the large cardinal hypothesis is used to show that $\textbf{sSet}$ has universe types, and also to get around the problem of functoriality for substitution.
Jan
10
comment sSet is a model for Martin-lof type theory
According to Streicher, "simplicial sets organize into a model of Martin-Löf type theory. Moreover, we explain Voevodsky's Univalence Axiom which holds in this model and implements the idea that isomorphic types are identical as suggested in [HS]." But my point was that any model of homotopy type theory is in particular a model of intensional Martin-Löf type theory.
Jan
10
comment sSet is a model for Martin-lof type theory
Homotopy type theory is an extension of Martin–Löf type theory, so I suppose the answer is yes in principle...
Jan
9
answered Geometric interpretation of the fundamental theorem for coalgebras?
Jan
9
comment Geometric interpretation of the fundamental theorem for coalgebras?
Very interesting. I think you have to be a bit more modest about "any recursion equation" though; obviously we can only use algebraic operations.
Jan
9
comment spectral sequence computing invariants
I must be misunderstanding something, because the only $G$-action I can see on $H^i (Y, g_* F)$ is trivial...
Jan
9
comment Axiom of choice for infinite strictly descending chains of subsets.
What's your definition of infinite set?
Jan
9
comment Interesting verification of functoriality
Are you asking about when it is difficult to verify that a given pair of maps $\operatorname{ob} \mathcal{C} \to \operatorname{ob} \mathcal{D}$ and $\operatorname{mor} \mathcal{C} \to \operatorname{mor} \mathcal{D}$ is a functor? In that case I would say it boils down to how easy it is to compute the composition and equality of morphisms in $\mathcal{C}$ and $\mathcal{D}$. This can be extremely non-trivial, but the best example I know of is the bicategory of polynomials.
Jan
9
comment Definition of a diagram in a category
@Makoto I don't agree with any definition that says that a diagram is necessarily a substructure of a category. Like it or not, diagram is now a technical word in category theory, and it is a synonym for functor.
Jan
8
comment Definition of a diagram in a category
@Makoto I mean a diagram with one vertex and one non-identity arrow.
Jan
8
comment Definition of a diagram in a category
I don't agree. Let us suppose we have an endomorphism $X \to X$. Then $X \to X$ and $X ↺$ are two different diagrams. They even have different (co)limits. In some textbooks you will find an extremely general definition of diagram as a certain kind of homomorphism from a certain kind of graph, but I have never found a use for that.
Jan
8
comment Axiom of choice in set theory
The axiom of choice is not needed to pick one thing out of each bin if there are only ten bins, all of which are non-empty. That's actually a fairly straightforward consequence of the definition of non-emptiness. The problem is when you have infinitely many bins...
Jan
8
revised Interpretation of impure set theory within pure set theory?
deleted 178 characters in body; edited tags
Jan
8
comment Definition of a diagram in a category
Sure. It corresponds to a different diagram, namely one with fourth vertices and two arrows. The shape of the diagram is the shape of the indexing category and vice-versa.
Jan
8
comment Definition of a diagram in a category
No, of course not. The diagram $X \to Y$ corresponds to a functor $F : \mathbb{2} \to \mathcal{C}$, where $\mathbb{2}$ is the category with two objects and one non-identity morphism. Open any good category theory textbook and you will see why this is a reasonable definition.
Jan
8
comment complete partial order by adjoint functor theorem
Yeah, using the adjoint functor theorem to prove this is somehow overkill.
Jan
8
answered complete partial order by adjoint functor theorem
Jan
8
comment Definition of a diagram in a category
@MakotoKato That is the correct definition of diagram. Wikipedia is incorrect in saying that the index category is irrelevant, and your idea of defining it as a subcategory also does not work. (The functor associated to a diagram need not be injective or even faithful.)
Jan
8
answered Category objects