Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorMike Shulman
   • CommentTimeJan 25th 2015
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexCan a discrete object have a non-discrete subobject?

   Can a discrete object have a non-discrete subobject?

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeJan 25th 2015
   • (edited Jan 25th 2015)
   • PermaLink
   Author: Urs
   Format: MarkdownItexNot 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?

   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?

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeJan 25th 2015
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI'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?

   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?

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeJan 25th 2015
   • PermaLink
   Author: Urs
   Format: MarkdownItexMaybe it's me who is not awake. I am thinking like this: If $A \hookrightarrow 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(\int X,D)$. Hence $Hom(X,A)$ is $Hom(\int X,A)$ and so $A$ is discrete.

   Maybe it’s me who is not awake. I am thinking like this:

   If $A \hookrightarrow 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(\int X,D)$. Hence $Hom(X,A)$ is $Hom(\int X,A)$ and so $A$ is discrete.

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeJan 25th 2015
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI don't follow, how do you know that a map $X\to A$ factors through $ʃ X$?

   I don’t follow, how do you know that a map $X\to A$ factors through $ʃ X$?

6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeJan 25th 2015
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexSome other thoughts: subobjects of a discrete $D$ are the same as maps $D\to \Omega$, hence maps $D \to \flat \Omega$, and thus also to maps $\sharp D \to \sharp \Omega$. By contrast, *discrete* subobjects of $D$ are the same as codiscrete subobjects of $\sharp D$, hence to maps $D \to \Omega_\sharp \coloneqq \sum_{X:\Omega} is\sharp(X)$. So the question is equivalently whether the natural map $\sharp \Omega \to \sum_{X:\Omega} is\sharp(X)$ is an equivalence, which externally is whether every subterminal object is codiscrete.

   Some other thoughts: subobjects of a discrete $D$ are the same as maps $D\to \Omega$, hence maps $D \to \flat \Omega$, and thus also to maps $\sharp D \to \sharp \Omega$. By contrast, discrete subobjects of $D$ are the same as codiscrete subobjects of $\sharp D$, hence to maps $D \to \Omega_\sharp \coloneqq \sum_{X:\Omega} is\sharp(X)$. So the question is equivalently whether the natural map $\sharp \Omega \to \sum_{X:\Omega} is\sharp(X)$ is an equivalence, which externally is whether every subterminal object is codiscrete.

7. • CommentRowNumber7.
   • CommentAuthorUrs
   • CommentTimeJan 25th 2015
   • PermaLink
   Author: Urs
   Format: MarkdownItexTrue, I have only argued so far that $$ \array{ Hom(\int(-),A) &\hookrightarrow& Hom(\int(-),D) \\ \downarrow && \downarrow^{\mathrlap{\simeq}} \\ Hom(-,A) &\hookrightarrow& Hom(-,D) } $$ hence that $Hom(\int(-),A) \to Hom(-,A)$ is mono. Sorry.

   True, I have only argued so far that

   $$\array{ Hom(\int(-),A) &\hookrightarrow& Hom(\int(-),D) \\ \downarrow && \downarrow^{\mathrlap{\simeq}} \\ Hom(-,A) &\hookrightarrow& Hom(-,D) }$$

   hence that $Hom(\int(-),A) \to Hom(-,A)$ is mono. Sorry.

8. • CommentRowNumber8.
   • CommentAuthorUrs
   • CommentTimeJan 25th 2015
   • PermaLink
   Author: Urs
   Format: MarkdownItexre #6: the issue of subterminal objects being codiscrete reminds me of what we discussed at _[[Aufhebung]]_ where one considers whether $\emptyset$ is codiscrete. Seems to hold over cohesive sites.

   re #6: the issue of subterminal objects being codiscrete reminds me of what we discussed at Aufhebung where one considers whether $\emptyset$ is codiscrete. Seems to hold over cohesive sites.

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeJan 25th 2015
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexHere's something that can be said: suppose $U$ is a subterminal object such that $\sharp U = 1$. Then also $\flat U = 1$, since $1$ is both discrete and codiscrete. But then the map $\flat U \to U$ implies that $U=1$ as well. In particular, if $U$ and $V$ are such that $\sharp (U=V)$, then also $U=V$. But $\sharp (U=V)$ isn't the same as $\sharp U = \sharp V$...

   Here’s something that can be said: suppose $U$ is a subterminal object such that $\sharp U = 1$. Then also $\flat U = 1$, since $1$ is both discrete and codiscrete. But then the map $\flat U \to U$ implies that $U=1$ as well. In particular, if $U$ and $V$ are such that $\sharp (U=V)$, then also $U=V$. But $\sharp (U=V)$ isn’t the same as $\sharp U = \sharp V$…

10. • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeJan 25th 2015
    • PermaLink
    Author: Urs
    Format: MarkdownItexCould you maybe say what the bigger question is that you are after here?

    Could you maybe say what the bigger question is that you are after here?

11. • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeJan 25th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI 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 $\mathbb{N}$) are projective (though possibly not internally projective). Some other classicality principles like WLPO and MP are about subobjects of $\mathbb{N}$, so if all subobjects of a discrete object are discrete, then their truth in $S$ would carry over to $H$.

    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 $\mathbb{N}$) are projective (though possibly not internally projective). Some other classicality principles like WLPO and MP are about subobjects of $\mathbb{N}$, so if all subobjects of a discrete object are discrete, then their truth in $S$ would carry over to $H$.

