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

Discussion Tag Cloud

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.
    • CommentAuthorUrs
    • CommentTimeNov 15th 2013
    • (edited Nov 15th 2013)

    I noticed by accident that we have an entry coinvariant. Then I noticed that we also have an entry homotopy coinvariant functor.

    I have now added cross-links between these entries and with invariant and orbit, so that they no longer remain hidden.

    I also edited the first case of group representation coinvariants at coinvariant a little.

    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 15th 2013
    • (edited Nov 15th 2013)

    Is there a HoTT formulation as for invariants?

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeNov 15th 2013

    So the coinvariant should just be the dependent sum, where the invariants is the dependent poduct.

    In this sense: for GG a group object, types VV with GG-action ρ V\rho_V are BG\mathbf{B}G-dependent types.

    The homotopy invariants are BGρ VH Grp(G,V)\underset{\mathbf{B}G}{\prod} \rho_V \simeq H_{Grp}(G,V).

    The homotopy co-invariants are BGρ VV//G\underset{\mathbf{B}G}{\sum} \rho_V \simeq V//G.