English
Any morphism with property Pσ can be written as a standardσ L for some admissible L, up to composition with degeneracies.
Русский
Любой морфизм с Pσ может быть записан как стандартное σ L для некоторого допустимого L, по отношению к композиции с операторами упрощения.
LaTeX
$$$\\\\exists L, m, b, h_1, h_2, h: IsAdmissible(m,L) \\\\wedge f = standardσ L \\'⋯\\' $$$
Lean4
theorem simplicialEvalσ_of_isAdmissible (m₁ m₂ : ℕ) (hL : IsAdmissible m₂ L) (hk : m₂ + L.length = m₁) (j : ℕ)
(hj : j < m₁ + 1) : (toSimplexCategory.map <| standardσ L hk).toOrderHom ⟨j, hj⟩ = simplicialEvalσ L j := by
induction L generalizing m₁ m₂ with
| nil =>
obtain rfl : m₁ = m₂ := by grind
simp [simplicialEvalσ]
| cons a L h_rec =>
simp only [List.length_cons] at hk
subst hk
set a₀ := hL.head
have aux (t : Fin (m₂ + 2)) : (a₀.predAbove t : ℕ) = if a < ↑t then (t : ℕ) - 1 else ↑t :=
by
simp only [Fin.predAbove, a₀]
split_ifs with h₁ h₂ h₂
· rfl
· simp only [Fin.lt_def, Fin.coe_castSucc, IsAdmissible.head_val] at h₁; grind
· simp only [Fin.lt_def, Fin.coe_castSucc, IsAdmissible.head_val, not_lt] at h₁; grind
· rfl
have := h_rec _ _ hL.tail (by grind) hj
have ha₀ : Fin.ofNat (m₂ + 1) a = a₀ := by ext; simpa [a₀] using hL.head.prop
simpa only [toSimplexCategory_obj_mk, SimplexCategory.len_mk, standardσ_cons, Functor.map_comp,
toSimplexCategory_map_σ, SimplexCategory.σ, SimplexCategory.mkHom, SimplexCategory.comp_toOrderHom,
SimplexCategory.Hom.toOrderHom_mk, OrderHom.comp_coe, Function.comp_apply, Fin.predAboveOrderHom_coe,
simplicialEvalσ, ha₀, ← this] using aux _
