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 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 limit 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 subobject 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).
  1. I created a short page: regular action (of a group). It mainly just contains the definition and a simple-minded proof that a faithful transitive action *:G×XX* : G \times X \to X acts freely (and hence regularly) on XX if and only if the automorphism group Aut G(X)Aut_G(X) acts transitively (and hence regularly) on XX. If anyone knows of a more abstract proof, please feel free (and hence regular) to insert it.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeMay 2nd 2016


    I noticed that action did not cross-link to any of the related entries, so I added some more pointers here.

    • CommentRowNumber3.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 2nd 2016

    Is there a way to express this in HoTT, given a dependent type

    *:BGX(*):Type? \ast: \mathbf{B} G \vdash X(\ast): Type ?
    • CommentRowNumber4.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 2nd 2016

    Oh, is it just that the dependent sum is contractible.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeMay 2nd 2016

    Yes, that’s one of the places where geometric homotopy theory beautifies traditional theory: the condition that an action be transitive and free together just means that its homotopy quotient is contractible: transitivity ensures that all the points in the homotopy quotient are connected by equivalences, freeness means that the space of equivalences between two points is itselef contractible. (E.g. the homotopy quotient of a non-free action with stabilizer G xG_x of some point xx remembers all the non-freedom by sending that point to BG x\mathbf{B}G_x.)

    That in turn makes the theory of principal bundles in homotopy theory more beautiful than the classical theory: in geometric homotopy theory every quotient map PP/GP \to P/G is GG-principal.

    (Here “geometric homotopy theory” = “\infty-topos”) .

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeMay 2nd 2016

    So can we prove the theorem Noam mentioned in HoTT? At least the direction that if GG acts regularly on XX then so does Aut G(X)Aut_G(X)? How do we define Aut G(X)Aut_G(X)? Maybe something like

    BAut G(X) P:BG𝒰P=X\mathbf{B}Aut_G(X) \coloneqq \sum_{P:\mathbf{B}G\to \mathcal{U}} \Vert P = X\Vert


    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeMay 2nd 2016
    • (edited May 2nd 2016)

    The key fact is that Act G(H)H /BGAct_G(\mathbf{H}) \simeq \mathbf{H}_{/\mathbf{B}G}.

    A GG-action on XX is a type in context BG\mathbf{B}G with fiber XX, hence a homotopy fiber sequence of the form

    X X/G BG. \array{ X &\longrightarrow& X/ G \\ && \downarrow \\ && \mathbf{B}G } \,.

    A homomorphism of GG-actions is just a function in context BG\mathbf{B}G. Hence Aut G(X)Aut_G(X) is just the automorphisms group formed in in context BG\mathbf{B}G and then base changed (via dependent product) down to the empty context (or else to the ambient context Γ\Gamma, of course).

    The action of GG on XX is regular if X/G*X / G \simeq \ast.

    From this, it is plausible that Aut G(X)Aut_G(X), whose elements are cells in the bottom of the following diagram, has regular action on XX precisely if X/G*X/G \simeq \ast

    X X X/G X/G BG \array{ X && \longrightarrow && X \\ \downarrow && && \downarrow \\ X/G && \longrightarrow && X/G \\ & \searrow && \swarrow \\ && \mathbf{B}G }
    • CommentRowNumber8.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 3rd 2016

    I added the HoTT version of regularity.

    Presumably then one can speak of the regularity of an infinity-action.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeMay 3rd 2016

    Presumably then one can speak of the regularity of an infinity-action.

    As I said, GG \infty-acts regularly on XX if the homotopy quotuent is contractible, X/G*X/G\simeq \ast.

    • CommentRowNumber10.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 3rd 2016

    I guess I meant is that worth saying here. It’s of course trivial in a sense, but then has ’regular \infty-action’ ever appeared in print?

    Where did the term ’regular action’ come from? Was it derived from ’regular representation’? I seem to remember from my undergraduate days that the regular representation of a finite group was quite a useful device containing all its irreducible representations.

    Is there then a regular \infty-representation of an \infty-group GG, achieved through some kind of linearization of GG?

    But of course we have \infty-group \infty-rings at infinity-group of units. Ah, but that’s only for abelian \infty-groups.

    Then there’s all of infinity-representation and (infinity,1)-module bundle. But this is heading towards being a distraction. Still you’d think someone in the HoTT community could usefully look into such matters.

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeMay 3rd 2016
    • (edited May 3rd 2016)

    Where did the term ’regular action’ come from?

    I’d guess it derives from regularity of quotients, as in “regular point”, etc.. But I don’t know the history.

    • CommentRowNumber12.
    • CommentAuthorEgbertRijke
    • CommentTimeMay 4th 2016

    Here are the claims with their proofs. Of course, in the email list, Mike finished the argument of the first claim.

    Let BGBG be a pointed connected type with loop space GG. Let X:BGUX : BG \to U be a type X(*)X(\ast) with a GG-action on it, and define BAut G(X):= (P:BGU)P=XBAut_G(X) := \sum_{(P:BG \to U)} \|P=X\|. Then we have Y:BAut G(X)UY : BAut_G(X) \to U given by Y(P,):=P(*)Y(P,-) := P(\ast).

    Claim 1. If XX is regular, then YY is regular.

    Proof. First, we need to argue that X(*)X(\ast) is merely inhabited. Since XX is regular, we have (b:BG)X(b)\sum_{(b:BG)} X(b) contractible. This gives a center of contraction (b,x)(b,x). Now, since BGBG is connected, it follows that b=*\|b=\ast\|. Since we are proving the mere proposition X(*)\|X(\ast)\|, we get to use b=*b=\ast. Now we obtain X(*)\|X(\ast)\| .

    Next, to show that XX is regular we need to show that XX has a contractible total space. The type (b:BAut G(X))Y(b)\sum_{(b : BAut_G(X))} Y(b) is equivalent to (P:BGU)P=X×P(*)\sum_{(P:BG \to U)} \|P=X\| \times P(\ast). Contractibility is a mere proposition, and we have X(*)\|X(\ast)\|, so we get to use a point x:X(*)x:X(\ast). This gives us a center of contraction (X,refl,x)(X,refl,x) of the total space of YY.

    Now let P:BGUP : BG \to U, let P=X \| P = X \|, let p 0:P(*)p_0 : P(\ast). To show regularity, it suffices to find a term of type

    α:P=Xtrans(α)(p 0)=x\sum_{\alpha : P = X} \mathrm{trans}(\alpha)(p_0) = x

    This type is equivalent to showing that there are

    K: b:BGP(b)X(b)K : \prod_{b:BG} P(b) \simeq X(b), and K(*,p 0)=x 0K(*,p_0) = x_0

    Now we use that X(b)X(b) is equivalent to b=*b=\ast (we get this fact from regularity, together with a point x:X(*)x:X(\ast)). Since we need this particular fiberwise equivalence, it suffices to show that

    b:BGP(b)\sum_{b:BG} P(b)

    is contractible. Now this is a mere proposition, so we can eliminate t:P=Xt : \| P = X \| to obtain the proof.

    Claim 2. If XX is a principal homogeneous space on GG, in the sense that the type (g:G)g *(x)=y\sum_{(g:G)} g_\ast(x)=y is contractible for all x,y:X(*)x,y:X(\ast), and YY is regular, then XX is regular.

    Proof. Again, we first show that X(*)X(\ast) is merely inhabited. The total space of YY has center of contraction (P,p 0)(P,p_0). Since P=X\|P=X\| and since we are proving a mere proposition, we get to use P=XP=X. Now X\|X\| follows from p 0:P(*)p_0:P(\ast). The regularity of XX is a mere proposition, so we get to use x 0:X(*)x_0:X(\ast). This gives us the center of contraction (*,x 0)(\ast,x_0). It remains to show that

    (b:BG) (x:X(b)) (α:b=*)trans(α,x)=x 0\prod_{(b:BG)} \prod_{(x:X(b))} \sum_{(\alpha : b=\ast)} \mathrm{trans}(\alpha,x) = x_0.

    Of course, it would suffice to prove the stronger statement

    (b:BG) (x:X(b))isContr( (α:b=*)trans(α,x)=x 0)\prod_{(b:BG)} \prod_{(x:X(b))} \mathrm{isContr} (\sum_{(\alpha : b=\ast)} \mathrm{trans}(\alpha,x) = x_0).

    However, now we get to use that BGBG is connected. Therefore it suffices to show that

    x:X(*)isContr( α:Gtrans(α,x)=x 0)\prod_{x:X(*)} isContr (\sum_{\alpha : G} \mathrm{trans}(\alpha,x) = x_0)

    This holds by assumption.

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeMay 4th 2016

    Thanks, Egbert, that’s really nice.

    The idea would be that such stuff should go into the nLab entry, as there it is more usefully recorded. Might you have time to copy it over?

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeMay 4th 2016

    Yes please!

    • CommentRowNumber15.
    • CommentAuthorEgbertRijke
    • CommentTimeMay 4th 2016

    I’ve put it on the nLab page. As it is my first contribution to the nLab, please have a quick look to see whether it is okay.

    • CommentRowNumber16.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 4th 2016
    • (edited May 4th 2016)

    Any other candidates for the HoTT treatment? Burnside’s lemma?

    Maybe too 1-group-like, but there may be generalisable components of the proof.

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeMay 4th 2016
    • (edited May 4th 2016)

    Egbert, thanks. That’s impressive for a first nnLab edit. Hopefully you’ll get the chance to do more such!

    I just went through your text, here, and added a bunch of hyperlinks to keywords. Such as mere proposition, inhabited type, contractible type, etc. Also to automorphism infinity-group in HoTT

    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeMay 4th 2016

    Yes, thanks!

    Burnside’s lemma happens a special case of the linearity of traces. Developing the latter in HoTT would be a good deal of work, but might pay off.

    • CommentRowNumber19.
    • CommentAuthorEgbertRijke
    • CommentTimeMay 4th 2016

    Possibly the condition of being a principal homogeneous space over GG can be weakened, because right now we only use the regularity of X˜\tilde{X} to conclude that X(*)\|X(\ast)\|. Any suggestions?

    • CommentRowNumber20.
    • CommentAuthorLuis_Scoccola
    • CommentTimeMay 6th 2016

    Here I have some (very brief and informal) notes about infinity groups in HoTT. I’m sorry to share a link to a pdf but if some of the things written there make any sense I will write them down in an nLab entry. The notes include (potential) definitions for transitive actions, free actions and faithful actions, and some informal arguments to motivate them. I’m afraid I did not have the time to see if this definition of faithful action serves to generalize the lemma that started this thread, but I will think about it.

    Are these defintions reasonable or maybe already known? Also I have a question regarding infinity groups is HoTT. Is there a standard definition for infinity-subgroup, or for the kernel of an infinity-group morphism? I was thinking of maybe being able to prove some kind of Orbit-Stabilizer theorem.

    Remark: I used a computer-language-like notation for dependent sums and dependent products: a dependent sum is written (a:A)×P(a)(a : A) \times P(a) and a dependent product (a:A)P(a)(a:A)\to P(a).

    • CommentRowNumber21.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 7th 2016
    • (edited May 7th 2016)

    It would be great to have \infty-group theory written out somewhere in full HoTT style. Urs has written extensively on infinity-actions. Regarding a Orbit-Stabilizer theorem, the place to look, as I said on the transitive action thread, is stabiliser group.

    There, sub-\infty-groups are being taken as monomorphisms:

    in contrast to the classical situation, this morphism is not in general a monomorphism anymore, hence the stabilizer Stab ρ(x)Stab_\rho(x) is not a sub-group of GG in general.

    That tallies with why what’s at normal+subgroup#NormalMorphismOfInfinityGroups is not called a normal sub-\infinity-group, which would need the extra mono condition. We should, but don’t, have something on this at subgroup.

    infinity-group has other links, such as center of an infinity-group.

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeMay 7th 2016

    I have not read this, but it seems possibly relevant: Sylow theorems for ∞-groups

    Viewing Kan complexes as ∞-groupoids implies that pointed and connected Kan complexes are to be viewed as ∞-groups. A fundamental question is then: to what extent can one “do group theory” with these objects? In this paper we develop a notion of a finite ∞-group: an ∞-group with finitely many non-trivial homotopy groups which are all finite. We prove a homotopical analog of the Sylow theorems for finite ∞-groups. We derive two corollaries: the first is a homotopical analog of the Burnside’s fixed point lemma for p-groups and the second is a “group-theoretic” characterization of (finite) nilpotent spaces.

    • CommentRowNumber23.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 8th 2016
    • (edited Feb 20th 2018)

    One of the authors, Matan Prasma (used to be written Prezma), has worked on normal maps of \infty-groups, as it says at normal+subgroup#NormalMorphismOfInfinityGroups. In the general setting, for normal f:KGf: K \to G there is a long fiber sequence

    GKBKBfBGB(GK). G\sslash K \to \mathbf{B}K \stackrel{\mathbf{B}f}{\to}\mathbf{B}G \to \mathbf{B}(G\sslash K) \,.

    Does the normal sub-\infty-group case, where ff is a monomorphism, merit special attention, I wonder. A Jordan-Holder decomposition?

    How about the isomorphism theorems?

    • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeApr 16th 2021

    mentioned definition via shear map isomorphism and made the equivalent notion of torsor more explicit.

    diff, v10, current