V
Да
Size: a a a
2019 November 15
V
Так получится в любом элементарном топосе
KV
Действительно. Круто
LB
Из сюръективности легко следует эпиморфность. Наоборот, пусть f : A -> B — эпи. Тогда определим пару функций B -> Prop, одна из которых все элементы B отправляет в истинное утверждение, а другая отправляет элемент B в утверждение о том, что у него есть прообраз в A. Тогда композиции этих двух функций с f равны. Т.к. f — эпи, то эти функции равны. Другими словами, у любого элемента B есть прообраз в A.
Это охуенно ловко
KV
are_you_a_wizard.jpg
LB
Из сюръективности легко следует эпиморфность. Наоборот, пусть f : A -> B — эпи. Тогда определим пару функций B -> Prop, одна из которых все элементы B отправляет в истинное утверждение, а другая отправляет элемент B в утверждение о том, что у него есть прообраз в A. Тогда композиции этих двух функций с f равны. Т.к. f — эпи, то эти функции равны. Другими словами, у любого элемента B есть прообраз в A.
А можно попросить "из суръективнсти легко следует эпиморфность" показать?
AH
Из сюръективности легко следует эпиморфность. Наоборот, пусть f : A -> B — эпи. Тогда определим пару функций B -> Prop, одна из которых все элементы B отправляет в истинное утверждение, а другая отправляет элемент B в утверждение о том, что у него есть прообраз в A. Тогда композиции этих двух функций с f равны. Т.к. f — эпи, то эти функции равны. Другими словами, у любого элемента B есть прообраз в A.
Похоже на чит)
KV
Похоже на чит)
Вообще-то, конечно, стандартное категорное рассуждение: нарисовали диаграмму, заметили, что она коммутативна, готово
LB
Похоже на чит)
Вообще чит. Истина/ложь это прост значения в сете , как можно использовать значения одного из сетов в рассуждении о сетах :)
LB
(я про сеты узнал вчера, может и можно)
AH
Вообще чит. Истина/ложь это прост значения в сете , как можно использовать значения одного из сетов в рассуждении о сетах :)
Мне тоже показалось это странным ведь так можно доказать любой абсурд, не?
Пусть первая функция отправляет все в ложь, а вторая останется такой же.
Функции все ещё равны, а значит...
Пусть первая функция отправляет все в ложь, а вторая останется такой же.
Функции все ещё равны, а значит...
V
А можно попросить "из суръективнсти легко следует эпиморфность" показать?
Здесь никаких трюков нет. Нам нужно показать, что две функции B -> C равны на всех элементах B, если мы знаем, что они равны на всех элементах вида f(a), но так как f сюръективна, то все элементы имеют такой вид.
V
Вообще-то, конечно, стандартное категорное рассуждение: нарисовали диаграмму, заметили, что она коммутативна, готово
Это как раз пример рассуждений из категорной логики, про которую выше спрашивали.
V
Мне тоже показалось это странным ведь так можно доказать любой абсурд, не?
Пусть первая функция отправляет все в ложь, а вторая останется такой же.
Функции все ещё равны, а значит...
Пусть первая функция отправляет все в ложь, а вторая останется такой же.
Функции все ещё равны, а значит...
Такие функции равны только если у f ни у какого элемента B нет прообраза в A, что может быть верно только если A пусто.
V
Вообще чит. Истина/ложь это прост значения в сете , как можно использовать значения одного из сетов в рассуждении о сетах :)
Разумеется мы можем использовать множества. Как можно что-то доказать про категорию, если мы не можем говорить про ее объекты?
LB
Разумеется мы можем использовать множества. Как можно что-то доказать про категорию, если мы не можем говорить про ее объекты?
Ну значение "ложь" и "истина" в разговоре (лингвистике), отличаются от значений "ложь" и "истина" в булевом сете, разве нет? Т.е. они пишутся однаково, но в случае сетов это просто набор чего-то, без смысла , нельзя же взять и назначит им смысл
V
Ну значение "ложь" и "истина" в разговоре (лингвистике), отличаются от значений "ложь" и "истина" в булевом сете, разве нет? Т.е. они пишутся однаково, но в случае сетов это просто набор чего-то, без смысла , нельзя же взять и назначит им смысл
В интуиционистской логике под множеством утверждений понимается не обычное двуэлементное множество. Вместо этого у нас есть отдельное множество Prop, про которое мы знаем какие-то факты. Например, что она является решеткой, что соответствует наличию конъюнкции и дизъюнкции. Кроме того, на нем есть и другие операции. В категориальных терминах такой объект называется классификатором подобъектов.
V
В данном доказательстве кроме наличия максимального элемента в Prop (истинного утверждения) я ещё использовал тот факт, что квантор существования классифицируется Prop.
LB
В интуиционистской логике под множеством утверждений понимается не обычное двуэлементное множество. Вместо этого у нас есть отдельное множество Prop, про которое мы знаем какие-то факты. Например, что она является решеткой, что соответствует наличию конъюнкции и дизъюнкции. Кроме того, на нем есть и другие операции. В категориальных терминах такой объект называется классификатором подобъектов.
А, Prop это не какой-то абстрактный сет, а такой про который мы знаем чуть больше? Чем это отличается от "сделаем сет из утверждений ,что эта теорема верна. Рисуем стрелочку в этот сет, вот видите, теорема верна"
V
А, Prop это не какой-то абстрактный сет, а такой про который мы знаем чуть больше? Чем это отличается от "сделаем сет из утверждений ,что эта теорема верна. Рисуем стрелочку в этот сет, вот видите, теорема верна"
Да, вполне конкретное множество. Составить множество таких утверждений можно, но потом ещё нужно будет доказать, что эта стрелка существует, что верно только если это утверждение верно.