準同型¶
群準同型や環準同型は，単なる関数ではなく，関数と保存性の証明をまとめた構造体です． このような表現を bundled map と呼びます．
モノイド準同型は M →* N，加法モノイド準同型は M →+ N，環準同型は R →+* S と書きます．
#check MonoidHom
#check AddMonoidHom
#check RingHom
section Homomorphisms
variable {M N P : Type*} [Monoid M] [Monoid N] [Monoid P]
example (f : M →* N) (x y : M) : f (x * y) = f x * f y := by
exact f.map_mul x y
example (f : M →* N) : f 1 = 1 := by
exact f.map_one
example (f : M →* N) (g : N →* P) : M →* P :=
g.comp f
variable {R S : Type*} [Ring R] [Ring S]
example (f : R →+* S) (x y : R) : f (x + y) = f x + f y := by
exact map_add f x y
example (f : R →+* S) (x y : R) : f (x * y) = f x * f y := by
exact map_mul f x y
example (f : R →+* S) : f 0 = 0 := by
exact map_zero f
end Homomorphisms
準同型 f : R →+* S は関数として使えます．
一方で，普通の関数合成 g ∘ f ではなく，構造を保った合成には comp を使います．
これは，合成後の写像が演算を保存することも一緒に記録する必要があるためです．
演習問題¶
以下の問題は，講義中または自習で by 以下を埋めることを想定しています．
まずは #check で使えそうな補題を探し，simp，group，abel，ring，ext を試してください．
モノイド準同型の合成が積を保つことを示してください．