sequentialFunctor_initial — Mathlib

English

The sequentialFunctor J is Initial.

Русский

Последовательный функтор J является начальным.

LaTeX

$$$ (\\text{sequentialFunctor } J).\\text{Initial} $$$

Lean4

instance sequentialFunctor_initial : (sequentialFunctor J).Initial where
  out
    d := by
    obtain ⟨n, (g : (sequentialFunctor J).obj ⟨n⟩ ≤ d)⟩ := sequentialFunctor_initial_aux J d
    have : Nonempty (CostructuredArrow (sequentialFunctor J) d) := ⟨CostructuredArrow.mk (homOfLE g)⟩
    apply isConnected_of_zigzag
    refine fun i j ↦ ⟨[j], ?_⟩
    simp only [List.isChain_cons_cons, Zag, List.isChain_singleton, and_true, ne_eq, not_false_eq_true,
      List.getLast_cons, List.getLast_singleton', reduceCtorEq]
    clear! C
    wlog h : (unop i.left) ≤ (unop j.left)
    · exact or_comm.1 (this J d n g inferInstance j i (le_of_lt (not_le.mp h)))
    · right
      exact ⟨CostructuredArrow.homMk (homOfLE h).op rfl⟩

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