What should a generic object be Jonathan Sterling Updated March 10 2023

2025-04-29 0 0 488.27KB 27 页 10玖币
侵权投诉
What should a generic object be?
Jonathan Sterling
Updated March 10, 2023
Abstract
Jacobs has proposed definitions for (weak, strong, split) generic objects for
a fibered category; building on his definition of (split) generic objects, Jacobs
develops a menagerie of important fibrational structures with applications
to categorical logic and computer science, including higher order fibrations,
polymorphic fibrations,
𝜆
2-fibrations,triposes, and others. We observe that a
split generic object need not in particular be a generic object under the given
definitions, and that the definitions of polymorphic fibrations, triposes, etc.
are strict enough to rule out some fundamental examples: for instance, the
fibered preorder induced by a partial combinatory algebra in realizability
is not a tripos in this sense. We propose a new alignment of terminology
that emphasizes the forms of generic object appearing most commonly in
nature, i.e. in the study of internal categories, triposes, and the denotational
semantics of polymorphism. In addition, we propose a new class of acyclic
generic objects inspired by recent developments in higher category theory
and the semantics of homotopy type theory, generalizing the realignment
property of universes to the setting of an arbitrary fibration.
Contents
1 Introduction 2
1.1 Introduction to fibered categories . . . . . . . . . . . . . . . . . . 3
1.1.1 Small categories, internal categories . . . . . . . . . . . . 5
1.1.2 Cleavages and splittings . . . . . . . . . . . . . . . . . . . 8
1.2 Goals and structure of this paper . . . . . . . . . . . . . . . . . . 9
2 Four kinds of generic object 9
2.1 Separating generic objects from strong generic objects . . . . . . 10
2.2 A split generic object need not be a generic object . . . . . . . . . 10
2.3 Skeletal and gaunt small categories . . . . . . . . . . . . . . . . . 11
2.4 Generic objects from weak generic objects . . . . . . . . . . . . . 12
2.5
Weak generic objects are the correct generalization of split generic
objects ................................. 13
3 Consequences for internal categories, tripos theory, polymorphism,
etc.14
3.1 Consequences for internal category theory . . . . . . . . . . . . 14
3.2 Consequences for tripos theory . . . . . . . . . . . . . . . . . . . 15
3.3 Consequences for polymorphism . . . . . . . . . . . . . . . . . . 15
1
arXiv:2210.04202v3 [cs.LO] 9 Mar 2023
3.4 Consequences for type theory and algebraic set theory . . . . . 15
4 A proposal for a new alignment of terminology 16
4.1 Generic objects: ordinary, skeletal, and gaunt . . . . . . . . . . . 16
4.2 Weak generic objects and stack completions . . . . . . . . . . . . 17
4.3 A new class: acyclic generic objects . . . . . . . . . . . . . . . . . 19
4.3.1 Incomparability of acyclic and skeletal generic objects . . 21
4.4 Splittings and generic objects . . . . . . . . . . . . . . . . . . . . 22
4.5 In univalent mathematics . . . . . . . . . . . . . . . . . . . . . . 22
5 Concluding remarks 22
1 Introduction
Since the latter half of the 20th century, fibered category theory or the theory of
fibrations has played an important background role in both the applications
and foundations of category theory [
17
,
8
]. Fibered categories, also known as
fibrations, are a formalism for manipulating categories that are defined relative to
another category, generalizing the way that ordinary categories can be thought
of as being defined relative to the category of sets.
The sense in which ordinary category theory is pinned to the category of
sets can be illustrated by considering the definition of when a category
𝒞
“has
products”:
Definition 1.
A category
𝒞
has
products
when for any indexed family
{𝐸𝑖∈𝒞}𝑖∈𝐼
of objects, there exists an object
Î𝑖∈𝐼𝐸𝑖∈𝒞
together with a family of morphisms
𝑝𝑘
:
Î𝑖∈𝐼𝐸𝑖𝐸𝑘
such that for any family of morphisms
ℎ𝑘
:
𝐻 𝐸𝑘
there
exists a unique morphism ℎ:𝐻Î𝑖∈𝐼𝐸𝑖factoring each ℎ𝑘through 𝑝𝑘.
In the above, the dependency on the category
Set
is clear: the indexing object
𝐼
is a set. If we had required
𝐼
to be drawn from a proper subcategory of
Set
(e.g. finite sets) or a proper supercategory (e.g. classes), the notion of product
defined thereby would have been different. The purpose of the formalism of
fibered categories is to explicitly control the ambient category that parameterizes
all indexed notions, such as products, sums, limits, colimits, etc.
Remark 2
(Relevance to computer science)
.
The ability to explicitly control the
parameterization of products and sums is very important in theoretical computer
science, especially for the denotational semantics of polymorphic types of the
form
∀𝛼.𝜏[𝛼]
. Such a polymorphic type should be understood as the product
of all
𝜏[𝛼]
indexed in the “set” of all types, but a famous result of Freyd
[14]
shows that if a category
𝒞
has products of this form parameterized in
Set
, then
𝒞
must be a preorder. Far from bringing to an early end the study of polymorphic
types in computer science, awareness of Freyd’s result sparked and guided the
search for ambient categories other than
Set
in which to parameterize these
products [
37
,
21
,
23
]. Fibered category theory provides the optimal language
to understand all such indexing scenarios, and the textbook of Jacobs
[24]
,
discussed at length in the present paper, provides a detailed introduction to the
applications of fibered category theory to theoretical computer science.
2
1.1 Introduction to fibered categories
Before giving a general definition, we will see the way that fibered categorical
language indeed makes parameterization explicit by considering the prototype
of all fibered categories, the category
Fam(𝒞)
of
Set
-indexed families of objects
of a category 𝒞.
Construction 3
(The category of families)
.
We define
Fam(𝒞)
to be the category
of Set-indexed families in 𝒞, such that
1. an object of Fam(𝒞)is a family {𝐸𝑖∈𝒞}𝑖∈𝐼where 𝐼is a set,
2.
a morphism
{𝐸𝑖}𝑖∈𝐼{𝐹𝑗}𝑗∈𝐽
in
Fam(𝒞)
is given by a function
𝑢
:
𝐼 𝐽
together with for each 𝑖∈𝐼a morphism ¯
𝑢𝑖:𝐸𝑖𝐹𝑢𝑖.
There is an evident functor 𝑝:Fam(𝒞)Set taking ({𝐸𝑖}𝑖∈𝐼)to 𝐼.
Construction 4
(Fiber categories)
.
For each
𝐼∈Set
, we may define the fiber
Fam(𝒞)𝐼
of
Fam(𝒞)
over
𝐼
to be the category of
𝐼
-indexed families
{𝐸𝑖∈𝒞}𝑖∈𝐼
in
𝒞
, with morphisms
{𝐹𝑖}𝑖∈𝐼{𝐸𝑖}𝑖∈𝐼
given by morphisms
ℎ𝑖
:
𝐹𝑖𝐸𝑖
for
each 𝑖∈𝐼.
More abstractly, the fiber category Fam(𝒞)𝐼is the following pullback:
Fam(𝒞)𝐼
1
Fam(𝒞)
Set
𝑝
𝐼
Construction 5
(Reindexing functors)
.
For any function
𝑢
:
𝐽 𝐼
, there is a
corresponding reindexing functor
𝑢∗
:
Fam(𝒞)𝐼Fam(𝒞)𝐽
that restricts an
𝐼-indexed family into a 𝐽-indexed family by precomposition.
With the reindexing functors in hand, can now rephrase the condition that
𝒞has products (Definition 1) in terms of Fam(𝒞).
Proposition 6.
A category
𝒞
has products if and only if for each product projection
function
𝜋𝐼,𝐽
:
𝐼×𝐽 𝐼
, the reindexing functor
𝜋𝐼,𝐽
:
Fam(𝒞)𝐼Fam(𝒞)𝐼×𝐽
has a
right adjoint
Î(𝐼,𝐽)
:
Fam(𝒞)𝐼×𝐽Fam(𝒞)𝐼
such that the following Beck–Chevalley
condition holds: for any function
𝑢
:
𝐾 𝐼
, the canonical natural transformation
𝑢∗◦Î(𝐼,𝐽)Î(𝐾,𝐽)◦ (𝑢×id𝐽)∗is an isomorphism.
The characterization of products in terms of the category of families may
seem more complicated, but it has a remarkable advantage: we can replace
Fam(𝒞)Set
with a different functor satisfying similar properties in order to
speak more generally of when one category has “products” that are parame-
terized in another category. The properties that this functor has to satisfy for
the notion to make sense are embodied in the definition of a fibration or fibered
category; a functor
ℰ ℬ
will be called a fibration when it behaves similarly to
the functor projecting the parameterizing object from a category of families of
objects. We begin with an auxiliary definition of cartesian morphism:
3
Definition 7.
Let
𝑝
:
ℰ ℬ
and let
𝐸 𝐹
be a morphism in
ℰ
, which we
depict as follows:
𝐸
𝑝𝐸
𝐹
𝑝𝐹
In the diagram above, we say that
𝐸 𝐹 lies over 𝑝𝐸 𝑝𝐹
. We say that
𝐸 𝐹
is
cartesian
in
𝑝
when for any morphism
𝐻 𝐹
in
ℰ
and
𝑝𝐻 𝑝𝐸
such that the former lies over the composite
𝑝𝐻 →𝑝𝐸 →𝑝𝐹
in
ℬ
, there exists
a unique morphism
𝐻 𝐸
lying over
𝑝𝐻 𝑝𝐸
such that
𝐻 𝐹
lies over the
composite 𝑝𝐻 𝑝𝐸 as depicted below:
𝐻
𝑝𝐻
𝐸
𝑝𝐸
∃!𝐹
𝑝𝐹
Remark 8
(Explication of cartesian maps)
.
Returning to our example of the
category of families
Fam(𝒞)
over
Set
, we can make sense of the notion of a
cartesian map. Given a function
𝑢
:
𝐽 𝐼
of indexing sets, the reindexing
functor
𝑢∗
takes
𝐼
-indexed families to
𝐽
-indexed families. Given an
𝐼
-indexed
family
{𝐸𝑖}𝑖∈𝐼
, we may define a morphism
𝑢∗{𝐸𝑖}𝑖∈𝐼{𝐸𝑖}𝑖∈𝐼
in
𝒞
whose first
component is
𝑢
:
𝐽 𝐼
and whose second component is the identity function
𝐸𝑢𝑗 𝐸𝑢𝑗
at each
𝑗∈𝐽
. The morphism
𝑢∗{𝐸𝑖}𝑖∈𝐼{𝐸𝑖}𝑖∈𝐼
is then cartesian in
𝑝:Fam(𝒞)Set.
Exercise 9.
Verify that the morphism
𝑢∗{𝐸𝑖}𝑖∈𝐼{𝐸𝑖}𝑖∈𝐼
constructed in Re-
mark 8is indeed cartesian in 𝑝:Fam(𝒞)Set.
In fact, we can strengthen Exercise 9to give an extrinsic characterization of
cartesian morphisms in
Fam(𝒞)
: cartesian morphisms are exactly the “fiberwise
isomorphisms”.
Exercise 10.
Let
𝐸={𝐸𝑖}𝑖∈𝐼
and
𝐹={𝐹𝑗}𝑗∈𝐽
be objects of
Fam(𝒞)
, and let
𝑓
:
𝐸 𝐹
be a morphism between them. Show that the following are equivalent:
1. the morphism 𝑓:𝐸 𝐹 is cartesian;
2. for each 𝑖∈𝐼, the component 𝑓𝑖:𝐸𝑖𝐹𝑝 𝑓 𝑖 is an isomorphism.
The name “cartesian morphism” is inspired by pullbacks, as we see in
Exercise 11 below.
Exercise 11.
Let
ℬ→
be the arrow category of
ℬ
, whose objects are morphisms
of
ℬ
and whose morphisms are commuting squares between them; let
cod
:
ℬ→ℬ
be the codomain functor that projects the codomain of a map
𝐴 𝐵
.
Show that a morphism
𝐸 𝐹 ∈ℬ→
is cartesian if and only if the corresponding
square in ℬis a pullback square (also called a cartesian square).
4
The relationship between cartesian morphisms and pullback squares ex-
pressed by Exercise 11 suggests a generalization of the conventional “pullback
corners” notation to an arbitrary fibration, which we shall use liberally.
Convention 12
(Generalized “pullback corners”)
.
Let
𝑝
:
ℰ ℬ
be a functor;
when we wish to indicate that a morphism
𝐸 𝐹
in
ℰ
is cartesian over
𝑝𝐸 𝑝𝐹
,
we will display it using a “pullback corner” notation as follows:
𝐸
𝑝𝐸
𝐹
𝑝𝐹
Finally we may give the definition of a fibration.
Definition 13.
A functor
𝑝
:
ℰ ℬ
is called a
fibration
when for any object
𝐸∈ℰ
and morphism
𝐵 𝑝𝐸 ∈ℬ
there exists a cartesian morphism
𝐻 𝐸
lying over
𝐵 𝑝𝐸
. The cartesian morphism is often called the
cartesian lift
of
𝐵 𝑝𝐸 at 𝐸.
Convention 14.
We will depict a fibration
𝑝
:
ℰ ℬ
using triangular arrows.
When we wish to leave the functor implicit, we refer to
ℰ
as a
fibered category
over
ℬ
. In the same way that one writes
𝐴×𝐵
for the apex of a product diagram,
we will often write
¯
𝑢
:
𝑢∗𝐸 𝐸
for the cartesian lift of
𝑢
:
𝐵 𝑝𝐸
at
𝐸
as
depicted below:
𝑢∗𝐸
𝐵
𝐸
𝑝𝐸
¯
𝑢
𝑢
In the case of
Fam(ℰ)
, the existence of cartesian lifts for each
𝑢
:
𝐵 𝑝𝐸
corresponds to the reindexing functors 𝑢∗:Fam(𝒞)𝑝𝐸 Fam(𝒞)𝐵.
Exercise 15. Verify that the functor Fam(𝒞)Set is a fibration.
Exercise 16.
Conclude from Exercise 11 that the codomain functor
ℬ→ℬ
is
a fibration if and only if ℬhas all pullbacks.
When the codomain functor
ℬ→ℬ
is a fibration, we will refer to it as
the fundamental fibration, written Pℬfollowing Streicher [52].
1.1.1 Small categories, internal categories
An ordinary category need not have a set of objects — for instance, the category
Set
of all sets has a proper class of objects.
1
Likewise, it is possible to find categories
such that between two objects there may be a proper class of morphisms (e.g. the
1
In this paper, we are somewhat agnostic about set theoretic foundations. Our discussion is
compatible with the viewpoint of ZFC, in which classes are taken to be formulas at the meta-level;
our discussion is, however, also compatible with other accounts of the “set–class” distinction, such as
NBG set theory, MK set theory, or the universe-based approaches of Grothendieck [
2
] and Mac Lane
[29].
5
摘要：

Whatshouldagenericobjectbe?JonathanSterlingUpdatedMarch10,2023AbstractJacobshasproposeddenitionsfor(weak,strong,split)genericobjectsforaberedcategory;buildingonhisdenitionof(split)genericobjects,Jacobsdevelopsamenagerieofimportantbrationalstructureswithapplicationstocategoricallogicandcomputersc...

展开>> 收起<<
What should a generic object be Jonathan Sterling Updated March 10 2023.pdf

共27页,预览5页

还剩页未读， 继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

相关推荐

更多
立即下载
分类：图书资源 价格：10玖币 属性：27 页 大小：488.27KB 格式：PDF 时间：2025-04-29

开通VIP享超值会员特权

  • 多端同步记录
  • 高速下载文档
  • 免费文档工具
  • 分享文档赚钱
  • 每日登录抽奖
  • 优质衍生服务

作者详情

相关内容

更多

热门标签

人际关系 配电装置 动力学连接体 力的合成 高考理综 全宋诗作者索引 公务员考试
/ 27
评分 收藏
分享
立即下载
客服
关注