Характеризация внутренних автоморфизмов групп https://mathoverflow.net/questions/7782/are-the-inner-automorphisms-the-only-ones-that-extend-to-every-overgroup

Случайно наткнулся на тред. Потрясен уровнем близости мыслей (правда автор очень пессимистичен и несколько драматизирует ситуацию по-моему)

> 3. Shall I face the fact that I've been defeated in my deepest desire, becoming exactly the kind of mathematician (and human being) I've always hated, the one who uses a theorem like a black box and makes guesses about things he ignores the true meaning of? But mathematics works this way: there is no point in knowing that something is true, until you ignore why it's true. Following a quite common idea among category theorists, I would like to go further, knowing why something is trivial. I don't want to know a definition, I want to know why that definition is the only possible way to speak about the definiendum. And if it's not, I want to be aware of the totality of such ways: does this totality carry a structure? The presence/absence of it have a meaning? Is there a totality of totalities, and how it behaves? When I first approached HTT I thought that answering these very questions was its main task. You can see how deeply I'm disappointed. And you can see the source of my sense of defeat: I feel stupid, way more limited, distracted from learning technicalities, way more than people that do not tackle this search for an absolute meaning. Younger than me, many colleagues began studying HTT, rapidly reaching a certain command of the basic words and subsequently began producing mathematics out of this command.

> 4. The questions I raised at point 3 do not pertain mathematics; I should do something else. In fact, the only reason why I tried to become a mathematician was that I felt that mathematics is the only correct meaning of the word "philosophy", and the only correct way to pursue it. But turning to philosophy would be, if possible, even a more unfortunate choice: philosophers tend to be silly, ignorant people who claim to be able to explain ethics (=a complicated and elusive task) ignoring linear algebra (=something that shall be the common core of knowledge of every learned person).

Мне очень нравится ответ Шульмана

Недавно появился занятный сайт: mathjobrumors.com. Питер Войт хорошо описал:

> I noticed yesterday a website named Math Job Rumors that has been operating for a couple months. No idea what the story behind it is other than that it’s clearly a descendant of Economics Job Market Rumors, which had some small participation by mathematicians, but is somewhat of a dumpster fire of misinformation, trolling, misogyny and various sorts of juvenile behavior. It looks like someone is trying to provide something similar aimed specifically at mathematicians, with some improvement over the EJMR environment.

Есть интересные темы

Naive question: in what sense is condensed mathematics "foundational"?
Best young topologists?
Recent works and young mathematicians
we should know about

> I would prefer this site be a place where professional mathematicians can have useful discussions, not 4chan-lite with mathematical flavoring. There's already EJMR for people who want that.

up

Is math the closest thing to real life magic?

In its tenets and practice, I’d say no. Organized religion is probably the closest analog to magic in terms of image, ritual, and belief in the supernatural. That said, I actually think in some respect it totally is the closest thing we have. Here’s why.

Mathematics has a similar structure to certain conceptions of magic. It requires years of studying something entirely incorporeal, it seems to exist independent of the physical realm, it’s very powerful and has the ability to predict and influence the world around us, and it’s practitioners are BIZARRE.

It’s this last point that I’d like to focus on for a bit. You see, mathematicians often get grouped in with scientists when people discuss various pursuits, but I’m of the mind that the mindset and spirit of science couldn’t be further from that of pure math. Firstly, science is an essentially evidence-based field of study, whereas mathematics is a purely logically-based field of study. It, much like many conceptions of magic, is based in creativity that’s subject to certain laws. This is a very different vibe than something like chemistry, which focuses on experimentation and observation of physical phenomena as well. For some reason, this attracts a lot of people with very unique personalities. Despite the popular image of the math genius who mostly likes comic books and LEGOs and is globally ranked in Dota 2 (all noble pursuits, don’t think I’m disparaging them), most of the very serious math people I know are very interested in aesthetics, art, music, poetry, literature, and philosophy. I don’t know if this is indicative of mathematicians as a whole, as my sample size is admittedly limited, but it’s what I’ve seen in my experience. The most notable feature about math people that I’ve seen is their fanatical devotion to the subject. Math people LOVE math. It’s the air they breathe, the essence of everything they see around them, a source of beauty and inspiration in the world. To them it’s equal parts mysterious and awe-inspiring. I know a number of math students who would gladly spend their lives living in a mountain cave, studying motivic homotopy theory and scrawling esoteric theorems on the stones.

