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 H, consider some property P on morphisms f:A→B (such as being an equivalence, being étale, …), and consider the question of forming “the” (sub-)object [A,B]P of the internal hom [A,B] on those maps satisfying this condition.
Consider then the special case that H is local with sharp modality ♯. Then a candidate for the internal [A,B]P is the fiber product H(A,B)P×♯[A,B][A,B].
(Here H(A,B)P↪H(A,B) denotes the external space of maps satisfying P, regarded as “codiscretely” embedded back into H.)
Is that fiber product equivalent to what one ends up with a formulation of [A,B]P in the internal logic?
Interesting question; I think the answer is no. A map f:X→[A,B] corresponds to a map ˆf:X×A→B, hence to a map ˉf:X×A→X×B in H/X, and f factors through Equiv(A,B) just when ˉf is an equivalence in H/X. But I think f will factor through your fiber product just when the fiber of ˉf over each point of X is an equivalence, which is a weaker statement.
Yes, true, what I wrote sees only the global points. But assuming that A and B and hence also [A,B] are concrete, then it should work, right?
Why does concreteness of A and B help? It seems to me like the problem is possible non-concreteness (or maybe non-co-concreteness) of X.
So if A and B are concrete, then so is [A,B] and hence maps into it are characterized by maps into ♯[A,B], which are maps into [A,B] out of ♭(−), hence out of all points of the domain.
Where by “characterized by” you mean that the map from X→[A,B] to X→♯[A,B] is monic, so that two maps X→[A,B] are equal as soon as they become so when postcomposing with [A,B]→♯[A,B]; hence two maps X×A→X×B over X are equal as soon as they become so after pulling back along ♭X→X. Right? Why does that imply that a single map X×A→X×B over X is an equivalence as soon as it becomes so after pulling back to ♭X? A priori it seems that its inverse ♭X×B→♭X×A might not come from any map over X.
I see, thanks!
1 to 7 of 7