final_of_isFiltered_of_pUnit — Mathlib

English

If C is filtered, then every functor F: C ⥤ Discrete PUnit is final.

Русский

Если C фильтрована, то любой функтор F: C ⥤ Discrete PUnit является финальным.

LaTeX

$$$[IsFiltered(C)] \Rightarrow \forall F : C \to \mathrm{Discrete}(PUnit), \ \mathrm{Final}(F)$$$

Lean4

/-- If `C` is filtered, then every functor `F : C ⥤ Discrete PUnit` is final. -/
theorem final_of_isFiltered_of_pUnit [IsFiltered C] (F : C ⥤ Discrete PUnit) : Final F :=
  by
  refine final_of_exists_of_isFiltered F (fun _ => ?_) (fun {_} {c} _ _ => ?_)
  · use Classical.choice IsFiltered.nonempty
    exact ⟨Discrete.eqToHom (by simp)⟩
  · use c; use 𝟙 c
    apply Subsingleton.elim

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