Well-defined

数学だといろんなところで聞く用語なわけですけどね。Agda だと、

　　f-cong : {A B : Set} → {f : A → B} → → A < x ≈ y > → B < f x ≈ f y >

こんな感じ。数学だと型書かなかったりするから、x = y → f x = f y とか書いてある。

自明なのになんでと思うわけですが、≈ が関係だと自明にならない。ところが ≡ だと自明になる。後者は

　　data _≡_ {A : Set} (a b : A) → Set where
　　　 refl : x ≡ x

なので、Agdaの項として等しいという意味ね。

　 _≈_ : {A : Set} (a b : A) → Set
　 a ≈ b = ?

で自分で勝手に定義する。剰余群だと、mod 2 で等しいとかそんなの。なので自明じゃないので証明する必要がある。

なんで、Well-defined っていうかっていうと、関数の定義が集合論だと二つの集合の関係で well-defined なものだから。

　 F : {A : Set} (a b : A) → Set
　 well-defined-F : {A B : Set} {a b : B} {c d : A} → A < c ≈ d > → F c a → F d b → B < a ≈ b >

まぁ、にてるっちゃにてるけど、別なものだよな。

Agda / 直観主義論理だと関数が先だから、それは必要ない。

凖同型写像 f : A → B は群の構造を保存するわけで、それは A < a ≈ b > が保存する、つまり、B < f a ≈ f b > だってこと。
同値関係を保存するっていう方が明確な用語だよね。

面白いのは、圏論でもこの問題はあるのだが、大体省略されてる。圏の性質を保存する関手の定義には実は cong が必要。

剰余群 G / K は、Gの要素を a ∙ b ⁻¹ ∈ K という同値関係を持つ群に読み替えただけなので、f : G → H はそのまま f : G / K → H
になる。違いは

　　G < a ≈ b > → H < f a ≈ f b >

と

　　G/K < a ≈ b > → H < f a ≈ f b >

だけってことね。 GK < a ≈ b > は a ∙ b ⁻¹ ∈ K なので、x ∈ K → f x ≈ ε が凖同型定理の仮定なので、

　　f x ≈ f x ∙ f y ⁻¹ ∙ f y　≈ f (x ∙ y ⁻¹ ) ∙ f y ≈ ε ∙ f y ≈ f y

ってだけ。 これが凖同型定理だった。G / Ker f ≈ Im f も問題はそれだけでした。

剰余群の GK < a ≈ b > → GK < c ≈ d > → GK < a ∙ c ≈ b ∙ d > も、

　　a ∙ c ∙ (b ∙ d) ⁻¹ ≈ a ∙ c ∙ d ⁻¹ ∙ b ⁻¹ ≈ (a ∙ b ⁻¹) ∙ (b ∙ (c ∙ d ⁻¹) ∙ b ⁻¹)

で、(a ∙ b ⁻¹) ∈ K , (c ∙ d ⁻¹) ∈ K そして、共役元 (b ∙ (c ∙ d ⁻¹) ∙ b ⁻¹) ∈ から出る。

こうすると、共役元が K に属するのが剰余群の条件だってのが良く見える。

残りは自明だってのを納得するのに時間がかかった感じ。