eq_comp_δ_of_not_surjective' — Mathlib

English

If θ: Δ ⟶ ⟦n+1⟧ is not surjective, then there exists i and θ' with θ = θ' ∘ δ_i.

Русский

Если θ: Δ ⟶ ⟦n+1⟧ не сюръективен, то существует i и θ' такие что θ = θ' ∘ δ_i.

LaTeX

$$$\\\\forall {n} {Δ} \\\\big( θ: Δ \\\\to \\\\langle n+1 \\\\rangle \\\\big), \\\\ Not(Surjective(OrderHom.instFunLike.coe (SimplexCategory.Hom.toOrderHom θ))) \\\\Rightarrow \\\\Exists θ': Δ \\\\to \\\\langle n \\\\rangle, \\\\ θ = θ' \\\\circ δ_i$$$

Lean4

theorem eq_comp_δ_of_not_surjective' {n : ℕ} {Δ : SimplexCategory} (θ : Δ ⟶ ⦋n + 1⦌) (i : Fin (n + 2))
    (hi : ∀ x, θ.toOrderHom x ≠ i) : ∃ θ' : Δ ⟶ ⦋n⦌, θ = θ' ≫ δ i :=
  by
  use θ ≫ σ (.predAbove (.last n) i)
  ext x : 3
  suffices ∀ j ≠ i, i.succAbove (((Fin.last n).predAbove i).predAbove j) = j
    by
    dsimp [δ, σ]
    exact .symm <| this _ (hi _)
  intro j hj
  cases i using Fin.lastCases <;> simp [hj]

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