a
но топосы тоже слишком мощные ребята
Size: a a a
2019 August 22
a
слишком много структуры
a
Set^KЕО
Есть такая штука -- реверс-математикс. Берётся теорема какая-нибудь и дальше ищется минимальные условия, чтобы она была верна
ЕО
Можно выбрать, например, лемму Йонеды и искать для чего она соблюдаться будет. А иначе это беспредметный разговор
a
@odomontois ты вот написал доказательство йонеды для сетов в аренде. А какие требования к сету, что нужно требовать от категории К, чтобы заменить SetCat на K?
a
о том и речь
к
Но ослабляя условия меньше теорем доказывается. По-моему это очевидно :)
но те что все еще доказываются, работают для более общих теориях
NI
Set^KЭто категория, которая нужна?
a
нет
a
я пока сам не думал над вопросом особо. надо аренд поставить, поиграться
ЕО
@odomontois ты вот написал доказательство йонеды для сетов в аренде. А какие требования к сету, что нужно требовать от категории К, чтобы заменить SetCat на K?
Ну это уже какое-то другое утверждение получается
ЕО
Доказать лемму Йонеды internally это одно, сформулировать лемму Йонеды для классических категорих и другой структуры это другое (но я не думаю, что такая есть)
ЕО
А возможно ты просто хочешь энричмент лемму Йонеды, это третье
ЕО
Если брать NGB, то Set в нём это очень естественная структура
a
что такое NGB?
ЕО
Если брать универсумы Гротендика, то лемму Йонеды для универсума U будет верна только для U-малых категорий, это будет частный случай https://ncatlab.org/nlab/show/enriched+Yoneda+lemma
ЕО
что такое NGB?
Теория классов, аксиоматика Фон Неймана, Гёделя, Бернайса
ЕО
Но вопрос что нужно чтобы доказать лёмму Йонеды internally менч заинтересовал, он, наверное, самый нетривиальный
NI
что такое NGB?
Одна из двух наиклассических теорий множеств, наряду с ZF.
В NBG ввели понятие "собственные классы" - они могут иметь элементы, но сами элементом являться не могут.
И можно говорить, например, о классе всех множеств.
В NBG ввели понятие "собственные классы" - они могут иметь элементы, но сами элементом являться не могут.
И можно говорить, например, о классе всех множеств.