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.
I gave index an Idea-section.
In the course of this I created some stubby auxiliary entries, such as (in rapidly increasing order of stubbieness)
Added to Maslov index and to Lagrangian Grassmannian the following quick cohomological definition of the Maslov index:
The first ordinary cohomology of the stable Lagrangian Grassmannian with integer coefficients is isomorphic to the integers
H1(LGrass,ℤ)≃ℤ.The generator of this cohomology group is called the universal Maslov index
u∈H1(LGrass,ℤ).Given a Lagrangian submanifold Y↪X of a symplectic manifold (X,ω), its tangent bundle is classified by a function
i:Y→LGrass.The _Maslov index of Y is the universal Maslov index pulled back along this map
i*u∈H1(Y,ℤ).[spam]
An early survey is
Added the Yoneda-embedding way to talk about group objects and hence supergroups.
added pointer to
which provides a wealth of computational details and illustrative graphics.
I wrote about Dmitri Pavlov’s concept of measurable locales.
brief category:people-entry for hyperlinking references at Nielsen-Schreier theorem
Added reference
Anonymouse
I gather the following is true and is shown in Battenfield-Schröder-Simpson (pdf), but I haven’t really fully absorbed yet how AdmRep is actually embedded in RT(𝒦2).
The subcategory on the effectively computable morphisms of the function realizability topos RT(𝒦2) is the Kleene-Vesley topos KV. The category of “admissible representations” AdmRep (whose morphisms are computable functions (analysis), see there) is a reflective subcategory of RT(𝒦2) (BSS) and the restriction of that to KV is AdmRepeff
AdmRepeff↪KV↓↓AdmRep↪RT(𝒦2)
This is currently stated this way in the entry function ralizability and computable function (analysis), but please criticize/handle with care, I’ll try to further fine-tune as need be.
I added to decidable equality some remarks on the difference between the propositions-as-types version and the propositions-as-some-types version.
added to closed monoidal category a proof that the pointwise tensor product on a functor category with complete codomain is closed.
this is a bare section, spelling out in full detail the construction of the super Lie group integrating the translational part of the “supersymmetry algebra”, namely of the super Poincaré Lie algebra
(this is of course known to experts, but I am not aware of any literature showcasing how this works in full detail – if such literature exist, please drop a note [the group law itself appears in CAIP99 (2.1) (2.6)])
this entry is meant to be !include-ed as an Example-subsection into relevant entries, such as at super translation group
wrote a few lines at differential calculus, just so that the link does point somewhere. Clearly just a stub, to be expanded.