English
Let J1, J2 be directed preorders and f: J1 → J2 monotone. Then f is final iff for every j2 ∈ J2 there exists j1 ∈ J1 with j2 ≤ f(j1).
Русский
Пусть J1, J2 — ориентированные предобраза, и f: J1 → J2 монотонен. Тогда f финален тогда и только тогда, когда для каждого j2 ∈ J2 существует j1 ∈ J1 такой, что j2 ≤ f(j1).
LaTeX
$$$[\text{Monotone}(f)] \Rightarrow (hf: f) \text{ is Final } \iff \forall j_2, \exists j_1, j_2 \le f(j_1)$$$
Lean4
theorem final_functor_iff {J₁ J₂ : Type*} [Preorder J₁] [Preorder J₂] [IsDirected J₁ (· ≤ ·)] {f : J₁ → J₂}
(hf : Monotone f) : hf.functor.Final ↔ ∀ (j₂ : J₂), ∃ (j₁ : J₁), j₂ ≤ f j₁ :=
by
rw [Functor.final_iff_of_isFiltered]
constructor
· rintro ⟨h, _⟩ j₂
obtain ⟨j₁, ⟨φ⟩⟩ := h j₂
exact ⟨j₁, leOfHom φ⟩
· intro h
constructor
· intro j₂
obtain ⟨j₁, h₁⟩ := h j₂
exact ⟨j₁, ⟨homOfLE h₁⟩⟩
· intro _ c _ _
exact ⟨c, 𝟙 _, rfl⟩
