Oℕ
Ну если вы возьмёте такую h, что pi1. h = f, pi2.h = g
Size: a a a
2019 December 02
Oℕ
То довольно очевидно чему равна h
МБ
Кстати, есть же альтернативное определение? Что-то типа для всех
h должно выполняться h = <h . pi_1, h . pi_2>. Или нечто похожее?Oℕ
Кстати, есть же альтернативное определение? Что-то типа для всех
h должно выполняться h = <h . pi_1, h . pi_2>. Или нечто похожее?тут композиция не в том порядке?
МБ
Хотя, муть написана. Наверное, так надо `h = <pi_1 . h, pi_2 . h>.
Oℕ
Кстати, есть же альтернативное определение? Что-то типа для всех
h должно выполняться h = <h . pi_1, h . pi_2>. Или нечто похожее?не знаю, у меня это не очень вяжется с формой "существует единственный, такой что"
Oℕ
обычно ∃!x :A , P(x) я рассматриваю это как тройку (x :A , P(x), ∀(y: A) P(y) -> x = y)
ЕО
обычно ∃!x :A , P(x) я рассматриваю это как тройку (x :A , P(x), ∀(y: A) P(y) -> x = y)
Ты много на агде пишешь?
Oℕ
Ты много на агде пишешь?
нет
A
ща, стоп, а проблема в чем, доказать, что декартово произведение в set является произведением в категории set?
A
ну то есть надо показать, что для любого C со стрелками в A и B существует единственный способ пропустить эти стрелки через AxB
A
для декартова произведения этот способ строится естественным образом
A
потому что AxB дается сразу с парой стрелок-проекций AxB->A и AxB->B
МБ
Ну, как бы, да. Меня смущает, что там в конце всё сводится к "маслу маслянному". Что если есть пара
Моя настоящая проблема: есть определение классов эквивалентности, весьма специфичное. Там не понятно, почему вдруг конкретная конструкция для
(f(x), g(x)), то есть пара (f(x), g(x)) на языке проекций. Но, может быть, это нормально.Моя настоящая проблема: есть определение классов эквивалентности, весьма специфичное. Там не понятно, почему вдруг конкретная конструкция для
<f, g> должна быть единственной, в том смысле, который указал @odomontois(x :A , P(x), ∀(y: A) P(y) -> x = y)Oℕ
ну механическое доказательство у меня есть, а как ещё очевиднее словами сказать - не знаю
МБ
Ну, потому что речь идёт об ассемблерном коде, задающем функции. Мало ли чего там можно накостылять на этом ассемблере? Но вот что-нибудь, начинающееся на "для любого h" вполне может подойти.
МБ
Ну, в механическом же уже сразу зашито, что вот декартово произведение - оно такое. Но ладно. Это, нормально, наверное.
NI
Да. И ещё. А какие есть подходы к доказательству такой единственности? В тех случаях, когда определение
<f, g> не совсем прямолинейное. Мне приходится сравнивать на классах эквивалентности, у которых определение на полстраницы.Подход один — два произведения одного и того же изоморфны.
Oℕ
Ну естественно, речь здесь может идти только о "множествах" с функциональной экстенсиональностью
Oℕ
Без неё непонятно, как вообще хоть одно категорное свойство для таких категорий доказать