final_iff_isFiltered_structuredArrow

English

If F : C → D is Final with D is IsCofilteredOrEmpty, then F.Initial holds whenever for every d there exists c with a morphism F.obj c ⟶ d.

Русский

Если F : C → D финален, а D является IsCofilteredOrEmpty, то F.Initial выполняется, если для каждого d существует c с морфизм F(c) → d.

LaTeX

$$Initial F ⇔ (∀ d, ∃ c, Nonempty (F.obj c ⟶ d)) ∧ (∀ {d} {c} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s')$$

Lean4

/-- If `C` is filtered, then `F : C ⥤ D` is final if and only if `StructuredArrow d F` is filtered
for all `d : D`. -/
theorem final_iff_isFiltered_structuredArrow [IsFilteredOrEmpty C] : Final F ↔ ∀ d, IsFiltered (StructuredArrow d F) :=
  by
  refine ⟨?_, fun h => final_of_isFiltered_structuredArrow F⟩
  rw [final_iff_of_isFiltered]
  exact fun h => isFiltered_structuredArrow_of_isFiltered_of_exists F h.1 h.2

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