OP
Borceux, lemma 6.5.6
Lemma 6.5.6
Let A be a small category in which every idempotent splits.
Then each retract of a representable functor A(—, C) is itself representable.
Size: a a a
2018 March 13
2018 March 14
λ
Удивительно, вызов функции это оказывается морфизм.
λ
Слишком всё сходится, слишком всё красиво.
DM
я не понял, что значит вызов функции в контексте?
λ
ну применение функции к некоторому аргументу
DM
я понимаю так, что функция есть сама по себе морфизм
а всунутый в нее аргумент, это уже другой объект
а всунутый в нее аргумент, это уже другой объект
DM
потому что о продолжительности действия речи не заводится и всё "мгновенно"
λ
ну да, можно сказать более общо - referentially transparent
λ
Вот в том то и дело, что мы не можем рассматривать всунутый в неё аргумент как объект, так как это элемент множества. Удивительно!
λ
А в множества нам нельзя заглядывать. Зато каждому вызову, вернее каждой тройке (аргумент, тип функции, результат) мы можем сопоставить морфизм, причём оставаясь в рамках Set.
λ
Всё-таки, что бы не говорили, Set даёт хороший толчок интуиции.
NI
я понимаю так, что функция есть сама по себе морфизм
а всунутый в нее аргумент, это уже другой объект
а всунутый в нее аргумент, это уже другой объект
Всунутый в неё агрумент типа X, это что-то типаа морфизма из терминального объекта.
Т.е., 1→X
Т.е., 1→X
DM
т.е. другой уже морфизм в тот же кодомен
DM
напрашивается вопрос, а есть ли еще одна стрелка, так чтобы все копмозилось?
NI
Всё-таки, что бы не говорили, Set даёт хороший толчок интуиции.
На самом деле, "программистские" категории, не так уж сильно отличаются от Set.
И поэтому, если дальше них не идти, ну хорошо, Set даёт нужную интуицию.
Только дальше уже получается унутря.
Например, всякие категории алгебр.
И поэтому, если дальше них не идти, ну хорошо, Set даёт нужную интуицию.
Только дальше уже получается унутря.
Например, всякие категории алгебр.
NI
1→X можно считать значением типа X.
NI
Другое дело, что в более других категориях (даже таких хороших, как (пре)топосах), терминальный объект может быть очень непохож на множество из одного элемента ;-)
NI
напрашивается вопрос, а есть ли еще одна стрелка, так чтобы все копмозилось?
Что именно "всё"?
Не понимаю. Функция X→Y с аргументом на входе, это композиция 1→X→Y.
Очевидно, что это стрелка 1→Y, т.е., значение типа Y.
Не понимаю. Функция X→Y с аргументом на входе, это композиция 1→X→Y.
Очевидно, что это стрелка 1→Y, т.е., значение типа Y.
DM
Что именно "всё"?
Не понимаю. Функция X→Y с аргументом на входе, это композиция 1→X→Y.
Очевидно, что это стрелка 1→Y, т.е., значение типа Y.
Не понимаю. Функция X→Y с аргументом на входе, это композиция 1→X→Y.
Очевидно, что это стрелка 1→Y, т.е., значение типа Y.
я перепутал Х и У