I have tried to brush-up *Kleisli category*; also made *Kleisli composition* redirect to it and cross-linked with *monad (in computer science)*

at *monoidal adjunction* the second item says

while the left adjoint is necessarily strong

but should it not say

while the left adjoint is necessarily oplax

?

]]>Warning: What follows is just trivia. But since we had related discussion here before, maybe I am excused to waste time with this.

Way back, we (maybe mostly Mike and me) had agreed on symbols for the three modalities of cohesion – $ʃ, \flat, \sharp$ – and seemed to have been happy with ever since.

Moreover, in the last months I have been stabilizing myself on writing $\Re$ and $\Im$ for the reduction modality and the infinitesimal flat modality of differential cohesion. The choice of $\Re$ works really well, I think, both with the “re” in “reduction” as well as with the intuitive meaning that the reduced types are what is *real* about a formal geometry. This suggests to use $\Im$ for one of the other two. It doesn’t really seem to work for the infinitesimal shape, but using it for infinitesimal flat seems okay.

In any case, that leaves the infinitesimal shape modality in need of a good symbol.

Originally (and still on several $n$Lab pages) I had denoted it $\mathbf{\Pi}_{inf}$, alluding to the fact that it produces “infinitesimal path $\infty$-groupoids”. I still think that’s a great way to think about it, but since finite shape has come to be called $ʃ$ and also since now the other two differential modalities don’t carry an ${}_{inf}$-subscript anymore, it feels a bit anachronistic now.

Better would be one single nice symbol for infinitesimal shape. Which one?

One idea I have is this: the modal types of infinitesimal shape in the slice over $X$ are precisely the (formally) *étale* types over $X$. Maybe there is a nice 1-symbol reflection of “étale”.

And there is, of sorts: a ligature of the two letters “et” is what became “&”. Aren’t there also some other versions of a ligature of “et” somewhere in the common TeX collection of symbols?

]]>I added the definition of uniform space in terms of covering families. But I don’t know the covering version of the constructive “axiom (0)”.

]]>I was in the differential cohesion group at the HOTT MRC last week and one thing we struggled with was that we only knew one model (sheaves over formally thickened Cartesian space) which is pretty complicated to construct. Also this specific model has extra properties so not all of the axiomatics can really be explained with just one model, for instance Felix told me that every object in this topos is formally smooth.

Plain cohesion, on the other hand, has some very elementary toy models like reflexive graphs and the sierpinski topos that are very nice for getting intuition.

Do we have any analogous toy models for differential cohesion? All the better if they are “thickenings” of sierpinski or reflexive graphs. Ideas are also welcome, I’d be happy to work through some details myself.

]]>created *arithmetic jet space*, so far only highlighting the statement that at prime $p$ these are $X \underset{Spec(\mathbb{Z})}{\times}Spec(\mathbb{Z}_p)$ (regarded so in Borger’s absolute geometry by applying the Witt ring construction $(W_n)_\ast$ to it).

This is what I had hoped that the definition/characterization would be, so I am relieved. Because this is of course just the definition of synthetic differential geometry with $Spec(\mathbb{Z}_p)$ regarded as the $p$th abstract formal disk.

Well, or at least this is what Buium defines. Borger instead calls $(W_n)_\ast$ itself already the arithmetic jet space functor. I am not sure yet if I follow that.

I am hoping to realize the following: in ordinary differential geometry then synthetic differential infinity-groupoids is cohesive over “formal moduli problems” and here the flat modality $\flat$ is exactly the analog of the above “jet space” construction, in that it evaluates everything on formal disks. Moreover, $\flat$ canonically sits in a fracture suare together with the “cohesive rationalization” operation $[\Pi_{dR}(-),-]$ and hence plays exactly the role of the arithmetic fracture square, but in smooth geometry. I am hoping that Borger’s absolute geometry may be massaged into a cohesive structure over the base $Et(Spec(\mathbb{F}_1))$ that makes the cohesive fracture square reproduce the arithmetic one.

If Borger’s absolute direct image were base change to $Spec(\mathbb{Z}_p)$ followed by the Witt vector construction, then this would come really close to being true. Not sure what to make of it being just that Witt vector construction. Presently I have no real idea of what good that actually is (apart from giving any base topos for $Et(Spec(Z))$, fine, but why this one? Need to further think about it.)

]]>while writing out the proof of the fundamental product theorem in K-theory I had occasion to record that

]]>Created doctrinal adjunction. The page could probably use some examples and/or fleshing out.

]]>I put a disambiguation block at the top of inverse image to point to preimage.

]]>created *induced metric*, just for completeness

The page regular monomorphism includes a proof that all monomorphisms in Grp are regular, and I was wondering whether the statement holds for group objects in a topos. Does anyone know about this? The proof given on that page doesn’t look constructive enough for it to transport over to the topos setting.