As a quick bonus, one of the founders of modern algebraic geometry, Alexander Grothendieck, wrote a number of multi-thousand-page, hand-written tomes detailing brilliant advances in the subject that took years to fully disseminate. This is what he looked like:

If he’s not a wizard, I don’t know who is!

Asaf Karagila:
> Category theory is an impressive tool for abstraction, but analysis is not always in need for abstraction - it looks for concrete solutions and ideas. In that aspect categories are not too useful.

В чем смысл этого тезиса? Теория чисел, которую тоже интересуют конкретные утверждения:

> In the late 1920s, André Weil demonstrated profound connections between algebraic geometry and number theory with his doctoral work leading to the Mordell–Weil theorem
> In 1949, André Weil posed the landmark Weil conjectures about the local zeta-functions of algebraic varieties over finite fields. These conjectures offered a framework between algebraic geometry and number theory that propelled Alexander Grothendieck to recast the foundations making use of sheaf theory (together with Jean-Pierre Serre), and later scheme theory, in the 1950s and 1960s. Grothendieck developed étale cohomology theory to prove two of the Weil conjectures (together with Michael Artin and Jean-Louis Verdier) by 1965.
> Between 1956 and 1957, Yutaka Taniyama and Goro Shimura posed the Taniyama–Shimura conjecture (now known as the modularity theorem) relating elliptic curves to modular forms. This connection would ultimately lead to the first proof of Fermat's Last Theorem in number theory through algebraic geometry techniques of modularity lifting developed by Andrew Wiles in 1995
> ....
> Arithmetic geometry, Anabelian geometry, Teichmüller theory, Frobenioid, Automorphic form, Langlands, Perfectoid space..

Тем временем

> As analysts have become more and more attuned to the deep relationships between functional analysis and geometry, they have turned to ideas from category theory to help keep things organized. K-theory and K-homology have become indispensable tools in operator theory; there is even a bivariant functor KK(−,−) from the category of C-algebras to the category of abelian groups relating the two constructions, and many deep theorems can be subsumed in the assertion that there is a category whose objects are C-algebras and whose morphism spaces are given by KK(A,B). Cyclic homology and cohomology has also become extremely relevant to the interface between analysis and topology (Paul Siegel)
> Algebraic analysis and D-geometry: hyperfunctions, microlocalization, D-modules (Sheaves on Manifolds, Secondary calculus and cohomological physics)
> Goodwillie calculus
> Lawvere metric spaces (много литературы см. на Analysis from the categorical viewpoint).

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

Сумасшествие

https://www.quantamagazine.org/mathematicians-cut-apart-shapes-to-find-pieces-of-equations-20191031/

В 2022-2023 году люди затехали:
* Адамс - Синяя Книга
* Милнор, Сташеф - Характеристические классы
* Квиленн - Гомотопическая алгеба
и другие прекрасные книги.

> Мы включили много современного форматирования, например, гиперссылки между разными разделами книги, гиперссылки на цитаты, более современные шрифты, все диаграммы перерисованы, чтобы они были более современными, tikz и т.д.

https://aareyanmanzoor.github.io/Texromancers.html

С форума:

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

Об этом было несколько тредов на MathOverflow (например, What does it mean to suspect that two conjectures are logically equivalent?) и, судя по всему, ничего удовлетворительного (и даже ничего похожего за исключением обратной математики, которая упоминается в каждом таком трэде, в том числе см. первый ответ по ссылке) у нас пока нет.

Идея обратной математики: взять достаточно слабую логическую систему (обычно используется RCA_0: арифметика Робинсона + две аксиомы см. в вики), в которой большая часть интересных утверждений не будут доказываться непосредственно, поэтому можно будет изучать связи между ними. Действительно именно наличие в каком-то смысле тривиальной равносильности между двумя сложными теоремами интерпретируется нами как их "равносильность" и "существенная необходимость одной для доказательства другой".

Так обратная математика предлагает такую картину: ZFC |- верные утверждения, а RCA_0 |- верные по тривиальным причинам. Проблема с этой формализацией как минимум в том, что в каждой области есть свое понятие "тривиальности", которое часто включает намного более сложные вещи, чем те, что доступны в RCA_0. Но что важнее сами доказательства и изучение их эквивалентности тут не фигурирует.

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

P.S. Очень рекомендую прочитать ответ Андрея Бауэра по последней ссылке (в треде Is rigour just a ritual that most mathematicians wish to get rid of if they could?) -- он и (среди прочего) исчерпывает вопрос, и настолько замечателен, что, возможно, мне стоило просто вставить его целиком.

Категории математических структур

Понятие категории мотивировано тем, что все математические структуры естественным образом формируют категории. Но при этом
(A) Реальные категории математических структур обладают многими хорошими свойствами (скажем, биполнота) сильно отличающими их от произвольных категорий (когда это не так, рядом всегда скрывается либо более правильное понятие, либо более правильный сеттинг).
(B) В произвольной плохой категории теория категорий "не работает", нет продуктивных понятий, категорная точка зрения мало что помогает понять (примеры относительно безнадежных: категория гомотопических типов, категория гладких многообразий).

Каково формальное понятие категорий математических структур, то есть категорий внутри которых мы хотим работать? (в отличие от, например, категорий, которые хотим использовать как индексации диаграмм и тому подобное – от которых мы не ожидаем духа математически структур (и часто вообще думаем как о бездушных точках и стрелочках)). С ноября у меня начали складываться пазлы убеждающие в том, что, по-видимому, несомненный ответ: локально представимые категории
1. LP категории включают все топосы Гротендика, в частности, алгебраические, голоморфные, гладкие пространства и прочие категории пространств всевозможных ароматов. Также, в частности, сюда попадают симплициальные множества sSet, как и все остальные топосы симплициальных пучков.
2. Категории алгебр над всеми монадами (удовлетворяющими определенному естественному свойству ограниченности) на LP категориях являются LP.
2a) В частности, LP категории включают все алгебраические категории (любой бесконечной, но ограниченной арности) над всеми топосами Гротендика (в частности, все обычные алгебраические категории как случай нашего терминального топос Set)).
2b) В частности, рефлективная подкатегория (удовлетворяющая естественному свойству ограниченности) LP категории является LP (например, категория банаховых пространств является LP, как рефлексивная подкатегория некоторой счетно-арной категории алгебр).
3. LP категории обладают множеством категорных совершенств, таких как биполнота, идеальная теорема о сопряженном функторе, разумное поведение mono-epi морфизмов, правых-левых ортогональных классов и многое другое. В частности, многие из этих свойств настолько витальны для теории гомотопий, что (насколько я понимаю) люди почти всегда работают с комбинаторными модельными категориями (= кофибрантно порожденными и LP).

Итак, что такое локально представимая категория?

Вот синтаксическое определение.

Классическое понятие алгебраической теории из универсальной алгебры имеет естественное обобщение, в которым операции не обязаны быть тотальными, но их области определения контролируются равенствами других операций. Например, таково определение категорий Cat:
* носители: Ob, Mor
* операции: dom, cod: Mor -> Ob, id: Ob -> Mor, ◌: Mor x_{Ob} Mor -> Mor
* аксиомы: (понятно)
Здесь область определения операция композиции описывается на Mor x Mor равенством cod(pr_1) = dom(pr_) (что можно в некотором пока неясном смысле рассматривать также как пулбек Mor -> Ob <- Mor). Так же как естественная область интерпретации алгебраических теорий --- категории с произведениями (носители рассматриваются как объекты, операции как морфизмы, аксиомы как коммутативности соответствующих диаграмм), естественная область интерпретации существенно алгебраических теорий --- категории с пределами. Равенства, описывающие область определения операций, интерпретируются как уравнители (соответствующая операция действуют из полученного объекта). Через T[C] я обозначаю категорию T-объектов в C. T[Set] называется категорией алгебр теории T.

