haskell - 为什么反函数不暗示同构

Question

假设我有两个名为 f :: a -> b 的函数它是相反的g :: b -> a这样f . g ≡ id .

现在不是 g . f ≡ id ? (因此暗示同构)

我试图写一个类似的例子并想出了这个:

myRead :: String -> Int
myRead = read

myShow :: Int -> String
myShow = show

在 ghci 中:

λ> myRead . myShow $ 3
3
λ> myShow . myRead $ "33"
"33"

但似乎 inverse function doesn't imply isomorphism .那么有人可以指出我在这里做错了什么吗？

Answer 1

这是一个非常简单的例子。如果 A是集合{1,2}和 B套装{1}然后是功能:

f :: A -> B
f = const 1

g :: B -> A
g 1 = 1

有关系 f . g = id但不是关系 g . f = id .一个反例是

g (f 2) = 1

事实证明，如果您有两个函数，例如 f . g = id和 g . f = id那么这就说明了很多关于这些函数的域和共域的信息。特别是，它建立了一个同构，表明这两个域在某种意义上是等价的。

从范畴论的角度来看，这意味着它们无法通过范畴的态射来区分。范畴论强调范畴的态射是获取对象信息的唯一途径，所以这种不可区分性非常重要。

当你只有单向逆时，你仍然在学习很多关于这两个域的知识……但并不是说它们是同构的。

单向逆给你的一件事是幂等的。幂等是一个函数 i从域到自身(自同态)使得 i . i = i .给定任意两个函数，其中 f . g = id , g . f是幂等的，证明很明显:

i . i = (g . f) . (g . f) = g . f . g . f = g . (f . g) . f = g . f = i

另一个要考虑的好事情是每个函数 f :: A -> B产生“反像”函数 inv f :: B -> (A -> Bool) .

inv :: Eq b => (a -> b) -> b -> a -> Bool
inv f b a = f a == b

在更数学的术语中，逆图像函数是来自 codomain B 的映射。到域的子集 A使得 A 的每个此类子集中的每个元素映射到 B 的相同元素.这些子集划分 A (这是函数的定义)。

如果我们有另一个函数 g :: B -> A这样 g b在子集中 inv f b (即 inv f b (g b) == True 对于所有 b )然后我们有

f . g == id

但这远比 A 弱得多，技术性更强。和 B只是同构。这只是意味着 g正在发送 B 的元素到 A 的子集其中 f将立即发送回来。

例如，它承认 "fibration" 的一个有趣的概念。的一个空间。