English
For the simplex category, the top morphism property is determined by δ and σ morphisms via Boolean algebra completion.
Русский
Для простой симплексной категории верхнее свойство морфизмов задаётся δ и σ через завершающую булеву алгебру.
LaTeX
$$$\\\\text{morphismProperty}_{top} = \\text{top}$ in SimplexCategory$$
Lean4
theorem morphismProperty_eq_top (W : MorphismProperty SimplexCategory) [W.IsMultiplicative]
(δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (SimplexCategory.δ i))
(σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (SimplexCategory.σ i)) : W = ⊤ :=
by
have hW (d : ℕ) : W.inverseImage (Truncated.inclusion d) = ⊤ :=
Truncated.morphismProperty_eq_top _ (fun _ _ i ↦ δ_mem i) (fun _ _ i ↦ σ_mem i)
ext a b f
simp only [MorphismProperty.top_apply, iff_true]
change W.inverseImage (Truncated.inclusion _) (f : ⟨a, Nat.le_max_left _ _⟩ ⟶ ⟨b, Nat.le_max_right _ _⟩)
simp only [hW, MorphismProperty.top_apply]
