initial_of_final_op

Mathlib.CategoryTheory.Limits.Final

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.initial_of_final_op

← MathLib Explorer

English

Let F: C → D be a functor. If Final F^{op}, then Initial F.

Русский

Пусть F: C → D — функтор. Если Final(F^{op}), тогда Initial(F).

LaTeX

$$$$ \operatorname{Final}(F^{op}) \Rightarrow \operatorname{Initial}(F). $$$$

Lean4

theorem initial_of_final_op (F : C ⥤ D) [Final F.op] : Initial F :=
  {
    out := fun d =>
      @isConnected_of_isConnected_op _ _ (isConnected_of_equivalent (costructuredArrowOpEquivalence F d).symm) }

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru