nLab

There are several contexts in which it is of relevance that a certain property of a morphism is preserved (or stable) under pullback, i.e. also shared by the the morphism for any pullback diagram Geometers prefer to say “stable under base change”. Monomorphisms are always stable under pullback; that is, if is a monomorphism, then so is . Epimorphisms are not necessarily stable under pullback. In …

In physics, a local Lagrangian induces a covariant phase space equipped with a canonical presymplectic form. The quotient of this by symmetries that, in good cases, make the pre-symplectic form a genuine symplectic form, is called the reduced phase space. Generally, given a symplectic manifold or presymplectic manifold or Poisson manifold regarded as a phase space equipped with a suitable (Hamilt…

∞-Lie theory (higher geometry) Background Smooth structure Higher groupoids Lie theory ∞-Lie groupoids ∞-Lie algebroids Formal Lie groupoids Cohomology Homotopy Related topics Examples -Lie groupoids -Lie groups -Lie algebroids -Lie algebras A Lie 2-groupoid is a 2-truncated ∞-Lie groupoid. Every Lie groupoid is a special case of a Lie 2-groupoid. For an abelian Lie group, its double delooping is…

On the Nielsen-Schreier theorem in homotopy type theory/univalent foundations: On path types and identity types: On separable metric spaces in function realizability:

A major difference between cubical path types and Martin-Löf identity types is the behaviour of the J rule. In Martin-Löf identity types the J rule holds up to definitional equality, but for cubical path types, the J rule only holds up to a path. Another difference is that transport generally behaves better with cubical path types. Certain rules for the computation of transports in concrete type …

In cubical type theory, regularity is the condition where composition along a degenerate? open box is the identity.

The Jordan-Hölder theorem says that every composition series of a given group, and every Jordan-Hölder sequence on a given object in an abelian category, has the same length, and the same simple factors, up to permutation. In particular says that the length of an object in an abelian category is well defined. More generally, a form of the theorem holds in any homological category. This is a proof…

Background Basic concepts Universal constructions Local presentation Theorems (∞,1)-Yoneda lemma (∞,1)-Grothendieck construction adjoint (∞,1)-functor theorem (∞,1)-monadicity theorem Extra stuff, structure, properties Models As for localization of ordinary categories, there are slightly different notions of what a localization of an (∞,1)-category is. One definition is in terms of simplicial loc…

Postdoc at the University of Regensburg. On G-semiadditivity: On an approach to the six functor formalism via the universality of certain -categories of higher correspondences: On global equivariant homotopy theory and cohesive homotopy theory applicable to differential orbifold cohomology: On formal (infinity,1)-category theory: On localization of -categories and the relative Rezk nerve:

homotopy theory, (∞,1)-category theory, homotopy type theory flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed… models: topological, simplicial, localic, … see also algebraic topology Introductions Introduction to Basic Homotopy Theory Introduction to Abstract Homotopy Theory geometry of physics – homotopy types Definitions Paths and cylinders Homotopy groups B…

homotopy theory, (∞,1)-category theory, homotopy type theory flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed… models: topological, simplicial, localic, … see also algebraic topology Introductions Introduction to Basic Homotopy Theory Introduction to Abstract Homotopy Theory geometry of physics – homotopy types Definitions Paths and cylinders Homotopy groups B…

This entry is about the notion of naturalness in (particle-)physics. For the notion in mathematics see at natural transformation. In (particle-)physics the term “naturalness” [‘t Hooft 1980, Gell- Mann 1983] refers to the vague idea that a model of physics is expected to work without requiring unlikely-looking ad-hoc coincidences or “fine-tuning” of its parameters (such as the choice of renormali…

Ben Allanach, Finding Z’s responsible for , talk at Moriond 2019 (pdf) Ben Allanach, Ben Gripaios, Tevong You, The Case for Future Hadron Colliders From Decays, JHEP03(2018)021 (arXiv:1710.06363) Ben Allanach, Explanation of the Neutral Current −Anomalies (arXiv:2009.02197) On naturalness:

The initiality conjecture in type theory states that the term model of a type theory should be an initial object in the category of models of that type theory. Initiality guarantees that the relation between type theory and category theory works as expected, hence that formal syntactical proofs in type theory match theorems in categories that interpret these type theories. A careful proof of init…

On aspects of the 2-Grothendieck construction: A 2-comonad characterizing Grothendieck fibrations: On 2-colimits in slide 2-categories: On the indexed Grothendieck construction: Discussion of 2-classifiers for 2-toposes/2-categorical logic: Luca Mesiti: Pointwise Kan extensions along 2-fibrations and the 2-category of elements, Theory and Applications of Categories 41 30 960–994 (2024) [arXiv:230…

On fibrations of enriched groupoids as categorical semantics for identity types in homotopy type theory: A 2-comonad characterizing Grothendieck fibrations: On a candidate for a 2-topos version of the effective topos:

Thomas Streicher (1958–2025) On categorical semantics of (dependent) type theory (and proving an initiality conjecture in Ch. 4), see at categorical model of dependent types: Introducing the homotopy type theory-interpretation of identity types (the “groupoid model”) and introducing what came to be known the univalence axiom (under the name “universe extensionality”): Martin Hofmann, Thomas Strei…

Given a -coalgebra-Galois extension of a -algebra , which is the appropriate generalization of a Hopf-Galois extension, where is faithfully flat over the base as a left -module, one constructs a coring, Ehresmann coring, out of these data. Its role is somewhat analogous to the gauge groupoid (see Atiyah Lie groupoid), and in Hopf-Galois case it is an intermediate stage in constructing another ana…

Content Context Equivariant higher algebra Equivariant categories and symmetric monoidal categories Equivariant operads edit this sidebar Higher algebra Content Idea A --operad is an -operad if it is infinitely connected (or equivalently, -truncated), unital, and prescribes binary multiplications on fixed points for all subgroups. These are meant to model the equivariant commutative operads …

mathematical logic deduction system, natural deduction, sequent calculus, lambda-calculus, judgment type theory, simple type theory, dependent type theory collection, object, type, term, set, element equality, judgmental equality, typal equality universe, size issues higher-order logic Formalism is one of the classical schools of the philosophy of mathematics. Under this view, “mathematics is (be…