Для понимания в данном случае достаточно зафиксировать некоторое каноническое вложение.

Правильно. И канонического вложения колец в группы - таки нет. Как и 2-категорий в 1-категории.

Естественно.

Упрощаем задачу. По-вашему, понятие «два человека» - частный случай понятия «один человек»?

> Правильно. И канонического вложения колец в группы - таки нет. Как и 2-категорий в 1-категории.

Так нам не надо вкладывать кольца в группы и 2-категории в 1-категории. Нам надо наоборот - группы в кольца и 1-категории в 2-категории. А такие вложения есть.

> Упрощаем задачу. По-вашему, понятие «два человека» - частный случай понятия «один человек»?

Правильно «хотя бы из одного». И «хотя бы из двух».

Так нам не надо вкладывать кольца в группы

Как раз надо.

Нам надо наоборот - группы в кольца

Тоже не вложатся, кстати. Нет ни одного разумного вложения класса групп в класс колец, как и наоборот.

Правильно «хотя бы из одного».

Так. Теперь дальше: кто вам сказал, что «множество с двумя структурами» - это значит «множество с хотя бы двумя структурами»? В определении слово «хотя» есть?

> Тоже не вложатся, кстати. Нет ни одного разумного вложения класса групп в класс колец, как и наоборот.

Целые классы то зачем?

В определении слово «хотя» есть?

В математике всегда сказано только то, что сказано. Если сказано, что в множестве есть элемент X - значит в множестве есть элемент Х. Это не значит, что в этом множестве нету, например, элемента Y. Вот если бы было сказано, что Y там нет...

Да ни какой из них не более «высокоуровневый».

Если я беру язык Foo и добавляю к нему разных выразительных средств, то получившийся Foo++ имею полное право называть более высокоуровневым.

«Чисто технически» любое категорное утверждение - это и так теоретико-множественное утверждение. И его вообще не надо переводить.

Да? Т.е. нарисованную струнную диаграмму не нужно переводить?

Задаем набором множеств. Причем _тем же самым_, что самое забавное. Просто в теоркате мы взяли и этот набор обозвали «2-категорией».

Вот есть классы и множества — это основа, есть все высказывания о классах и множествах — это теоретико-множественный язык с определённой логикой. Теперь, категория это два класса с дополнительными свойствами. Все высказывания теории множеств имеют место быть и в ТК как высказывания о классах категории, но _никак не_ о самих категориях. Мы можем сказать «счётное множество», и «счётное множество объектов категории», но не можем сказать «счётная категория» (если не определим что это такое). Аксиоматика категорий агрегирует аксиоматику множеств. Какое-то высказывание о категориях, например «категория моноидальна», переводится в ряд теоретико-множественных высказываний о классах категории, тут я согласен (хотя, есть и разница — сказать «сопряжённый функтор бла-бла-бла», или написать длинную портянку утверждений о множествах). Однако, дело в том, что в ТК есть свой язык который не имеет аналога в теории множеств и называется теоретико-стрелочным языком, он и не может иметь аналога, так как это _графический_ язык коммутативных и струнных диаграмм. Можно только говорить, что этот язык «компилируется» в теоретико-множественный, но это имеет значение только если мы обсуждаем _генезис_ (вот как сейчас), если же мы просто берём ТК как инструмент, то мы используем её теоретико-стрелочный язык как таковой и наши высказывания имеют к теории множеств опосредованное отношение.

Это про 0-категории по отношению к 1-категориям.

То же самое с 2-категориями — аксиоматика 2-категорий агрегирует аксиоматику 1-категорий, любое высказывание о 1-категории справедливо по отношению к 1-категории которая соответствует данной 2-категории, но _никак не_ к самой этой 2-категории (для неё такое высказывание просто не определено). При этом графический язык 2-категорий также расширяется и какие-то диграммы не имеют аналогов в графическом языке 1-категорий.

Вы просили пример такого утверждения — 2-аналог симметричной моноидальной категории не является симметричной моноидальной 2-категорией.

Да при чем тут ключевые слова?

При том, что их можно гуглить.

Хотя я понимаю, чего - теорем-то таких нет. Вот и приводить в пример - нечего.

Вы отрицаете возможность сформулировать теорему на категорном языке? Или возможность сформулировать новую теорему? Или что?

Кстати, теоремы о когерентности есть в той самой книжке Маклейна :) Осталось только увидеть связь с CR. Это и будет выражением в терминах предметной области теорем о когерентности.

Вы не поверите - эти разделы _изначально_ были изложены на одном языке. И нетривиальные аналогии _сперва_ появляются в рамках какой-либо предметной области и только _потом_ описываются в рамках теорката. Когда они уже есть.

Например, Карри-Говард? А какие ещё аналогии появились _сперва_?

