精益定义组

Question

这是Lean pass type as parameter的后续问题。

我尝试了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))

我在第一个+上得到了一个错误。精益似乎认为这指的是H.add，而应该是指G.add。

Answer 1

您正在重新定义+表示法，这将很快导致头痛。有一个多态+表示法是非常有用的。(你将如何表示圆环中的加法？)

进一步要点：

您应该使用class

• mathematically，而不是，您定义的是一元和单半群，而不是组和组。

不过，这是可行的。

(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))