final_of_initial_op — Mathlib

English

Let F: C → D be a functor. If the opposite functor F^{op} is initial, then F is final; equivalently, for every object d in D the structured arrow category (d ↓ F) is connected.

Русский

Пусть F: C → D — функтор. Если F^{op} является начальнoй, то F является финальным; эквивалентно, для каждого объекта d в D категория структурированных стрелок (d ↓ F) связна.

LaTeX

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

Lean4

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

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