К слову, на счет необходимости типов для задания нетипизированного лямбда-исчисления. Вы можете взять в качестве объектов теперь стрелки, в качестве стрелок - 2-стрелки, в результате получаете категорию, которая эффективно содержит всю структуру вашей первоначальной 2-категории. Типы - не нужны.

Потому это и нетипизированное лямбда-исчисление :) Та или иная модель имеет смысл только если она удобна — в данном случае может быть удобна такая 1-категория без внимания к типам (так как там только 1 и Term объекты). Но вот добавим мы квази-цитирование и нам уже будут нужны типы (Term × Term) отражающие структуры термов, то есть, исходя из удобства, нужна будет полная 2-категория. Ну и в какой-то ситуации может быть удобны не 2-категории, а 1-категории с функторами.

но _никак не_ к самой этой 2-категории (для неё такое высказывание просто не определено)

Вот, к примеру, если взять агду (можно считать, что берём теорию Мартина-Лёфа) и дать определения 1- и 2-категориям, то высказывания о 1-категориях просто с точки зрения тайпчека не подойдут к 2-категориям.

Вы не поверите - эти разделы _изначально_ были изложены на одном языке.

Да, на бедном языке. А в более богатом становится видно, что (структурно) это разные языки — «классические» (декартово-замкнутые категории — классическая теория вычислений и классическая логика) и «неклассические» (компактные симметричные моноидальные категории — квантовая физика, топология, линейная логика).

> Любое определение однозначно описывает определяемый объект, без всяких НЁХ.

Это категория с дополнительной структурой, не являющиеся частным случаем категорий. Так же, как кольца не являются частным случаем групп, например.

Квадрат - частный случай прямоугольника? Можешь показать разницу между квадратом/прямоугольником и категорией/2-категорией?

Целые классы то зачем?

А как же иначе?

В математике всегда сказано только то, что сказано.

Угу. И если сказано «два множества» («класса», whatever), то это не значит «хотя бы два множества».

Квадрат - частный случай прямоугольника? Можешь показать разницу между квадратом/прямоугольником и категорией/2-категорией?

Да. Вот смотри: допустим, я тебе показываю прямоугольники. Ты можешь сказать - вот это квадрат, а это нет. Просто? Весьма. Ну, если отвлечься от физической невозможности провести абсолютно точные измерения, мы не о физике говорим, а о математике.

Кроме того, если я в хорошем настроении, то я могу показать такие прямоугольники, среди которых найдутся-таки квадраты.

А вот если я буду тебе показывать категории, то фига с два ты сможешь указать среди них 2-категории. Просто потому, что нужна ДОПОЛНИТЕЛЬНАЯ СТРУКТУРА, которую я тебе не показываю. Максимум, ты сможешь сказать, что «эта категория МОГЛА БЫТЬ получена из 2-категории» (не несущее информации утверждение, так как ЛЮБАЯ 1-категория может быть получена из 2-категории выкидыванием 2-морфизмов).

http://iml.univ-mrs.fr/~girard/truth.pdf

Is there something more frozen than «foundations»? A quick glance at the list «foundations of mathematics»:

http://www.cs.nyu.edu/mailman/listinfo/fom

shows a paradigm close to archaic astronomy: truth is a primitive (like Earth), around which several systems and meta-systems gravitate (like the epicycles of Ptolemy). This being orchestrated by Doctors of the Law, in charge of the latest developments of Hilbert’s program, i.e., of a certain form of finitism obsolete since Gödel’s theorem (1931!), but still in honour in this sort of Jurassic Park.

Let us put it bluntly: these people confuse foundations with prejudices. Of course, it cannot be excluded that the deep layers behave accordingly to our preconceptions; but who thinks in that way should draw the conclusions and quit. My personal bias, the one followed in this paper, is that the real hypostases are very different from our familiar (mis)conceptions: I shall thence propose a disturbing approach to foundations. This viewpoint is by no means A non standard B, it is on the contrary most standard; but it relies on ideas developed in the last century and prompted by quantum physics, the claim being that operator algebra is more primitive than set theory.

[...]

In terms of foundations, the most impressive achievement of the turn of the century is to be found outside logic — not to speak of the the aforementioned Jurassic Park — : in the non commutative geometry of Connes [1], a paradigm violently anti-set-theoretic, based upon the familiar result:

A commutative operator algebra is a function space.

Typically, a commutative C∗-algebra can be written C(X), the algebra of continuous functions on the compact X. Connes proposes to consider non commutative operator algebras as sorts of algebras of functions over ... non existing sets, an impressive blow against set-theoretic essentialism!

> Если я беру язык Foo и добавляю к нему разных выразительных средств, то получившийся Foo++ имею полное право называть более высокоуровневым.

