Strongly cartesian morphism
Пусть у нас есть функтор $F : C \to I$. Мы можем построить его цилиндр $\mathrm{Cyl}(F)$.

Это когда мы добавляем в $C \sqcup I$ для каждого $c \in C$ по формальной стрелке $F_c : c \to F(c)$ так, чтобы для каждой стрелки $f : c' \to c$ из $C$ квадрат из стрелок $f$, $F(f)$, $F_c$ и $F_{c'}$ был коммутативен. То есть реализуем функтор в виде естественного преобразования, так сказать.

Точнее, $\mathrm{Cyl}(F)$ --- это категория, множество объектов которой --- это дизъюнктное объединение множеств объектов $C$ и $I$, стрелки между объектами из $C$ такие же, как в $C$, то же и для $I$, а стрелки из $x \in C \subset \mathrm{Cyl}(F)$ в $y \in I \subset \mathrm{Cyl}(F)$ биективны стрелкам $F(x) \to y$ в $I$ (морально это формальные композиции $x \to F(x) \to y$, где первая стрелка --- это $F_x$). Композиция определяется очевидным образом, учитывая, что мы хотим коммутативность наших квадратов. Ассоциативность проверяется легко, всё имеет смысл.


Так вот, пусть у нас есть функтор $F : C \to I$ и морфизм $f : c' \to c$ из $C$. Морфизм $f$ называется strongly cartesian morphism, если (коммутативный) квадрат из $f$, $F(f)$, $F_c$ и $F_{c'}$ является пуллбэком в $\mathrm{Cyl}(F)$.

(Правильно?)

Tags: math