Более точно, для данной существенно алгебраической теории можно выбрать такой кардинал λ (я всюду использую слово кардинал просто как синоним слова множество, это всего лишь указание на то, что оно рассматривается с точностью до изоморфизма = важно только число его элементов. По-моему какой-то выбор цепи множеств разных мощностей, которое подают как определение кардинала, не выполняет никакой полезной функции и только путает. Впрочем, это касается всех этих рудиментов material set theory, которая почему-то преподается как язык математики, вместо намного более простой, естественной, удобной, свободной от кодирований structural set theory), что каждое из следующих множеств имеет мощность меньше λ:
* арность каждой операции
* множество уравнений описывающих область определения каждой операции
Тогда её естественная область интерпретации -- категории с λ-малыми пределы (в частности, финитарные теории, у которых все эти множества конечны, интерпретируются в категориях с конечными пределами). Наименьший такой регулярный кардинал λ называется арностью теории. Определение регулярности и объяснение почему её естественно требовать – чуть дальше; сейчас важно только, что для любого бесконечного кардинала k кардинал следующий за ним succ(k) (то есть наименьший кардинал больший k) является регулярным, следовательно любая теория имеет арность.

Def. Категория называется локально λ представимой, если она эквивалентна категории алгебр λ-арной существенно алгебраической теории. В случае λ = N есть синоним: локально конечно представимые категории.

Некоторые первые примеры локальные представимых категорий:
1) Финитарные алгебраические категории (говоря алгебраические категории я всегда имею ввиду категории алгебр алгебраической теории, а не вот это их, имхо, неестественое обобщение; финитарность = все операции теории имеют конечную арность).
2) Топосы предпучков. Частный случай (1): все операции унарны и тотальны, а все аксиомы имеют вид f ◌ g = h. В частности, симплициальные множества sSet и комбинаторные виды Species таковы.
3) Категория (малых) категорий Cat (как описана выше)
4) Категория ориентированных графов OrGraph
* носители: вершины V и ребра E
* операции: dom, cod: E -> V, edge: E x_V E -> E (edge определена для тех пар ребер у которых равны dom и равны cod)
* аксиомы: edge(e, f) = e, edge(e, f) = f

То есть используя эту "фиктивную" операцию мы фактически записали аксиому "(dom(e) = dom(f), cod(e) = cod(f)) => (e = f)". Так вообще в существенно алгебраических теориях можно сразу писать любые аксиомы вида импликация "(equations1) => (equations2)". Более того можно писать аксиомы вида "(equations1 без x) => ∃! x т.ч. (equations2 c x)" потому что мы можем

∃: завести операцию f:equations1 -> equations2 (то есть определенную на кортежах для которых выполняются equations1 и возвращаю x, удовлетворяющий, вместе с аргументами f, equations2)

!: написать (equations1, equations2 на x, equations2 на y => x = y) //как мы научились писать импликации через частичные операции ранее

Rem. Значок ∃, конечно, не должен создавать впечатления, что можно написать аксиому с квантором существования, потому что здесь имеется ввиду конструктивное существование: нам задана операция, строящая этот объект -- это дополнительные данные, а не свойство. Но когда мы добавляем ещё и единственность, то получаем тоже самое свойство, что и с неконструктивным существованием.

Упоминавшаяся регулярность кардинала это просто такая легкая замкнутость/недостижимость: дезъюнктное объединение (= копроизведение) семейства множеств мощности меньше λ, каждое из которых имеет мощность меньше λ, остается множеством мощности меньше λ. Это естественно требовать от арности теории потому, что в уравнениях все равно будут возникать композиции операций (в операдном смысле т.е. подстановки) и их арности как раз будут дезъюнктыми объединениями арностей подставляемых операций, индексированных арностью верхней операции.

Конечно, с таким определением есть три конечных регулярных кардинала: 0, 1 и 2. Факт "не более чем 1-элементные суммы не более чем 1-элементных множеств не могут дать 2" (как и аналогичный ему про 0 и 1) кажется мне красивым (остальные натуральные числа в этом отношении не выделены, достижимы из меньшего мира). Я не подумал пока о том интересно ли рассматривать локально представимые категории соотв. рангов, поэтому буду предполагать (как это принято), что регулярный кардинал по определению бесконечен.

Натуральные числа N являются регулярным кардиналом, что соответствует явлению "конечное копроизведение конечных множеств конечно". Как отмечалось ранее, можно показать, что для любого кардинала k следующий за ним кардинал succ(k) является регулярным. В частности, таковы N_i для натуральных i (где N_i кардинал следующий за N_{i-1}, а N_0 = N). Но, например, копроизведение кардиналов N_i по всем натуральным i не является регулярным прямо по определению.(для ясности напомню, что "N_1 = R" – это и есть гипотеза континуума).

Некоторые первые примеры локально λ-представимых категорий:
1) Алгебраические категории арности λ (то есть все операции имеют арность меньше λ)
2) Топосы Гротендика. Сайт C (просто coverage, не обязательно сайт Гротендика) определяет существенно алгебраическую теорию:
* носители -- Ob C
* основные операции -- Mor C (все унарные и тотальные), далее ещё будут добавляться "фиктивные"
* аксиомы -- коммутативные треугольники f ◌ g = h
и плюс аксиома пучка (в терминах последней ссылки): для каждого покрывающего семейства f_i, для каждой пары стрелок g, h (c указанным условием) пишем аксиому вида: "(x_i, x_j удовл. equations1) => ∃! x (equations2)". Для λ наименьшего регулярного строго большого Mor C, имеем что все множества уравнений меньше λ, так это заведомо оценка сверху арности построенной теории.

Теперь семантическое определение.

Категория I называется λ-фильтрованной, если любая диаграмма размера меньше λ (где размер диаграммы это, конечно, множество морфизмов) имеет коконус. N-фильтрованные категории просто называются фильтрованными. Например, категория * -> * -> * -> ... (категория предпорядка стандартного порядка на натуральных числах) фильтрованная. Как и любая направленность.

Для категории C имеющей все λ-фильтрованные копределы, функтор F: C -> D называется функтором ранга λ, если F сохраняет λ-фильтрованные копределы. Мне очень нравится это понятие, функтор такой ( λ-) конечной природы и не способен сам решать, что ему делать с достаточно большими индуктивными системами объектов (представляю встраивающиеся друг в друга группы), они не управляются им, а просто сохраняются.

Кстати, на самом деле, направленный копредел это по существу основной пример фильтрованного копределы: категория имеет λ-направленные копределы <=> имеет λ-фильтрованные копределы, функтор сохраняет λ-направленные копределы <=> сохраняет λ-фильтрованные копределы ([AR94].1.21)

Объект категории A \in C называется λ-представимым, если функтор Hom(A, -): A -> Set имеет ранг λ. Для λ = N синоним: конечно-представимый. То есть объект A конечно представим, если для любой фильтрованной диаграммы X_i и любого морфизма A -> colim X_i этот морфизм пропускается через какой-то конечный уровень A -> X_i и при этом по существу единственным образом (то есть для любого другого пропускания A -> X_j индуцированные морфизмы на некотором дальнем k >= sup(i, j) совпадают). Я представляю как, например, отображение из конечного множества A в копредел индуктивной системы множеств всегда попадает на какой-то конечный уровень т.к. каждая точка образа лежит в каком-то элементе системы и значит (по определению направленности) есть элемент системы, через который факторизуется отображение.

Очевидно, что λ-представимые объекты замкнуты относительно λ-малых копределов т.к. Hom(colim A_i, colim X_j) = lim Hom(A_i, colim X_j) = lim colim Hom(A_i, X_j) = colim lim Hom(A_i, X_j) = colim Hom(colim A_i, X_j). Здесь используется, что λ-фильтрованные копределы и λ-малые пределы коммутируют в Set для любого регулярного λ (см. [B94].I.2.13 для λ = N, прямо обобщается на произвольное).