Ну вот здесь ваша ошибка. По-вашему исходный foo это теория множеств, а обогащенный выразительными средствами foo++ - теоркат. Проблема в том, что когда мы говорим о ЯП, то тут все однозначно - мы можем только foo++ задать как расширение foo, но не наоборот. У нас же все иначе - и теоркат задается как «расширение» теории множеств и, одновременно с этим, теория множеств задается как «расширение» теорката. Здесь полная симметрия. Каждая теория выступает сразу и в роли foo и в роли foo++

Да? Т.е. нарисованную струнную диаграмму не нужно переводить?

Еще раз. Чисто технически ваша струнная диаграмма - это высказывание в теории множеств. Изначально. Куда вы его собрались переводить? Переводить имеет смысл из одной теории в другую. А вы как были в рамках теории множеств, так в ней и остаетесь, когда струнные диаграммы рисуете. И никуда, ни на миллиметр, за ее пределы не выходите.

Аксиоматика категорий агрегирует аксиоматику множеств.

одновременно с этим аксиоматика теории множеств агрегирует аксиоматику категорий.

(хотя, есть и разница — сказать «сопряжённый функтор бла-бла-бла», или написать длинную портянку утверждений о множествах)

Аналогично, есть разница - сказать «счетное множество» или изрисовать всю доску коммутативными диаграммами :)

Однако, дело в том, что в ТК есть свой язык который не имеет аналога в теории множеств и называется теоретико-стрелочным языком

Что это за чушь вы несете? Ваш «теоретико-стрелочный» язык строго ортогонален теоркату и теории множеств. Коммутативная диаграмма - это не более чем система равенств. И записать вы эту систему равенств можете как вашей душе угодно - либо в виде обычного текста, либо в виде диаграммы. либо еще как. Это просто _нотация_, которую вы можете применять _в любой_ теории (если только в этой теории вам надо записывать равенства). И от используемой теории эта нотация не зависит. К слову, нотация не всегда удобная - например, утверждения о существовании единственного морфизма (ну короче все ко-пределы, например) эквивалентны утверждению о существовании единственного решения системы уравнений. Очень часто в виде системы такие утверждения выписываются гораздо удобнее. Но обычно удобной записью пренебрегают и рисуют лапшу из диаграмм. Вот как раз такие упоротые как вы, которым лишь бы теоркат лишь бы стрелки. То, что это неэффективно - пофиг. Зато стрелки! И потом вместо того, чтобы написать какое-нибудь банальное a(bc) = (ab)c малюют диаграммную ересь, которая с первого взгляда и не понятно что значит.

> любое высказывание о 1-категории справедливо по отношению к 1-категории которая соответствует данной 2-категории, но _никак не_ к самой этой 2-категории

А какой есть смысл их разделять, если эта 1-категория определяется по данной 2-категории вполне естественным образом?

При этом графический язык 2-категорий также расширяется и какие-то диграммы не имеют аналогов в графическом языке 1-категорий.

Все эти диаграммы, опять же - системы равенств. И любая нотация позволяет описать любую систему. так что не идет речь ни о каком «не имеют аналогов».

Вы просили пример такого утверждения — 2-аналог симметричной моноидальной категории не является симметричной моноидальной 2-категорией.

Пример какого утверждения?

Вы отрицаете возможность сформулировать теорему на категорном языке? Или возможность сформулировать новую теорему? Или что?

Я отрицаю возможность того, что на основании общих свойств 2-стрелок можно получить нетривиальное утверждение о редукциях. Так вы назовете теорему или нет?

Например, Карри-Говард? А какие ещё аналогии появились _сперва_?

Вообще все. В рамках теорката еще никто никаких аналогий не находил. теоркат он не для поиска аналогий, он для их удобного описания. То есть когда мы аналогию уже _нашли_ нам в рамках теорката достаточно удобно потом с этими аналогиями работать.

Но вот добавим мы квази-цитирование и нам уже будут нужны типы (Term × Term) отражающие структуры термов

Не, не нужны.

> А вот если я буду тебе показывать категории, то фига с два ты сможешь указать среди них 2-категории.

Т.е. нет критерия, по которому одних можно отличить от других? Судя по дальнейшему тексту твоего поста не верное предположение, но тем не менее.

которую я тебе не показываю.

Почему? Или, точнее, зачем ты не показываешь эту структуру?

Ты же у прямоугольников не прятал две стороны?

Или эта «дополнительная структура» - сугубо субъективное понятие, существующее только в твоём сознании?

> Вот, к примеру, если взять агду (можно считать, что берём теорию Мартина-Лёфа) и дать определения 1- и 2-категориям, то высказывания о 1-категориях просто с точки зрения тайпчека не подойдут к 2-категориям.

