Бережливое определение групп

Это дополнительный вопрос о типе прохода в качестве параметра

Я попробовал предложение 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, кажется, думает, что это относится к H.add, тогда как предполагается, что это относится к G.add.


type-theory lean
person Tempestas Ludi    schedule 16.04.2021    source источник
comment
Краткое предложение: если хотите, можете посмотреть, как это делается в mathlib. Существует огромная библиотека теории групп и теории категорий: github.com/leanprover-community/mathlib< /а>   -  person jmc    schedule 16.04.2021
comment
Хорошо, это имеет смысл. Тем не менее, это отняло бы у меня немного удовольствия от того, чтобы делать это (почти) самостоятельно, и усложнило бы задачу, поскольку mathlib добавляет всевозможные промежуточные структуры, такие как моноиды.   -  person Tempestas Ludi    schedule 16.04.2021
comment
Обратите внимание, что для получения интерактивной помощи я бы посоветовал вам присоединиться к нашему чату Zulip: leanprover.zulipchat.com. Это большое и очень дружелюбное сообщество бережливых пользователей.   -  person jmc    schedule 16.04.2021
comment
О, точно, я об этом не подумал! Спасибо за предложение!   -  person Tempestas Ludi    schedule 16.04.2021

Ответы (2)


arrow_upward
2
arrow_downward

Проблема в том, что группа не должна быть классом. Если вы посмотрите на тип group.add, по #check @group.add вы получите

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

Квадратные скобки вокруг c : group указывают, что это неявный аргумент, который будет выводиться путем вывода класса типов. Вам не нужно явно вводить этот аргумент, но Lean попытается выяснить, что это такое. Вывод класса типов лучше всего работает для типов, в которых есть только один обитатель, который вы хотите использовать.

В mathlib определение группы ближе к

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

В конкретном типе обычно есть только одна групповая структура, на которую вы хотите сослаться, поэтому в mathlib тип, подобный add_group int, имеет только одного обитателя, о котором вы заботитесь.

Lean автоматически выбрал H в качестве канонического представителя типа group, но это не тот тип, который вам нужен.

Поэтому обычно, когда вы имеете дело с группами, тип и структура группы сохраняются как отдельные объекты, а не объединяются в пару. Однако для теории категорий обычный подход не работает, объект представляет собой пару типа и групповой структуры.

Настройка в mathlib ближе к следующему. coe_to_sort сообщает Lean, как взять group_obj и интерпретировать его как тип без явного написания 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))
person Christopher Hughes    schedule 16.04.2021

arrow_upward
0
arrow_downward

Вы переопределяете нотацию +, что очень быстро приведет к головной боли. Иметь полиморфную нотацию + очень полезно. (Как вы будете обозначать сложение в кольце?)

Дополнительные пункты:

  • вы должны использовать structure вместо class
  • математически вы определяете моноиды и моноидные хомы, а не группы и групповые хомы

Это работает, хотя

(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))
person jmc    schedule 16.04.2021
comment
Почему structure, а не class? Разве класс не позволит мне иметь полиморфизм, например, между кольцами и группами? - person Tempestas Ludi; 16.04.2021
comment
Справедливо, вы правы, что это моноиды. На самом деле я работаю над группами, но удалил строки, которые не способствовали проблеме, которая у меня была. - person Tempestas Ludi; 16.04.2021