Как уже намекалось ранее, разумеется, конечно-представимые множества = конечные множества:
* одноэлементное множество представляет тождественный функтор => конечные множества (будучи конечными копределами одноэлементных) конечно представимы.
* если A конечно-представимо, то так как любое множество является направленным копределом своих конечных подмножеств, то тождественное отображение id: A -> A должно факторизоваться через какое-то конечное подмножество => A конечно.

Вообще для финитарной алгебраической категории конечно-представимые объекты = конечно-представимые в обычном алгебраическом смысле (определяемые конечным числом образующих и соотношений). Поразительная эффективность простого категорного понятия конечности.

Так легко видеть, что для любой финитарной алгебраической категории
* конечно-представимых объектов (с точностью до изоморфизма) малое множество
* каждый объект является копределом диаграммы отображающихся в него конечно-представимых (типа мы выбрали в каждом классе изоморфизма по объекту A, составили такую slice-категорию A -> X, определи функтор из неё в нашу алгебраическую категорию C, который просто возвращает dom стрелки (A) => копредел этого функтора X). Причем этот копредел фильтрованный, так как каждая конечная диаграмма просто имеет копредел в подлежащей категории (без slice), а доп. структура в виде морфизмов A -> X как раз определяет согласованный морфизм colim -> X --- построили коконус.

В этом все и дело.

Def. Кополная категория называется локально λ представимой, если она имеет (с точностью до изоморфизма) малое множество λ-представимых объектов и каждый объект является их λ-фильтрованным копределом.

Exr. В любой такой категории каноничная диаграмма A -> X по λ-представимым A будет λ-фильтрованной и X будет её копределом.

Обозначим через C_λ малую полную подкатегорию λ-представимых объектов. Нетрудно показать ([AR94].1), что для λ-представимой категории C функтор Йонеды C -> Func(C_λ^op, Set)
* является полным вложением ранга λ
* является правым сопряженным
* функторы (C_λ)^op -> Set представимые объектами C это в точности функторы сохраняющие λ-малые пределы

Так мы из семантического определения видим, что λ-представимые категории биполны как рефлективные подкатегории биполных категорий (мне кажется, из синтаксического определения это также видно непосредственно: (надо подумать и убедиться, что) произведения/копроизведения и уравнители/коуравнители для всех существенно алгебраических теорий описываются также одинаково и просто, как и для (обычных) алгебраических теорий). Более того, на самом деле, можно получить следующую переформулировку семантического определения ([AR94].1.46)

Def. λ-представимые категории это (с точностью до эквивалентности) рефлексивные подкатегории ранга λ топосов предпучков.

Конечно, из данной локально представимой категории нельзя восстановить существенно алгебраическую теорию, потому что классическое определение существенно алгебраической теории выделяет некоторую точку зрения на алгебры (фактически некоторый забывающий функтор в категорию Set^C, где C выделенное им же множество носителей), которая отсутствует в самой категории. Например, для любых двух морита-эквивалентных колец R_1 и R_2 (скажем R_2 = End(R_1^n) т.е. кольцо матриц n x n), категории модулей над ними эквиваленты (а теории, как и забывающие функторы в Set -- Hom(R_i, -) -- разные).

Чтобы избавиться от привязки к выделенному набору носителей и операций, естественно рассматривать просто весь дуал категории представимых объектов (C_λ)^op как инвариантное понятие существенно алгебраической категории.

Def. Предельной теорией ранга λ называется малая категория, имеющая все λ-малые пределы. Для λ-предельной теории T и категории с λ-малыми пределами C, категорий T-объектов в С T[C] называется категория сохраняющих λ-малые пределы функторов T -> C и естественных преобразований между ними.

Конечно, естественные морфизмы предельных теорий -- функторы сохраняющие λ-малые пределы, так -[-] функториальна по обоим аргументам. Это задает двойственность между синтаксисом и семантикой:

Двойственность Габриэля-Улмера

2-категория предельных теорий ранга λ антиэквивалентна 2-категории локально λ-представимых категорий

Теперь точные формулировки анонсированных свойств категорий математических структур.