Так агда не умеет определять эквивалентность определений. У вас в агде так же тайпчек не пройдет если вы на место группы определенной через нейтральный объект, как нульарную операцию, поставите группу с определением нейтрального объекта как элемента. Вообще, знаете, если у нас есть некое определение некоего математического объекта и мы хотим узнать является ли некая НЕХ этим объектом, то мы проверяем а подходит ли он под определение. Не важно там, является ли эта НЕХ каким-то реальным процессом/явлением или сама - математический объект. Вот основываясь на этом берем мы группу по 1 определению и смотрит - а удовлетворяет ли она группе по второму? и видим, что удовлетворяет. И наоборот. аналогично с категориями. Берем мы 2-категорию и по порядку проверяем, удовлетворяет ли 2-категорию определению 1-категории, итак:

1. есть класс объектов. есть? Есть.

2. по классу морфизмов на каждую пару объектов. есть? есть

3. определена композиция. определена? определена

4. композиция ассоциативна и имеет соответствующие единицы. так? так

значит, перед нами категория. и все. ваше словоблудие тут уже никакого веса не имеет. Удовлетворяет определению категории - значит категория.

> Да, на бедном языке.

Ну уж извините. Пока что математика обладает только бедными языками - теория множеств там, теоркат, другие эквивалентные им языки, быть может. Вот когда придумают более богатые - тогда и предъявляйте свои претензии, а пока - на безрыбье и рак рыба.

> А как же иначе?

А в чем проблема? единственное, что нам надо уметь - это просто владеть каким-то естественным способом «не заметить» лишнюю структуру. Если эта структура независима (то есть ее сокрытие не влияет на все остальное) - то все в порядке.

Угу. И если сказано «два множества» («класса», whatever), то это не значит «хотя бы два множества».

Давайте так, воспользуемся банальной логикой. У нас есть два утверждения:

1. Сказано: «два множества»

2. Не сказано: «ничего кроме этих двух множеств»

Дальше имеем некоторое утверждение:

3. сказано: «хотя бы два множества»

На мой взгляд (1 и 2 => 3). А как по-вашему?

А тебе вопрос на засыпку - почему квадраты/прямоугольники ты показываешь целиком, а 1-категории/2-категории - кусками? Если ты вместо квадратов/прямоугольников целиком будешь показывать только их 4 угла, то тоже способа отделить первые от вторых у тебя не будет. Да и не совсем ясно какое это имеет отношение к разговору. Давай уже определимся - что именно ты понимаешь под «X есть частный случай Y»? Я вот дал вполне четкое, строгое объяснение. Очередь за тобой.

Можешь показать разницу между квадратом/прямоугольником и категорией/2-категорией?

я, конечно, дилетант в столь высоких материях, но предложил бы рассмотреть несколько другой пример: квадрат и квадрат с окружностью внутри (некоторое подобие дополнительной структуры). можно ли квадрат считать частным случаем квадрата с окружностью? да, если окружность нулевого радиуса. можно ли квадрат с окружностью считать частным случаем квадрата? как минимум, определению не удовлетворяет

вот это - ближе к группам/кольцам и 1-категориям/2-категориям. квадрат и прямоугольник - это как раз разница в ограничениях, в то время как спор идёт вокруг недостающей структуры

На мой взгляд (1 и 2 => 3). А как по-вашему?

исходя из такой логики и вспоминая приведённый тут ранее пример, квадратом можно считать любую кляксу, из которой можно выделить квадрат (то есть практически любую кляксу). ведь нигде не сказано, что в квадрате не должно быть ничего, кроме четырёх сторон - так?

Ну вот здесь ваша ошибка.

Да нет, тут такой генезис — сначала множества, затем (более богатые!) категории. Всё — можно говорить на языке категорий и множеств. Путь от категорий обратно к моделям (категорным) разных теорий множеств это уже уберлогика и математический бустрап, т.е. никому кроме логиков это не нужно.

Аналогично, есть разница - сказать «счетное множество» или изрисовать всю доску коммутативными диаграммами :)

Не надо интерпретировать теорию множеств категорно, просто говорите «счетное множество» и всё.

Т.е. с обогащением языка категорными концепциями вы ничего не теряете — говорите о множествах как о множествах, но разные модели изучаемых теорий стройте категорно.

Весь изначальный посыл был в том, что языки _удобно_ представлять категориями.

А какой есть смысл их разделять

Затем же зачем 0- и 1- категории разделяют. Множества != категории, категории != 2-категории. Если мы говорим что-то про множество, то это не относится к категории, говорим что-то про категорию - не относится к 2-категории.

Пример какого утверждения?

Утверждения которое справедливо для категории и не справедливо для 2-категории. 2-аналог SMC это SyllepticM2C, то что будет SM2C требует дополнительных свойств от 2-стрелок.

Я отрицаю возможность того, что на основании общих свойств 2-стрелок можно получить нетривиальное утверждение о редукциях.

