范畴论框架下证明集合X到指数对象Ω^X的单射函数存在性

嘿，我来帮你把这个证明用范畴论的纯语言理清楚——不用把Ω^X具体当成函数集，完全基于指数对象的泛性质和赋值映射来推导：

第一步：回顾指数对象的核心结构 #

在集合范畴Set中，给定集合X和真值对象Ω，指数对象Ω^X满足两个关键条件：

• 存在赋值态射 eval: Ω^X × X → Ω，它将Ω^X中的元素（范畴意义上的“函数”）与X中的元素映射到对应的真值；
• 满足泛性质：对任意集合Y和态射 f: Y × X → Ω，都存在唯一的态射 curry(f): Y → Ω^X，使得复合态射 eval ∘ (curry(f) × id_X) = f（这里curry(f) × id_X是Y×X到Ω^X×X的乘积态射）。

第二步：构造从X到Ω^X的态射 #

我们先定义一个态射 δ: X × X → Ω——这是X上对角关系的特征态射：对任意x,y ∈ X，δ(x,y) = t（真）当且仅当x=y，否则为f（假）。

根据指数对象的泛性质，这个δ对应唯一的态射 η = curry(δ): X → Ω^X。这就是我们要找的目标态射，接下来要证明它是单射（Set范畴里的单态射等价于单射函数）。

第三步：证明η是单射 #

假设对于X中的两个元素x₁和x₂，有 η(x₁) = η(x₂)，我们来推导x₁=x₂：

1. 根据curry的定义，对任意y ∈ X，有：
   eval(η(x₁), y) = δ(x₁, y)
eval(η(x₂), y) = δ(x₂, y)
2. 因为η(x₁)=η(x₂)，所以对所有y，δ(x₁,y)=δ(x₂,y)。
3. 取y=x₁，那么δ(x₁,x₁)=t，因此δ(x₂,x₁)=t。根据δ的定义，这直接意味着x₂=x₁。

由此可得，η是单射，也就是存在从X到Ω^X的单射函数。

内容的提问来源于stack exchange，提问作者Squirtle