Теорема о сопряженном функторе. Для F: С -> D морфизма λ-представимых категорией (то есть функтора ранга λ)
* F сохраняет все малые пределы <=> F является правым сопряженным
* F сохраняет все малые копределы <=> F является левым сопряженным
Кроме того,
* Любой сопряженный функтор между λ-представимыми категориями является морфизмом

Rem.
1) Конечно в случае копределов условие о ранге функтора выполнено заведомо, также как и для левых сопряженных функторов последняя часть тривиальна.
2) Ранги всех трех объектов (двух категорий и функтора) могут быть даны произвольными -- можно перейти к большему и применять теорему.

При этом интересно (и очень просто), что для любого сопряжения L : C <-> D : R следующие два условия равносильны
* R имеет ранг λ
* L сохраняет λ-представимые объекты

Так как при любом предположении в круговом равенстве

= Hom(A, R(colim X_i)) = Hom(A, colim R(X_i)) = colim Hom(A, R(X_i)) = colim Hom(L(A), X_i) = Hom(L(A), colim X_i) =

все "=" кроме одного (из двух едва различимо выделенных) будут известны (λ-представимость A, λ-фильтрованность X_i и сопряженность). Значит по теореме выше, в частности, таковы все забывающие (R) и свободные (L) функторы между λ-представимыми категориями (только надо проверить что забывающий функтор (в смысле синтаксиса существенно алгебраических теорий) является правым -- мне кажется, это очевидно, попозже напишу).

Внутренние свойства.
(1) В λ-представимой категории λ-малые пределы коммутируют с λ-фильтрованными копределами (для предпучков т.к. пределы и копределы вычисляются поточечно => верно для любых их подкатегорий замкнутых относительно пределов и λ-фильтрованных копределов)
(2) Рефлексивная λ-подкатегория λ-представимой категории является λ-представимой (рефлектор сохраняет λ-представимые объекты и копределы => для каждого объекта рефлексивной подкатегории берем внешний копредел λ-представимых и рефлективизируем его)
(3) Для M монады ранга λ (= её подл. функтор таков) на λ-представимой категории, категория Alg M λ-представима. Это обобщает (2), как случай идемпотентных монад.
(4) В λ-представимой все slice и colsice категории λ-представимы

Ещё одно интересное не упоминавшееся свойство:

Недуализируемость. Если C и C^op локально представимы => C предпорядок.

Естественно из свойства (3) следует, что для любой монады имеющий ранг (синоним: допустимая монада) её категория алгебр локально представима, если подлежащая такова (выбираем больший из рангов монады и подлежащей категории). Если монада недопустима, то и для Set категория алгебр не обязательно локально представима. Например, категория алгебр монады ультрафильтров -- то есть категория компактных хаудсорфовых пространств, не является локально представимой т.к. двойственная ей категория коммутативных унитальных C^*-алгебр локально представима. Мне кажется, что для любой монады без ранга это верно -- интересно найти (возможно в литературе?) общее объяснение этого.

Про epi-mono морфизмы напишу позже, там сама по себе отдельная большая супер интересная тема.

[AR94] Adamek, Rosicky - Locally presentable and accessible categories (1994)
[FB94] Francis Borceux - Handbook of categorical algebra (1994)

Egbert Rijke - Introduction to Homotopy Type Theory (Dec 2022)

Активное влияние на написание книги оказывали: Steve Awodey, Dan Grayson, Andrej Bauer

Ранние версии книги читали и обсуждали: William Barnett, Katja Berčič, Marc Bezem, Ulrik Buchholtz, Ali Caglayan, Dan Christensen, Thierry Coquand, Peter Dybjer, Jacob Ender, Martín Escardó, Sam van Gool, Kerem Güneş, Bob Harper, Matej Jazbec, Urban Jezernik, Tom de Jong, Ivan Kobe, Anders Mortberg, Clive Newstead, Charles Rezk, Emily Riehl, Mike Shulman, Elif Uskuplu, Chetan Vuppulury, Blaž Zupančič

