Lean4
/-- The obvious extra degeneracy on the standard simplex. -/
protected noncomputable def extraDegeneracy (Δ : SimplexCategory) :
SimplicialObject.Augmented.ExtraDegeneracy (stdSimplex.obj Δ)
where
s' _ := objMk (OrderHom.const _ 0)
s _ f := objEquiv.symm (shift (objEquiv f))
s'_comp_ε := by
dsimp
subsingleton
s₀_comp_δ₁ := by
dsimp
ext1 x
apply objEquiv.injective
ext j
fin_cases j
rfl
s_comp_δ₀
n := by
ext1 φ
apply objEquiv.injective
apply SimplexCategory.Hom.ext
ext i : 2
dsimp [SimplicialObject.δ, SimplexCategory.δ, SSet.stdSimplex, objEquiv, Equiv.ulift, uliftFunctor]
s_comp_δ n
i := by
ext1 φ
apply objEquiv.injective
apply SimplexCategory.Hom.ext
ext j : 2
dsimp [SimplicialObject.δ, SimplexCategory.δ, SSet.stdSimplex, objEquiv, Equiv.ulift, uliftFunctor]
cases j using Fin.cases <;> simp
s_comp_σ n
i := by
ext1 φ
apply objEquiv.injective
apply SimplexCategory.Hom.ext
ext j : 2
dsimp [SimplicialObject.σ, SimplexCategory.σ, SSet.stdSimplex, objEquiv, Equiv.ulift, uliftFunctor,
Function.comp_def]
cases j using Fin.cases <;> simp
