Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
gave representation theory a little Idea-section, then added some words on its incarnation as homotopy type theory in context/in the slice over $\mathbf{B}G$ and added the following homotopy type representation theory – table, which I am also including in other relevant entries:
homotopy type theory | representation theory |
---|---|
pointed connected context $\mathbf{B}G$ | ∞-group $G$ |
dependent type | ∞-action/∞-representation |
dependent sum along $\mathbf{B}G \to \ast$ | coinvariants/homotopy quotient |
context extension along $\mathbf{B}G \to \ast$ | trivial representation |
dependent product along $\mathbf{B}G \to \ast$ | homotopy invariants/∞-group cohomology |
dependent sum along $\mathbf{B}G \to \mathbf{B}H$ | induced representation |
context extension along $\mathbf{B}G \to \mathbf{B}H$ | |
dependent product along $\mathbf{B}G \to \mathbf{B}H$ | coinduced representation |
Relevant material happening at the nCafe here.
added pointer to
added pointer to:
for when the editing functionality is back: the entry representation theory should have a pointer to:
added textbook
Quinn
What is the relation with “representation theory in HoTT” and representation theory? I’m sure I could work out the details if I sat down, but reading the article it doesn’t really give a clear link. It would be good if that section was linked back with better understood concepts.
What do you understand by “representation theory”? The standard theory of group actions on vector spaces? One would think linear HoTT best suited for that.
Right, what you would usually learn in a first course on representation theory. How exactly does linear HoTT help here? My understanding is that linear HoTT comes from linear logic. Is there a connection there to linear algebra?
added pointer to:
1 to 12 of 12