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 wanted to be able to use the link without it appearing in grey, so I created a stub for general relativity.
moving material about the limited principle of omniscience from principle of omniscience to its own page at limited principle of omniscience
Anonymouse
moving material about the lesser limited principle of omniscience from principle of omniscience to its own page at lesser limited principle of omniscience
Anonymouse
added publication data to:
Have been polishing and expanding the first part of invariant polynomial.
I rewrote a good bit of the entry sheaf, trying to polish and strengthen the exposition.
The rewritten material is what now constituttes the section “Definition”. This subsumes essentially everything that was there before, except for some scattered remarks which I removed and instad provided hyperlinks for, since they have meanwhile better discussions in other entries.
I left the discussion of sheaves and the general notion of localization untouched (it is now in the section “Sheaves” and localization”). This would now need to be harmonized notationally a bit better. Maybe later.
For some text I need to explain the relation between sequents in the syntax of dependent type theory and morphisms in their categorical semantics.
I wanted to explain this table:
| types | terms | |
|---|---|---|
| (∞,1)-topos theory | X⊢E→Type | X⊢t→XE |
| homotopy type theory | x:X⊢E(x):Type | x:X⊢t(x):E(x) |
So I was looking for a place where to put it. This way I noticed that sequent used to redirect to sequent calculus. I think this doesn’t do justice to the notion and so I have
split off a new entry sequent
added a brief Idea-blurb
added my table and some explanation leading up to it
leaving the whole entry in genuinely stubby state. But no harm done, I think, if we compare to the previous state of affairs.
created adjoint triangle theorem.
Todd,
when you see this here and have a minute, would you mind having a look at monoidal category to see if you can remove the query-box discussion there and maybe replace it by some crisp statement?
Thanks!
created carrying
I added to star-autonomous category a mention of “*-autonomous functors”.
Created:
The category of Beck modules over a C^∞-ring A is equivalent to the category of ordinary modules over the underlying real algebra of A.
This is established using the proof given at Beck module for ordinary rings, using the fact that ideals of C^∞-rings coincide with ideals in the ordinary sense and the square zero extension construction used there can be promoted to a C^∞-ring using Taylor expansions.
Furthermore, the resulting notion of a Beck derivation coincides with that of a C^∞-derivation.
A different, nonequivalent definition was proposed by Kainz–Kriegl–Michor in 1987.
Suppose k is a commutative ring. Denote by Polyk the following category. Objects are k-modules. Morphisms M→N are polynomial maps M→N, i.e., elements of SymM*⊗kN.
A commutative algebra A can be identified with a product-preserving functor FinPolyk→Set, where FinPolyk is the full subcategory of Polyk on finitely generated free modules. The value A(X) for X∈FinPolyk can be thought of as the space of regular functions SpecA→X, where SpecA is the Zariski spectrum of A.
The starting observation is that a module M over a commutative k-algebra A can be identified with a dinatural transformation (dinatural in X∈CartPoly)
η:Polyk(X,M)×A(X)→M.We require η to be linear in the first argument.
That is to say, to specify an A-module M, we have to single out polynomial maps kn→M, together with a way to compose a polynomial map kn→M with a regular function SpecA→kn, obtaining a regular map SpecA→M. Interpreting M as the module of sections of a quasicoherent sheaf over SpecA, a regular map SpecA→M can be restricted to the diagonal SpecA, obtaining an element of M as required.
The proposal of Kainz–Kriegl–Michor is then to replace polynomial maps with smooth maps:
A C^∞-module over a C^∞-ring A is a Hausdorff locally convex topological vector space M together with a dinatural transformation
η:C∞(X,M)×A(X)→Mthat is linear in the first argument. If η is also continuous in the first argument, we say that M is a continuous C^∞-module.
Topological vector spaces in the above definition can be replaced by any notion of a vector space that allows for smooth maps, e.g., convenient vector space etc.
have cross-linked with entry with
the author’s pages
further relevant entries, such as Frölicher space
Created Beck module, mentioned it (once) on the tangent category page.
Created:
The abstract notion of a derivation corresponding to that of a Beck module.
Given a category C with finite limits, a Beck module in C over an object A∈C is an abelian group object in the slice category C/A.
The forgetful functor from modules to rings is modeled by the forgetful functor
UA:Ab(C/A)→C/A.Given M∈Ab(C/A), a Beck derivation A→M is a a morphism idA→UA(M) in C/A.
If UA has a left adjoint ΩA, then ΩA is known as the Beck module of differentials over A. Thus, Beck derivations A→M are in bijection with morphisms of Beck modules
ΩA→M,generalizing the universal property of Kähler differentials.
For ordinary commutative algebras, Beck derivations coincide with ordinary derivations.
For C^∞-rings, Beck derivations coincide with C^∞-derivations.
The original definition is due to Jon Beck. An exposition can be found in Section 6.1 of
added to the Properties-section at Hopf algebra a brief remark on their interpretation as 3-vector spaces.
I started an idea section at transgression, but it could probably use some going over by an expert. I hope I didn’t mess things up too badly. I was reading Urs’ note on “integration without integration” on the train ride home and fooled myself into thinking I understood something.
By the way, this reminded me of a discussion we had a while back
Started this, following this comment.
I wrote a little piece at general covariance on how to formalize the notion in homotopy type theory. Just for completeness, I also ended up writing a little blurb at the beginning about the genera idea of general covariance.
added publication details for this reference:
and am copying it over to compactly generated topological space, too