Эти свойства позволяют классифицировать модельные категории на те в которых работает CR и те в которых нет. Чем эти категории при этом являются конкретно не важно. По-моему мило :)

Вообще все.

Упоминалось четыре раздела, значит должно быть 12 аналогий — из них только связи (логика ~ вычисления) и (физика ~ топология) разрабатывались сами по себе.

Вот когда придумают более богатые - тогда и предъявляйте свои претензии, а пока - на безрыбье и рак рыба.

Цитата Girard'а выше как раз о том.

ну и чтобы спалось лучше, предложу ещё вариант сравнений сущностей с дополнительной структурой в одном из случаев: вещественные и комплексные числа. дополнительная структура хорошо видна из определения: вместо числа a у нас пара чисел (a, b) формы a + ib

является ли вещественное число частным случаем комплексного? да, с нулевой мнимой частью. является ли комплексное число частным случаем вещественного? я бы не сказал - хотя, казалось бы, нигде ведь не сказано, что кроме единственной компоненты у вещественного числа больше нет никаких компонет. одномерное векторное пространство - это ведь пространство хотя бы одного измерения, а не ровно одного? :)

Вообще, знаете, если у нас есть некое определение некоего математического объекта и мы хотим узнать является ли некая НЕХ этим объектом, то мы проверяем а подходит ли он под определение.

Ну да, я с этим не спорю.

удовлетворяет ли 2-категорию определению 1-категории

Удовлетворяет.

значит, перед нами категория.

Представьте, что вы работаете в системе с record subtyping. Если вы берёте структуру 2Cat, которая агрегирует Cat, то весь этот алгоритм проверки осуществляется на поле типа Cat и пока вы работаете со всеми утверждениями для Cat вы будете работать только с этим полем, так что то что там есть дополнительные свойства вообще не играет роли, вы по сути и не используете никаких 2-категорий (можно переписать все функции без использования типа 2Cat). Нужно только иметь ввиду где 2Cat, а где Cat - утвержденеи SM (symmetric monoidal) для Cat будет одним, а для 2Cat - другим.

Т.е. нет критерия, по которому одних можно отличить от других?

Примерно как отличить ворона от письменного стола.

Или, точнее, зачем ты не показываешь эту структуру?

Меня просили показать категорию — я показал. Что такого-то?

Вообще, разницу между законом и пистолетом понимаешь? Первое — правила, которые надо выполнять. Второе — дополнительный предмет, который можно купить. А можно не покупать. А можно купить два.

Не сказано: «ничего кроме этих двух множеств»

Конечно, есть ещё операции.

Вот если бы было сказано «Категория включает в себя два множества...» — тогда да. А когда сказано «Категория состоит из двух множеств» — фигли.

А тебе вопрос на засыпку - почему квадраты/прямоугольники ты показываешь целиком, а 1-категории/2-категории - кусками?

Не кусками. Меня просили показать категорию — я показал. А то, что кто-то рассматривает ещё и структуру 2-категории на ней — это его личное дело. Кто-то другой может рассматривать ДРУГУЮ структуру 2-категории на ней же, мне что — все возможные показывать?

> Да нет, тут такой генезис — сначала множества, затем (более богатые!) категории.

Верно будет так: «сначала множества, затем (эквивалентные!) категории».

Не надо интерпретировать теорию множеств категорно, просто говорите «счетное множество» и всё.

Так я же это и пытаюсь до вас донести. Какой смысл категорно определять то, для чего теория множеств более удобна (то есть для чего теория множеств является более высокоуровневым языком)? Но нет вы уперлись - давайте определять категорно все. Вне зависимости от того. имеет ли это смысл.

Весь изначальный посыл был в том, что языки _удобно_ представлять категориями.

Так в том и дело, что _нет_. Языки удобно представлять именно при помощи теории множеств. Хотя бы сравнить ваше категорное определение лямбда-исчисление и классическое. Классическое проще, короче, удобнее в использовании и интерпретации и кроме того оно более абстрактно, то есть содержит меньше непринципиальных для теории сущностей. Но вы предпочли категорное. только потому что там стрелки. Но не потому, что оно более удобно или дает какие-то профиты.

Если мы говорим что-то про множество, то это не относится к категории, говорим что-то про категорию - не относится к 2-категории.

Конечно же относится.

Утверждения которое справедливо для категории и не справедливо для 2-категории.

Ну хорошо, приведите пример такого утверждения. То, что привели вы - не подходит по очевидным причинам.

Эти свойства позволяют классифицировать модельные категории на те в которых работает CR и те в которых нет.

И? Зачем лезть в теоркат, если в теормноже это проще, удобнее и естественнее?

Упоминалось четыре раздела, значит должно быть 12 аналогий — из них только связи (логика ~ вычисления) и (физика ~ топология) разрабатывались сами по себе.

