Глава 3. Категория систем Sys(L)

Где стоит глава

Глава 14.1 дала категорию как метасистему; Глава 14.2 — функторы, естественные преобразования и вложение Йонеды, чьим итогом был тезис «объект определяется своими ролями» (категорная форма P3). Эта глава замыкает круг: мы строим категорию самих систем $\text{Sys}(L)$ — ту, ради которой затевался весь ToS, — и показываем, что в ней P3 получает свою изначальную, наиболее конкретную форму:

изоморфизм строго слабее лейбницева равенства — существуют системы, изоморфные в $\text{Sys}(L)$, но не равные как объекты Rocq (P3_strictly_stronger_than_iso).

Вложение Йонеды из 14.2 (локальный слой) — абстрактная тень этого факта. Здесь же он доказан машинно на конкретной категории систем. Все якоря главы — в основной ветке (origin/main): можно ссылаться уверенно.

Система — объект, морфизм — сохранение критерия

Возврат к Главе 1.5. Система на уровне $L$ несёт свои элементы (ElemOf $S$) и критерий (роль-правило, конституирующее, что принадлежит системе). Морфизм $f:S_1\to S_2$ — отображение элементов $‘ElemOf‘S_1\to ‘ElemOf‘S_2$, сохраняющее критерий: оно переносит «быть элементом $S_1$» в «быть элементом $S_2$».

Машинно это запись с композицией и сетоидным равенством морфизмов.¹ Композиция ассоциативна, тождество нейтрально — ровно условия, чтобы системы и их морфизмы образовали категорию (следующий раздел). Вводятся и роли морфизмов: вложение (is_embedding, инъективно на элементах), сюръекция (is_surjection) и изоморфизм (is_isomorphism — двусторонне обратимая пара).

Категория $\text{Sys}(L)$

Собранная категория — SystemCat $L$: объекты — системы уровня $L$, морфизмы — SystemMorphism, композиция — compose_morphism, равенство морфизмов — сетоидное.²

Машинно проверено, что категорные понятия совпадают с системными: изоморфизм в SystemCat равносилен системному изоморфизму (SystemCat_iso_iff_isomorphism); вложение влечёт мономорфность, сюръекция — эпиморфность (embedding_ implies_ SystemCat_mono, surjection_ implies_ SystemCat_epi). То есть категорный язык 14.1 действительно описывает системы: «моно/эпи/изо» сети стрелок суть «вложение/сюръекция/изоморфизм» систем.

Инициальный и терминальный объекты: иерархия снизу

В $\text{Sys}(L)$ есть инициальный и терминальный объекты: пустая система empty_system (единственная стрелка из неё в любую) и единичная система unit_system (единственная стрелка в неё).³

Тонкость P4: их нельзя поставить на дно. Построение empty_system и unit_system требует свидетеля $w\ll L$ — уровня ниже $L$. На уровне $L1$ такого нет (no_system_at_L1_with_witness), и SystemCat $L1$ вырождена (SystemCat_L1_vacuous); инициальный и терминальный объекты появляются лишь на уровнях вида $LSL$ (SystemCat_ LS_ has_ initial_ and_ terminal). Это честный P4-урок: «пустое» и «единичное» суть роли в иерархии, а не первичные объекты на дне — они сами опираются на уровень-под-собой. (Параллель с Частью X: пустое множество — не беспредпосылочный объект.)

Функтор Элементов: забывание до носителя

Категорное прочтение E/R/R даёт забывающий функтор «система$\mapsto$её элементы»:

$$‘ElementsFunctor‘L:\text{Sys}(L)⟶\mathbf{TypeCat},$$

который объекту сопоставляет тип его элементов, а морфизму — действие на элементах. Он верен (ElementsFunctor_faithful: морфизм определяется своим действием на элементах) и сохраняет изоморфизмы (ElementsFunctor_ preserves_ iso). ⁴

С точки зрения E/R/R: «элементы» — это образ забывающего функтора; «роли» — структура морфизмов; «правила» — законы категории и (ниже) разделение P3. Изоморфизм систем даёт биекцию их элементов (iso_gives_element_bijection) — но, как мы сейчас увидим, не лейбницево равенство систем.

Ядро P3: изоморфизм $\ne$ лейбницево равенство

Это центр главы и одна из вершин Части XIV. Соотношение «равенство / изоморфизм» машинно разложено на две несимметричные половины:

{

• Лейбницево равенство влечёт изоморфизм: равные системы изоморфны (P3_eq_implies_iso) — тривиальная сторона.
• Изоморфизм не влечёт лейбницева равенства: существуют системы, изоморфные в SystemCat, но не равные как объекты Rocq (P3_strictly_stronger_than_iso, iso_not_implies_P3). }

Вместе это и есть P3_separation_categorical: изоморфизм строго слабее лейбницева равенства. Изоморфизм сохраняет всё, что видно «снаружи» — предикат-критерий (iso_implies_predicate_equiv), биекцию элементов, корректность, — но не всякую внутреннюю разметку: например, граница позиции не инвариантна относительно изоморфизма (position_ bound_ not_ iso_ invariant). ⁵

