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 75 of 75
Can a discrete object have a non-discrete subobject?
Not in the present of shape, right? What’s the context of the question? Just any concrete category with a left adjoint to the fiber functor?
I’m happy to assume the presence of shape. I thought the answer should be no, but I failed to produce an easy argument; maybe I’m just not awake?
Maybe it’s me who is not awake. I am thinking like this:
If A↪D and D is discrete, then for any X the set Hom(X,A) is naturally a subset of Hom(X,D), which is Hom(∫X,D). Hence Hom(X,A) is Hom(∫X,A) and so A is discrete.
I don’t follow, how do you know that a map X→A factors through ʃX?
Some other thoughts: subobjects of a discrete D are the same as maps D→Ω, hence maps D→♭Ω, and thus also to maps ♯D→♯Ω. By contrast, discrete subobjects of D are the same as codiscrete subobjects of ♯D, hence to maps D→Ω♯≔∑X:Ωis♯(X). So the question is equivalently whether the natural map ♯Ω→∑X:Ωis♯(X) is an equivalence, which externally is whether every subterminal object is codiscrete.
True, I have only argued so far that
Hom(∫(−),A)↪Hom(∫(−),D)↓↓≃Hom(−,A)↪Hom(−,D)hence that Hom(∫(−),A)→Hom(−,A) is mono. Sorry.
re #6: the issue of subterminal objects being codiscrete reminds me of what we discussed at Aufhebung where one considers whether ∅ is codiscrete. Seems to hold over cohesive sites.
Here’s something that can be said: suppose U is a subterminal object such that ♯U=1. Then also ♭U=1, since 1 is both discrete and codiscrete. But then the map ♭U→U implies that U=1 as well. In particular, if U and V are such that ♯(U=V), then also U=V. But ♯(U=V) isn’t the same as ♯U=♯V…
Could you maybe say what the bigger question is that you are after here?
I started out by wondering if H is cohesive over S, to what extent classicality properties of S carry over to H. For instance, if S satisfies AC, I think it follows that all discrete objects in H (including ℕ) are projective (though possibly not internally projective). Some other classicality principles like WLPO and MP are about subobjects of ℕ, so if all subobjects of a discrete object are discrete, then their truth in S would carry over to H.
I can show that every subobject of a discrete object is discrete under some additional hypotheses – basically, we have to make everything indexed over the base. Let Δ:𝒮→ℰ be a functor satisfying the following conditions:
Then, for each object I in 𝒮:
Indeed, πI0:ℰI→𝒮I preserves finite products, so it must preserve subterminal objects. The same argument applies to ΔI:𝒮I→ℰI and ΓI:ℰI→𝒮I. Thus, the canonical morphism ΓIX→πI0X is a strong epimorphism between subterminal objects in 𝒮I, so it must be an isomorphism. That in turn implies ΔΓX→X→Δπ0X is an isomorphism, but all three objects appearing there are subterminal objects in ℰI, so ΔΓX→X and X→Δπ0X are indeed isomorphisms.
Nice! Indexedness is not really an additional assumption, I think — if it isn’t automatic, we ought to be assuming it anyway when S is general. I think the real point is your use of the “pieces have points” axiom.
Johnstone has in his 2011 TAC paper on the nullstellensatz a theorem (3.4) that says that for 𝒮 with NNO a bounded p:ℰ→𝒮 satisfies the nullstellensatz iff p is locally connected, hyperconnected & local. One can then use the characterisation of hyperconnected morphisms in the elephant I p.226 that the image of p* is closed under subobjects. Johnstone has some discussion of the requirements involved and says that dispensation of NNO is probable, of boundedness problematic and gives an example with hyperconnected&local but not locally connected p which shows that the nullstellensatz is probably not really necessary.
Thanks for the pointer, Thomas! My first thought was that Johnstone’s argument ought to β-reduce to Zhen’s, but I’m having trouble making sense of it in the ∞-case when monos and “epis” (the relevant notion of epi being the effective ones) are not dual, whereas I think Zhen’s works fine in that case. Maybe they are actually different?
[…]
I have now formalized Zhen’s argument in #12 in the special case when I=1 (so the result is that all subterminals, i.e. hprops, are discrete). The code is here (unstable link). I expect that the general case should be a fairly straightforward generalization, replacing products by pullbacks.
I’m using the approach to comodalities with modules that I suggested a couple months ago here. Formalizing this argument required also proving a number of intermediate lemmas, such as that ♭ preserves products and hprops and equivalences. So far, I think the evidence is that this method works fairly well. There are a couple of wrinkles (including one bug in Coq that has to be worked around) which are discussed in the comments to the code, but once you get used to the boilerplate required, it’s not so bad; it feels to me basically like a more verbose sort of tactic language.
Nice!
A while back you said that you are in the process of reworking some HoTT libraries, including those for modalities, and that people who’d like to do coding in cohesive HoTT should wait until you’d be done with that. Is that now?
Pretty close. The basic theory of modalities and lex modalities is now in the main library. But I’m still feeling my way around the comodality modules, deciding on conventions, learning the tricks, and trying to make sure there are no other nasty surprises waiting to bite us down the road, which is why I haven’t submitted a pull request to put them in the main library yet. Formalizing this argument was a good experiment for that purpose; in fact it was how I discovered the bug in Coq.
I want to try to formalize a couple more sample results before saying definitely that I think this is the best way to do cohesion. One that’s on the table is the G-action on the Maurer-Cartan form that we constructed here, which you suggested in the other thread. Another possibility that comes to mind is the passage of G-actions to n-concretifications discussed here. However, of those the first uses only ♭ while the second uses only ♯; Zhen’s argument was a good example because it uses both ♭ and ʃ. Can you think of a good result to formalize that uses both ♭ and ♯ (or, if possible, all three)?
Here is an example involving all three:
consider difference between [ʃX,A] and [X,♭A]. With a suitable filtration chosen on ♭A then in good cases [ʃX,A] will be equivalent to the differential concretification of [X,♭A].
I know sufficient conditions in my main models. It’s long overdue to think about general abstract conditions.
In the main models we may consider for instance A=BG, with G 0-truncated and concrete, and then
[ʃX,A]≃♯−1[X,♭A]×♯−1[X,A][X,A](where, as a courtesy, I am sticking to your preferred numbering).
Very interesting! So you’re saying that in the models, for that pullback equation to hold, it suffices for G to be 0-truncated and concrete? Is there any chance that those conditions suffice abstractly?
I have to admit that I haven’t thought about this as abstractly as one could. I have been thinking about this in cases where A is given by Lie groups and deloopings of abelian Lie groups. But this is just me being lazy. I feel this should work much more generally.
But the connectedness in A=BG will be crucial. The fiber product on the right may be understood as taking care of the fact that ♭BG is not in general connected.
I’ll need to think about this more…
Can you say anything about how the proof goes, even in the case of Lie groups?
Actually in #20 I have oversimplified, one needs also non-flat connections to make this work.
Not sure if this is going to be useful for your purposes, but here is how it works:
for G a Lie group, write BGconn≔Ω1(−,𝔤)//G as usual. (We have a canonical map ♭BG→BGconn coming from the inclusion Ω1flat(−,𝔤)↪Ω1(−,𝔤).) Then for X a manifold, the issue with [X,BGconn] is that over some U this is maps U×X→BGconn, hence is connections on U×X. We’d like to restrict this to just a U-parameterized collection of connections on X, hence to a single connection on U×X which has however none of its connection forms parallel to U.
Now evaluating such connection on U×X on any point of U kills connection forms parallel to U. So ♯−1[X,BGconn] is over U the groupoid whose objects are smooth collections of connections on X, but whose morphisms are not-necessarily smoothly U-parameterized collections of gauge transformations between these. The fiber product
GConn(X)≔♯−1[X,BGconn]×♯1[X,BG][X,BG]fixes this by restricting the collections of gauge transformations again to be smooth. This is hence the correct moduli stack of G-connections on X. Now to restrict this in turn to the flat connections we take one more fiber product:
GFlatConn(X)≔♯[X,♭BG]×♯[X,BGconn]GConn(X).This is now the correct moduli stack of flat G-connections on X. So this is [∫X,BG].
Thanks. I’m not sure whether this will help, but I’d like to understand it anyway.
Now evaluating such connection on U×X on any point of U kills connection forms parallel to U. So ♯−1[X,BGconn] is over U the groupoid whose objects are smooth collections of connections on X
Can you explain that in more detail (or point me to where it is explained)? Why is that what ♯−1 does?
As for the abstract picture, you’re saying that we have a factorization of ♭BG→BG through some other object BGconn, such that
[ʃX,BG]=♯[X,♭BG]×♯[X,BGconn]♯−1[X,BGconn]×♯−1[X,BG][X,BG].This factorization ♭BG→BGconn→BG seems to be “dual” in some way to the factorization A→♯−1A→♯A. Why is it that we see only ♯−1 appearing and not other ♯n’s? Is it because G is 0-truncated (hence BG is 1-truncated)? Or is it because BG is 0-connected? Or because G is (−1)-concrete?
Is there any situation in which the oversimplified version would hold? I would expect that to be
[ʃX,A]=♯[X,♭A]×♯[X,A][X,A](omitting the ♯−1 in between ♯ and the identity, to correspond to also omitting the middle Aconn in between ♭A and A). I suppose this is true if A is the delooping of a (−1)-truncated group, but that case is rather trivial…
One thought: because ♯ is lex, the RHS ♯[X,♭A]×♯[X,A][X,A] of the oversimplified version is representable in HoTT as
∑f:X→A♯(∑g:X→♭Aε∘g=f).Motivated by this, we might rewrite the LHS as
∑f:X→A∑h:ʃX→Ah∘η=fso we are equivalently asking whether given f:X→A, the type of extensions of f to ʃX is equivalent to ♯ of the type of liftings of f to ♭A. That seems slightly odd; I don’t even see any reason why the former would be codiscrete. Is there even a canonical map from one side to the other?
I guess one more thing we can say is that since ♭A is discrete, maps into it factor uniquely through ʃX, so we have
(∑g:X→♭Aε∘g=f)=(∑g:ʃX→♭Aε∘g∘η=f).Unfortunately, since the coreflection ♭ is not “internal”, we can’t say internally that “every map ʃX→A factors through ♭A”. But we could say ♯[ʃX,A]=♯[ʃX,♭A], and the presence of the ♯ above seems to be suggesting a similar direction (I think since ♯ is lex, it “distributes” over Σ in a certain way). But, interestingly, if we had to go that way, it would push us back towards using ♯, rather than modules, to express the externality of ♭.
Here is more explanation (hopefully) of why that is what ♯−1 does. One place where I have written this elsewhere is section 2.3.2 of arXiv:1304.0236.
On 0-cells ♯−1[X,BGconn] gives the image of the map η:[X,BGconn]⟶♯[X,BGconn]. Over an object U of the site, this map takes a G-principal connection ∇U on X×U and sends it to the ♭U-parameterized collection of G-principal connections on X which are obtained by restricting ∇U to each point of U. Under this restriction to points in U the spurious components of ∇U (those connection forms which are non-zero on vectors tangent to U) disappear (are not in the image). So on 0-cells the image of η is those ♭U-parameterized collections of connections on X which vary smoothly with U, in that they do come from a smooth connection on U×X. In fact given such smooth collection of connections in the image, then there is a connection on U×X in the pre-image whose connection form has no component along U.
This is the correct image on 0-cells. But now the 1-cells are wrong. The 1-cells in ♯−1[X,BGconn] are those of ♯[X,BGconn] and hence are ♭U-parameterized collections of gauge transformations of connections, without smoothness constraint. That fiber product is to pick among these the smoothly parameterized collections of gauge transformations.
Now for the over-simplified version: in view of this one might think that ♯−1[X,♭BG] is the correct moduli stack of flat connections on X. But now the image of η:[X,♭BG]⟶♯[X,♭BG] is not all smoothly U-parameterized flat connections on X, but only those that come from restricting a flat connection on U×X to all points of U. The flatness constraint here also applies to the connection on U×X, and hence is a condition on how the connection may vary with U. This is an extra condition that one does not have in [∫X,BG] and hence this is not the right thing to do.
So instead to get it right one has to first build the correct moduli stack GConn(X) of all G-connections by that iterated fiber product, and then do one more fiber product to restrict the 0-cells of the result to be collections of flat connections.
Regarding the second question about the towers of truncations: yes, above only ♯−1 appeared because I assumed for simplicity that G is 0-truncated. When G is n-truncated, then we are to do an interated fiber product involving ♯−1 through to ♯n−1. The idea is to form ♯[X,BGconn] and then incrementally, working from the bottom to the top, enforce smooth structure on the collections of k-cells.
On the nLab this is indicated at differential concretification. I have been trying to polish this a bit more meanwhile, in section 4.3.6.4 of dcct (pdf).
In fact given such smooth collection of connections in the image, then there is a connection on U×X in the pre-image whose connection form has no component along U.
Ah, thanks, I think that this fact is what I was missing. I don’t usually think of the (−1)-image as involving the set-theoretic image of the action on 0-cells, but rather having the same 0-cells as the domain and the 1-cells (and higher cells) between them coming from the codomain. From that point of view, ♯−1[X,BGconn] has 0-cells that are connections on U×X and 1-cells that are ♭U-indexed (discontinuous) families of gauge transformations, and the point is that every connection on U×X is related by such a family of gauge transformations to one that is trivial in the U-direction, so that up to equivalence we might as well consider those to be the objects. (Does this depend on the fact that U is topologically contractible?)
Now let me see if I can figure out the fiber product by myself. The 0-cells of ♯−1[X,BG] are G-bundles over U×X (without connection), and its 1-cells are ♭U-indexed (discontinuous) families of bundle isomorphisms; while [X,BG] has the same 0-cells but 1-cells that are actual bundle isomorphisms over U×X. Thus, the 0-cells of the pullback might as well be the same as those of ♯−1[X,BGconn], while its 1-cells are discontinuous families of gauge transformations that underlie an actual bundle isomorphism.
So is the claim that a discontinuous families of gauge transformations that underlie an actual bundle isomorphism is automatically a continuous family as long as its domain and codomain are connections on U×X that are trivial in the U-direction?
One obstacle to doing any of this abstractly, of course, is the question of whether BGconn can be defined, or at least characterized, abstractly. Do you have any thoughts about that?
Regarding this pullback: yes, exactly, the pullback forces the possibly discontinues family of gauge transformations of the connection to have underlying it a smooth family of gauge transformations of the underlying bundles. But gauge transformations of connections are just those of the underlying bundles that respect the connection, so the effect is that the pullback on the 1-cells combines the property of families of gauge transformation to respect the connection and be smoothly varying.
Regarding BGconn: yes, I have thought about this a lot, and after doing so it seems to me that there is no general abstract characterization. What does exist is a good abstract definition B𝔾conn for abelian ∞-groups 𝔾, and then building objects of the form BGconn is a specific matter of lifting specific cocycles BG⟶B𝔾 to the differential refinement, i.e. the purpose of objects BGconn is to complete diagrams of the form
BGconn⟶B𝔾conn↓↓BG⟶B𝔾For the definition of B𝔾conn for abelian (or at least braided 𝔾) the best abstract picture I have is this: we are to make one choice, namely that of a filtration on ♭dRB2𝔾. When 𝔾=BnU(1) then ♭dRB2𝔾≃(Ω1→Ω2→⋯→Ωn+1cl) and the natural filtration is the standard Hodge filtration. In lowest degree this is Ωn+1cl. Generally then, write Ω2cl(−,𝔾) for the lowest degree of the chosen filtration.Then
B𝔾conn≔B𝔾×♭dRB2𝔾Ω2flat(−,𝔾).Hmm.
Is GG a typo?
Yes, sorry, I am still editing. The formulas don’t work in preview, so to check them I need to submit first. Sorry. Should be fixed now.
So you write 𝔾 when it is abelian and G when it is not?
Yes, I started doing that some time back. The rationale is that G is to stand for any group, clearly, and that the coefficient group here is generically something that over an analytic or algebraic site one would call the multiplicative group, which is often denoted 𝔾m.
Are there any good axioms that such a filtration satisfies, that we might be able to use to deduce the concretification result abstractly?
Yeah, I don’t know. It would be good to think about this more abstractly than I have so far.
Maybe it would help to turn this around and look for a systematic way to adjust [X,♭A] such as to become equivalent to [∫X,A]. Maybe there is a good abstract way to characterize the failure of the two to be equivalent and then maybe a way to systematically to correct that failure.
Phrased this way this looks like a question of general interest in the context of internal adjunctions. Might this have shown up in some disguise in the literature already?
Yes, I’ve been thinking in that direction too. Since ʃ is an internal reflector, we do have [X,♭A]=[ʃX,♭A], and a map [ʃX,♭A]→[ʃX,A], which becomes an equivalence upon applying ♯ (or, of course, ♭). But I’m not sure where to go from there.
If the above is anything to go by, then we should ask: Since it is an equivalence under ♯, but we want to produce an equivalence under ♯∞=id, how do we get there stagewise by ♯k-equivalences. Or something like this.
By the way, I should highlight: ♭B𝔾 is itself part of that Hodge filtration tower. The whole tower should be thought of as interpolating between B𝔾 and ♭B𝔾, by this tower of homotopy pullbacks:
♭B𝔾⟶*↓↓B𝔾conn⟶Ω2cl(−,𝔾)↓↓⋮⋮↓↓B𝔾θB𝔾⟶♭dRB2𝔾how do we get there stagewise by ♯k-equivalences
That makes sense. And since BG is concrete, so is [ʃX,BG], and that says that once k gets big enough we have an actual equivalence. Right?
That makes sense. And since BG is concrete, so is [ʃX,BG], and that says that once k gets big enough we have an actual equivalence. Right?
Keeping in mind that saying “BG is concrete” already involves some “filtered” concept of concreteness. When G is truncated then it becomes ♯k modal for large enough k simply by truncation. When G is 0-truncated and concrete and abelian then it makes sense to call all BnG concrete. But as soon is G has structure in more than one degree, one needs to apply something filtered to ask whether it is concrete.
By the way, coming back to the Hodge filtration business: one might ask what singles out the choice
Ωn+1cl→♭dRBn+1U(1)≃[Ω1→⋯→Ωn+1cl]of the first non-trivial stage in the filtration for BnU(1). And one relevant characteristic of this map might be this:
this is a map into ♭dRBn+1U(1) whith the property that
it goes out of a 0-truncated object;
it is a 1-epi “relative to manifolds”, in that for X any smooth manifold, then under [X,−] the map becomes a 1-epi.
(The second point reflecting the fact that over manifolds every de Rham hyper-cocycle is represented by a globally defined closed differential form.)
It would also seem to me that the map is uniquely characterized by this property, though I don’t have a proof for this. Mainly, I just don’t see how one would build a different map having these two properties.
So I am wondering if this aspect of the first stage in the filtration – being a 0-truncated atlas relative the given base object – is a hint for what the general abstract pattern should be.
What does ≃[Ω1→⋯→Ωn+1cl] mean?
I just don’t see how one would build a different map having these two properties.
What about the copairing Ωn+1cl+Ωn+1cl→♭dRBn+1U(1)?
True. Clearly I’d need to add some minimality condition.
it is a 1-epi “relative to manifolds”, in that for X any smooth manifold, then under [X,−] the map becomes a 1-epi.
If that is true when X=R, does it follow automatically for all manifolds?
Oh, I had missed #42:
here I am identifying sheaves of chain complexes of abelian group with the ∞-stacks which they represent under the Dold-Kan correspondence (followed by ∞-stackification).
So [Ω1→⋯→Ωn+1cl] is meant to denote the de Rham complex, truncated as indicated, being a sheaf of complexes of abelian groups (with Ω1 in degree n) and regarded as an ∞-stack. As such it is equivalent to the abstractly defined ∞-stack ♭dRBn+1U(1).
re #45:
no, I don’t think so. Over X=ℝ we have π0[X,♭dRBn+1U(1)]≃Hn+1dR(X)≃* and so the point already constitutes an atlas-relative-ℝ for ♭dRBn+1U(1).
Re 46, oh, I see. Thanks.
Re 47 okay. I’m having trouble imagining how a property having to do with manifolds would come into proving something about modalities; the only connection I could think of is that as we’ve discussed, sometimes ʃ is localization at RD and ♯ is localization at RC→RD, but if R isn’t enough then I don’t know how that would help.
Oh, so what I have in mind is that imposing these conditions for manifolds will make the statement true for X a manifold only.
Generally, the idea would be that it is unlikely that we could make the comparison be an equivalence in full generality, but we might have a chance if X is tame enough, reflected by the fact that relative to a class of objects that we may consider X to be a member of there is a suitably nice filtration on ♭A.
Sorry for this being so vague. I am just trying to feel my way from the form of the statement as I know it holds in one case in one kind of model to a possibly more general case.
So in the models, is the equivalence true for all X or only for manifolds?
It’s true for X a manifold, yes. Probably also for orbifolds etc. But I don’t know it more generally.
The arguments that I indicated above all work by representing the connection on U×X by a Cech cocycle with respecto to a good cover of X which trivially extends to a good cover of U×X, using that we may assume U≃ℝn.
Sorry, I should have been clearer about this.
Okay, got it. So since [X,−] preserves pullbacks, it should also be true that [X,B𝔾conn]→[X,B𝔾] is 1-epi when X is a manifold, right?
You know, this is an interesting research question, but neither of us sees immediately how to attack it, so maybe it’s not a good choice for a formalization test. Do you have any other ideas for a fairly simple result that uses both ♯ and ♭?
Hm, so far I have always only used ♯ for purposes of concretification. So right now I don’t seem to have a further suggestion. But I’ll think about it…
There aren’t any results about concretification that you already know abstract proofs of?
I use abstract results about concretification, but they don’t seem to mix in ♭ in an interesting way.
Abstract such results which I used include
the statement that Ω(𝔾Conn(X))≃(Ω𝔾)FlatConn(X), which follows from the definitions discussed above and the fact that looping commutes with ♯k up to shift in degree. Here ♭ is involved, but the proof of the statement doesn’t depend on it;
the statement that the Aut(X)-action on [X,B𝔾conn] passes to 𝔾Conn(X) – but you already provided the abstract proof of that recently, and again it only involves any filtration and for the proof it is irrelevant that it involves ♭.
Interesting — so in the abstract theory of cohesion, we don’t actually have any use yet for the relationship between ♯ and ♭?
Well, the interpretation of ♯ is of course crucially given by it being right adjoint to ♭, that’s what makes ♯−1 have the interpretation of concretification on 0-types, etc. So I wouldn’t say that there is no use of the relation between ♯ and ♭. But what is true is that I don’t yet see the appearance of a web of interrelations as for instance ∫ and ♭ exhibit in the differential hexagon. It may be noteworthy that for differential cohomology purposes the differential hexagon in itself wouldn’t help so much if we had no way to concretify the resulting moduli stacks of differential cocycles, so having the further right adjoint to ♭ is crucial, even if beyond this adjunction there is no further subtlety involved.
But only because I haven’t seen them yet of course doesn’t mean that further such phenomena don’t exist…
But in terms of the abstract theory of cohesion, i.e. before we do the interpretation as stacks, is there any application of the fact that ♭ and ♯ have any relationship whatsoever?
It matters that they do speak about the same concept of points. For 0-truncated objects X, A (for simplicity) the fact that we consider the concretification ♯−1A is because we want the object underlying A whose structure is detected by maps out of ♭X. The structure removed by passing from A to ♯−1A or equivalently by passing from X→A to ♭X→A is in both cases the very “differential cohomology” structure which the aim is to capture axiomatically. If ♭ and ♯ were not adjoint, there’d be no reason to consider ♯−1A as far as the axiomatization of differential cohomology is concerned.
Similarly for ∫ and ♭, the story started (if you recall) by observing that the statement of higher Galois theory is simply the statement that ♭ has a left adjoint at all, because this means that locally constant ∞-stacks are classified by representations of the the fundamental ∞-groupoid defined by ∫ thereby. Here, too, initially all the interest was in just having this adjunction at all. Only later did further additional neat implications of this adjunction appear. Even without them, I would still be interested in just the adjunction itself.
But let’s turn this around and look for further additional neat implications. For instance, also ♭ and ♯ should induce exact hexagons on stable homotopy types. Maybe we should look into those. While you work on formalizing their construction in HoTT, I’ll work on figuring out what they “mean”.
I understand very well that it matters intuitively. But what I’m hearing is that at a precise mathematical level, that axiom is not yet used.
I understand that you are hoping for something deeper, but what you refer to as intuitive statements are all little lemmas that do follow from the axiom. For instance that for X,A 0-truncated, then
♭[X,♯−1A]→♭[♭X,♭A]is a monomorphism, which is what expresses the intuitive meaning of concretification.
That’s the sort of statement I was looking for! Now I can go try to formalize that.
Hmm, here’s another thing that would be interesting to try to formalize: C3.6.11, the right adjoint part of a local geometric morphism preserves the Dedekind real numbers object RD. Internally, that would mean that if we construct “RD” entirely inside the codiscrete types, starting from ♯N, defining a codiscrete version of Q from that (which would probably automatically be equivalent to ♯Q), and then looking at cuts therein using Prop♯ for predicates and ∃♯ and ∨♯ as necessary, then the result would be equivalent to ♯(RD). This statement involves only ♯, but its proof must use ♭ too, since I doubt that RD is preserved by the left adjoint part of any old geometric inclusion. However, I don’t immediately have any idea how to prove it internally, since the proof in the Elephant is very external. Maybe it could be β-reduced into an internal one?
re #64, Ah, okay, I thought this would be a consequence of the adjunction too immediate to deserve special attention. But, okay, I see.
re #65: interesting, but i’d have no idea here. Hopefully Zhen Lin sees this.
insisting on #61: I still think that those exact hexagons are one of the coolest implications of cohesion. It would be fantastic if you could formalize them! I would prefer seeing you formalize the hexagon for (∫⊣♭), but if you rather look into (♭⊣♯) at the moment, they will induce exact hexagon’s, too, and they should be interesting, too.
Of course the hexagons are exact on stable types. Not sure if the internal characterization of them is already well enough understood? On the other hand, the proof of the exactness needs only one single lemma about stable types, namely the fiberwise characterization of pullbacks.
@Urs
Yes, I see the posts but I do not understand them (particularly the notation). I might think about it if someone could explain all the background (but perhaps in another conversation to avoid derailing the thread).
The notation?
(ʃ⊣♭⊣♯) denotes the adjoint triple of (co-)monads on the topos induced from the adjoint quadruple of functors that exhibits the cohesion;
♯k denotes the k-truncation of the unit of ♯;
♭dR denotes the homotopy fiber of the counit of ♭;
[−,−] denotes the internal hom; (:-)
What else?
This thread has already been pretty well derailed from its original topic (my fault I guess)…
Can you explain this k-truncation business so that an ordinary category theorist such as myself can understand? And also ∃♯ and ∨♯?
There is a factorization X→♯kX→♯X where the second map is k-truncated and the first is k-connected. By ∃♯ and ∨♯ I just mean to apply ♯ to the ordinary ∃ and ∨.
Urs, by a “stable type” you just mean a spectrum object, right? We know how to talk about those in principle (although not much about them has been formalized yet.) Or are you saying you want to use the more speculative “synthetic stable homotopy theory” instead (the internal language of a tangent topos)?
For the proof of exactness as I see it (at differential hexagon) we seem to need two properties:
homotopy fiber sequences are homotopy cofiber sequences (or whatever it takes to prove this lemma);
homotopy pullback squares need to be detected by equivalences beween the fibers of the horizontal morphisms over a fixed base point (for this proposition);
I’ll put the hexagon and its associated fracture squares on the to-do list, but it’ll be a little ways down because it requires first formalizing spectra and their fiber sequences. I’ve been working towards that, but it’s fiddly to set things up so that the non-strict-preservation of basepoints doesn’t make things intractable.
I think I have an idea about how to start 65 too. There should be a canonical map R→R♯ and hence ♯R→R♯; for the other direction a map R♯→♯R is the same as a map ♭R♯→♭♯R=♭R, hence to a map ♭R♯→R. That seems like it might be possible to construct.
Sure, sounds good!
1 to 75 of 75