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

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


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

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


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

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


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

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


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

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


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

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


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

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

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

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


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

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


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

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


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

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


20/08/14
6497
Рассмотрим диаграмму
$\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
884
Да, по умолчанию не предполагается, что диаграмма коммутативна.

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


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

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


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

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


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

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

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



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

Сейчас этот форум просматривают: нет зарегистрированных пользователей


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

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