2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




Начать новую тему Ответить на тему На страницу Пред.  1, 2, 3, 4, 5, 6 ... 11  След.
 
 Re: Написал учебник теории категорий
Сообщение20.04.2017, 03:47 
Заслуженный участник


31/12/15

895
Вообще, немножко удивляет частое желание непременно формализовать до оснований. Единственный случай, когда обычному математику (не специалисту по основаниям) приходится что-то формализовать до оснований -- это если он решил проверить свои результаты пруфчекером. А в этом случае формализуют в современной теории типов, по техническим причинам она гораздо лучше подходит для пруфчекера.

 Профиль  
                  
 
 Re: Написал учебник теории категорий
Сообщение20.04.2017, 11:14 
Заслуженный участник
Аватара пользователя


20/08/14
6545
Это детская травма. Рассел как-то выгуливал свой парадокс без поводка и ошейника. Он нас сильно покусал, и с тех пор мы очень его боимся.

 Профиль  
                  
 
 Re: Написал учебник теории категорий
Сообщение20.04.2017, 18:42 
Заслуженный участник
Аватара пользователя


27/04/09
27503
Мне почему-то желание убедиться в том, что у аксиом, скажем, $\mathbb R$ есть модели, кажется достаточно сходным с желанием «основать». Кто насколько далеко зайдёт. (У меня это притом тоже есть, и вообще я заинтересовался в своё время матлогикой по таким причинам.)

 Профиль  
                  
 
 Re: Написал учебник теории категорий
Сообщение23.04.2017, 09:00 
Заслуженный участник
Аватара пользователя


02/08/11
6098
george66 в сообщении #1210926 писал(а):
Вообще, немножко удивляет частое желание непременно формализовать до оснований. Единственный случай, когда обычному математику
А нематематику — тем более. Так что это желание внематематическое. Но разве анафункторы, появившиеся, если я правильно понимаю, благодаря этому желанию, не красивы?

 Профиль  
                  
 
 Re: Написал учебник теории категорий
Сообщение23.04.2017, 10:10 
Заслуженный участник
Аватара пользователя


20/08/14
6545
Б. Рассел писал(а):
Я жаждал определенности, как иные жаждут религиозной веры.
Я его понимаю, надо сказать.

 Профиль  
                  
 
 Re: Написал учебник теории категорий
Сообщение23.04.2017, 10:32 
Заслуженный участник


31/12/15

895
Поставьте пруфчекер Agda
https://en.wikipedia.org/wiki/Agda_(pro ... g_language)
и попробуйте что-нибудь доказать. Это, грубо говоря, как Microsoft studio, только для построения математических доказательств, они же лямбда-термы, они же программы на языке Haskell (с некоторыми добавлениями). Доказательства строятся шаг за шагом, на каждом шаге программа проверяет правильность и подсказывает возможные ходы. Это отучит от теории множеств навсегда. Правда, это тоже фигня, зато современная.

 Профиль  
                  
 
 Re: Написал учебник теории категорий
Сообщение23.04.2017, 16:51 
Заслуженный участник
Аватара пользователя


27/04/09
27503
george66 в сообщении #1211806 писал(а):
они же программы на языке Haskell (с некоторыми добавлениями)
По моим поверхностным впечатлением, Agda никак нельзя назвать хаскелем с добавлениями, это довольно другой язык.

-- Вс апр 23, 2017 18:52:10 --

Зато она на нём сама написана.

 Профиль  
                  
 
 Re: Написал учебник теории категорий
Сообщение23.05.2017, 13:41 
Заслуженный участник
Аватара пользователя


20/08/14
6545
Я про протоморфизмы чего-то не понял. Итак, они отличаются от морфизмов только тем, что протоморфизм может иметь сколько угодно начал и концов. Затем мы берем упорядоченную тройку "объект $A$, объект $B$ и протоморфизм $\varphi$ такой, что одним из его начал является $A$ и одним из его концов является $B$" и называем эту тройку морфизмом $f: A \to B$.
В учебнике сказано, что такое построение категории "обычно используется на практике". Можно ли развернуть этот тезис, проиллюстрировать примерами? Пока никакой практики я в нем не вижу, вижу "почесать левой ногой правое ухо". В частности, не понимаю, что означает фраза
Цитата:
Именно так мы строили категорию Set, протоморфизмами в этом случае были теоретико-множественные функции
Сколько я помню теоретико-множественное определение функции, у функции ровно одно "начало" (область определения) и ровно один "конец" (область значений). Где же тут протоморфизм, когда это морфизм в чистом виде?

 Профиль  
                  
 
 Re: Написал учебник теории категорий
Сообщение23.05.2017, 13:59 
Заслуженный участник


31/12/15

895
Теоретико-множественная функция определяется как множество пар. Например, функция на натуральных числах, тождественно равная нулю, определяется как множество пар $(0,0), (1,0), (2,0)\ldots$ По ней можно восстановить область определения, но нельзя восстановить область значений (виден один 0), что написано в Примере 1.3

 Профиль  
                  
 
 Re: Написал учебник теории категорий
Сообщение23.05.2017, 14:21 
Заслуженный участник
Аватара пользователя


20/08/14
6545
Понятно. Мы с Вами привыкли к разным определениям функции. Вы определяете функцию как множество упорядоченных пар с определенными свойствами. Я - как упорядоченную тройку $(X, Y, \Gamma)$, где $\Gamma \subset X \times Y$ - то самое множество упорядоченных пар, которое в этом определении называется не функцией, а графиком функции. Каким из этих двух определений пользоваться - вопрос вкуса, но в математической литературе они встречаются со сравнимой частотой, и стоит иметь в виду, что читатель может исходить из второго определения.

 Профиль  
                  
 
 Re: Написал учебник теории категорий
Сообщение26.05.2017, 13:13 
Заслуженный участник
Аватара пользователя


20/08/14
6545
Рассмотрим диаграмму
$\xymatrix{X\ar[rd]_h\ar[rr]^f&&Y\ar[ld]^{g}\\&Z}$
где $f, g, h$ - некоторые морфизмы, о которых мы знаем только то, что нарисовано на диаграмме.
Правильно ли я понимаю, что мы не можем сказать, коммутативна эта диаграмма или нет? А чтобы сказать, что она коммутативна, надо удостовериться, что $h = g \circ f$ (что из изображенной диаграммы не следует)?

 Профиль  
                  
 
 Re: Написал учебник теории категорий
Сообщение26.05.2017, 14:22 
Заслуженный участник


31/12/15

895
Да, по умолчанию не предполагается, что диаграмма коммутативна.

 Профиль  
                  
 
 Re: Написал учебник теории категорий
Сообщение26.05.2017, 14:29 
Заслуженный участник
Аватара пользователя


20/08/14
6545
В связи с этим интересно, что в пособиях по набору формул в $\TeX$ соответствующий раздел неизменно называется "коммутативные диаграммы", как будто некоммутативных не бывает. Это сбивает с толку.

 Профиль  
                  
 
 Re: Написал учебник теории категорий
Сообщение26.05.2017, 14:38 
Заслуженный участник


13/12/05
4036
Ни разу не видел, чтобы диаграмма была нарисована и при этом не была коммутативной.

 Профиль  
                  
 
 Re: Написал учебник теории категорий
Сообщение26.05.2017, 14:49 
Заслуженный участник
Аватара пользователя


20/08/14
6545
Почему? Некоммутативные диаграммы никому не нужны?

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 157 ]  На страницу Пред.  1, 2, 3, 4, 5, 6 ... 11  След.

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: lel0lel


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group