编辑“︁Lean同态与同构”︁（章节）

== Lean中的实现 ==  
在Lean的数学库Mathlib中，同态和同构通过类型类定义。以下是群同态和同构的示例：

=== 群同态示例 ===  
<syntaxhighlight lang="lean">
import Mathlib.Algebra.Group.Defs

-- 定义两个群G和H
variables (G H : Type*) [Group G] [Group H]

-- 群同态的结构
structure GroupHomomorphism (f : G → H) : Prop where
  map_mul : ∀ a b : G, f (a * b) = f a * f b

-- 示例：恒等同态
def id_hom : GroupHomomorphism (id : G → G) where
  map_mul := λ a b => rfl
</syntaxhighlight>

=== 群同构示例 ===  
<syntaxhighlight lang="lean">
import Mathlib.Algebra.Group.Defs

-- 群同构的结构
structure GroupIsomorphism (f : G → H) extends GroupHomomorphism f where
  bijective : Function.Bijective f

-- 示例：逆映射也是同态
def inv_iso {f : G → H} (iso : GroupIsomorphism f) : GroupIsomorphism (Function.invFun f) :=
  ⟨⟨λ a b => ?_⟩, iso.bijective.2⟩  -- 省略具体证明
</syntaxhighlight>