Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

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 comma 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 finite 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 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

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 19th 2017

    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 EE are regular. Here’s a sketch. Every epimorphism ee in Grp(E)Grp(E) has a (regular epi)-mono factorization e=ipe = i p where pp is the projection GG/ker(e)G \to G/\ker(e) and ii is here both monic and epic, so it suffices to prove that mono-epis in Grp(E)Grp(E) are isomorphisms. So let i:HGi: H \to G be a mono-epi in Grp(E)Grp(E); we want to prove that G/H1G/H \cong 1 in EE. It will suffice to prove that for any abelian group AA in EE and any map j:G/HAj: G/H \to A in EE, the composite

    GπG/HjAG \stackrel{\pi}{\to} G/H \stackrel{j}{\to} A

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

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

    ( h:H)hjπ(g)=jπ(gh 1)=j(gh 1H)=j(gH)=jπ(g)(\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 ui=viu i = v i and the fact ii is epi, we have u=vu = v, so indeed ( g)gff=0(\forall_g)\; g \cdot f - f = 0 and f=jπf = j \pi is a constant, as required.

    • CommentRowNumber2.
    • CommentAuthorDavidRoberts
    • CommentTimeJun 19th 2017

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

    • CommentRowNumber3.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 19th 2017

    Thanks. Grp(E)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.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeJun 19th 2017

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

    • CommentRowNumber5.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 20th 2017
    • (edited Jun 20th 2017)

    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.

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeJun 20th 2017

    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.
    • CommentRowNumber7.
    • CommentAuthorDavidRoberts
    • CommentTimeJun 20th 2017

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

    • CommentRowNumber8.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 20th 2017
    • (edited Jun 20th 2017)

    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 XX can be embedded in an abelian group (object). You can form the free abelian group on XX as a coend

    FX= n:FinT(n)X nF X = \int^{n: Fin} T(n) \cdot X^n

    where T:FinSetT: Fin \to Set is the restriction of the free abelian group monad T:SetSetT: 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 XUF(X)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/KH/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 gg 1H=gHg' g^{-1} H = g' H iff g 1H=Hg^{-1} H = H iff gHg \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.

    • CommentRowNumber9.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 20th 2017
    • (edited Jun 20th 2017)

    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.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeJun 20th 2017

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

    • CommentRowNumber11.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 21st 2017

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