Почему это P3. P3 (Различение) утверждал, что интенсиональная идентичность тоньше экстенсиональной совпадаемости. Здесь это становится точной категорной теоремой: «вести себя одинаково по отношению ко всем стрелкам» (изоморфизм) строго слабее, чем «быть тем же объектом» (лейбницево равенство). Связь с 14.2 прямая: вложение Йонеды (локальный слой 14.2) говорит, что объект определяется ролями с точностью до изоморфизма — а P3 добавляет, что эта точность не есть тождество. Категорная структура инвариантно работает с изоморфизмом; лейбницево равенство остаётся мета-уровневым отношением объектов Rocq и не является категорным инвариантом — это честная граница, а не дефект.

Разбор E/R/R: категория систем как E/R/R категорно

Правила (L5). Законы категории $\text{Sys}(L)$ (ассоциативность/единицы) + критерий-сохранение морфизмов + разделение P3 (изоморфизм $\ne$ лейбницево равенство). Универсальные роли empty_system/unit_system требуют уровня-под-собой (P4-иерархия).

Роли (L4). Система — объект; морфизм — критерий-сохраняющий перенос; вложение/ сюръекция/изоморфизм — роли морфизмов; ElementsFunctor — роль-забывание (до носителя); изоморфизм — роль «неотличимо ролями», но не «тождественно».

{

Элементы (L1$+$P4). Конкретные данные: ElemOf $S$, компоненты морфизмов, биекции элементов при изоморфизме. Не элемент категорной наблюдаемости: лейбницево равенство систем — как Prop оно существует, но не восстанавливается из сети морфизмов (тоньше изоморфизма) — именно это и фиксирует P3.}

Компонент	Что фиксирует	E/R/R-категория
законы $\text{Sys}(L)$ + критерий-сохранение + P3-разделение	конституцию категории систем	Правило (L5)
система$=$объект; морфизм$=$перенос; iso$=$«неотличимо ролями»	статус систем и отображений	Роль (L4)
ElemOf $S$; компоненты морфизмов; биекции при iso	вычислимые носители	Элемент (L1$+$P4)

Что снимает разбор. Вопрос «когда две системы суть одно и то же?» часто смешивает два понятия. ToS различает их машинно: изоморфизм (одинаковость ролей) и лейбницево равенство (тождество объекта) — разные отношения, и первое строго слабее. Категория систем видит первое и не видит второго; это не пробел, а конституция P3.

Что глава подготовила

Построена категория систем $\text{Sys}(L)$ (SystemCat, 29 Qed) с морфизмами как критерий-сохраняющими переносами (SystemMorphism, 17 Qed); категорные iso/mono/epi совпали с системными; инициальный и терминальный объекты существуют (на уровнях $LSL$, не на дне — P4); забывающий ElementsFunctor верен и сохраняет изоморфизмы. Ядро — машинная теорема P3_strictly_stronger_than_iso: изоморфизм строго слабее лейбницева равенства. Всё в origin/main, 0 аксиом.

Дальше — Глава 14.4: функторы между уровнями (embed/forget) и их сопряжение — корона Части XIV, где принцип P2 (Дополнительность) оказывается категорным сопряжением $‘embed‘⊣‘forget‘$ (embed — левый, forget — правый).

---

---

Часть: Часть XIV. Категория систем · Том: «Математика»

Понятия: Формализация

Навигация: ← Глава 2. Функторы, естественные преобразования, лемма Йонеды · Глава 4. Функторы между уровнями и сопряжение →

Footnotes

1. src/SystemMorphism.v (17 Qed, 0 Admitted; в origin/main; изоморфизм определён конструктивно, без аксиомы выбора — файл заявляет 0 аксиом): ElemOf, Record SystemMorphism (mkSystemMorphism), id_morphism, compose_morphism, morphism_eq (+ рефл./сим./транз.), compose_assoc, compose_id_left/_right; is_embedding, is_surjection, is_isomorphism (+ iso_symmetric, iso_pair_predicate_equiv). ↩

2. src/SystemCategory.v (29 Qed, 0 аксиом; в origin/main): SystemCat $L$ как Category; SystemCat_valid, SystemCat_comp_is_compose, SystemCat_id_is_id; SystemCat_ iso_ iff_ isomorphism, embedding_ implies_ SystemCat_mono, surjection_ implies_ SystemCat_epi, SystemCat_iso_compose. ↩

3. SystemCategory.v: empty_system, empty_is_initial; unit_system, unit_is_terminal; SystemCat_initial_unique, SystemCat_terminal_unique; SystemCat_LS_has_initial_and_terminal. ↩

4. src/ERR_Categorical.v (24 Qed, 0 аксиом; в origin/main): ElementsFunctor, ElementsFunctor_obj/_mor, ElementsFunctor_faithful, ElementsFunctor_ preserves_ iso; iso_gives_element_bijection. ↩

5. ERR_Categorical.v: P3_eq_implies_iso, iso_implies_predicate_equiv, P3_strictly_stronger_than_iso, iso_not_implies_P3, P3_separation_categorical, position_ bound_ not_ iso_ invariant, well_formed_iso_invariant, err_decomposition. ↩