degeneracy_comp_PInfty — Mathlib

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]

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