For a comparison, I think one can prove that epimorphisms of groups in a topos $E$ are regular. Here’s a sketch. Every epimorphism $e$ in $Grp(E)$ has a (regular epi)-mono factorization $e = i p$ where $p$ is the projection $G \to G/\ker(e)$ and $i$ is here both monic and epic, so it suffices to prove that mono-epis in $Grp(E)$ are isomorphisms. So let $i: H \to G$ be a mono-epi in $Grp(E)$; we want to prove that $G/H \cong 1$ in $E$. It will suffice to prove that for any abelian group $A$ in $E$ and any map $j: G/H \to A$ in $E$, the composite

$G \stackrel{\pi}{\to} G/H \stackrel{j}{\to} A$is a constant (factors through $1$). Form the exponential $A^G$ of $A, G$ as objects of $E$, give $A^G$ the pointwise abelian group structure, and let $G$ act on $A^G$ by the formula $(g \cdot f)(g') = f(g' g^{-1})$ so that $A^G$ is a $G$-module. An element $f$ of $A^G$ is a constant precisely when it is a fixed point under the $G$-action, i.e., when $(\forall_g)\; g \cdot f - f = 0$, so it will suffice to show this equation holds for all $f = j \pi$ as displayed above.

Now for any element $f$ of $A^G$, the map $\phi_f: G \to A^G$ defined by $\phi_f(g) = g \cdot f - f$ is a derivation, so that the map into the wreath product $u: G \to A^G \rtimes G$ defined by $u(g) = (\phi_f(g), g)$ is a homomorphism. So is the map $v: G \to A^G \rtimes G$ defined by $v(g) = (0, g)$. Now observe that when $f = j\pi$, the map $i: H \to G$ equalizes $u$ and $v$; this follows from the calculation

$(\forall_{h: H})\; h \cdot j \pi(g) = j \pi(g h^{-1}) = j(g h^{-1} H) = j(g H) = j \pi(g)$But now from $u i = v i$ and the fact $i$ is epi, we have $u = v$, so indeed $(\forall_g)\; g \cdot f - f = 0$ and $f = j \pi$ is a constant, as required.

]]>Created parametric right adjoint.

]]>More or less a vague reference request: do you recommend some articles or books which (somehow) treat categories in the style of “combinatorial group theory”, in particular, developing notation for “relators” and results on “finitely presented” categories (both in the sense of combinatorial group theory).

For obvious reasons, every book on combinatorial group theory, and many articles within semigroup theory are something in that direction, but the question is rather asking for a more category-theoretic treatment.

Something of a moderate extension of combinatorial group theory to (some classes of) categories?

]]>created *diagram chasing lemmas - contents* (with some information on what implies what) and included it as a floating TOC into the relevant entries.

created over-topos

]]>I had started an entry “exponentiation” but then thought better of it and instead expanded the existing exponential object: added an examples-section specifically for $Set$ and made some remarks on exponentiation of numbers.

]]>Added Eric’s illustrations to the Idea-section at Yoneda embedding.

]]>Before changing the PROP entry to add this variant, i would like to have a nice reference on this. ]]>

Although referred to in a couple of place, it seems we had no entry for spatial topos, so I’ve made a start.

]]>Created equivariant_related_illustration20170619, for future use.

]]>[[twosets_op_with_names20170618]] is identical to [[twosets_op_nonames20170618]] except for the morphisms having names. ]]>

A long time ago we had a discussion at graph about notions of morphism. I have written an article category of simple graphs which collects some properties of the category under one of those definitions (corresponding better, I think, to graph-theoretic practice).

]]>"An algebraic Kan complex is a Kan complex equipped with a choice of horn fillers for all horns.

A morphism of algebraic Kan complexes is a morphism of the underlying Kan complexes that sends chosen fillers to chosen fillers.

This defines the category AlgKan of algebraic Kan complexes."

and refers to the paper by Thomas Nikolaus, Algebraic models for higher categories, arXiv/1003.1342.

Thomas writes to me that AlgKan is not a Cartesian closed category. It seems that the requirement that morphisms send chosen fillers to chosen fillers is rather strong, and causes difficulties in defining a well-behaved exponent in AlgKan. Would there be a case for a notion that could be called "functional Kan complex", where one has filler functions, but the morphisms are just as in the case of simplicial sets? In particular, morphisms do not have to send chosen fillers to chosen fillers (they will send fillers to fillers anyway, by naturality, but not necessarily to the chosen ones). I am well aware that, *under AC and classical logic* this would be equivalent to the usual notion of Kan simplicial set. However, with "functional Kan" one would have the same benefits regarding AC as mentioned on http://ncatlab.org/nlab/show/algebraic+Kan+complex. Constructively, "functional Kan" is perhaps more natural and a little stronger than "Kan". In some cases it is interesting to work with weaker axioms (then the results have greater generality). For example, it can be hoped that the category of "functional Kan" simplicial sets can be proved to be Cartesian closed without using AC. (There is little hope to eliminate classical logic here.)

Marc ]]>