Еще раз - в рамках самого теорката еще не было придумано _ни одной_ аналогии. Вы легко можете меня опровергнуть - вам достаточно эту аналогию назвать.

> Цитата Girard'а выше как раз о том.

О том, что никакого более богатого языка, чем язык эквивалентный теории множеств, еще не придумано? А к чему вы это вообще? Я это и так знаю. Кстати, не надо забывать еще один ньюанс - язык вообще значения не имеет. Имеет значение лишь модель. Когда мы рассуждаем в рамках какой-то математической теории, мы рассуждаем о конкретной _модели_ это теории. И лишь затем, постфактум, натягиваем наши интуитивные выводы на синтаксический каркас этой теории - лишь для того, чтобы проверить корректность наших построений. Вот есть некоторая модель теормножа и некоторая модель теорката. И в зависимости от задачи - нам удобно применять ту или иную модель. Именно _модель_, а не язык. Если мы подберем какую-то другую модель для тех же теорий все и будет по-другому. Фактически, никто не гарантирует, что мы не сможем подобрать для теормножа модель которая будет удобнее теорката для описания тех явлений, для которых теоркат наиболее удобен на данный момент. Ну и наоборот.

> Удовлетворяет.

Ну вот и все. Дальнейшее смысла не имеет. Если X удовлетворяет определению некоего объекта, то Х является этим объектом. То, что Х может является _еще_ каким-то объектом - это никого не волнует. Вы же не отвергаете тот факт, что группа Ли - собственно, группа, на основании того, что эта группа является еще и гладким многообразием? Так и с 2-категорией. Группа Ли имеет две структуры - группа и гладкое многообразие. Причем структуры согласованы. 2-категория имеет две стурктуры - категория и категория. Причем эти структуры согласованы. Ну так что, группа Ли - это все-таки группа или же нет?

Представьте, что вы работаете в системе с record subtyping.

Именно так. 2-категория - подтип категории. То есть - частный случай.

Нужно только иметь ввиду где 2Cat, а где Cat - утвержденеи SM (symmetric monoidal) для Cat будет одним, а для 2Cat - другим.

Да, вы правильно заметили - это _разные утверждения_. Которые задаются разными формулами. Если же мы возмьем одно утверждения с forall по категориям, то это утверждение останется истинным и для forall по 2-категориям.

> Вот если бы было сказано «Категория включает в себя два множества...» — тогда да. А когда сказано «Категория состоит из двух множеств» — фигли.

Повторяю вопрос. Там сказано, что ничего кроме двух множеств и операций нет, или не сказано?

> Не кусками. Меня просили показать категорию — я показал. А то, что кто-то рассматривает ещё и структуру 2-категории на ней — это его личное дело.

Нет, погодите, что значит «рассматривает структуру»? Структура там либо однозначно есть, либо ее однозначно нет. И плевать кто что рассматривает. Если вы показываете категорию, которая содержит дополнительную структуру - это однозначно будет 2-категорией. Если показываете категорию, которая не содержит дополнительной структуры - это не будет 2-категорией. так что посмотрев на спорный объект мы сразу скажем - 2-категория это или нет. Так же. как посмотрев на прямоугольник, мы сразу скажем - квадрат это или нет.

> является ли вещественное число частным случаем комплексного? да, с нулевой мнимой частью.

Нет. Комплексное число с нулевой мнимой частью - это комплексное число с нулевой мнимой частью. Оно вещественным не является. И вещественные числа частным случаем комплексных тоже не являются. А вот обратное - верно. Комплексное число - частный случай вещественного, т.к. в любой ситуации мы можем заменить вещественную переменную комплексной и все будет хорошо.

одномерное векторное пространство - это ведь пространство хотя бы одного измерения, а не ровно одного? :)

Одномерное пространство - это пространство с мощностью базиса равной единице. Не >=, а =. Тут никакие «состоиз из...» не прокатят.

эквивалентные!

В том же смысле, в котором эквивалентны все тьюринг-полные языки программирования.

Хотя бы сравнить ваше категорное определение лямбда-исчисление и классическое.

Определение здесь особо ни при чём. Лямбда-исчисление нужно не только определить, нужно ещё и работать с ним. И категорный подход позволяет делать это лучше и проще.

язык вообще значения не имеет.

Язык имеет принципиальное значение.

Когда мы рассуждаем в рамках какой-то математической теории, мы рассуждаем о конкретной _модели_ это теории.

Это ещё с чего вдруг? Конкретной моделью, как раз, обычно не заморачиваются.

Там сказано, что ничего кроме двух множеств и операций нет, или не сказано?

Конечно. Там сказано «состоит из двух множеств».

Могу найти, если желаете, учебник, где сказано ещё более явно: «категория - это пара множеств, для которой...»

Комплексное число с нулевой мнимой частью - это комплексное число с нулевой мнимой частью. Оно вещественным не является.

