Здравствуйте, Lazy Cjow Rhrr, Вы писали:
LCR>Привет.
LCR>Пусть у нас задана категория C с множеством объектов O и множеством морфизмов M={f}.
LCR>1. Верно ли, что область определения каждого морфизма ? один и только один элемент из O. Область значений ? тоже один, и только один элемент из O?
Конечно верно. Это следует из определения категории. Категория — это два множества: стрелок и объектов, и две функции, первая — DOM — сопоставляет каждой стрелке объект и тоде самое делает вторая функция — CODOM. Иначе говоря, если у нас есть стрелка f, то значение DOM(f) — это некоторый объект, начало этой стрелки, а CODOM(f) — соответственно, ее конец. Ключевое слово здесь "функция". Функция всегда сопоставляет каждому элементу области определения единственный элемент образа. Значит, для каждой стрелки существует единственное ее начало и конец.
LCR>2. Почему морфизм можно отождествить с информацией о типе элементов? Элементов ли?
Здесь много чего сказано и, наверное, сначала надо разобраться, что такое элементы в категориях. Элементы — это точки множеств. Когда мы смотрим на множества категорным взглядом, то образуем категорию всех множеств, в которой стрелки между объектами — это функции между множествами, а сами множества — объекты. Композиция функций — это композиция стрелок, а тождественная функция множества X, это вполне себе стрелка IdX, пропускающая без изменений любый другие функции-стрелки. Вот с этой точки зрения множества совсем не содержат элементов, а представляются как такие монолитные структуры — объекты категории. Это резко контрастирует с теоретико-множественным подходом, который можно назвать атомарным и в котором множество всегда уже расчленено на свои составляющие. В школе нас учат именно такому взгляду на математику и вообще на Мир. Между тем, это не обязательно единственная и верная точка зрения. В качестве оснований математики вполне можно взять и категорию, как монолитный элемент нашего мышления. Это когда строго обосновал Ловер. Сам такой подход к математике называется top-down в сравнении с теоретико-множественным bottom-up. Но что-же тогда есть элементы множеств? Элементами мы называем указатели из точки в объект. Иначе говоря, в категорном множестве мы указываем элементы стрелками из специального объекта — точки. Мы не "заглядываем внутрь" множества а смотрим снаружи и сколько видим элементов, на столько и указываем. Специальный объект "точка" можно тоже охарактеризовать в терминах стрелок, а именно: в точку из любого множества можно построить только одну функцию, не больше и не меньше. По этой причине, точку часто называют терминальным объектом. Итак, элемент объекта A — это стрелка f : T --> A из терминального объекта T в объект A. Сколько таких стрелок есть, столько и элементов у объекта. Но конечно, одного только терминального объекта недостаточно чтобы сделать произвольную категорию похожей на множества. Ведь с множествами можно делать многие вещи — различным образом строить новые множества. Для двух множеств мы можем построить из объединение, пересечение, дополнение и т.д. Также, декартово произведение и множество всевозможных функций из одного множества в другое (это ведь тоже множество!). Все эти процессы необходимо тоже описать категорно. И удивительно, но это было сделано Ловером и Тирни в конце 60-х годов. они охарактеризовали все эти теоретико-множественные операции в терминах взаимоотношений между стрелками в категории. Кроме того, очень важная вещь — это возможность говорить о множестве, является ли оно или нет подмножеством другого. Как это сделать категорно — понять очень трудно. Оказывается, все же можно. С этой целью Ловер и Тирни ввели специальную категорную конструкцию — классификатор подобъектов. Вот оказалось, что категория со всеми такими свойствами позволяет делать все те вещи, что можно делать и со множествами. Такую категорию назвали элементарным топосом. элементарный топос — это категорный аналог множества. Почему элементарный? Потому, что слово "топос"появилось не у Ловера и Тирни, а у Гротендика, который обобщал одну интересную математическую конструкцию. Эта конструкция встречается еще у Римана в его теории аналитических функций, а также в алгебраической геометрии, топологии и даже в теории дифференциальных уравнений. Это конструкция носит название пучок. Оказывает, пучок удовлетворяет всем требованиям элементарного топоса и таким образом может рассматриваться как топос, т.е. как некое обобщенное множество. Пучки — это нечто среднее между множеством и топологией. Так вот, когда мы говорим об элементах, подмножествах и т.п. в категориях, мы всегда имеем ввиду, что такая категория является топосом. С помощью топосов можно можелировать теории точно также как и с помощью множеств. Но здесь есть несколько важных отличий. Некоторые конструкции, например семантику Крипке в модальной логике, очень трудно промоделировать с помощью множеств. Что есть семантика Кримпке? У Крипке понятие истинности не абсолютно, у него в логику введено время. Т.е. есть такая временная прямая, и на каждом элементе прямой (моменте времени) — есть свой мир — модель теории. Мы движемся по времени и миры меняются — то что раньше не было истинным, может стать таковым. Так мы моделируем процесс познания. Пучком эта вещь моделируется очень просто. На самом деле пучок и есть такая конструкция. Есть базовое индексной множество с топологией на нем, в случае семантики Крипке это прямая времени, и куча палок, " вертикально воткнутых в каждую точку пространства" — это миры. Ну раз можно моделировать такие сложные структуры, то можно моделировать и более простые вещи, такие как лямбда-исчисление или еще что-то. Что такое тип? Это некое множество элементов, котрому мы обычно даем имя, но можем и не давать. Что тогда значит фраза: элемент такого-то типа? Да очень просто, это значит что мы указываем в этом множестве некий элемент, т.е. есть стрелка из терминального объекта в объект множества.
mefrill,
LCR>>Пусть у нас задана категория C с множеством объектов O и множеством морфизмов M={f}.
LCR>>1. Верно ли, что область определения каждого морфизма f один и только один элемент из O. Область значений f тоже один, и только один элемент из O? M>Конечно верно.
Хорошо, я просто сомневался.
LCR>>2. Почему морфизм можно отождествить с информацией о типе элементов? Элементов ли? M>Здесь много чего сказано и, наверное, сначала надо разобраться, что такое элементы в категориях. ...
Ууууу, вот это ответищщще!
Но всё-таки... Возвращаясь к картинке: пусть тот мой граф на 7-ми вершинах задаёт категорию (подозреваю для таких категорий, порождённых обыкновенными ациклическими ориентированными графами есть специальный термин).
Но здесь я совсем не вижу терминальных объектов. И мои размышления (возможно ошибочные) приводят к выводу, что каждая стрелка — отдельный тип, и я имею следующую картину:
1. единичные стрелки — 7 штук.
2. нарисованные стрелки — 8 штук.
3. стрелки полученные замыканием — 4 штуки.
Итого 19 стрелок, то есть типов.
Есть ли нетривиальный пример? Такой, чтобы типов было мало, а стрелок — много
Здравствуйте, Lazy Cjow Rhrr, Вы писали:
LCR>Но всё-таки... Возвращаясь к картинке: пусть тот мой граф на 7-ми вершинах задаёт категорию (подозреваю для таких категорий, порождённых обыкновенными ациклическими ориентированными графами есть специальный термин). LCR>Но здесь я совсем не вижу терминальных объектов. И мои размышления (возможно ошибочные) приводят к выводу, что каждая стрелка — отдельный тип, и я имею следующую картину: LCR>1. единичные стрелки — 7 штук. LCR>2. нарисованные стрелки — 8 штук. LCR>3. стрелки полученные замыканием — 4 штуки. LCR>Итого 19 стрелок, то есть типов.
Объект категории — не обязательно тип. Вообще, категория — это некая математическая абстракция — специальный язык для описания математических конструкций. Точно также, множество — это специальная математическая абстракция и не предназначено специально для описания типов. Множества, также как и категории, можно использовать для моделирования типов. Каким образом? Тип — это объединение элементов нашего мышления на основании каких-либо общих свойств. Таким образом, тип — это множество элементов. Так и моделируют во множествах типы, т.е. задают каждый тип некоторым множеством. В категориях типы можно задавать объектами. Причем, не обязательно указывая их элементы. Все зависит от цели, от того, для чего мы производим такое моделирование. Если нашей целью является просто задание какого-то отношения между типами, то вполне возможно задать каждый тип просто объектом, а отношение между двумя объектами — стрелкой. Надо конечно, чтобы такое отношение удовлетворяло условиям категории, т.е. было как говорят, предпорядком. Предпорядок — это отношение <=, в котором для любого объекта a выполняется a <= a и для любых трех объектов a, b, c — если a <= b и b <= c, то a <= c. В таком случае мы можем образовать категорию предпорядка, в которой объектами являются элементы отношения, а стрелки определяются так: если a <= b, то полагаем что есть стрелка a --> b. Тогда все аксиомы категории выполнены. Я думаю, что на самом деле что-то такое имелось ввиду. Здесь категория задает отношение между типами, а сами типы рассматриваются как атомарные объекты. Смысл такого отношения может быть разным. Например, если мы моделируем типы в ООП, то отношение — это наследование. Транзитивность выполняется, а если положить, что каждый тип может являться наследником самого себя, то мы вполне можем задать такое отношение категорией. Понятно, что там надо вводить дополнительные ограничения, типа ацикличности и т.п. чего в произвольной категории нет.
LCR>Есть ли нетривиальный пример? Такой, чтобы типов было мало, а стрелок — много
Ну если есть одно отношение между типами, то максимум одна стрелка между объектами может быть. Но можно ввести более одного отношения. Например, кроме отношения наследование ввсти отношение использования или еще какое. Короче. придумывай что хочешь, моделируй как хочешь. Только я очень сомневаюсь, что от такого моделирования будет какая-то польза, ведь основного аппарата теории категорий здесь не применишь.
Здравствуйте, EvilChild, Вы писали:
EC>А есть в природе книга, где ТК была бы описана так же доступно и увлекательно и таким же живым языком?
На русском есть Голдблатт "Теория топосов. Категорный анализ логики" и есть перевод знаменитой, ставшей уже классической, книги Маклейна "Категории для работающего математика". Последняя книжка требует уже хорошего математического образования и потому читается непросто. Есть ее хорошее изложение в элементарной форме, книжка Стива Эводи, к сожалению на английском, но доступна онлайн (точнее была доступна, сейчас не нашел, и у себя на компе не нашел. В прошлом году я себе распечатал в бумажном виде, потому не озаботился электронной версией). Полное название: Steve Awodey "Category theory". Вот эту книжку я советую для чтения, а потом уже Маклейна можно будет читать если интересно станет.
Здравствуйте, EvilChild, Вы писали:
EC>Здравствуйте, mefrill.
EC>А есть в природе книга, где ТК была бы описана так же доступно и увлекательно и таким же живым языком?
Здравствуйте, mefrill, Вы писали:
M>На русском есть Голдблатт "Теория топосов. Категорный анализ логики" и есть перевод знаменитой, ставшей уже классической, книги Маклейна "Категории для работающего математика". Последняя книжка требует уже хорошего математического образования и потому читается непросто. Есть ее хорошее изложение в элементарной форме, книжка Стива Эводи, к сожалению на английском, но доступна онлайн (точнее была доступна, сейчас не нашел, и у себя на компе не нашел. В прошлом году я себе распечатал в бумажном виде, потому не озаботился электронной версией). Полное название: Steve Awodey "Category theory". Вот эту книжку я советую для чтения, а потом уже Маклейна можно будет читать если интересно станет.
mefrill, Вы писали:
M> Здесь категория задает отношение между типами, а сами типы рассматриваются как атомарные объекты. Смысл такого отношения может быть разным. Например, если мы моделируем типы в ООП, то отношение — это наследование. Транзитивность выполняется, а если положить, что каждый тип может являться наследником самого себя, то мы вполне можем задать такое отношение категорией. Понятно, что там надо вводить дополнительные ограничения, типа ацикличности и т.п. чего в произвольной категории нет.
Вопрос в сторону — а в произвольной категории допустимы циклы? Вроде как если есть цикл, то мы автоматически получаем морфизмы каждого объекта в каждый для объектов из этого цикла. Этот цикл тогда можно "выкусить" и заменить объектом. Так что можно без ограничения общности считать, что категория не содержит циклов. Я нигде не ошибся?
M>Ну если есть одно отношение между типами, то максимум одна стрелка между объектами может быть. Но можно ввести более одного отношения. Например, кроме отношения наследование ввсти отношение использования или еще какое. Короче. придумывай что хочешь, моделируй как хочешь. Только я очень сомневаюсь, что от такого моделирования будет какая-то польза, ведь основного аппарата теории категорий здесь не применишь.
Хорошо, спущусь на самую землю: читаю определение (из статьи "don't panic").
3. Тернарное отношение называется информацией о типах категории C. Мы хотим, чтобы каждый морфизм имел тип, поэтому категория требует .
Мы пишем . Также мы хотим, чтобы типы были уникальными, поэтому потребуем ещё
Это даёт нам возможность рассматривать морфизм как отображение одного объекта на другой...
Так вот, поскольку каждый морфизм имеет ровно один вход и один выход, то множество точек отношения \cal{T} оказывается подмножеством множества морфизмов. Но требование того, чтобы каждый морфизм имел тип приводит нас к тому, что \cal{T} оказывается равномощно множеству морфизмов \cal{M}.
Вот я и не понимаю, зачем мутить воду, а не просто сказать, что вот пусть у нас дано множество типов, и существует биективное отображение морфизмов на это множество... Я не понимаю, почему типы определяются именно так.
Здравствуйте, Lazy Cjow Rhrr, Вы писали:
LCR>Вопрос в сторону — а в произвольной категории допустимы циклы? Вроде как если есть цикл, то мы автоматически получаем морфизмы каждого объекта в каждый для объектов из этого цикла. Этот цикл тогда можно "выкусить" и заменить объектом. Так что можно без ограничения общности считать, что категория не содержит циклов. Я нигде не ошибся?
Циклы вполне допустимы. Категория может иметь довольно сложную структуру. Например, как представить моноид как категорию? Моноид — это множество с операцией * на парах его элементов, такой что для любых трех элементов a,b,c выполняется a*(b*c)=(a*b)*c. Также есть специальный элемент e, для которого e*a=a*e=a для любого элемента a. Пример моноида — множество натуральных чисел, включая нуль, и + в качестве операции. Тогда e — это и есть ноль. Любой моноид можно представить категорией с одним объектом, а именно: множество элементов моноида — единственный объект категории, а каждый элемент — стрелка из этого объекта в него самого. Тогда элемент e — это единичная стрелка для единственного объекта, а операция на элементах — это просто умножение стрелок. Все аксиомы категории выполнены ввиду выполнения аксиом моноида. В частности, множество натуральных чисел N — это категория с бесконечным количеством стрелок 0,1,2,... и одним объектом N.
В теории категорий выделяются специальные пары стрелок, которые называются изострелками. Изострелка — это стрелка f из a в b, для которой существует обратная стрелка, т.е. стрелка g из b в a, такая что g*f=Ida и f*g=Idb. Иначе говоря, композиции (это ведь тоже стрелки!) этих стрелок — это единичные стрелки на объектах a и b соответственно. Вот отсюда можно вывести, что такие изомофрные объекты можно безболезненно склеить. Ведь чем объекты в произвольной категории отличаются друг друга? Сами по себе они совершенно одинаковы, разница заключается в стрелках, котрые приходят в эти объекты и исходят из них. Значит, два объекта одинаковы, если в них приходят примерно одни и те же стрелки и примерно одни и те же стрелки исходят из них. Что значит примерно это надо подумать. Вот если два объекта изоморфны, то оказывается их можно безболезненно склеить, склеив и соответствующие стрелки. Почему так можно понять, если увидеть, что любая стрелка в любой из этих двух объектов пропускается через композицию f и g и снова в себя, так как композиция — это единичная стрелка. Вообще, нам и склеивать эти стрелки не надо, достаточно просто их не различать. Что в теории категорий и делают — считают одинаковыми изоморфные объекты. Есть даже такое выражение: с точностью до изоморфизма. Многие категорные конструкции определяются с точностью до изоморфизма.
M>>Ну если есть одно отношение между типами, то максимум одна стрелка между объектами может быть. Но можно ввести более одного отношения. Например, кроме отношения наследование ввсти отношение использования или еще какое. Короче. придумывай что хочешь, моделируй как хочешь. Только я очень сомневаюсь, что от такого моделирования будет какая-то польза, ведь основного аппарата теории категорий здесь не применишь.
LCR>Хорошо, спущусь на самую землю: читаю определение (из статьи "don't panic").
LCR>
LCR>3. Тернарное отношение называется информацией о типах категории C. Мы хотим, чтобы каждый морфизм имел тип, поэтому категория требует .
LCR>Мы пишем . Также мы хотим, чтобы типы были уникальными, поэтому потребуем ещё
LCR>Это даёт нам возможность рассматривать морфизм как отображение одного объекта на другой...
LCR>Так вот, поскольку каждый морфизм имеет ровно один вход и один выход, то множество точек отношения \cal{T} оказывается подмножеством множества морфизмов. Но требование того, чтобы каждый морфизм имел тип приводит нас к тому, что \cal{T} оказывается равномощно множеству морфизмов \cal{M}.
LCR>Вот я и не понимаю, зачем мутить воду, а не просто сказать, что вот пусть у нас дано множество типов, и существует биективное отображение морфизмов на это множество... Я не понимаю, почему типы определяются именно так.
Я тоже не знаю. Думаю, что сделано это затем, чтобы построить категорию на основе отношения между типами. Т.е. категория заранее не дана, а строится по ходу дела на основе этого самого тернарного отношения. Поэтому вводятся ограничения чтобы удовлетворять аксиомам категории. Типы здесь это некоторые метамножества стрелок, сами не входящие в категорию. Написано об этом довольно бессвязно и непонятно, поэтому я тоже мог понять не в ту сторону, но мне кажется, что автор это имел ввиду.
Здравствуйте, Lazy Cjow Rhrr, Вы писали:
LCR>Так вот, поскольку каждый морфизм имеет ровно один вход и один выход, то множество точек отношения \cal{T} оказывается подмножеством множества морфизмов. Но требование того, чтобы каждый морфизм имел тип приводит нас к тому, что \cal{T} оказывается равномощно множеству морфизмов \cal{M}.
Почему равномощно? Вса морфизмы из a в b могут иметь один тип или подразделяться на красные и зеленые.
quicksort =: (($:@(<#[),(=#[),$:@(>#[)) ({~ ?@#)) ^: (1<#)
.
называется информацией о типах категории C. Мы хотим, чтобы каждый морфизм имел тип, поэтому категория требует
.
. Также мы хотим, чтобы типы были уникальными, поэтому потребуем ещё
