精益定义组

问题描述

的后续问题

我尝试了 jmc 的建议，这似乎奏效了，但后来我又陷入了困境。问题的最初目的是定义群和环的类别，但现在显然我无法定义群态射：

class group :=
(set: Type)
(add: set → set → set)

infix + := group.add

class group_morphism (G H: group) :=
(f: G.set → H.set)
(additive: ∀ g h : G.set,f(g + h) = (f g) + (f h))

我在第一个 + 处遇到错误。 Lean 似乎认为 this 指的是 H.add，而它应该指的是 G.add。

解决方法

问题是组不应该是一个类。如果查看 group.add 的类型，通过 #check @group.add 你会得到

group.add : Π [c : group],group.set → group.set → group.set

c : group 周围的方括号表示这是一个隐式参数，将由类型类推断进行推断。您不必显式键入此参数，但 Lean 会尝试弄清楚它是什么。类型类推断最适用于您只想使用一个居民的类型。

在 mathlib 中，group 的定义更接近于

class group (set : Type) :=
(add : set → set → set)

对于一个特定的类型，通常只有一个组结构你想引用，所以在 mathlib 中，像 add_group int 这样的类型只有一个你关心的居民。

Lean 自动选择 H 作为类型 group 的规范代表，但这不是您想要的。

所以通常当你处理组时，类型和组结构作为单独的对象保存，它们不会成对。但是对于范畴论来说，通常的方法是行不通的，一个对象是一个类型和一个组结构的对。

mathlib 中的设置更接近于以下内容。 coe_to_sort 告诉 Lean 如何获取 group_obj 并将其解释为 Type 而无需显式编写 G.set，group_obj_group 实例告诉 Lean 如何自动推断类型上的组结构group_obj

class group (set : Type) :=
(add: set → set → set)

structure group_obj :=
(set : Type)
(group : group set)

instance coe_to_sort : has_coe_to_sort group_obj :=
{ S := Type,coe := group_obj.set }

instance group_obj_group (G : group_obj) : group G := G.group

infix `+` := group.add

structure group_morphism (G H : group_obj) :=
(f: G → H)
(additive: ∀ g h : G.set,f(g + h) = (f g) + (f h))

您正在重新定义 + 表示法，这会很快导致头痛。多态 + 表示法很有帮助。（你将如何表示环中的加法？）

其他要点：

你应该使用 structure 而不是 class
在数学上，您是在定义幺半群和幺半群 homs，而不是群和群 homs

虽然有效

(set: Type)
(add: set → set → set)

def add {G : group} := group.add G

class group_morphism (G H: group) :=
(f: G.set → H.set)
(additive: ∀ g h : G.set,f(add g h) = add (f g) (f h))

lean type-theory