bundled structure，morphism，subobject¶
Mathlib では，数学的対象を structure として束ねることがよくあります．
たとえば準同型は，単なる関数ではなく「関数本体」と「演算を保つ証明」を持つ structure です．
これを bundled structure と呼ぶことがあります．
bundled にすると，写像そのものと構造保存の証明を 1 つの対象として渡せるため，定理の仮定や合成の記述が整理されます．
#check MonoidHom
#check RingHom
#check MonoidHom.map_one
#check map_add
example : (RingHom.id ℤ) 3 = 3 := by
rfl
example (f : ℤ →+* ℤ) (x y : ℤ) : f (x + y) = f x + f y := by
exact map_add f x y
ℤ →+* ℤ は，整数環から整数環への環準同型です．
map_add は，加法を保つことを表す典型的な補題名です．
Mathlib では，map_zero，map_one，map_mul，map_add のように，写像が構造を保つ定理が統一的な名前で用意されています．
準同型 f : ℤ →+* ℤ は関数のように f x と適用できますが，内部的には関数だけでなく保存性の証明も持っています．
部分構造も bundled な対象として扱われます．
たとえば線形代数では Submodule R M，代数では Subgroup G や Subsemiring R，位相では部分空間に関する構造が現れます．
各論は次章以降で扱いますが，ここでは名前だけ確認しておきます．