final_of_exists_of_isFiltered_of_fullyFaithful

English

If D is filtered and F : C → D is full and faithful, then Final F iff a certain explicit condition holds (the Final criterion).

Русский

Если D фильтрован и F : C → D полно и верно, тогда F финальный тогда и только тогда, когда выполняется явное условие Финальной критерий.

LaTeX

$$[IsFiltered D] [F.Full] [F.Faithful] (h : ∀ d, ∃ c, Nonempty (d ⟶ F.obj c)) ⟺ Final F$$

Lean4

/-- In this situation, `C` is also filtered, see
`IsFilteredOrEmpty.of_exists_of_isFiltered_of_fullyFaithful`. -/
theorem final_of_exists_of_isFiltered_of_fullyFaithful [IsFilteredOrEmpty D] [F.Full] [F.Faithful]
    (h : ∀ d, ∃ c, Nonempty (d ⟶ F.obj c)) : Final F :=
  by
  have := IsFilteredOrEmpty.of_exists_of_isFiltered_of_fullyFaithful F h
  refine Functor.final_of_exists_of_isFiltered F h (fun {d c} s s' => ?_)
  obtain ⟨c₀, ⟨f⟩⟩ := h (IsFiltered.coeq s s')
  refine ⟨c₀, F.preimage (IsFiltered.coeqHom s s' ≫ f), ?_⟩
  simp [reassoc_of% (IsFiltered.coeq_condition s s')]

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