English
For a final functor F : C → D and arrows s,s' : d → F.obj c, there exist c' and t : c ⟶ c' with s ≫ F.map t = s' ≫ F.map t.
Русский
Для финального функторa F : C → D и стрел s,s' : d → F(c) существует c' и t : c ⟶ c' такое, что s ∘ F(t) = s' ∘ F(t).
LaTeX
$$Exists (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t$$
Lean4
/-- If `C` is filtered, then we can give an explicit condition for a functor `F : C ⥤ D` to
be final. -/
theorem final_iff_of_isFiltered [IsFilteredOrEmpty C] :
Final F ↔
(∀ d, ∃ c, Nonempty (d ⟶ F.obj c)) ∧
(∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t) :=
by
refine ⟨fun hF => ⟨?_, ?_⟩, fun h => final_of_exists_of_isFiltered F h.1 h.2⟩
· intro d
obtain ⟨f⟩ : Nonempty (StructuredArrow d F) := IsConnected.is_nonempty
exact ⟨_, ⟨f.hom⟩⟩
· let s₁ : C ≌ AsSmall.{max u₁ v₁ u₂ v₂} C := AsSmall.equiv
let s₂ : D ≌ AsSmall.{max u₁ v₁ u₂ v₂} D := AsSmall.equiv
have : IsFilteredOrEmpty (AsSmall.{max u₁ v₁ u₂ v₂} C) := .of_equivalence s₁
intro d c s s'
obtain ⟨c', t, ht⟩ :=
Functor.Final.exists_coeq_of_locally_small (s₁.inverse ⋙ F ⋙ s₂.functor) (AsSmall.up.map s) (AsSmall.up.map s')
exact ⟨AsSmall.down.obj c', AsSmall.down.map t, s₂.functor.map_injective (by simp_all [s₁, s₂])⟩
