Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 7 of 7
In some topos , consider some property on morphisms (such as being an equivalence, being étale, …), and consider the question of forming “the” (sub-)object of the internal hom on those maps satisfying this condition.
Consider then the special case that is local with sharp modality . Then a candidate for the internal is the fiber product .
(Here denotes the external space of maps satisfying , regarded as “codiscretely” embedded back into .)
Is that fiber product equivalent to what one ends up with a formulation of in the internal logic?
Interesting question; I think the answer is no. A map corresponds to a map , hence to a map in , and factors through just when is an equivalence in . But I think will factor through your fiber product just when the fiber of over each point of is an equivalence, which is a weaker statement.
Yes, true, what I wrote sees only the global points. But assuming that and and hence also are concrete, then it should work, right?
Why does concreteness of and help? It seems to me like the problem is possible non-concreteness (or maybe non-co-concreteness) of .
So if and are concrete, then so is and hence maps into it are characterized by maps into , which are maps into out of , hence out of all points of the domain.
Where by “characterized by” you mean that the map from to is monic, so that two maps are equal as soon as they become so when postcomposing with ; hence two maps over are equal as soon as they become so after pulling back along . Right? Why does that imply that a single map over is an equivalence as soon as it becomes so after pulling back to ? A priori it seems that its inverse might not come from any map over .
I see, thanks!
1 to 7 of 7