Category product 続き

通りすがり 『「AxBとXはisom」の定義は「f:AxB→Xとg:X→AxBをどう選んでも逆射になってる」ではなく「f:AxB→Xとg:X→AxBをうまいこと選んでやると逆射になってる」ことだと思います。
Product と言うだけで存在が保証される射(X, AxB の間にどっち方向にも存在しなくてはならない射)は1つだけなので、f=(a,b)とg=(a’,b’)とします。これらから定義したi=f.gを使うと、x.i=yという仮定からx=yが導けます。なので、「f,gが逆射でない」は成り立ちません。(あるいは、i=f.gかつx≠yと仮定してしまうとその時点で矛盾が生じています。なのでそれを前提にした結論から何が出てきても無意味です。)…といったところでしょうか。』

通りすがりさん、毎回違う人かもしれないけどいつもありがとう。
確かに間違ってるとしたらそこ (¬ x≠y) しかありませんね。isom の定義については了解しています。下図の圏では X←→AxB な射が f = , g = しか無いつもりだったので暗黙に f^{-1} = g が導けるものと決めつけてます。
でも、どーしても何で x.i = y → x = y になるのかわからない。どうやって導くんだこれ。
わからないので google 先生でカンニングすると、出てきた証明が理解不能だったので、自分での証明はとりあえず断念。これはどっかで何かの定義を勘違いしてるかも知れない。
Link 先にある証明をちょっと訳してみる:

A, B を適当な圏の対象とする。3-tuple (AxB, a, b) と (X, a', b') は A と B の積であるとする。ここに、a と a' は A への射影、b と b' は B への射影をあらわす射である。積の定義により、射 f:AxB→X (= ) と g:X→AxB (= ) が存在し、各射影 morphism と commute する、すなわち

  • a'.f = a
  • b'f = b
  • a.g = a'
  • b.g = b'

である。これらの等式から、

  • a.(g.f) = a (1)
  • b.(g.f) = b (2)

を導くことができる。ここに a.id = a, b.id = b, ただし id は AxB→AxB の恒等射。ここで、積の定義により (1), (2) の等式を成立させる AxB→AxB の射は一つしかない事が保証されている (原文: The definition of product says there is a unique morphism from c into c that makes all the triangles commute.) から、g.f = id である。同様にして f.g も恒等射になることが示せる。

で、強調した部分が意味不明。定義で一意性が保証されているのは f, g, と各種射影 morphism だけのはず。確かに f.g と g.f が A, B への射影 morphism との合成について、恒等射と区別できないのは納得。でもそれ以外の射まで含めて恒等射と区別不可能なようでなくては f.g, g.f が恒等射そのものであるとは言えないはず。そこで持ち出したのが下に図示した C と i, x, y, h と特に x.i = y (≠x) の条件だったんだけど、これは何故どういう風に矛盾するのか。そしてこれ以外の形でも k.(f.g) ≠ k なる射 k が存在し得ないというのはどうして言えるのか。
誰か説明してくださいお願いします。(へこへこ