Конечно, но так как есть каноническое вложение всей совокупности вещественных чисел в комплексные, стандартная математическая вольность речи позволяет отождествить их.

Комплексное число - частный случай вещественного

Всё. Остаётся констатировать, что в математике вы полный балбес.

Комплексное число - частный случай вещественного, т.к. в любой ситуации мы можем заменить вещественную переменную комплексной и все будет хорошо.

OMG, перечитайте, что вы написали.

> вещественные и комплексные числа

О! Это уже красивей.

является ли комплексное число частным случаем вещественного?

В такой постановке аналогия понятна, и, судя по всему, понятна позиция анонимуса.

> В том же смысле, в котором эквивалентны все тьюринг-полные языки программирования.

Ну да.

И категорный подход позволяет делать это лучше и проще.

нет.

Язык имеет принципиальное значение.

Математик не работает с языком, он работает с моделью, которая находится в голове. И у каждого - своя. Формализация происходит только в самом конце - когда результат уже получен.

Это ещё с чего вдруг? Конкретной моделью, как раз, обычно не заморачиваются.

Да, я плохо написал. Тут подразумевалась не модель в смысле модели формальной теории, а некий комплекс свойств объектов, которыми мы оперируем на уровне интуиции. Ну то есть, например, когда мы рассуждаем о множествах, то де-факто множество для нас это не то, что задается набором аксиом, а некое интуитивное понятие, которое сложилось на основании жизненного опыта (математического в том числе). И этим понятием мы оперируем. И только потом, когда уже сделаны какие-то выводы об этом интуитивном объекте (который у каждого, кстати, свой) мы пытаемся эти выводы формализовать.

Конечно. Там сказано «состоит из двух множеств».

А где сказано, что кроме этих двух множеств там ничего больше нет?

Могу найти

Вот уж нет, вас попросили дать определение и вы его дали. Нечего теперь вилять задницей и пытаться его заменить. Я сходу могу вам дать десяток определений категории, которые будут эквивалентны вашему и в которых будет явное «хотя бы два множества».

Конечно, но так как есть каноническое вложение всей совокупности вещественных чисел в комплексные, стандартная математическая вольность речи позволяет отождествить их.

Нет, не позволяет. Вы путаете частное с общим. Вы не можете рассматривать вещественное число в качестве комплексного, потому что у вещественного числа просто нету необходимых свойств. С другой стороны, комплексное число обладает всеми свойствами вещественного, по-этому любое комплексное число может быть рассмотрено в качестве вещественного - достаточно просто отбросить мнимую часть.

Всё. Остаётся констатировать, что в математике вы полный балбес.

Вы прежде чем делать выводы о чьих-то математических знаниях разобрались бы сами с основами хотя бы, а то несете полную чушь в каждом посте. Вы, кстати, так и не определили, что значит «X есть частный случай Y», по-этому разговор вообще беспредметен. Я вам формально строго _доказал_ что 2-категория есть частный случай 1-категории, если под частным случаем понимать то, что понимаю под этим я. Вы же свой тезис даже не сформулировали.

> OMG, перечитайте, что вы написали.

Перечитайте определение частного случая. Комплексные числа - подтип вещественных? Да. Значит - частный случай.

Так в том и дело, что _нет_.

На «нет» и суда нет. Будем считать это делом вкуса.

Конечно же относится.

Ну хорошо, приведите пример такого утверждения.

Да может быть сколько угодно утверждений вроде «категория симметрична и моноидальна» или «категория дискретна» которые либо определены на разных n-категориях по-разному, либо вообще не имеют смысла для высших категорий (n-категория может быть дискретна по разным k-стрелкам).

Но это конечно просто разные утвержденя которые, допуская вольность речи, называют одинаково.

И ещё. Если вы говорите «возьмём 2-категорию» и делаете утверждения только про её объекты и стрелки, то вы по сути и не берёте никакой 2-категории - только 1-категорию которая однозначно определяется по данной 2-категории.

Еще раз - в рамках самого теорката еще не было придумано _ни одной_ аналогии.

Аналогии вообще не придумывают, а изучают - либо местными методами, либо категорно.

Вы легко можете меня опровергнуть - вам достаточно эту аналогию назвать.

Мне трудно судить, но примерно так:

CT      ~ Topology       50s  *    Algebraic topology, homological algebra, homotopy theory.

CT      ~ Logic          60s  *    Categorical logic.

Logic   ~ Topology       70s  *    Topos theory.

Logic   ~ CS             70s       Curry-Howard correspondence.

CT      ~ CS             70s       The connections between CT, type theory, domain theory and algebraic semantics.

                         80s  *    Formal languages (as well as ADTs) reasoning and optimizations.

Physics ~ Topology       80s       Topological QFT.

