English
If θ : ⟨n⟩ ⟶ Δ' is not mono, then X.map θ.op ≫ PInfty.f n = 0; in particular, a degeneracy map composed with PInfty annihilates.
Русский
Если θ не моно, то X.map θ.op ≫ PInfty.f n = 0; следовательно, композиция редергирования с PInfty нуль.
LaTeX
$$$$ X.map(\\theta)^{op} \\circ PInfty.f(n) = 0. $$$$
Lean4
@[reassoc]
theorem degeneracy_comp_PInfty (X : SimplicialObject C) (n : ℕ) {Δ' : SimplexCategory} (θ : ⦋n⦌ ⟶ Δ') (hθ : ¬Mono θ) :
X.map θ.op ≫ PInfty.f n = 0 := by
rw [SimplexCategory.mono_iff_injective] at hθ
cases n
· exfalso
apply hθ
intro x y h
fin_cases x
fin_cases y
rfl
· obtain ⟨i, α, h⟩ := SimplexCategory.eq_σ_comp_of_not_injective θ hθ
rw [h, op_comp, X.map_comp, assoc, show X.map (SimplexCategory.σ i).op = X.σ i by rfl, σ_comp_PInfty, comp_zero]