Начал читать -- по-моему, выглядит потрясающим введением, намного более функциональным для начинающего, чем HoTT Book. Не предполагает пререквизитов в теории типов.
(UPD 14.10.2023 После понимания основ по этой книге, рекомендую переключаться на существенно более богатую темами HoTT Book)

Очень хочется, по возможности, везде уже переходить на этот язык -- многое будет становится более естественно и ясно (вчера вот перечитал, например: anafunctor; вспоминается также this). Если действительно (как я надеюсь) несложно быстро переводить любого через языковой барьер при необходимости. На самом деле, у меня сложилось впечатление, что вот такое изучение языка в реальных курсах, как правило, получается намного более интересным и эффективным, чем изучение его самого по себе (хотя и одна лекция под введение, конечно, необходима).

Почему мы хотим изучать кольца с точностью до изоморфизма, а категории с точностью до эквивалентности?

Какое-то время я подумывал над этим вопросом, не понимая что же это вообще значит / как можно превратить это в строгие утверждения?

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

В двух словах, гомотопическая теория типов отличается от обычного (дискретного) взгляда на математику в том, что в ней "структура равенства" не обязана быть бинарным отношением "да/нет", а может представлять собой ∞-группоид. В частности, это может быть тот же 0-группоид / отношение эквивалентности (обычное равенство для элементов множеств), но может быть и более общий 1-группоид (релевантное понятие равенства для объектов многих 1-категорий), и ещё более общий 2-группоид (соотв. для объектов 2-категорий) и т.д.

К слову, часто в популярных пересказах (в том числе кажется на вики) фразу "в гомотопической теории типов отождествляются изоморфные объекты" понимают неправильно думая, что богатое понятие изоморфизма в ней редуцируется до бедного понятия 0-равенства, когда, на самом деле, это понятие равенства расширяется так, что потенциально может совпадать с изоморфизмом (и быстро становится видно, что это принципиально естественнее, что так и было с самого начала)

По умолчанию типы и простые алгебраические структуры образованные из них — высшие (в семантике теории гомотопий / sSet: типы — ∞-множества т.е. ∞-группоиды, кольца — ∞-кольца и т.д.). Но можно определить n-усеченные типы и n-усечения (в семантике sSet соответствуют усечениям в смысле теории гомотопий — то есть этажам башни Постникова) следующим образом:

X (-1)-усеченный := для любых x, y : X верно, что x = y. В теории типов кванторы и логика устроены так, что эта фраза означает "задана функция, которая по x, y строит элемент типа x = y" (элементы этого типа называют свидетелями равенства — скажем, в некоторых 1-ситуациях это может быть изоморфизм x -> y, ). Ясно, что гомотопически, в предположении исключенного третьего, это условие означает " стягиваемый или пустой": если есть хотя бы одна точка, то функториальное семейство путей реализует стягивание к ней. Эти типы играют роль простых предложений / логических значений (в предположении исключенного третьего соответственно true и false)

X (n+1)-усеченный := для любых x, y : X верно, что тип x = y n-усеченный.

Множества определяются как 0-типы и в гомотопической семантике они в точности совпадают с классическими множествами (для каждых двух элементов их равенство — это просто утверждение/факт). Но тип множеств автоматически является 1-типом, равенство в нем и есть изоморфизм множеств. Тоже самое касается типа групп (определенных через эти множества, а не произвольные типы, я имею в виду, т.е. 1-групп).

1-категория задается следующими данными:
* тип объектов Ob
* для каждых a, b: Ob задано множество Hom(a, b)
* композиция, id
* обычные аксиомы
* естественное отображение =(a, b) -> iso(a, b) является эквивалентностью этих типов [аксиома унивалентности, гарантирующая согласованность изначального равенства на типе Ob и того, что приходит из структуры категории — вообще говоря первое может быть более строгим, что собственно и имеет место для всех категорий в дискретных основаниях, кроме очень узкого класса gaunt категорий]

Итак, легко показать, что тип 1-категорий является 2-типом, а равенством 1-категорий является эквивалентность.

Подробнее объясню скоро на планируемом мини-курсе по HoTT для гомотопистов (анонс будет позже)