12. • CommentRowNumber12.
    • CommentAuthorZhen Lin
    • CommentTimeJan 26th 2015
    • (edited Jan 26th 2015)
    • PermaLink
    Author: Zhen Lin
    Format: MarkdownItexI 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 $\Delta : \mathcal{S} \to \mathcal{E}$ be a functor satisfying the following conditions: * $\mathcal{S}$ has finite limits and $\Delta : \mathcal{S} \to \mathcal{E}$ preserves them. * $\mathcal{E}$ has pullbacks along morphisms in the image of $\Delta : \mathcal{S} \to \mathcal{E}$. * The $\mathcal{S}$-indexed functor $\Delta : \mathbb{S} \to \mathbb{E}$ has an $\mathcal{S}$-indexed left adjoint $\pi_0 : \mathbb{E} \to \mathbb{S}$, i.e. for each object $I$ in $\mathcal{S}$, the functor $\Delta^I : \mathcal{S}^I \to \mathcal{E}^I$ has a left adjoint $\pi_0^I : \mathcal{E}^I \to \mathcal{S}^I$, where $\mathcal{S}^I = \mathcal{S}_{/ I}$ and $\mathcal{E}^I = \mathcal{E}_{/ \Delta I}$, and these moreover satisfy the evident Beck–Chevalley condition. * For each object $I$ in $\mathcal{S}$, the functor $\pi_0^I : \mathcal{E}^I \to \mathcal{S}^I$ preserves finite products. * $\Delta : \mathcal{S} \to \mathcal{E}$ is fully faithful. * The $\mathcal{S}$-indexed functor $\Delta : \mathbb{S} \to \mathbb{E}$ has an $\mathcal{S}$-indexed right adjoint $\Gamma : \mathbb{E} \to \mathbb{S}$. * For each object $I$ in $\mathcal{S}$, the components of the canonical natural transformation $\Gamma^I \Rightarrow \pi_0^I$ are strong epimorphisms in $\mathcal{S}^I$. Then, for each object $I$ in $\mathcal{S}$: * The functor $\pi_0^I : \mathcal{E}^I \to \mathcal{S}^I$ preserves subterminal objects. * If $X$ is a subteminal object in $\mathcal{E}^I$, then the counit $\Delta^I \Gamma^I X \to X$ and unit $X \to \Delta^I \pi_0^I X$ are isomorphisms in $\mathcal{E}^I$. * In particular, the functor $Sub_{\mathcal{E}} (\Delta I) \to Sub_{\mathcal{S}} (\pi_0 \Delta I)$ induced by $\pi_0 : \mathcal{E} \to \mathcal{S}$ is an equivalence of categories. Indeed, $\pi_0^I : \mathcal{E}^I \to \mathcal{S}^I$ preserves finite products, so it must preserve subterminal objects. The same argument applies to $\Delta^I : \mathcal{S}^I \to \mathcal{E}^I$ and $\Gamma^I : \mathcal{E}^I \to \mathcal{S}^I$. Thus, the canonical morphism $\Gamma^I X \to \pi_0^I X$ is a strong epimorphism between subterminal objects in $\mathcal{S}^I$, so it must be an isomorphism. That in turn implies $\Delta \Gamma X \to X \to \Delta \pi_0 X$ is an isomorphism, but all three objects appearing there are subterminal objects in $\mathcal{E}^I$, so $\Delta \Gamma X \to X$ and $X \to \Delta \pi_0 X$ are indeed isomorphisms.

    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 $\Delta : \mathcal{S} \to \mathcal{E}$ be a functor satisfying the following conditions:

    • $\mathcal{S}$ has finite limits and $\Delta : \mathcal{S} \to \mathcal{E}$ preserves them.
    • $\mathcal{E}$ has pullbacks along morphisms in the image of $\Delta : \mathcal{S} \to \mathcal{E}$.
    • The $\mathcal{S}$-indexed functor $\Delta : \mathbb{S} \to \mathbb{E}$ has an $\mathcal{S}$-indexed left adjoint $\pi_0 : \mathbb{E} \to \mathbb{S}$, i.e. for each object $I$ in $\mathcal{S}$, the functor $\Delta^I : \mathcal{S}^I \to \mathcal{E}^I$ has a left adjoint $\pi_0^I : \mathcal{E}^I \to \mathcal{S}^I$, where $\mathcal{S}^I = \mathcal{S}_{/ I}$ and $\mathcal{E}^I = \mathcal{E}_{/ \Delta I}$, and these moreover satisfy the evident Beck–Chevalley condition.
    • For each object $I$ in $\mathcal{S}$, the functor $\pi_0^I : \mathcal{E}^I \to \mathcal{S}^I$ preserves finite products.
    • $\Delta : \mathcal{S} \to \mathcal{E}$ is fully faithful.
    • The $\mathcal{S}$-indexed functor $\Delta : \mathbb{S} \to \mathbb{E}$ has an $\mathcal{S}$-indexed right adjoint $\Gamma : \mathbb{E} \to \mathbb{S}$.
    • For each object $I$ in $\mathcal{S}$, the components of the canonical natural transformation $\Gamma^I \Rightarrow \pi_0^I$ are strong epimorphisms in $\mathcal{S}^I$.

    Then, for each object $I$ in $\mathcal{S}$:

    • The functor $\pi_0^I : \mathcal{E}^I \to \mathcal{S}^I$ preserves subterminal objects.
    • If $X$ is a subteminal object in $\mathcal{E}^I$, then the counit $\Delta^I \Gamma^I X \to X$ and unit $X \to \Delta^I \pi_0^I X$ are isomorphisms in $\mathcal{E}^I$.
    • In particular, the functor $Sub_{\mathcal{E}} (\Delta I) \to Sub_{\mathcal{S}} (\pi_0 \Delta I)$ induced by $\pi_0 : \mathcal{E} \to \mathcal{S}$ is an equivalence of categories.

    Indeed, $\pi_0^I : \mathcal{E}^I \to \mathcal{S}^I$ preserves finite products, so it must preserve subterminal objects. The same argument applies to $\Delta^I : \mathcal{S}^I \to \mathcal{E}^I$ and $\Gamma^I : \mathcal{E}^I \to \mathcal{S}^I$. Thus, the canonical morphism $\Gamma^I X \to \pi_0^I X$ is a strong epimorphism between subterminal objects in $\mathcal{S}^I$, so it must be an isomorphism. That in turn implies $\Delta \Gamma X \to X \to \Delta \pi_0 X$ is an isomorphism, but all three objects appearing there are subterminal objects in $\mathcal{E}^I$, so $\Delta \Gamma X \to X$ and $X \to \Delta \pi_0 X$ are indeed isomorphisms.

13. • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeJan 26th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexNice! 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.

    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.

14. • CommentRowNumber14.
    • CommentAuthorThomas Holder
    • CommentTimeJan 26th 2015
    • PermaLink
    Author: Thomas Holder
    Format: MarkdownItexJohnstone has in his 2011 TAC paper on the nullstellensatz a theorem (3.4) that says that for $\mathcal{S}$ with NNO a bounded $p:\mathcal{E}\to\mathcal{S}$ 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.

    Johnstone has in his 2011 TAC paper on the nullstellensatz a theorem (3.4) that says that for $\mathcal{S}$ with NNO a bounded $p:\mathcal{E}\to\mathcal{S}$ 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.

15. • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeJan 26th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexThanks for the pointer, Thomas! My first thought was that Johnstone's argument ought to $\beta$-reduce to Zhen's, but I'm having trouble making sense of it in the $\infty$-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?

    Thanks for the pointer, Thomas! My first thought was that Johnstone’s argument ought to $\beta$-reduce to Zhen’s, but I’m having trouble making sense of it in the $\infty$-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?

16. • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeJan 27th 2015
    • (edited Jan 27th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItex[...]

    […]

17. • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 8th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI 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](https://github.com/mikeshulman/HoTT/blob/comodalities/theories/Cohesion/Shape.v#L47) (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](http://nforum.mathforge.org/discussion/6361/modules-for-comodalities). Formalizing this argument required also proving a number of intermediate lemmas, such as that $\flat$ 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.

    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 $\flat$ 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.

18. • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeFeb 10th 2015
    • PermaLink
    Author: Urs
    Format: MarkdownItexNice! 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?

    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?

19. • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 10th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexPretty 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](http://nforum.mathforge.org/discussion/6331/higher-penroseward-transform-in-cohesive-homotopy-theory/), which you suggested in the other thread. Another possibility that comes to mind is the passage of $G$-actions to $n$-concretifications discussed [here](http://nforum.mathforge.org/discussion/4576/nimage/). However, of those the first uses only $\flat$ while the second uses only $\sharp$; Zhen's argument was a good example because it uses both $\flat$ and $ʃ$. Can you think of a good result to formalize that uses both $\flat$ and $\sharp$ (or, if possible, all three)?

    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 $\flat$ while the second uses only $\sharp$; Zhen’s argument was a good example because it uses both $\flat$ and $ʃ$. Can you think of a good result to formalize that uses both $\flat$ and $\sharp$ (or, if possible, all three)?

20. • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeFeb 10th 2015
    • (edited Feb 10th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexHere is an example involving all three: consider difference between $[ʃ X,A]$ and $[X,\flat A]$. With a suitable filtration chosen on $\flat A$ then in good cases $[ʃ X,A]$ will be equivalent to the differential concretification of $[X,\flat 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 = \mathbf{B}G$, with $G$ 0-truncated and concrete, and then $$ [ʃ X,A] \simeq \sharp_{-1} [X,\flat A] \underset{\sharp_{-1} [X,A]}{\times} [X,A] $$ (where, as a courtesy, I am sticking to your preferred numbering).

    Here is an example involving all three:

    consider difference between $[ʃ X,A]$ and $[X,\flat A]$. With a suitable filtration chosen on $\flat A$ then in good cases $[ʃ X,A]$ will be equivalent to the differential concretification of $[X,\flat 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 = \mathbf{B}G$, with $G$ 0-truncated and concrete, and then

    $$[ʃ X,A] \simeq \sharp_{-1} [X,\flat A] \underset{\sharp_{-1} [X,A]}{\times} [X,A]$$

    (where, as a courtesy, I am sticking to your preferred numbering).

21. • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 10th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexVery 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?

    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?

22. • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeFeb 10th 2015
    • PermaLink
    Author: Urs
    Format: MarkdownItexI 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 = \mathbf{B}G$ will be crucial. The fiber product on the right may be understood as taking care of the fact that $\flat \mathbf{B}G$ is not in general connected. I'll need to think about this more...

    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 = \mathbf{B}G$ will be crucial. The fiber product on the right may be understood as taking care of the fact that $\flat \mathbf{B}G$ is not in general connected.

    I’ll need to think about this more…

23. • CommentRowNumber23.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 10th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexCan you say anything about how the proof goes, even in the case of Lie groups?

    Can you say anything about how the proof goes, even in the case of Lie groups?

24. • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeFeb 10th 2015
    • (edited Feb 10th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexActually 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 $\mathbf{B}G_{conn} \coloneqq \Omega^1(-,\mathfrak{g})/\!/G$ as usual. (We have a canonical map $\flat \mathbf{B}G \to \mathbf{B}G_{conn}$ coming from the inclusion $\Omega^1_{flat}(-,\mathfrak{g}) \hookrightarrow \Omega^1(-,\mathfrak{g})$.) Then for $X$ a manifold, the issue with $[X,\mathbf{B}G_{conn}]$ is that over some $U$ this is maps $U \times X \to \mathbf{B}G_{conn}$, hence is connections on $U \times X$. We'd like to restrict this to just a $U$-parameterized collection of connections on $X$, hence to a single connection on $U \times X$ which has however none of its connection forms parallel to $U$. Now evaluating such connection on $U \times X$ on any point of $U$ kills connection forms parallel to $U$. So $\sharp_{-1}[X,\mathbf{B}G_{conn}]$ 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 $$ G\mathbf{Conn}(X) \coloneqq \sharp_{-1}[X,\mathbf{B}G_{conn}] \underset{\sharp_1[X,\mathbf{B}G]}{\times} [X,\mathbf{B}G] $$ 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: $$ G\mathbf{FlatConn}(X) \coloneqq \sharp[X,\flat \mathbf{B}G] \underset{\sharp[X,\mathbf{B}G_{conn}]}{\times} G\mathbf{Conn}(X) \,. $$ This is now the correct moduli stack of flat $G$-connections on $X$. So this is $[\int X, \mathbf{B}G]$.

    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 $\mathbf{B}G_{conn} \coloneqq \Omega^1(-,\mathfrak{g})/\!/G$ as usual. (We have a canonical map $\flat \mathbf{B}G \to \mathbf{B}G_{conn}$ coming from the inclusion $\Omega^1_{flat}(-,\mathfrak{g}) \hookrightarrow \Omega^1(-,\mathfrak{g})$.) Then for $X$ a manifold, the issue with $[X,\mathbf{B}G_{conn}]$ is that over some $U$ this is maps $U \times X \to \mathbf{B}G_{conn}$, hence is connections on $U \times X$. We’d like to restrict this to just a $U$-parameterized collection of connections on $X$, hence to a single connection on $U \times X$ which has however none of its connection forms parallel to $U$.

    Now evaluating such connection on $U \times X$ on any point of $U$ kills connection forms parallel to $U$. So $\sharp_{-1}[X,\mathbf{B}G_{conn}]$ 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

    $$G\mathbf{Conn}(X) \coloneqq \sharp_{-1}[X,\mathbf{B}G_{conn}] \underset{\sharp_1[X,\mathbf{B}G]}{\times} [X,\mathbf{B}G]$$

    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:

    $$G\mathbf{FlatConn}(X) \coloneqq \sharp[X,\flat \mathbf{B}G] \underset{\sharp[X,\mathbf{B}G_{conn}]}{\times} G\mathbf{Conn}(X) \,.$$

    This is now the correct moduli stack of flat $G$-connections on $X$. So this is $[\int X, \mathbf{B}G]$.

25. • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 10th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexThanks. I'm not sure whether this will help, but I'd like to understand it anyway. > Now evaluating such connection on $U \times X$ on any point of $U$ kills connection forms parallel to $U$. So $\sharp_{-1}[X,\mathbf{B}G_{conn}]$ 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 $\sharp_{-1}$ does? As for the abstract picture, you're saying that we have a factorization of $\flat \mathbf{B}G \to \mathbf{B}G$ through some other object $\mathbf{B}G_{conn}$, such that $$[ʃX, \mathbf{B}G] = \sharp[X,\flat\mathbf{B}G] \underset{\sharp[X,\mathbf{B}G_{conn}]}{\times} \sharp_{-1}[X,\mathbf{B}G_{conn}] \underset{\sharp_{-1}[X,\mathbf{B}G]}{\times} [X,\mathbf{B}G]. $$ This factorization $\flat \mathbf{B}G \to \mathbf{B}G_{conn} \to \mathbf{B}G$ seems to be "dual" in some way to the factorization $A \to \sharp_{-1} A \to \sharp A$. Why is it that we see only $\sharp_{-1}$ appearing and not other $\sharp_n$'s? Is it because $G$ is 0-truncated (hence $\mathbf{B}G$ is 1-truncated)? Or is it because $\mathbf{B}G$ 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] = \sharp[X,\flat A] \underset{\sharp[X,A]}{\times} [X,A] $$ (omitting the $\sharp_{-1}$ in between $\sharp$ and the identity, to correspond to also omitting the middle $A_{conn}$ in between $\flat A$ and $A$). I suppose this is true if $A$ is the delooping of a $(-1)$-truncated group, but that case is rather trivial...

    Thanks. I’m not sure whether this will help, but I’d like to understand it anyway.

    Now evaluating such connection on $U \times X$ on any point of $U$ kills connection forms parallel to $U$. So $\sharp_{-1}[X,\mathbf{B}G_{conn}]$ 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 $\sharp_{-1}$ does?

    As for the abstract picture, you’re saying that we have a factorization of $\flat \mathbf{B}G \to \mathbf{B}G$ through some other object $\mathbf{B}G_{conn}$, such that

    $$[ʃX, \mathbf{B}G] = \sharp[X,\flat\mathbf{B}G] \underset{\sharp[X,\mathbf{B}G_{conn}]}{\times} \sharp_{-1}[X,\mathbf{B}G_{conn}] \underset{\sharp_{-1}[X,\mathbf{B}G]}{\times} [X,\mathbf{B}G].$$

    This factorization $\flat \mathbf{B}G \to \mathbf{B}G_{conn} \to \mathbf{B}G$ seems to be “dual” in some way to the factorization $A \to \sharp_{-1} A \to \sharp A$. Why is it that we see only $\sharp_{-1}$ appearing and not other $\sharp_n$’s? Is it because $G$ is 0-truncated (hence $\mathbf{B}G$ is 1-truncated)? Or is it because $\mathbf{B}G$ 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] = \sharp[X,\flat A] \underset{\sharp[X,A]}{\times} [X,A]$$

    (omitting the $\sharp_{-1}$ in between $\sharp$ and the identity, to correspond to also omitting the middle $A_{conn}$ in between $\flat A$ and $A$). I suppose this is true if $A$ is the delooping of a $(-1)$-truncated group, but that case is rather trivial…

26. • CommentRowNumber26.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 11th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexOne thought: because $\sharp$ is lex, the RHS $\sharp[X,\flat A] \underset{\sharp[X,A]}{\times} [X,A]$ of the oversimplified version is representable in HoTT as $$ \sum_{f:X\to A} \sharp\left( \sum_{g:X\to\flat A} \epsilon \circ g = f \right). $$ Motivated by this, we might rewrite the LHS as $$ \sum_{f:X\to A} \sum_{h:ʃX\to A} h\circ \eta = f $$ so we are equivalently asking whether given $f:X\to A$, the type of extensions of $f$ to $ʃX$ is equivalent to $\sharp$ of the type of liftings of $f$ to $\flat 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 $\flat A$ is discrete, maps into it factor uniquely through $ʃ X$, so we have $$ \left(\sum_{g:X\to\flat A} \epsilon \circ g = f\right) = \left(\sum_{g:ʃ X\to\flat A} \epsilon \circ g \circ \eta = f\right). $$ Unfortunately, since the coreflection $\flat$ is not "internal", we can't say internally that "every map $ʃX \to A$ factors through $\flat A$". But we could say $\sharp[ʃX,A] = \sharp[ʃX,\flat A]$, and the presence of the $\sharp$ above seems to be suggesting a similar direction (I think since $\sharp$ is lex, it "distributes" over $\Sigma$ in a certain way). But, interestingly, if we had to go that way, it would push us back towards using $\sharp$, rather than modules, to express the externality of $\flat$.

    One thought: because $\sharp$ is lex, the RHS $\sharp[X,\flat A] \underset{\sharp[X,A]}{\times} [X,A]$ of the oversimplified version is representable in HoTT as

    $$\sum_{f:X\to A} \sharp\left( \sum_{g:X\to\flat A} \epsilon \circ g = f \right).$$

    Motivated by this, we might rewrite the LHS as

    $$\sum_{f:X\to A} \sum_{h:ʃX\to A} h\circ \eta = f$$

    so we are equivalently asking whether given $f:X\to A$, the type of extensions of $f$ to $ʃX$ is equivalent to $\sharp$ of the type of liftings of $f$ to $\flat 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 $\flat A$ is discrete, maps into it factor uniquely through $ʃ X$, so we have

    $$\left(\sum_{g:X\to\flat A} \epsilon \circ g = f\right) = \left(\sum_{g:ʃ X\to\flat A} \epsilon \circ g \circ \eta = f\right).$$

    Unfortunately, since the coreflection $\flat$ is not “internal”, we can’t say internally that “every map $ʃX \to A$ factors through $\flat A$”. But we could say $\sharp[ʃX,A] = \sharp[ʃX,\flat A]$, and the presence of the $\sharp$ above seems to be suggesting a similar direction (I think since $\sharp$ is lex, it “distributes” over $\Sigma$ in a certain way). But, interestingly, if we had to go that way, it would push us back towards using $\sharp$, rather than modules, to express the externality of $\flat$.

27. • CommentRowNumber27.
    • CommentAuthorUrs
    • CommentTimeFeb 11th 2015
    • (edited Feb 11th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexHere is more explanation (hopefully) of why that is what $\sharp_{-1}$ does. One place where I have written this elsewhere is section 2.3.2 of [arXiv:1304.0236](http://arxiv.org/abs/1304.0236). On 0-cells $\sharp_{-1} [X, \mathbf{B}G_{conn}] $ gives the image of the map $\eta \colon [X, \mathbf{B}G_{conn}] \longrightarrow \sharp [X, \mathbf{B}G_{conn}]$. Over an object $U$ of the site, this map takes a $G$-principal connection $\nabla_U$ on $X\times U$ and sends it to the $\flat U$-parameterized collection of $G$-principal connections on $X$ which are obtained by restricting $\nabla_U$ to each point of $U$. Under this restriction to points in $U$ the spurious components of $\nabla_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 $\eta$ is those $\flat U$-parameterized collections of connections on $X$ which vary smoothly with $U$, in that they do come from a smooth connection on $U \times X$. In fact given such smooth collection of connections in the image, then there is a connection on $U \times 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 $\sharp_{-1} [X, \mathbf{B}G_{conn}]$ are those of $\sharp [X, \mathbf{B}G_{conn}]$ and hence are $\flat 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 $\sharp_{-1} [X, \flat \mathbf{B}G]$ is the correct moduli stack of flat connections on $X$. But now the image of $\eta \colon [X, \flat \mathbf{B}G] \longrightarrow \sharp [X, \flat \mathbf{B}G]$ is not all smoothly $U$-parameterized flat connections on $X$, but only those that come from restricting a flat connection on $U \times X$ to all points of $U$. The flatness constraint here also applies to the connection on $U \times 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 $[\int X, \mathbf{B}G]$ 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 $G\mathbf{Conn}(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.

    Here is more explanation (hopefully) of why that is what $\sharp_{-1}$ does. One place where I have written this elsewhere is section 2.3.2 of arXiv:1304.0236.

    On 0-cells $\sharp_{-1} [X, \mathbf{B}G_{conn}]$ gives the image of the map $\eta \colon [X, \mathbf{B}G_{conn}] \longrightarrow \sharp [X, \mathbf{B}G_{conn}]$. Over an object $U$ of the site, this map takes a $G$-principal connection $\nabla_U$ on $X\times U$ and sends it to the $\flat U$-parameterized collection of $G$-principal connections on $X$ which are obtained by restricting $\nabla_U$ to each point of $U$. Under this restriction to points in $U$ the spurious components of $\nabla_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 $\eta$ is those $\flat U$-parameterized collections of connections on $X$ which vary smoothly with $U$, in that they do come from a smooth connection on $U \times X$. In fact given such smooth collection of connections in the image, then there is a connection on $U \times 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 $\sharp_{-1} [X, \mathbf{B}G_{conn}]$ are those of $\sharp [X, \mathbf{B}G_{conn}]$ and hence are $\flat 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 $\sharp_{-1} [X, \flat \mathbf{B}G]$ is the correct moduli stack of flat connections on $X$. But now the image of $\eta \colon [X, \flat \mathbf{B}G] \longrightarrow \sharp [X, \flat \mathbf{B}G]$ is not all smoothly $U$-parameterized flat connections on $X$, but only those that come from restricting a flat connection on $U \times X$ to all points of $U$. The flatness constraint here also applies to the connection on $U \times 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 $[\int X, \mathbf{B}G]$ 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 $G\mathbf{Conn}(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.

28. • CommentRowNumber28.
    • CommentAuthorUrs
    • CommentTimeFeb 11th 2015
    • (edited Feb 11th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexRegarding the second question about the towers of truncations: yes, above only $\sharp_{-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 $\sharp_{-1}$ through to $\sharp_{n-1}$. The idea is to form $\sharp [X,\mathbf{B}G_{conn}]$ and then incrementally, working from the bottom to the top, enforce smooth structure on the collections of $k$-cells. On the $n$Lab this is indicated at _[differential concretification](http://ncatlab.org/nlab/show/concretification#ConcretificationOfDifferentialModuli)_. I have been trying to polish this a bit more meanwhile, in section 4.3.6.4 of dcct ([pdf](https://dl.dropboxusercontent.com/u/12630719/dcct.pdf)).

    Regarding the second question about the towers of truncations: yes, above only $\sharp_{-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 $\sharp_{-1}$ through to $\sharp_{n-1}$. The idea is to form $\sharp [X,\mathbf{B}G_{conn}]$ and then incrementally, working from the bottom to the top, enforce smooth structure on the collections of $k$-cells.

    On the $n$Lab 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).

29. • CommentRowNumber29.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 11th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex> In fact given such smooth collection of connections in the image, then there is a connection on $U \times 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, $\sharp_{-1}[X,\mathbf{B}G_{conn}]$ has 0-cells that are connections on $U\times X$ and 1-cells that are $\flat U$-indexed (discontinuous) families of gauge transformations, and the point is that every connection on $U\times 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 $\sharp_{-1}[X,\mathbf{B}G]$ are $G$-bundles over $U\times X$ (without connection), and its 1-cells are $\flat U$-indexed (discontinuous) families of bundle isomorphisms; while $[X,\mathbf{B}G]$ has the same 0-cells but 1-cells that are actual bundle isomorphisms over $U\times X$. Thus, the 0-cells of the pullback might as well be the same as those of $\sharp_{-1}[X,\mathbf{B}G_{conn}]$, 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\times X$ that are trivial in the $U$-direction?

    In fact given such smooth collection of connections in the image, then there is a connection on $U \times 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, $\sharp_{-1}[X,\mathbf{B}G_{conn}]$ has 0-cells that are connections on $U\times X$ and 1-cells that are $\flat U$-indexed (discontinuous) families of gauge transformations, and the point is that every connection on $U\times 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 $\sharp_{-1}[X,\mathbf{B}G]$ are $G$-bundles over $U\times X$ (without connection), and its 1-cells are $\flat U$-indexed (discontinuous) families of bundle isomorphisms; while $[X,\mathbf{B}G]$ has the same 0-cells but 1-cells that are actual bundle isomorphisms over $U\times X$. Thus, the 0-cells of the pullback might as well be the same as those of $\sharp_{-1}[X,\mathbf{B}G_{conn}]$, 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\times X$ that are trivial in the $U$-direction?

30. • CommentRowNumber30.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 11th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexOne obstacle to doing any of this abstractly, of course, is the question of whether $\mathbf{B}G_{conn}$ can be defined, or at least characterized, abstractly. Do you have any thoughts about that?

    One obstacle to doing any of this abstractly, of course, is the question of whether $\mathbf{B}G_{conn}$ can be defined, or at least characterized, abstractly. Do you have any thoughts about that?

31. • CommentRowNumber31.
    • CommentAuthorUrs
    • CommentTimeFeb 11th 2015
    • (edited Feb 11th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexRegarding 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 $\mathbf{B}G_{conn}$: 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 $\mathbf{B}\mathbb{G}_{conn}$ for abelian $\infty$-groups $\mathbb{G}$, and then building objects of the form $\mathbf{B}G_{conn}$ is a specific matter of lifting specific cocycles $\mathbf{B}G \longrightarrow \mathbf{B}\mathbb{G}$ to the differential refinement, i.e. the purpose of objects $\mathbf{B}G_{conn}$ is to complete diagrams of the form $$ \array{ \mathbf{B}G_{conn} &\longrightarrow& \mathbf{B}\mathbb{G}_{conn} \\ \downarrow && \downarrow \\ \mathbf{B}G &\longrightarrow& \mathbf{B}\mathbb{G} } $$ For the definition of $\mathbf{B}\mathbb{G}_{conn}$ for abelian (or at least braided $\mathbb{G}$) the best abstract picture I have is this: we are to make one choice, namely that of a filtration on $\flat_{dR} \mathbf{B}^2 \mathbb{G}$. When $\mathbb{G} = \mathbf{B}^n U(1)$ then $\flat_{dR} \mathbf{B}^2 \mathbb{G} \simeq (\Omega^1 \to \Omega^2 \to \cdots \to \Omega^{n+1}_{cl})$ and the natural filtration is the standard Hodge filtration. In lowest degree this is $\Omega^{n+1}_{cl}$. Generally then, write $\Omega^2_{cl}(-,\mathbb{G})$ for the lowest degree of the chosen filtration.Then $$ \mathbf{B}\mathbb{G}_{conn} \coloneqq \mathbf{B}\mathbb{G} \underset{\flat_{dR}\mathbf{B}^2 \mathbb{G}}{\times} \Omega^2_{flat}(-,\mathbb{G}) \,. $$

    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 $\mathbf{B}G_{conn}$: 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 $\mathbf{B}\mathbb{G}_{conn}$ for abelian $\infty$-groups $\mathbb{G}$, and then building objects of the form $\mathbf{B}G_{conn}$ is a specific matter of lifting specific cocycles $\mathbf{B}G \longrightarrow \mathbf{B}\mathbb{G}$ to the differential refinement, i.e. the purpose of objects $\mathbf{B}G_{conn}$ is to complete diagrams of the form

    $$\array{ \mathbf{B}G_{conn} &\longrightarrow& \mathbf{B}\mathbb{G}_{conn} \\ \downarrow && \downarrow \\ \mathbf{B}G &\longrightarrow& \mathbf{B}\mathbb{G} }$$

    For the definition of $\mathbf{B}\mathbb{G}_{conn}$ for abelian (or at least braided $\mathbb{G}$) the best abstract picture I have is this: we are to make one choice, namely that of a filtration on $\flat_{dR} \mathbf{B}^2 \mathbb{G}$. When $\mathbb{G} = \mathbf{B}^n U(1)$ then $\flat_{dR} \mathbf{B}^2 \mathbb{G} \simeq (\Omega^1 \to \Omega^2 \to \cdots \to \Omega^{n+1}_{cl})$ and the natural filtration is the standard Hodge filtration. In lowest degree this is $\Omega^{n+1}_{cl}$. Generally then, write $\Omega^2_{cl}(-,\mathbb{G})$ for the lowest degree of the chosen filtration.Then

    $$\mathbf{B}\mathbb{G}_{conn} \coloneqq \mathbf{B}\mathbb{G} \underset{\flat_{dR}\mathbf{B}^2 \mathbb{G}}{\times} \Omega^2_{flat}(-,\mathbb{G}) \,.$$
32. • CommentRowNumber32.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 11th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexHmm. Is $\mathbf{G}G$ a typo?

    Hmm.

    Is $\mathbf{G}G$ a typo?

33. • CommentRowNumber33.
    • CommentAuthorUrs
    • CommentTimeFeb 11th 2015
    • (edited Feb 11th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexYes, 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.

    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.

34. • CommentRowNumber34.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 11th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexSo you write $\mathbb{G}$ when it is abelian and $G$ when it is not?

    So you write $\mathbb{G}$ when it is abelian and $G$ when it is not?

35. • CommentRowNumber35.
    • CommentAuthorUrs
    • CommentTimeFeb 11th 2015
    • PermaLink
    Author: Urs
    Format: MarkdownItexYes, 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 $\mathbb{G}_m$.

    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 $\mathbb{G}_m$.

36. • CommentRowNumber36.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 11th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexAre there any good axioms that such a filtration satisfies, that we might be able to use to deduce the concretification result abstractly?

    Are there any good axioms that such a filtration satisfies, that we might be able to use to deduce the concretification result abstractly?

37. • CommentRowNumber37.
    • CommentAuthorUrs
    • CommentTimeFeb 11th 2015
    • PermaLink
    Author: Urs
    Format: MarkdownItexYeah, 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,\flat A]$ such as to become equivalent to $[\int 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?

    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,\flat A]$ such as to become equivalent to $[\int 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?

38. • CommentRowNumber38.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 11th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexYes, I've been thinking in that direction too. Since $ʃ$ is an internal reflector, we do have $[X,\flat A] = [ʃX,\flat A]$, and a map $[ʃX,\flat A] \to [ʃX, A]$, which becomes an equivalence upon applying $\sharp$ (or, of course, $\flat$). But I'm not sure where to go from there.

    Yes, I’ve been thinking in that direction too. Since $ʃ$ is an internal reflector, we do have $[X,\flat A] = [ʃX,\flat A]$, and a map $[ʃX,\flat A] \to [ʃX, A]$, which becomes an equivalence upon applying $\sharp$ (or, of course, $\flat$). But I’m not sure where to go from there.

39. • CommentRowNumber39.
    • CommentAuthorUrs
    • CommentTimeFeb 11th 2015
    • (edited Feb 12th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexIf the above is anything to go by, then we should ask: Since it is an equivalence under $\sharp$, but we want to produce an equivalence under $\sharp_\infty = id$, how do we get there stagewise by $\sharp_{k}$-equivalences. Or something like this. By the way, I should highlight: $\flat \mathbf{B}\mathbb{G}$ is itself part of that Hodge filtration tower. The whole tower should be thought of as interpolating between $\mathbf{B}\mathbb{G}$ and $\flat \mathbf{B}\mathbb{G}$, by this tower of homotopy pullbacks: $$ \array{ \flat \mathbf{B}\mathbb{G} &\longrightarrow& \ast \\ \downarrow && \downarrow \\ \mathbf{B}\mathbb{G}_{conn} &\longrightarrow& \Omega^2_{cl}(-,\mathbb{G}) \\ \downarrow && \downarrow \\ \vdots && \vdots \\ \downarrow && \downarrow \\ \mathbf{B}\mathbb{G} &\stackrel{\theta_{\mathbf{B}\mathbb{G}}}{\longrightarrow}& \flat_{dR}\mathbf{B}^2 \mathbb{G} } $$

    If the above is anything to go by, then we should ask: Since it is an equivalence under $\sharp$, but we want to produce an equivalence under $\sharp_\infty = id$, how do we get there stagewise by $\sharp_{k}$-equivalences. Or something like this.

    By the way, I should highlight: $\flat \mathbf{B}\mathbb{G}$ is itself part of that Hodge filtration tower. The whole tower should be thought of as interpolating between $\mathbf{B}\mathbb{G}$ and $\flat \mathbf{B}\mathbb{G}$, by this tower of homotopy pullbacks:

    $$\array{ \flat \mathbf{B}\mathbb{G} &\longrightarrow& \ast \\ \downarrow && \downarrow \\ \mathbf{B}\mathbb{G}_{conn} &\longrightarrow& \Omega^2_{cl}(-,\mathbb{G}) \\ \downarrow && \downarrow \\ \vdots && \vdots \\ \downarrow && \downarrow \\ \mathbf{B}\mathbb{G} &\stackrel{\theta_{\mathbf{B}\mathbb{G}}}{\longrightarrow}& \flat_{dR}\mathbf{B}^2 \mathbb{G} }$$
40. • CommentRowNumber40.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 11th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex> how do we get there stagewise by $\sharp_{k}$-equivalences That makes sense. And since $\mathbf{B}G$ is concrete, so is $[ʃX,\mathbf{B}G]$, and that says that once $k$ gets big enough we have an actual equivalence. Right?

    how do we get there stagewise by $\sharp_{k}$-equivalences

    That makes sense. And since $\mathbf{B}G$ is concrete, so is $[ʃX,\mathbf{B}G]$, and that says that once $k$ gets big enough we have an actual equivalence. Right?

41. • CommentRowNumber41.
    • CommentAuthorUrs
    • CommentTimeFeb 12th 2015
    • (edited Feb 12th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItex> That makes sense. And since $\mathbf{B}G$ is concrete, so is $[ʃX,\mathbf{B}G]$, and that says that once $k$ gets big enough we have an actual equivalence. Right? Keeping in mind that saying "$\mathbf{B}G$ is concrete" already involves some "filtered" concept of concreteness. When $G$ is truncated then it becomes $\sharp_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 $\mathbf{B}^n G$ 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 $$ \Omega^{n+1}_{cl} \to \flat_{dR}\mathbf{B}^{n+1} U(1) \simeq [\Omega^1 \to \cdots \to \Omega^{n+1}_{cl}] $$ of the first non-trivial stage in the filtration for $\mathbf{B}^n U(1)$. And one relevant characteristic of this map might be this: this is a map into $\flat_{dR}\mathbf{B}^{n+1} U(1)$ whith the property that 1. it goes out of a 0-truncated object; 1. 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.

    That makes sense. And since $\mathbf{B}G$ is concrete, so is $[ʃX,\mathbf{B}G]$, and that says that once $k$ gets big enough we have an actual equivalence. Right?

    Keeping in mind that saying “$\mathbf{B}G$ is concrete” already involves some “filtered” concept of concreteness. When $G$ is truncated then it becomes $\sharp_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 $\mathbf{B}^n G$ 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

    $$\Omega^{n+1}_{cl} \to \flat_{dR}\mathbf{B}^{n+1} U(1) \simeq [\Omega^1 \to \cdots \to \Omega^{n+1}_{cl}]$$

    of the first non-trivial stage in the filtration for $\mathbf{B}^n U(1)$. And one relevant characteristic of this map might be this:

    this is a map into $\flat_{dR}\mathbf{B}^{n+1} U(1)$ whith the property that

    1. it goes out of a 0-truncated object;

    2. 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.

42. • CommentRowNumber42.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 12th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexWhat does $\simeq [\Omega^1 \to \cdots \to \Omega^{n+1}_{cl}]$ mean?

    What does $\simeq [\Omega^1 \to \cdots \to \Omega^{n+1}_{cl}]$ mean?

43. • CommentRowNumber43.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 12th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex> I just don’t see how one would build a different map having these two properties. What about the copairing $\Omega^{n+1}_{cl}+\Omega^{n+1}_{cl} \to \flat_{dR}\mathbf{B}^{n+1} U(1)$?

    I just don’t see how one would build a different map having these two properties.

    What about the copairing $\Omega^{n+1}_{cl}+\Omega^{n+1}_{cl} \to \flat_{dR}\mathbf{B}^{n+1} U(1)$?

44. • CommentRowNumber44.
    • CommentAuthorUrs
    • CommentTimeFeb 12th 2015
    • PermaLink
    Author: Urs
    Format: MarkdownItexTrue. Clearly I'd need to add some minimality condition.

    True. Clearly I’d need to add some minimality condition.

45. • CommentRowNumber45.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 12th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex> 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?

    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?

46. • CommentRowNumber46.
    • CommentAuthorUrs
    • CommentTimeFeb 13th 2015
    • (edited Feb 13th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexOh, I had missed #42: here I am identifying sheaves of chain complexes of abelian group with the $\infty$-stacks which they represent under the Dold-Kan correspondence (followed by $\infty$-stackification). So $[\Omega^1 \to \cdots \to \Omega^{n+1}_{cl}]$ is meant to denote the de Rham complex, truncated as indicated, being a sheaf of complexes of abelian groups (with $\Omega^1$ in degree $n$) and regarded as an $\infty$-stack. As such it is equivalent to the abstractly defined $\infty$-stack $\flat_{dR}\mathbf{B}^{n+1}U(1)$.

    Oh, I had missed #42:

    here I am identifying sheaves of chain complexes of abelian group with the $\infty$-stacks which they represent under the Dold-Kan correspondence (followed by $\infty$-stackification).

    So $[\Omega^1 \to \cdots \to \Omega^{n+1}_{cl}]$ is meant to denote the de Rham complex, truncated as indicated, being a sheaf of complexes of abelian groups (with $\Omega^1$ in degree $n$) and regarded as an $\infty$-stack. As such it is equivalent to the abstractly defined $\infty$-stack $\flat_{dR}\mathbf{B}^{n+1}U(1)$.

47. • CommentRowNumber47.
    • CommentAuthorUrs
    • CommentTimeFeb 13th 2015
    • (edited Feb 13th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexre #45: no, I don't think so. Over $X = \mathbb{R}$ we have $\pi_0 [X, \flat_{dR}\mathbf{B}^{n+1}U(1)] \simeq H^{n+1}_{dR}(X) \simeq \ast$ and so the point already constitutes an atlas-relative-$\mathbb{R}$ for $\flat_{dR}\mathbf{B}^{n+1}U(1)$.

    re #45:

    no, I don’t think so. Over $X = \mathbb{R}$ we have $\pi_0 [X, \flat_{dR}\mathbf{B}^{n+1}U(1)] \simeq H^{n+1}_{dR}(X) \simeq \ast$ and so the point already constitutes an atlas-relative-$\mathbb{R}$ for $\flat_{dR}\mathbf{B}^{n+1}U(1)$.

48. • CommentRowNumber48.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 13th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexRe 46, oh, I see. Thanks.

    Re 46, oh, I see. Thanks.

49. • CommentRowNumber49.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 13th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexRe 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 $R_D$ and $\sharp$ is localization at $R_C \to R_D$, but if $R$ isn't enough then I don't know how that would help.

    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 $R_D$ and $\sharp$ is localization at $R_C \to R_D$, but if $R$ isn’t enough then I don’t know how that would help.

50. • CommentRowNumber50.
    • CommentAuthorUrs
    • CommentTimeFeb 16th 2015
    • PermaLink
    Author: Urs
    Format: MarkdownItexOh, 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 $\flat 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.

    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 $\flat 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.

51. • CommentRowNumber51.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 16th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexSo in the models, is the equivalence true for all $X$ or only for manifolds?

    So in the models, is the equivalence true for all $X$ or only for manifolds?

52. • CommentRowNumber52.
    • CommentAuthorUrs
    • CommentTimeFeb 16th 2015
    • PermaLink
    Author: Urs
    Format: MarkdownItexIt'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 \times X$ by a Cech cocycle with respecto to a good cover of $X$ which trivially extends to a good cover of $U \times X$, using that we may assume $U\simeq \mathbb{R}^n$. Sorry, I should have been clearer about this.

    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 \times X$ by a Cech cocycle with respecto to a good cover of $X$ which trivially extends to a good cover of $U \times X$, using that we may assume $U\simeq \mathbb{R}^n$.

    Sorry, I should have been clearer about this.

53. • CommentRowNumber53.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 17th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexOkay, got it. So since $[X,-]$ preserves pullbacks, it should also be true that $[X,\mathbf{B}\mathbb{G}_{conn}] \to [X,\mathbf{B}\mathbb{G}]$ is 1-epi when $X$ is a manifold, right?

    Okay, got it. So since $[X,-]$ preserves pullbacks, it should also be true that $[X,\mathbf{B}\mathbb{G}_{conn}] \to [X,\mathbf{B}\mathbb{G}]$ is 1-epi when $X$ is a manifold, right?

54. • CommentRowNumber54.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 17th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexYou 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 $\sharp$ and $\flat$?

    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 $\sharp$ and $\flat$?

55. • CommentRowNumber55.
    • CommentAuthorUrs
    • CommentTimeFeb 17th 2015
    • PermaLink
    Author: Urs
    Format: MarkdownItexHm, so far I have always only used $\sharp$ for purposes of concretification. So right now I don't seem to have a further suggestion. But I'll think about it...

    Hm, so far I have always only used $\sharp$ for purposes of concretification. So right now I don’t seem to have a further suggestion. But I’ll think about it…

56. • CommentRowNumber56.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 17th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexThere aren't any results about concretification that you already know abstract proofs of?

    There aren’t any results about concretification that you already know abstract proofs of?

57. • CommentRowNumber57.
    • CommentAuthorUrs
    • CommentTimeFeb 17th 2015
    • (edited Feb 17th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexI use abstract results about concretification, but they don't seem to mix in $\flat$ in an interesting way. Abstract such results which I used include - the statement that $\Omega (\mathbb{G}\mathbf{Conn}(X)) \simeq (\Omega\mathbb{G}) \mathbf{FlatConn}(X)$, which follows from the definitions discussed above and the fact that looping commutes with $\sharp_k$ up to shift in degree. Here $\flat$ is involved, but the proof of the statement doesn't depend on it; - the statement that the $\mathbf{Aut}(X)$-action on $[X,\mathbf{B}\mathbb{G}_{conn}]$ passes to $\mathbb{G}\mathbf{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 $\flat$.

    I use abstract results about concretification, but they don’t seem to mix in $\flat$ in an interesting way.

    Abstract such results which I used include

    • the statement that $\Omega (\mathbb{G}\mathbf{Conn}(X)) \simeq (\Omega\mathbb{G}) \mathbf{FlatConn}(X)$, which follows from the definitions discussed above and the fact that looping commutes with $\sharp_k$ up to shift in degree. Here $\flat$ is involved, but the proof of the statement doesn’t depend on it;

    • the statement that the $\mathbf{Aut}(X)$-action on $[X,\mathbf{B}\mathbb{G}_{conn}]$ passes to $\mathbb{G}\mathbf{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 $\flat$.

58. • CommentRowNumber58.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 18th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexInteresting --- so in the abstract theory of cohesion, we don't actually have any use yet for the relationship between $\sharp$ and $\flat$?

    Interesting — so in the abstract theory of cohesion, we don’t actually have any use yet for the relationship between $\sharp$ and $\flat$?

59. • CommentRowNumber59.
    • CommentAuthorUrs
    • CommentTimeFeb 18th 2015
    • PermaLink
    Author: Urs
    Format: MarkdownItexWell, the interpretation of $\sharp$ is of course crucially given by it being right adjoint to $\flat$, that's what makes $\sharp_{-1}$ have the interpretation of concretification on 0-types, etc. So I wouldn't say that there is no use of the relation between $\sharp$ and $\flat$. But what is true is that I don't yet see the appearance of a web of interrelations as for instance $\int$ and $\flat$ 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 $\flat$ 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...

    Well, the interpretation of $\sharp$ is of course crucially given by it being right adjoint to $\flat$, that’s what makes $\sharp_{-1}$ have the interpretation of concretification on 0-types, etc. So I wouldn’t say that there is no use of the relation between $\sharp$ and $\flat$. But what is true is that I don’t yet see the appearance of a web of interrelations as for instance $\int$ and $\flat$ 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 $\flat$ 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…

60. • CommentRowNumber60.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 18th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexBut 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 $\flat$ and $\sharp$ have any relationship whatsoever?

    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 $\flat$ and $\sharp$ have any relationship whatsoever?

61. • CommentRowNumber61.
    • CommentAuthorUrs
    • CommentTimeFeb 18th 2015
    • PermaLink
    Author: Urs
    Format: MarkdownItexIt 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 $\sharp_{-1}A$ is because we want the object underlying $A$ whose structure is detected by maps out of $\flat X$. The structure removed by passing from $A$ to $\sharp_{-1}A$ or equivalently by passing from $X \to A$ to $\flat X \to A$ is in both cases the very "differential cohomology" structure which the aim is to capture axiomatically. If $\flat$ and $\sharp$ were not adjoint, there'd be no reason to consider $\sharp_{-1}A$ as far as the axiomatization of differential cohomology is concerned. Similarly for $\int$ and $\flat$, the story started (if you recall) by observing that the statement of higher Galois theory is simply the statement that $\flat$ has a left adjoint at all, because this means that locally constant $\infty$-stacks are classified by representations of the the fundamental $\infty$-groupoid defined by $\int$ 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 $\flat$ and $\sharp$ 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".

    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 $\sharp_{-1}A$ is because we want the object underlying $A$ whose structure is detected by maps out of $\flat X$. The structure removed by passing from $A$ to $\sharp_{-1}A$ or equivalently by passing from $X \to A$ to $\flat X \to A$ is in both cases the very “differential cohomology” structure which the aim is to capture axiomatically. If $\flat$ and $\sharp$ were not adjoint, there’d be no reason to consider $\sharp_{-1}A$ as far as the axiomatization of differential cohomology is concerned.

    Similarly for $\int$ and $\flat$, the story started (if you recall) by observing that the statement of higher Galois theory is simply the statement that $\flat$ has a left adjoint at all, because this means that locally constant $\infty$-stacks are classified by representations of the the fundamental $\infty$-groupoid defined by $\int$ 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 $\flat$ and $\sharp$ 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”.

62. • CommentRowNumber62.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 18th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI 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 very well that it matters intuitively. But what I’m hearing is that at a precise mathematical level, that axiom is not yet used.

63. • CommentRowNumber63.
    • CommentAuthorUrs
    • CommentTimeFeb 18th 2015
    • (edited Feb 18th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexI 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 $$ \flat[X, \sharp_{-1} A] \to \flat [\flat X, \flat A] $$ is a monomorphism, which is what expresses the intuitive meaning of concretification.

    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

    $$\flat[X, \sharp_{-1} A] \to \flat [\flat X, \flat A]$$

    is a monomorphism, which is what expresses the intuitive meaning of concretification.

64. • CommentRowNumber64.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 19th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex*That's* the sort of statement I was looking for! Now I can go try to formalize that.

    That’s the sort of statement I was looking for! Now I can go try to formalize that.

65. • CommentRowNumber65.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 19th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexHmm, 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 $R_D$. Internally, that would mean that if we construct "$R_D$" entirely inside the codiscrete types, starting from $\sharp N$, defining a codiscrete version of $Q$ from that (which would probably automatically be equivalent to $\sharp Q$), and then looking at cuts therein using $Prop_\sharp$ for predicates and $\exists_\sharp$ and $\vee_\sharp$ as necessary, then the result would be equivalent to $\sharp (R_D)$. This *statement* involves only $\sharp$, but its proof must use $\flat$ too, since I doubt that $R_D$ 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 $\beta$-reduced into an internal one?

    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 $R_D$. Internally, that would mean that if we construct “$R_D$” entirely inside the codiscrete types, starting from $\sharp N$, defining a codiscrete version of $Q$ from that (which would probably automatically be equivalent to $\sharp Q$), and then looking at cuts therein using $Prop_\sharp$ for predicates and $\exists_\sharp$ and $\vee_\sharp$ as necessary, then the result would be equivalent to $\sharp (R_D)$. This statement involves only $\sharp$, but its proof must use $\flat$ too, since I doubt that $R_D$ 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 $\beta$-reduced into an internal one?

66. • CommentRowNumber66.
    • CommentAuthorUrs
    • CommentTimeFeb 19th 2015
    • (edited Feb 19th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexre #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 $(\int \dashv \flat)$, but if you rather look into $(\flat \dashv \sharp)$ 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](http://ncatlab.org/nlab/show/homotopy%20pullback#FiberwiseRecognitionInStableCase).

    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 $(\int \dashv \flat)$, but if you rather look into $(\flat \dashv \sharp)$ 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.

67. • CommentRowNumber67.
    • CommentAuthorZhen Lin
    • CommentTimeFeb 19th 2015
    • PermaLink
    Author: Zhen Lin
    Format: MarkdownItex@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).

    @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).

68. • CommentRowNumber68.
    • CommentAuthorUrs
    • CommentTimeFeb 19th 2015
    • (edited Feb 19th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexThe notation? * $(ʃ \dashv \flat \dashv \sharp)$ denotes the adjoint triple of (co-)monads on the topos induced from the adjoint quadruple of functors that exhibits the cohesion; * $\sharp_k$ denotes the $k$-truncation of the unit of $\sharp$; * $\flat_{dR}$ denotes the homotopy fiber of the counit of $\flat$; * $[-,-]$ denotes the internal hom; (:-) What else?

    The notation?

    • $(ʃ \dashv \flat \dashv \sharp)$ denotes the adjoint triple of (co-)monads on the topos induced from the adjoint quadruple of functors that exhibits the cohesion;

    • $\sharp_k$ denotes the $k$-truncation of the unit of $\sharp$;

    • $\flat_{dR}$ denotes the homotopy fiber of the counit of $\flat$;

    • $[-,-]$ denotes the internal hom; (:-)

    What else?

69. • CommentRowNumber69.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 19th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexThis thread has already been pretty well derailed from its original topic (my fault I guess)...

    This thread has already been pretty well derailed from its original topic (my fault I guess)…

70. • CommentRowNumber70.
    • CommentAuthorZhen Lin
    • CommentTimeFeb 19th 2015
    • PermaLink
    Author: Zhen Lin
    Format: MarkdownItexCan you explain this $k$-truncation business so that an ordinary category theorist such as myself can understand? And also $\exists_\sharp$ and $\vee_\sharp$?

    Can you explain this $k$-truncation business so that an ordinary category theorist such as myself can understand? And also $\exists_\sharp$ and $\vee_\sharp$?

71. • CommentRowNumber71.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 19th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexThere is a [[n-connected object of an (infinity,1)-topos|factorization]] $X \to \sharp_k X \to \sharp X$ where the second map is [[n-truncated object of an (infinity,1)-category|k-truncated]] and the first is [[n-connected object of an (infinity,1)-topos|k-connected]]. By $\exists_\sharp$ and $\vee_\sharp$ I just mean to apply $\sharp$ to the ordinary $\exists$ and $\vee$.

    There is a factorization $X \to \sharp_k X \to \sharp X$ where the second map is k-truncated and the first is k-connected. By $\exists_\sharp$ and $\vee_\sharp$ I just mean to apply $\sharp$ to the ordinary $\exists$ and $\vee$.

72. • CommentRowNumber72.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 19th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexUrs, 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)?

    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)?

73. • CommentRowNumber73.
    • CommentAuthorUrs
    • CommentTimeFeb 19th 2015
    • (edited Feb 19th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexFor the proof of exactness as I see it (at [[differential hexagon]]) we seem to need two properties: 1. homotopy fiber sequences are homotopy cofiber sequences (or whatever it takes to prove [this lemma](http://ncatlab.org/nlab/show/differential+cohomology+diagram#ReconstructionOfFractureSquare)); 1. homotopy pullback squares need to be detected by equivalences beween the fibers of the horizontal morphisms over a fixed base point (for [this proposition](http://ncatlab.org/nlab/show/differential+cohomology+diagram#TheDifferentialFractureSquare));

    For the proof of exactness as I see it (at differential hexagon) we seem to need two properties:

    1. homotopy fiber sequences are homotopy cofiber sequences (or whatever it takes to prove this lemma);

    2. homotopy pullback squares need to be detected by equivalences beween the fibers of the horizontal morphisms over a fixed base point (for this proposition);

74. • CommentRowNumber74.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 19th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI'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 \to R_\sharp$ and hence $\sharp R \to R_\sharp$; for the other direction a map $R_\sharp \to \sharp R$ is the same as a map $\flat R_\sharp \to \flat\sharp R = \flat R$, hence to a map $\flat R_\sharp \to R$. That seems like it might be possible to construct.

    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 \to R_\sharp$ and hence $\sharp R \to R_\sharp$; for the other direction a map $R_\sharp \to \sharp R$ is the same as a map $\flat R_\sharp \to \flat\sharp R = \flat R$, hence to a map $\flat R_\sharp \to R$. That seems like it might be possible to construct.

75. • CommentRowNumber75.
    • CommentAuthorUrs
    • CommentTimeFeb 19th 2015
    • PermaLink
    Author: Urs
    Format: MarkdownItexSure, sounds good!

    Sure, sounds good!