English
Every morphism f : ⦋1⦌ ⟶ ⦋2⦌ is either one of the three degeneracy maps δ0, δ1, δ2 or a constant map to some a.
Русский
Любой морфизм f: ⦋1⦌ → ⦋2⦌ равен одному из трёх лица δ0, δ1, δ2 или константному отображению на некоторый a.
LaTeX
$$$\\exists i \\in \{0,1,2\\}, \\ f = δ i \\ \\lor \\ \\exists a, \\ f = (\\text{mk } 1).\\const (\\text{mk } 2) a$$$
Lean4
theorem eq_of_one_to_two (f : ⦋1⦌ ⟶ ⦋2⦌) : (∃ i, f = (δ (n := 1) i)) ∨ ∃ a, f = SimplexCategory.const _ _ a :=
by
have : f.toOrderHom 0 ≤ f.toOrderHom 1 := f.toOrderHom.monotone (by decide : (0 : Fin 2) ≤ 1)
match e0 : f.toOrderHom 0, e1 : f.toOrderHom 1 with
| 1, 2 =>
refine .inl ⟨0, ?_⟩
ext i : 3
match i with
| 0 => exact e0
| 1 => exact e1
| 0, 2 =>
refine .inl ⟨1, ?_⟩
ext i : 3
match i with
| 0 => exact e0
| 1 => exact e1
| 0, 1 =>
refine .inl ⟨2, ?_⟩
ext i : 3
match i with
| 0 => exact e0
| 1 => exact e1
| 0, 0 | 1, 1 | 2, 2 =>
refine .inr ⟨f.toOrderHom 0, ?_⟩
ext i : 3
match i with
| 0 => rfl
| 1 => exact e1.trans e0.symm
| 1, 0 | 2, 0 | 2, 1 =>
rw [e0, e1] at this
exact Not.elim (by decide) this