CS      ~ Physics        90s       Quantum computations.
Logic   ~ Physics

CT      ~ Physics        00s       CSMC in physics.

CS      ~ Topology       ?

(*) - всё то, что не есть переформулировка более ранних результатов. Ну а категорные переформулировки всего этого тоже есть. И, возвращаясь к удобству, категорные переформулировки могут оказаться предпочтительнее, так как позволяют проводить классификации теорий.

Перечитайте определение частного случая. Комплексные числа - подтип вещественных? Да. Значит - частный случай.

И ведь не поспоришь :)

Берём инверсные по отношению друг к другу определения отношения агрегирования и отношения подтипов, тогда:

ℝ :> ℂ
ℂ <: ℝ

Берём другой пример. Пусть есть (ООП) класс Server и его наследник MyServer. MyServer агрегирует Server, и MyServer есть подтип Server:

Server   :> MyServer
MyServer <: Server

В полном соответствии с LSP. При этом MyServer - частный слачай Server.

У нас может быть много подтипов (частных случаев, наследников) Server, также как поверх ℝ можно определять разные расширения. Но супертип для подтипа определяется однозначно.

> Да может быть сколько угодно утверждений вроде «категория симметрична и моноидальна» или «категория дискретна» которые либо определены на разных n-категориях по-разному, либо вообще не имеют смысла для высших категорий (n-категория может быть дискретна по разным k-стрелкам).

Так если определены по-разному - это уже _другое_ утверждение, о чем речь-то? Я говорю об утверждения не на естественно языке.

И ещё. Если вы говорите «возьмём 2-категорию» и делаете утверждения только про её объекты и стрелки, то вы по сути и не берёте никакой 2-категории - только 1-категорию которая однозначно определяется по данной 2-категории.

Если я взят 2-категорию, т взял 2-категорию. Какие там я делаю утверждения - это уже не важно.

Аналогии вообще не придумывают

а откуда эти самые аналогии берутся? Боженька дает?

Мне трудно судить, но примерно так:

А где там аналогии, конкретно?

Я вам формально строго _доказал_ что 2-категория есть частный случай 1-категории, если под частным случаем понимать то, что понимаю под этим я.

После утверждения «комплексные числа — частный случай вещественных» вы иначе как клоун не рассматриваетесь.

А вы не рассматриваетесь иначе как пустобрех. Уже давно причем.

> После утверждения «комплексные числа — частный случай вещественных» вы иначе как клоун не рассматриваетесь.

А вы не рассматриваетесь иначе как пустобрех. Уже давно причем.

Слава богу на личности перешли! Я уж испугался что весь тред будет выдержан в научно-уважительном стиле.

Ну все как обычно:

«В принципе, я не знаю, стоит ли еще пытаться получить какую-нибудь аргументацию, или можно, наконец, перейти к оскорблениям» (c)

> Слава богу на личности перешли!

Да погоди ты! Рано радоваться — я еще не слышал ни «норкоман», ни «упоролся». Вдруг они и ругаться будут в научно-уважительном стиле?

Так если определены по-разному - это уже _другое_ утверждение, о чем речь-то? Я говорю об утверждения не на естественно языке.

Тогда всё хорошо. Только нужно быть осторожным. Например, вы можете сказать «гильбертово пространство это частный случай множества, а линейный оператор - частный случай функции» и начнёте использовать гильбертовы пространства и линейные операторы как множества и функции в квантовой механике, а это совсем не хорошо.

Т.е. и разная алгебра и теория категорий это средства оперировать математическими вещами (множествами с дополнительными структурами, если угодно) так, чтобы они не расползались (на множества с разными структурными свойствами), иначе - говорить в терминах предметной области.

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

а откуда эти самые аналогии берутся?

Их открывают. А самим по себе аналогиям можно вообще приписать объективное существование, независимое от факта их открытия или неоткрытия. Например, то что определённые логика и LC это одно и то же с точность до - математически объективный факт.

А где там аналогии, конкретно?

Вся система аналогий что строится в Розетском камне. Я про это. Это как таблица Менделеева - хотя факты о валентности были известны до её создания (можно сказать, что она - переформулировка этих фактов), теперь эти факты изучаются с опорой на эту систему аналогий (между химическими элементами).

Вот, кстати, есть аналогия между hom-функтором, частицами/античастицами и ФВП.

Грамотный вброс!

ТС таки тонко вбросил (:

А ещё мне, как нематематику, непонятно, как комплексные числа являются «подмножеством» вещественных, хотя на вышке говорят как раз об обратном: есть множество комплексных чисел, а его подмножество, не содеращее мнимой составляющей, является множеством вещественных. Т.е., вещ-ные числа - частный случай комплексных. В этом смысле поддерживаю Мигеля: подмножество - это частный случай более общего множества.

Прошу камни не кидать, я не математик.