An official website of the United States government
For N∞ operads O and O' such that there is an inclusion of the associated indexing systems, there is a forgetful functor from incomplete Tambara functors over O' to incomplete Tambara functors over O. Roughly speaking, this functor forgets the norms in O' that are not present in O. The forgetful functor has both a left and a right adjoint; the left adjoint is an operadic tensor product, but the right adjoint is more mysterious. We explicitly compute the right adjoint for finite cyclic groups of prime order.
more »
« less
This content will become publicly available on September 22, 2026
Formalizing Colimits in 𝒞at
{"Abstract":["Certain results involving "higher structures" are not currently accessible to computer formalization because the prerequisite ∞-category theory has not been formalized. To support future work on formalizing ∞-category theory in Lean’s mathematics library, we formalize some fundamental constructions involving the 1-category of categories. Specifically, we construct the left adjoint to the nerve embedding of categories into simplicial sets, defining the homotopy category functor. We prove further that this adjunction is reflective, which allows us to conclude that 𝒞at has colimits. To our knowledge this is the first formalized proof that the nerve functor is a fully faithful right adjoint and that the category of categories is cocomplete."]}
more »
« less
- Award ID(s):
- 2204304
- PAR ID:
- 10655588
- Editor(s):
- Forster, Yannick; Keller, Chantal
- Publisher / Repository:
- Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- Date Published:
- Volume:
- 352
- ISSN:
- 1868-8969
- Page Range / eLocation ID:
- 20:1-20:19
- Subject(s) / Keyword(s):
- category theory infinity-category theory nerve simplicial set colimit Theory of computation → Logic and verification
- Format(s):
- Medium: X Size: 19 pages; 2070768 bytes Other: application/pdf
- Size(s):
- 19 pages 2070768 bytes
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
null (Ed.)Abstract For each integer $$t$$ a tensor category $$\mathcal{V}_t$$ is constructed, such that exact tensor functors $$\mathcal{V}_t\rightarrow \mathcal{C}$$ classify dualizable $$t$$-dimensional objects in $$\mathcal{C}$$ not annihilated by any Schur functor. This means that $$\mathcal{V}_t$$ is the “abelian envelope” of the Deligne category $$\mathcal{D}_t=\operatorname{Rep}(GL_t)$$. Any tensor functor $$\operatorname{Rep}(GL_t)\longrightarrow \mathcal{C}$$ is proved to factor either through $$\mathcal{V}_t$$ or through one of the classical categories $$\operatorname{Rep}(GL(m|n))$$ with $m-n=t$. The universal property of $$\mathcal{V}_t$$ implies that it is equivalent to the categories $$\operatorname{Rep}_{\mathcal{D}_{t_1}\otimes \mathcal{D}_{t_2}}(GL(X),\epsilon )$$, ($$t=t_1+t_2$$, $$t_1$$ not an integer) suggested by Deligne as candidates for the role of abelian envelope.more » « less
-
For separable ‐algebras and , we define a topology on the set consisting of homotopy classes of asymptotic morphisms from to . This gives an enrichment of the Connes–Higson asymptotic category over topological spaces. We show that the Hausdorffization of this category is equivalent to the shape category of Dadarlat. As an application, we obtain a topology on the ‐theory group with properties analogous to those of the topology on . The Hausdorffized ‐theory group is also introduced and studied. We obtain a continuity result for the functor , which implies a new continuity result for the functor.more » « less
-
We introduce a notion of complexity of diagrams (and, in particular, of objects and morphisms) in an arbitrary category, as well as a notion of complexity of functors between categories equipped with complexity functions. We discuss several examples of this new definition in categories of wide common interest such as finite sets, Boolean functions, topological spaces, vector spaces, semilinear and semialgebraic sets, graded algebras, affine and projective varieties and schemes, and modules over polynomial rings. We show that on one hand categorical complexity recovers in several settings classical notions of nonuniform computational complexity (such as circuit complexity), while on the other hand it has features that make it mathematically more natural. We also postulate that studying functor complexity is the categorical analog of classical questions in complexity theory about separating different complexity classes.more » « less
-
Abstract We present a domain-specific type theory for constructions and proofs in category theory. The type theory axiomatizes notions of category, functor, profunctor and a generalized form of natural transformations. The type theory imposes an ordered linear restriction on standard predicate logic, which guarantees that all functions between categories are functorial, all relations are profunctorial, and all transformations are natural by construction, with no separate proofs necessary. Important category-theoretic proofs such as the Yoneda lemma and Co-yoneda lemma become simple type-theoretic proofs about the relationship between unit, tensor and (ordered) function types, and can be seen to be ordered refinements of theorems in predicate logic. The type theory is sound and complete for a categorical model invirtual equipments, which model both internal and enriched category theory. While the proofs in our type theory look like standard set-based arguments, the syntactic discipline ensure that all proofs and constructions carry over to enriched and internal settings as well.more » « less
