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.
Since I was being asked I briefly expanded automorphism infinity-group by adding the internal version and the HoTT syntax.
Mike, what’s the best type theory syntax for the definition of Aut(X) via ∞-image factorization of the name of X?
∑Y:TypeIsInhab(Y=X), or any variant depending on your chosen notation for IsInhab and identity/path types. E.g. ∑Y:Type[IdType(Y,X)] would be another version.
Ah, thanks. I should have been able to come up with this myself.
Can we allow ourselves to write “∑Y:Type[X=Y]”?
I have added a general remark on this to infinity-image in a new section Syntax in homotopy type theory there.
Can we allow ourselves to write “∑Y:Type[X=Y]”?
Sure, although I would probably mention that [−] denotes the support (and, perhaps, = the intensional identity type / path type) whenever I start using this notation on a given page or in a given paper.
OOPS! I meant [∑Y:Type(X=Y)]. I’ve corrected the proof at infinity-image.
Hm, I was thinking that
im∞(A(idA,b)→A×B)→A×B→Bis equivalent to
im∞(Ab→B)→B.Hm…
That’s not even true for 0-truncated objects. In that case (1,b):A→A×B is already monic, so the top composite just gives you b:A→B rather than its image.
Ah, sorry. Right, I am being stupid.
In Proposition 6.3.49 here, what exactly is what is on top of the 1∈ℤ2 that sits at the 0th level of AUT(BU(1))? Is it just BU(1)×B2U(1), or is there a nontrivial action of the first factor on the second? Or, more to the point, suppose I want to describe a flat connection on the bundle controlled by maps BAut(1∈ℤ2) (computing Aut(1∈ℤ2) inside AUT(BU(1))). Are these just pairs consisting of a flat connection on a principal U(1) bundle along with a flat connection on a bundle gerbe, or can the curvature of the connection on the principal U(1) bundle be more general?
I think the answer is: Not more general, no.
Since this happens in low degrees, we can still get a good explicit model by 2-functors:
So B2U(1) is 2-groupoid with a single object and a single 1-morphism
Then we are to compute
(1.) its automorphic endo-2-functors,
(2.) their natural transformations and
(3.) their “modifications” (for the latter cf. p. 127 here).
Inspect the diagrams characterizing the transformations and the modifications, these involve 2-morphisms labeled in U(1) and nothing else.
Since U(1) is abelian and since there are no non-trivial 1-morphsims which could lead to non-trivial whiskering, the transformations and modications each just contribute a plain copy of U(1).
Great, thanks, Urs.
1 to 12 of 12