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

(0 2-category 2-category-theory abelian-categories accessible adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry beauty book bundle bundles categories category category-theory chern-simons-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology cohomolohy combinatorics complex complex-geometry computable-mathematics computer-science connection constructive constructive-mathematics cosmology deformation-theory descent differential differential-cohomology differential-geometry dold fibration duality elliptic-cohomology enriched factorization-system fibration foundations functional-analysis functor galois-theory gauge-theory gebra general topology geometric geometric-quantization geometry gravity group-theory higher higher-algebra higher-category-theory higher-geoemtry higher-geometry higher-lie-theory higher-topos-theory history homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory infinity integration-theory internal-categories k-theory kan lie-algebras lie-theory limit limits linear linear-algebra locale localization logic manifolds mathematics measure measure-theory meta modal-logic model model-category-theory monoidal-category monoidal-category-theory morphism motives motivic-cohomology n-groups newpage nonassociative noncommutative noncommutative-geometry number-theory operator operator-algebra order-theory 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 set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory subobject supergeometry symplectic-geometry synthetic-differential-geometry tannaka terminology theory topology topos topos-theory tqft type type-theory 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.
    • CommentAuthorTim_Porter
    • CommentTimeJan 10th 2012
    • (edited Jan 10th 2012)

    I created a stub for stabilizer subgroup as it was needed by orbit.

    This could do with a nPOV section, but I am not sure what to say for that. (I am still not sure how to ‘do’ an nPOV version of all the stuff around group actions. I would love to have it clear in my head as then a straightforward nPOV adaption of Grothendieck in SGA1 would be feasible. The treatment of SGA1 in the nLab still has some holes in it… e.g. the transition from the prorepresenting PP to the profinite group Aut(P)Aut(P). I hope to sketch a bit more detail there soon. In fact a lot of the detail is skated over in the original SGA1. Any thoughts anyone?)

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeJan 10th 2012

    This could do with a nPOV section

    I have added it here.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeJan 10th 2012
    • (edited Jan 10th 2012)

    Hm, the server went down briefly after my edit.

    So here is roughly what I typed: a group action ρ:G×XX\rho : G \times X \to X is equivalently encoded in the corresponding action groupoid, which is the ρ\rho-associated bundle to the the universal GG-bundle XX//GBGX \to X//G \to \mathbf{B}G. The stabilizer group of an element x:*Xx : * \to X is the first homotopy group of X//GX//G at this point. Or, what is equivalent for 1-groups, it is the loop space object Ω xX//G\Omega_{x} X//G .

    (Hm, of course also the formulas don’t all display as long as the nLab server is down…)

    In this last formulation the notion directly generalizes to stabilizer \infty-groups of \infty-group actions. And all of this goes through for cohesive \infty-groups, too.

    This is also in section 2.3.7 here. (Which of course is, however, also not available as long as the server is down.)

    • CommentRowNumber4.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 10th 2012

    Is there any need to revisit this thread, e.g., Mike’s suggestion?

    • CommentRowNumber5.
    • CommentAuthorzskoda
    • CommentTimeJan 10th 2012
    • (edited Jan 10th 2012)

    While stabilizer group, isotropy group, isotropy subgroup, stabilizer subgroup and small group are also used, I think that the modern default is the shortest: just stabilizer. The latter term subsumes also the categorified versions.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeJan 10th 2012
    • (edited Jan 10th 2012)

    Is there any need to revisit this thread, e.g., Mike’s suggestion?

    Okay, sure. I had forgotten about this.

    First, over there is discussed the stabilizer of a general morphism YXY \to X, whereas I was here talking about stabilizers of global elements *X* \to X only.

    Second, there the action in nn-categories is at least alluded to, whereas what I wrote here is for (n,1)(n,1)-categories.

    So there is room to generalize.

    What I don’t see right now is how Mike’s suggestion gives a group object, in general. What Mike defines one can think of as producing the homotopy fixed point data fibered over the group (over each element gg of the group the data that makes YXY \to X a homotopy fixed point under gg.) How is that a group object?

    (I am genuinely asking, I don’t see it right now.)

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeJan 10th 2012
    • (edited Jan 10th 2012)

    First, over there is discussed the stabilizer of a general morphism YXY \to X, whereas I was here talking about stabilizers of global elements *X* \to X only.

    Of course the definition of stabilizer \infty-groups as here immediately generalizes to this case:

    for GG an action on XX, and YY any other object, there is an induced action on the internal hom [Y,X][Y, X] leading to an action \infty-groupoid [Y,X]//G[Y,X]//G. So now for given f:YXf : Y \to X we can form the stabilizer \infty-group Ω f([Y,X]//G)\Omega_f ( [Y,X]//G ).

    edit:

    as action \infty-groupoids we obtain [Y,X]//GBG[Y,X]//G \to \mathbf{B}G from X//GBGX//G \to \mathbf{B}G as the \infty-pullback

    [Y,X]//G [Y,X//G] BG [Y,BG], \array{ [Y,X]//G &\to& [Y, X//G] \\ \downarrow && \downarrow \\ \mathbf{B}G &\to& [Y,\mathbf{B}G] } \,,

    where the bottom morphism picks the trivial cocycle and its global automorphisms (meaning that GG acts by the same element on all points of YY at once, as it should). So the bottom morphism is the hom-adjunct to the projection Y×BGBGY \times \mathbf{B}G \to \mathbf{B}G.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeJan 10th 2012
    • (edited Jan 10th 2012)

    Finally, I should say, for the definition that I was looking at, that and how there is a canonical morphism from the stabilizer \infty-group to the \infty-group GG. It’s given by the top left morphism i xi_x in the pasting diagram of homotopy pullbacks

    Stab G(x) i x G * x * x X X//G ρ * BG. \array{ Stab_G(x) &\stackrel{i_x}{\to}& G &\to& * \\ \downarrow && \downarrow && \downarrow^{\mathrlap{x}} \\ * &\stackrel{x}{\to}& X &\to& X//G \\ && \downarrow && \downarrow^{\rho} \\ && * &\to& \mathbf{B}G } \,.

    edit:

    what is maybe noteworthy here is that this is just producing the long fiber sequence for the case where we regard XX and X//GX//G as objects pointed by xx. So i xi_x here is simply the looping of the representation itself:

    i xΩ xρ. i_x \simeq \Omega_x \rho \,.
    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeJan 10th 2012

    I believe the two definitions are actually the same, both in the case of global points and of arbitrary morphisms YXY\to X. I actually found it easiest to prove this using HoTT, although quite possibly there is an easy arrow-theoretic proof too.

    Note that the following code uses some lemmas and tactics from my fork of the HoTT repository that I haven’t gotten around to merging back into the main trunk yet.

    Require Import Homotopy.
    

    Let’s assume a pointed type BGB G, with the group object GG defined as its loop space.

    Hypothesis BG : Type.
    Hypothesis pt : BG.
    Definition G := pt == pt.
    
    Section OfAPoint.
    

    Similarly, let’s assume the action groupoid as a fibration XGBGX\sslash G \to B G, with the type XX defined as its fiber over the basepoint. Note that the action of GG on XX is then via transport.

      Hypothesis XG : BG -> Type.
      Let X := XG pt.
    

    Let’s consider first the stabilizer of a point of XX.

      Hypothesis x : X.
    

    Urs’s definition of the stabilizer of a point x:Xx\colon X is as the loop space of that point, regarded as living in the total space XGX\sslash G rather than in XX.

      Definition Urs_stab_pt : Type
        := (existT XG pt x) == (existT XG pt x).
    

    On the other hand, my definition specializes to the following.

      Definition Mike_stab_pt : Type
        := { g : G & transport g x == x }.
    

    And their equivalence is just a special case of the characterization of path-spaces of total spaces.

      Definition stab_pt_equiv : Urs_stab_pt <~> Mike_stab_pt
        := total_paths_equiv BG XG (existT XG pt x) (existT XG pt x).
    
    End OfAPoint.
    
    Section OfAMap.
    

    Now let’s consider the stabilizer of a map f:YXf\colon Y\to X. Again we assume XX via its action groupoid.

      Hypothesis XG : BG -> Type.
      Let X := XG pt.
    
      Hypothesis Y : Type.
      Hypothesis f : Y -> X.
    

    The following definition is the fibration [Y,XG][Y,BG][Y, X\sslash G] \to [Y, BG].

      Let Y_XG : (Y -> BG) -> Type
        := fun h => (forall y:Y, XG (h y)).
    

    As a sanity check, we verify that its total space is, in fact, the function space [Y,XG][Y, X\sslash G].

      Lemma Y_XG_total : (Y -> sigT XG) <~> sigT Y_XG.
      Proof.
        apply section_total_equiv.
      Defined.
    

    Now this is the action groupoid [Y,X]G[Y,X]\sslash G, defined with a pullback as in comment #7 above.

      Let YX_G : BG -> Type
        := fun bg => Y_XG (fun _ => bg).
    

    Urs’s definition of the stabilizer of f:YXf\colon Y\to X is its stabilizer as a point of this action of GG on [Y,X][Y,X].

      Definition Urs_stab_map : Type
        := Urs_stab_pt YX_G f.
    

    Whereas here’s what my definition would give.

      Definition Mike_stab_map : Type
        := { g : G & (transport g) o f == f }.
    

    In this case, the proof of equivalence is a little longer, but it really only has two steps. First, we apply the characterization of path-spaces of total spaces to identify Urs’s definition with the total space of some fibration over GG.

      Definition stab_map_equiv : Urs_stab_map <~> Mike_stab_map.
      Proof.
        apply @equiv_compose with
          (B := { g : G & transport (P := fun bg => Y -> XG bg) g f == f }).
        refine (total_paths_equiv BG YX_G _ _).
    

    Now we just need to show that this fibration (g \mapsto transport g f == f) is fiberwise equivalent to g \mapsto transport g \circ f == f, and for this it suffices to show that transport g f is equivalent to (transport g) \circ f.

        assert (H : forall g:G,
          transport (P := fun bg => Y -> XG bg) g f == (transport g) o f).
    

    This should probably be a lemma in the standard library, but I don’t think it’s there yet, so we can just prove it here.

        intros g; apply funext; intros y.
        path_change ((fun h => h y) 
          (transport (P := fun bg => Y -> XG bg) g f)).
        path_change (transport g ((fun h => h y) f)).
        refine (trans_map _ (fun bg (h: Y -> XG bg) => h y) _).
    

    Now we can complete the proof.

        apply total_equiv with
          (g := fun g => concat (!H g)).
        intros g; apply concat_is_equiv_left.
      Defined.
    
    End OfAMap.
    
    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeJan 10th 2012

    By the way, I think that XGX\sslash G (iTex \sslash) looks much nicer than X//GX//G.

    • CommentRowNumber11.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 10th 2012

    It saddens me that I find #9 almost completely unreadable.

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeJan 10th 2012

    I believe the two definitions are actually the same, […] I actually found it easiest to prove this using HoTT,

    Mike, that is quite impressive. I literally have to run now, but thanks for this.

    And thanks for

    \sslash
    

    I didn’t know that code and didn’t bother to search for it.

    • CommentRowNumber13.
    • CommentAuthorzskoda
    • CommentTimeJan 10th 2012

    I can not read sslash in firefox on XP.

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeJan 10th 2012

    Zoran: That’s weird; I presume you have all the usual fonts installed. Can someone who knows more than I do suggest any reason why Zoran’s fonts might be missing that character?

    • CommentRowNumber15.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 11th 2012
    • (edited Jan 11th 2012)

    I have the same problem as Zoran. And, while I’m thinking of it, \preceq doesn’t render for me either. (That’s \preceq, in case it doesn’t render for you either.)

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeJan 11th 2012

    Todd, are you also in Firefox on Windows? Does it look okay in other browsers, or if you change the itex mode on the forum?

    • CommentRowNumber17.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 11th 2012

    Thanks for asking, Mike. Yes, I nomally use Firefox on Windows XP. The \preceq, but not the \sslash, shows up in IE 8.0.6001.18702. (There might be something I need to enable which would allow me to see \sslash?) Sorry, I don’t know what it means to change itex mode, unless you mean to change the filter for formatting comments (?).

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeJan 11th 2012

    I have briefly added some of the above stuff to stabilizer group (not yet Mike’s stuff, though). Maybe I’ll add more later. But now I need to be taking care of something else.

    • CommentRowNumber19.
    • CommentAuthorzskoda
    • CommentTimeJan 11th 2012

    I usually see all the fonts in nnLab and nnForum, sslash is one of rare exception, and example preceq from 15 as well.

    • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeJan 11th 2012

    @Todd: Go to “Account” at the top of the nForum page. On the left, click “change iTex mode”, select different things and see how it looks. This changes whether math is displayed as images or as MathML (which the browser has to understand — currently Firefox is the only major browser that supports MathML, so the “auto” setting selects MathML if you’re using Firefox and images otherwise. I think).

    You can also test whether math is currently displaying as MathML or as images by trying to select part, but not all, of a mathematical formula with the cursor. This is possible with MathML, but not with an image.