7.4: Топози
- Page ID
- 66454
Топози
Топос визначається як категорія снопів. \(^{9}\)Таким чином, для будь-якого топологічного простору (X, Op) категорія Shv (X, Op), визначена в Definition 7.35, є топосом. Зокрема, беручи одноточковий простір X = 1 з його унікальною топологією, ми виявляємо, що категорія Set є топосом, як ми вже говорили все разом і побачили знову явно в прикладі 7.48. І для будь-якої схеми бази даних - тобто кінцево представлена категорія - C, категорія C- Inst екземплярів бази даних на C також є топоз.10 Топози охоплюють обидва ці джерела прикладів, і багато іншого.
Топози - це неймовірно приємні структури, з безлічі, здавалося б, розрізнених причин. У цьому ескізі причина фокусування полягає в тому, що кожен топос має багато однакових структурних властивостей, що і категорія Set. Дійсно, ми обговорювали в розділі 7.2.1, що кожен топос має обмеження та коліміти, декартовий закритий, має епі-моно факторизації та має класифікатор підоб'єктів (див. Розділ 7.2.2). Використовуючи ці властивості, можна зробити логіку з семантикою в топосі Е. Ми пояснили це для множин, але тепер уявіть це для снопів на топологічному просторі. Там, ті ж логічні символи\(\land\), ¬\(\lor\), ⇒,,, ⟩ стають операціями, які означають щось про підшків—наприклад, векторні поля, секції неперервних функцій тощо - не тільки підмножини.
Щоб зрозуміти це глибше, слід сказати, що істинний класифікатор підоб'єктів: 1 → Ω є більш загальним. Ми сказали, що в topos Set, subobject класифікатор є множиною булевих Ω =\(\mathbb{B}\). У снопі topos\(\mathcal{E}\) = Shv (X, Op) об'єкт Ω\(\in\)\(\mathcal{E}\) - це сніп, а не просто безліч. Що це за сніп?
Суб'єктний класифікатор Ω в топосі снопа
У цьому підрозділі ми прагнемо зрозуміти підпредметний класифікатор Ω, тобто об'єкт значень істинності, в снопі топос Shv (X, Op). Оскільки Ω - це сніп, давайте розберемося в цьому випадку, проходячи через визначення сніпа (Визначення 7.35) повільно в цьому випадку. Сніп Ω - це пресноп, який задовольняє умові сніпа.
Як прешхеф це просто функтор Ω: Op\(^{op}\) → Set; він призначає набір Ω (U) кожному відкритому U\(\subseteq\) X і поставляється з картою обмежень Ω (U) → Ω (V) щоразу, коли V\(\subseteq\) U. Тож у нашому прагненні зрозуміти Ω ми спочатку задаємо питання: що це таке прешеф?
Відповідь на наше запитання полягає в тому, що Ω - це прешеф, який\(\in\) присвоює U Op безліч відкритих підмножин U:
Ω (U) := {U ′\(\in\) Оп | U ′\(\subseteq\) U} . (7,50)
Це було легко, правда? А з огляду на карту обмежень для V\(\subseteq\) U дається
Ω (U) → Ω (В) (7,51)
U ′\(\longmapsto\) U ′ V.
Можна перевірити, що це функціональний див. Вправа 7.53 - і після цього нам все одно потрібно буде побачити, що він задовольняє умові снопа. Але принаймні нам не потрібно боротися, щоб зрозуміти Ω: це дуже схоже на саму Оп.
Нехай X = {1} буде одним точковим простором. Ми говорили вище, що його підоб'єктний класифікатор - це набір\(\mathbb{B}\) булевих, але як це вирівнюється з визначенням Ω, наведеним у еквалайзері (7.50)? ♦
- Показати, що визначення Ω, наведене вище в Eqs. (7.50) і (7.51) є функціональним, тобто, що всякий раз, коли W\(\subseteq\) V\(\subseteq\) U, карта обмежень Ω (U) → Ω (V), за якою слідує карта обмежень Ω (V) → Ω (W) є те саме, що і карта обмежень Ω (U) → Ω (W).
- Це все, що потрібно, щоб зробити висновок, що Ω - це прешоп? ♦
Щоб побачити, що Ω, як визначено в Eq. (7.50) задовольняє умові снопа (див. Визначення 7.35), припустимо, що у нас є кришка U =\(\bigcup_{i \in I} U_{i}\), і припустимо, що даний елемент V\(_{i}\) \(\in\)Ω (U\(_{i}\)), тобто відкритий набір V\(_{i}\) \(\subseteq\)U\(_{i}\), для кожного \(\in\)я.
Припустимо далі, що для всіх \(\in\)i, j I, це той випадок,\(_{i}\) що V U\(_{j}\) = \(_{j}\)V U\(_{i}\), тобто що елементи утворюють відповідність сім'я.
Визначити V: =\(\bigcup_{i \in I} V_{i}\); це відкрита підмножина U, тому ми можемо розглядати V як елемент Ω (U).
Нижче перевіряється, що V дійсно є склеюванням для (V\(_{i}\))\(_{i \in I}\):
\(V \cap U_{j}=\left(\bigcup_{i \in I} V_{i}\right) \cap U_{j}=\bigcup_{i \in I}\left(V_{i} \cap U_{j}\right)=\bigcup_{i \in I}\left(V_{j} \cap U_{i}\right)=\left(\bigcup_{i \in I} U_{i}\right) \cap V_{j}=V_{j}\)
Іншими словами V U\(_{j}\) = V\(_{j}\) для будь-якого j\(\in\) I. Таким чином, наш Ω був модернізований з presheaf до снопа!
Орлиноокий читач помітить, що ми ще не дали всіх даних, необхідних для визначення класифікатора підоб'єктів. Щоб перетворити об'єкт Ω в підпредметний класифікатор у доброму стані, нам також потрібно дати морфізм сніпа true: {1} → Ω. Тут {1}: Оп\(^{op}\) → Встановити — це термінальний сніп; він зіставляє кожен відкритий набір до терміналу, один елемент встановлює {1}.
Правильний морфізм істинний: {1} → Ω для підоб'єктного класифікатора є морфізм сніпа, який призначає для кожної U\(\in\) Оп функцію {1} = {1} (U) → Ω (U) відправку 1 → U, найбільшу відкриту множину \(\subseteq\)U. Відтепер ми позначаємо {1} просто як 1.
Upshot: Значення істинності є відкритими множинами. Справа в тому, що значення істинності в топосах снопів на просторі (X, Op) є відкритими множинами цього простору. Коли хтось каже «чи вірно майно P? ,» відповідь не так чи ні, але «це правда на відкритій підмножині U». Якщо це U - це все, U = X, то P дійсно вірно; якщо U - ніщо, U = Ø, то P дійсно хибний. Але в цілому, це просто вірно в деяких місцях, а не інших.
Категорія Graph графіків є presheaf топос, і можна також думати про нього як категорію екземплярів для схеми бази даних, як ми бачили в прикладі 7.23. Суб'єктний класифікатор Ω в топосі Gr, таким чином, є графіком, тому ми можемо його намалювати. Ось як це виглядає:
Знайти Ω для себе найпростіше, використовуючи те, що називається Yoneda Lemma, але ми цього не представили. Для приємного, легкого введення в топос графіків див. [Vig03]. Термінальний граф є однією вершиною з одним циклом, а гомоморфізм графа істинний: 1 → Ω посилає цей цикл до (V, V; A).
З огляду на будь-який граф G та підграф i: H\(\subseteq\) G, нам потрібно побудувати гомоморфізм графа\(lceil{H}rceil\): G → Ω, що класифікує H. Ідея полягає в тому, що для кожної частини G ми вирішуємо «скільки його в H. Вершина в v в G або в H, або ні; якщо так, ми відправляємо її в V, а якщо ні, то відправляємо її до 0. А ось стрілки а - складніше. Якщо a знаходиться в Н, відправляємо його (V, V; A). Але якщо це не в Н, математика вимагає від нас задавати більше питань: чи є її джерело в H? чи є його ціллю в G»? обидва? ні? На основі відповідей на ці питання відправляємо a до (V, 0; 0), (0, V; 0), (V, V; 0), або (0, 0; 0) відповідно.
Розглянемо подграф H\(\subseteq\) G, показаний тут:
Знайдіть графік гомоморфізму\(lceil{H}rceil\): G → Ω класифікуючи його. Див. Приклад 7.54. ♦
7.4.2 Логіка в топосі снопа
Розглянемо логічні зв'язки, І, АБО, МАЄ НА УВАЗІ, А НЕ. Припустимо, у нас є топологічний простір X\(\in\) Op.
З огляду на дві відкриті множини U, V, які розглядаються як значення істинності U, V\(\in\) Ω (X), то їх сполучник 'U І V' є їх перетином, а їх диз'юнкція 'U АБО V' є їх об'єднанням;
(U\(land\) V) := U V і (U\(\lor\) V) := U\(\bigcup\) V. (7.56)
Ці формули легко запам'ятати, тому що\(land\) виглядає як і\(\lor\) виглядає як\(\bigcup\).
Імплікація U ⇒ V є найбільшою відкритою множиною R таким, що R U\(\subseteq\) V, тобто
\((U \Rightarrow V):=\bigcup_{\left\{R \in \mathbf{O}_{\mathbf{p}} \mid R \cap U \subseteq V\right\}} R .\)(7.57)
Загалом, зменшити еквалайзер (7.57) далі непросто, тому підтекст є найважчим логічним сполучним для топологічного мислення.
Нарешті, заперечення U задається ¬ U: = (U ⇒ брехня), і це виявляється відносно простим.
За формулою в Eq. (7.57) це об'єднання всіх R таких, що R U = Ø, тобто об'єднання всіх відкритих множин в доповненні U. Якщо ви знаєте топологію, ви можете визнати, що ¬ U - це «інтер'єр доповнення U».
Розглянемо дійсну пряму X =\(\mathbb{R}\) як топологічний простір (див. Вправа 7.27).
Нехай U, V\(\in\) Ω (X) відкриті множини U = {x\(\in\) R | x < 3} і V = {x\(\in\)\(\mathbb{R}\) | −4 < x < 4}. Використовуючи інтервальне позначення, U = (−∞, 3) та V = (−4, 4). Тоді
• U\(\land\) V = (−4, 3).
• U\(\lor\) V = (−∞, 4).
• ¬ U = (3, ∞).
• ¬ V = (−∞, −4) (4, ∞).
• (U ⇒ V) = (−4, ∞)
• (V ⇒ U) = U
Розглянемо дійсну пряму\(\mathbb{R}\) як топологічний простір, а відкриту підмножину U =\(\mathbb{R}\) − {0}.
1. Що таке відкрита підмножина ¬ U?
2. Що відкрита підмножина ¬¬ U?
3. Чи правда, що U\(\subseteq\) ¬¬ U?
4. Чи правда, що ¬¬ U\(\subseteq\) U? ♦
Вище ми пояснили операції над відкритими множинами, по одній відповідній кожній логічній сполучній; є також відкриті множини, відповідні символам true і false. Ми досліджуємо це у вправі.
Нехай (X, Op) є топологічним простором.
- Припустимо, символ true відповідає відкритій множині такий, що для будь-якого відкритого набору U\(\in\) Op ми маємо (true\(\land\) U) = U. Який це відкритий набір?
- Інші речі, які ми повинні очікувати від істинного включають (true\(\lor\) U) = true і (U ⇒ true) = true і (true ⇒ U) = U. Чи тримають вони для вашої відповіді на 1?
- Символ false відповідає відкритому множині U\(\in\) Оп такий, що для будь-якого відкритого набору U\(\in\) Op ми маємо (false\(\lor\) U) = U. Який це відкритий набір?
- Інші речі, які ми повинні очікувати від false включають (false\(\land\) U) = false і (false ⇒ U) = true. Чи тримають вони для вашої відповіді на 1? ♦
Для векторного пучка π: E → X над простором X відповідним сніпом є Secπ, що відповідає його ділянкам: до кожного відкритого множини i\(_{U}\): U\(\subseteq\) X ми пов'язуємо множину функцій s: U → Е, для яких s; π = i\(_{U}\). Наприклад, у випадку з дотичним пучком π: T M → M (див. Приклад 7.46) відповідний сніп, назвавши його VF, пов'язує з кожним U множину VF (U) векторних полів на U.
Внутрішня логіка топосу може бути використана для розгляду властивостей векторних полів. Наприклад, можна мати предикат Grad: VF → Ω, який запитує найбільший підпростір Grad (v), на якому задане векторне поле v походить від градієнта деякої скалярної функції. Можна також мати присудок, який запитує найбільший відкритий набір, на якому векторне поле є ненульовим. Логічні операції, такі як\(\land\) і потім\(\lor\) можуть бути застосовані для точних підмноговидів, протягом яких зберігаються різні бажані властивості, і логічно міркувати про те, які інші властивості змушені утримувати там.
7.4.3 Присудки
В англійській мові присудок - це частина речення, яка йде після підмета. Наприклад «.. є парним» або «.. любить погоду» є предикатами. Не кожен підмет має сенс для даного присудка; наприклад, речення «7 є парним» може бути помилковим, але це має сенс. На відміну від цього, речення «2.7 навіть» насправді не має сенсу, а «2.7 любить погоду», звичайно, не. в інформатиці вони можуть сказати, що «вираз '2.7 любить погоду» не набирає перевірку».
Справа в тому, що кожен присудок пов'язаний з типом, а саме типом суб'єкта, який має сенс для цього присудка. Коли ми застосовуємо присудок до суб'єкта відповідного типу, результат має значення істинності: «7 парно» - це або true, або false. Можливо, «Боб любить погоду» є правдою в одні дні і помилковим для інших. Насправді, це значення істини може змінюватися з роком (погана погода цього року), за сезоном, годинами тощо Англійською мовою ми очікуємо, що істинні значення речень змінюватимуться з часом, що саме є мотивацією для цієї глави. Ми працюємо над логікою, де цінності істини змінюються з часом.
У топосі\(\mathcal{E}\) = Shv (X, Op) предикат - це морфізм сніпа p: S → Ω, де S\(\in\)\(\mathcal{E}\) - сніп, а Ω\(\in\)\(\mathcal{E}\) - класифікатор підоб'єктів, сніп значень істини. За визначенням 7.35 отримуємо функцію p (U): S (U) → Ω (U) для будь-якого відкритого множини U\(\subseteq\) X. У наведеному вище прикладі, який ми обговоримо більш ретельно в розділі 7.5 - якщо S - це сніп людей (люди приходять і йдуть з часом), а Bob\(\in\) S (U) - це людина, яка існує протягом певного часу U, а p - присудок «любить погоду» то p (Bob) - це сукупність часів, протягом яких Бобу подобається погода. Тож відповідь на «Боб любить погоду» - це щось на кшталт «влітку так, а також у квітні 2018 та травні 2019 року так, але в усі інші часи ні». Це p (Bob), тимчасове значення істини, отримане шляхом застосування присудка p до підмета Боба.
Тільки зараз ми описали, як присудок p: S → Ω, типу «. любить погоду», діє на розділах s\(\in\) S (U), скажімо s = Bob. Але за визначенням 7.12 будь-який присудок p: S → Ω також визначає підоб'єкт {S | p}\(\subseteq\) S. Опишіть розділи цього підсніпа. ♦
Пост суб'єкт. Для топоса\(\mathcal{E}\) = Shv (X, Op) і об'єкта (сніп) S\(\in\)\(\mathcal{E}\) множина S -предикатів |Ω\(^{E}\) | =\(\mathcal{E}\) (S, Ω) природно дається структура позета, яку ми позначимо
(| Ом\(^{S}\) |, ≤\(^{S}\)) (7,63)
За даними двох предикатів p, q: S → Ω, скажемо, що p ≤\(^{S}\) q, якщо перший має на увазі другий. Точніше, для будь-якого U\(\in\) Op і розділу\(\in\) s S (U) отримаємо дві відкриті підмножини p (s)\(\subseteq\) U і q (s)\(\subseteq\) U. Ми говоримо, що p ≤\(^{S}\) q якщо p (s)\(\subseteq\) q (s) для всіх U\(\in\) Op і s\(\in\) S (U). Ми часто скидаємо верхній індекс з ≤\(^{S}\) і просто пишемо ≤. У формальних логічних позначеннях можна записати p ≤\(^{S}\) q за допомогою символу, наприклад, одним із таких способів:
s: S | p (s) q (s) або p (s)\(_{s:S}\) q (s).
Зокрема, якщо S = 1 є кінцевим об'єктом, ми позначаємо |Ω\(^{S}\) | по |ω|, а елементи p\(\in\) |ω| посилаємося на пропозиції. Вони всього лише морфізми р: 1 → Ω.
Цей попередній порядок є частково впорядкованою позицією, що означає, що якщо p ≤ q та q ≤ p, то p = q.
Причина в тому, що для будь-яких підмножин U, V\(\subseteq\) X, якщо U\(\subseteq\) V і V\(\subseteq\) U то U = V.
Наведіть приклад пробілу X, снопа S\(\in\) Shv (X) та двох предикатів p, q: S → Ω, для яких утримується p (s)\(_{s:S}\) q (s).
Ви не повинні бути офіційними. ♦
Всі логічні символи (true, false\(\land\),\(\lor\),,, ⇒, ¬) з розділу 7.4.2 мають сенс у будь-якій такій посаді |Ω\(^{S}\) |.
Для будь-яких двох предикатів p, q: S → Ω визначаємо (p\(\land\) q): S → Ω шляхом (p\(\land\) q) (s) := p (s)\(\land\) q (s), і аналогічно для\(\lor\). Таким чином, можна сказати, що ці операції обчислюються точково на S.
З цими визначеннями\(\land\) символ є зустріччю, а\(\lor\) символ є об'єднанням у значенні Визначення 1.81 для poset |Ω\(^{S}\) |.
З усією логічною структурою, яку ми визначили досі, poset |Ω\(^{S}\) | предикатів на S утворює те, що називається алгеброю Хейтінга. Ми не будемо його визначати тут, але більше інформації можна знайти в розділі 7.6. Тепер перейдемо до кількісної оцінки.
7.4.4 Кількісна оцінка
Кількісна оцінка поставляється в двох смаках: універсальний і екзистенційний, або «для всіх» і «існує». Кожен приймає предикат з n + 1 змінних і повертає предикат з n змінних.
Припустимо, у нас є два снопа S, T\(\in\) Shv (X, Op) і присудок p: S × T → Ω. Скажімо, T представляє те, що вважається новиною гідною, а S - це знову набір людей. Таким чином, для підмножини часу U, розділ t\(\in\) T (U) - це те, що вважається заслуговує новин протягом усього U, а розділ s\(\in\) S (U) - це людина, яка триває протягом усього весь U. Уявімо присудок p як «s турбується про t». Тепер нагадаємо з розділу 7.4.3, що присудок p не просто повертає true або false; з огляду на людину s і новинний пункт t, він повертає значення істинності, відповідне підмножині часів, на яких p (s, t) є істинним.
«Для всіх t в T,.. турбується про t» сам по собі присудок тільки на одну змінну, S, яку ми позначимо
(т: Т). р (с, т).
Застосування цього присудка до людини s повертає часи, коли ця людина турбується про все в новині. Аналогічно, «існує t в Т таке, що s турбується про t» - це також присудок на S, який ми позначаємо (t: T). р (с, т). Якщо застосувати цей присудок до людини s, ми отримуємо часи, коли людина s турбується хоча б про одну річ у новині.
У множині топосів, де Ω =\(\mathbb{B}\), розглянемо присудок p:\(\mathbb{N}\) ×\(\mathbb{Z}\) →,\(\mathbb{B}\) заданий
1. Що таке множина n,\(\in\)\(\mathbb{N}\) для якої присудок (z:\(\mathbb{Z}\)). р (п, з) тримає?
2. Що таке множина n,\(\in\)\(\mathbb{N}\) для якої присудок (z:\(\mathbb{Z}\)). р (п, з) тримає?
3. Що таке множина z,\(\in\)\(\mathbb{Z}\) для якої присудок (n:\(\mathbb{N}\)). р (п, з) тримає?
4. Що таке множина z,\(\in\)\(\mathbb{Z}\) для якої присудок (n:\(\mathbb{N}\)). р (п, з) тримає? ♦
Отже, враховуючи p, ми маємо універсально- та екзистенціально-кількісний присудок (t: T). р (с, т) і (т: Т). р (с, т) на С. Як ми формально розуміємо їх як морфізми сніпів S → Ω або, еквівалентно, як підснопи S?
Універсальна кількісна оцінка. Дано присудок p: S × T → Ω, універсально кількісний присудок (t: T). p (s, t) приймає секцію s\(\in\) S (U), для будь-якого відкритого набору U, і повертає певний відкритий набір V\(\in\) Ω (U). А саме, він повертає найбільшу відкриту множину V\(\subseteq\) U, для якої p (s |\(_{v}\), t) = V тримає для всіх t\(\in\) T (V).
Припустимо, s - людина жива протягом усього інтервалу U. Застосуйте вищевказане визначення до прикладу p (s, t) = «людина s турбується про новини t» з Прикладу 7.65. Тут T (V) - це набір пунктів, які знаходяться в новині протягом усього інтервалу V.
- Що відкрита підмножина U є (t: T). p (s, t) для людини s?
- Чи має він семантичне значення, яке ви очікуєте, враховуючи менш формальний опис у розділі 7.4.4? ♦
Абстрактно кажучи, універсально кількісний присудок відповідає підсніпу, заданому наступним відкотом:
де p ′: S → Ω\(^{T}\) - це каррірованіе S × T → Ω і\(^{T}\) істинним є каррірованіе складеного 1 ×\(T \stackrel{!}{\rightarrow} A \stackrel{true}{\rightarrow} Ω\).
Див. ур. (7.10).
Екзистенціальна кількісна оцінка. Дано присудок p: S × T → Ω, екзистенціально кількісний присудок (t: T). p (s, t) приймає ділянку s\(\in\) S (U), для будь-якого відкритого множини U, і повертає певну відкриту множину V\(\in\) Ω (U), а саме об'єднання V = \(\bigcup_{i}\) V\(_{i}\) всіх відкритих множин V i, для яких існує деякий ti\(\in\) T (V i), що задовольняє p (s |\(_{Vi}\), t\(_{i}\)) = V \(_{i}\). Якщо результатом є сам U, ви можете спокуситися подумати «ах, тому існує деякий t\(\in\) T (U), що задовольняє p (t)», але це не обов'язково так. Є просто обкладинка U =\(\bigcup{U_{i}}\) і локальні секції ti\(\in\) T (U\(_{i}\)), кожен задовольняє p, як пояснено вище. Таким чином, екзистенціальний квантор робить багато роботи «під капотом», враховуючи покриття, не відображаючи цей факт у позначеннях.
Застосуйте вищевказане визначення до присудка «людина s стурбована новинами t» з Прикладу 7.65.
1. Що відкрито набір (t: T). p (s, t) для людини s?
2. Чи має це смислове значення, яке ви очікуєте? ♦
Абстрактно кажучи, екзистенціально-кількісне присудок дається наступним чином.
Почніть з підоб'єкта, класифікованого за p, а саме {(s, t)\(\in\) S × T | p (s, t)}\(\subseteq\) S × T, складіть з проекцією π\(_{S}\): S × T → S як у верхньому правому куті; потім візьміть епімоно факторизацію композиту, як у нижньому лівому куті:
Тоді нижня карта - це бажаний підсніп S.
7.4.5 Модальності
Ще в прикладі 1.123 ми обговорювали модальні оператори, також відомі як модальності, кажучи, що вони є операторами закриття на попередніх замовленнях, які виникають у логіці. Попередні замовлення, на які ми посилалися, - це ті, що обговорюються в еквалайзері (7.63): для будь-якого об'єкта S\(\in\)\(\mathcal{E}\) є позиція (|Ω\(^{S}\) |, ≤\(^{S}\)) предикатів на S, де |Ω\(^{S}\) | =\(\mathcal{E}\) (S, Ω) - це лише безліч морфізмів S → Ω в категорії\(\mathcal{E}\).
Модальність в Shv (X) - це морфізм сніпа j: Ω → Ω, що задовольняє три властивості для всіх U\(\subseteq\) X і p, q\(\in\) Ω (U):
(а) р ≤ j (р);
(б) (j; j) (р) ≤ j (р); і
(в) j (р\(\land\) q) = j (р)\(\land\) j (q).
Припустимо, j: Ω → Ω - це морфізм снопів на X, такий, що p ≤ j (p) тримає для всіх U\(\subseteq\) X і p\(\in\) Ω (U). Показати, що для всіх q\(\in\) Ω (U) у нас є j (j (q)) ≤ j (q), якщо j (q)) = j (q) . ♦
У прикладі 1.123 ми неофіційно сказали, що для будь-якої пропозиції р, наприклад, «Боб знаходиться в Сан-Дієго», існує модальний оператор «припускаючи p,...» Тепер ми в змозі зробити це формальним.
Виправте пропозицію p\(\in\) |ω|. Тоді
(а) морфізм сніпа Ω → Ω, заданий відправкою q до p ⇒ q, є модальністю.
(б) морфізм сніпа Ω → Ω, заданий відправкою q до p\(\lor\) q, є модальністю.
(c) морфізм сніпа Ω → Ω, заданий відправкою q до (q ⇒ p) ⇒ р є модальністю.
Ми не можемо довести Пропозиція 7.71 тут, але ми даємо посилання в розділі 7.6.
Нехай S буде снопом людей, як у розділі 7.4.3, і нехай j: Ω → Ω бути «припускаючи, що Боб знаходиться в Сан-Дієго...»
- Назвіть будь-який присудок p: S → Ω, наприклад «любить погоду».
- Виберіть часовий інтервал U. Для довільної особи s\(\in\) S (U), що це за речі p (s), і що це означає?
- Що це за річ j (p (s)) і що це означає?
- Чи правда, що p (s) ≤ j (p (s))? Поясніть коротко.
- Чи правда, що j (j (p (s))) = j (p (s))? Поясніть коротко.
- Виберіть інший присудок q: S → Ω. Чи правда, що j (р\(\land\) q) = j (p)\(\land\) j (q)? Поясніть коротко. ♦
7.4.6 Теорії типів і семантика
Ми говорили про логіку топоса з точки зору відкритих множин, але це насправді поєднання двох ідей, які дійсно краще залишити необ'єднаними. Перший - це логіка, або формальна мова, а друге - семантика, або значення. Формальна мова виглядає так:
(т: Т). (s: S). ф (и) = т (7,73)
і смислові висловлювання схожі на «морфізм сніпу f: S → T - це епіморфізм». У колишньому, логічному світі всі висловлювання - це лінгвістичні вирази, сформовані за суворими правилами і всі докази - це відрахування, які також дотримуються суворих правил. В останньому смисловому світі висловлювання і докази йдуть про самих снопах, як про математичних об'єктах. Ми визнаємо, що це грубі твердження; знову ж таки, наша мета тут - лише дати смак, запрошення до подальшого читання.
Надати семантику логічної системи означає надати компілятор, який перетворює кожне логічне твердження формальною мовою в математичне твердження про конкретні снопи та їх зв'язки. Комп'ютер може здійснювати логічні відрахування, не знаючи, що будь-який з них «означає» про снопах. Ми говоримо, що семантика є здоровою, якщо кожне формальне доказ перетворюється на справжній факт про відповідні снопи.
Кожному топосу можна привласнити формальну мову, яку часто називають його внутрішньою мовою, в якій виконувати конструкції та формальні докази. Ця мова має звукову семантику свого роду компілятор логіки-на-сніп, який йде під назвою категорична семантика або семантика Кріпке-Joyal. Основні ідеї ми дали в розділі 7.4; ми даємо посилання на літературу в розділі 7.6.
У кожному топосі E, і для кожного f: S → T в E морфізм f є епіморфізмом тоді і тільки тоді, коли Eq. (7.73) тримає. Наприклад, розглянемо випадок екземплярів бази даних на схемі C, скажімо, зі 100 таблицями (одна з яких може бути позначена c\(\in\) Ob (C)) і 500 стовпців зовнішнього ключа (один з яких може бути позначений f: c → c ′ в C); див. Eq. (3.2).
Якщо S і T є двома екземплярами, а f є природним перетворенням між ними, то ми можемо задати питання про те, чи тримає Eq. (7.73). Ця проста формула складається семантикою Кріпке-Джояля в запитуванні:
Чи правда, що для кожної таблиці c\(\in\) Ob (C) і кожного рядка\(\in\) s S (c) існує рядок t\(\in\) T (c) такий, що f (s) = t?
Це саме те, що означає для f бути суб'єктивним. Можливо, це не надто вражає, але чи йдеться про бази даних або топологічні простори, або складні ідеї з алгебраїчної геометрії, Eq. (7.73) завжди компілюється в питання про сприйнятливість. Для топологічних просторів було б сказати щось на кшталт:
Чи правда, що для кожного відкритого набору U\(\subseteq\) X і кожної секції\(\in\) s S (U) зв'язки S існує відкрите покриття (U\(_{i}\) \(\subseteq\)U)\(_{i \in I}\) U і перетину t\(_{i}\) \(\in\)T (U\(_{i}\)) зв'язки T для кожного i\(\in\) I, такого, що f (t\(_{i}\)) = s |\(_{U_{i}}\) це обмеження s до U\(_{i}\)?