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 internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology 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 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.
   • CommentAuthorTodd_Trimble
   • CommentTimeJun 19th 2017
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexThe 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.

   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.

2. • CommentRowNumber2.
   • CommentAuthorDavidRoberts
   • CommentTimeJun 19th 2017
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexWould knowing Grp(E) is semiabelian help? I'm not saying it is, but it might.

   Would knowing Grp(E) is semiabelian help? I’m not saying it is, but it might.

3. • CommentRowNumber3.
   • CommentAuthorTodd_Trimble
   • CommentTimeJun 19th 2017
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexThanks. $Grp(E)$ is indeed semiabelian, but I'm not seeing how this would help right away. I should mention there's a related MO discussion; Paul Taylor gave a somewhat handwave-y answer [here](https://mathoverflow.net/a/46054/2926) which might contain sufficiently many hints to resolve the question, but it's hard for me to tell.

   Thanks. $Grp(E)$ is indeed semiabelian, but I’m not seeing how this would help right away. I should mention there’s a related MO discussion; Paul Taylor gave a somewhat handwave-y answer here which might contain sufficiently many hints to resolve the question, but it’s hard for me to tell.

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeJun 19th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI seem to recall this being discussed at the cafe somewhere as well, but I don't remember the conclusion.

   I seem to recall this being discussed at the cafe somewhere as well, but I don’t remember the conclusion.

5. • CommentRowNumber5.
   • CommentAuthorTodd_Trimble
   • CommentTimeJun 20th 2017
   • (edited Jun 20th 2017)
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexWell, it was sitting right in front of me, i.e., the proof looks almost identical to that of #1. [Here it is](https://mathoverflow.net/a/272617/2926). I think I'd like to add that proof to the [[regular monomorphism]] page (but please let me know if I goofed somewhere). Edit: it's been added.

   Well, it was sitting right in front of me, i.e., the proof looks almost identical to that of #1. Here it is.

   I think I’d like to add that proof to the regular monomorphism page (but please let me know if I goofed somewhere).

   Edit: it’s been added.

6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeJun 20th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexCute! Two thoughts: 1. I wonder whether this would go more naturally at [[Grp]]? Whichever page it is on it should be linked from the other. 2. It might help the reader if you recall quickly the definition of the relevant sort of "derivation" and the multiplication in the semidirect product.

   Cute! Two thoughts:

   1. I wonder whether this would go more naturally at Grp? Whichever page it is on it should be linked from the other.
   2. It might help the reader if you recall quickly the definition of the relevant sort of “derivation” and the multiplication in the semidirect product.
7. • CommentRowNumber7.
   • CommentAuthorDavidRoberts
   • CommentTimeJun 20th 2017
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexQuick question: is there any topos structure you don't use? That is, would it work internal to a more general category?

   Quick question: is there any topos structure you don’t use? That is, would it work internal to a more general category?

8. • CommentRowNumber8.
   • CommentAuthorTodd_Trimble
   • CommentTimeJun 20th 2017
   • (edited Jun 20th 2017)
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexLemme think: suppose we have a cartesian closed category with external countable colimits. The first thing I'd need to check is that any object $X$ can be embedded in an abelian group (object). You can form the free abelian group on $X$ as a coend $$F X = \int^{n: Fin} T(n) \cdot X^n$$ where $T: Fin \to Set$ is the restriction of the free abelian group monad $T: Set \to Set$, considered as a cartesian operad. (I can refer to the general theory developed [here](https://ncatlab.org/toddtrimble/published/Towards+a+doctrine+of+operads) although I also saw this discussed somewhere in the Elephant the other day.) I *think* the canonical map $X \to U F(X)$ will be injective in general but that's something to look into. Also, to what extent those external countable colimit considerations can be internalized by playing around with dependent sums/products and an NNO, I'm not sure, but I think a predicative topos would be much more than enough for that, and maybe an LCC pretopos with an NNO would be enough for that, but I won't swear to it. We use cartesian closed structure for the wreath product, and we use quotients for the coset space $H/K$, and we use the fact that a set/object can be embedded in an abelian group. From there, the reasoning is pretty much purely equational, up until the part where you begin to play with cosets, the part where you say $g' g^{-1} H = g' H$ iff $g^{-1} H = H$ iff $g \in H$. I *think* that part will be kosher because the equivalence relation used to form the coset space is effective, but that's the only thing I can see that would really warrant a closer look.

   Lemme think: suppose we have a cartesian closed category with external countable colimits. The first thing I’d need to check is that any object $X$ can be embedded in an abelian group (object). You can form the free abelian group on $X$ as a coend

   $$F X = \int^{n: Fin} T(n) \cdot X^n$$

   where $T: Fin \to Set$ is the restriction of the free abelian group monad $T: Set \to Set$, considered as a cartesian operad. (I can refer to the general theory developed here although I also saw this discussed somewhere in the Elephant the other day.) I think the canonical map $X \to U F(X)$ will be injective in general but that’s something to look into. Also, to what extent those external countable colimit considerations can be internalized by playing around with dependent sums/products and an NNO, I’m not sure, but I think a predicative topos would be much more than enough for that, and maybe an LCC pretopos with an NNO would be enough for that, but I won’t swear to it.

   We use cartesian closed structure for the wreath product, and we use quotients for the coset space $H/K$, and we use the fact that a set/object can be embedded in an abelian group. From there, the reasoning is pretty much purely equational, up until the part where you begin to play with cosets, the part where you say $g' g^{-1} H = g' H$ iff $g^{-1} H = H$ iff $g \in H$. I think that part will be kosher because the equivalence relation used to form the coset space is effective, but that’s the only thing I can see that would really warrant a closer look.

9. • CommentRowNumber9.
   • CommentAuthorTodd_Trimble
   • CommentTimeJun 20th 2017
   • (edited Jun 20th 2017)
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexMike: thanks! I added a Properties section to [[Grp]] and give the constructive proof there, with some linking back and forth to [[regular monomorphism]]. I reminded the reader about derivations and semidirect products.

   Mike: thanks! I added a Properties section to Grp and give the constructive proof there, with some linking back and forth to regular monomorphism. I reminded the reader about derivations and semidirect products.

10. • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeJun 20th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexWhat about in an elementary topos without NNO? Are symmetric differences constructive enough to generalize from FinSet to that case?

    What about in an elementary topos without NNO? Are symmetric differences constructive enough to generalize from FinSet to that case?

11. • CommentRowNumber11.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 21st 2017
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexI wondered about that a little, but didn't think it through. Could be worth considering more carefully.

    I wondered about that a little, but didn’t think it through. Could be worth considering more carefully.