Theorems · Definition · algebraic topology

AlgebraicTopology.DoldKan.HigherFacesVanish

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Preadditive C] →
      {X : CategoryTheory.SimplicialObject C} →
        {Y : C} → {n : ℕ} → ℕ → (Y ⟶ X.obj (Opposite.op { len := n + 1 })) → Prop

A morphism φ : Y ⟶ X _⦋n+1⦌ satisfies HigherFacesVanish q φ when the compositions φ ≫ X.δ j are 0 for j ≥ max 1 (n+2-q). When q ≤ n+1, it basically means that the composition φ ≫ X.δ j are 0 for the q highest possible values of a nonzero j. Otherwise, when q ≥ n+2, all the compositions φ ≫ X.δ j for nonzero j vanish. See also the lemma comp_P_eq_self_iff in Projections.lean which states that HigherFacesVanish q φ is equivalent to the identity φ ≫ (P q).f (n+1) = φ.

Defined in

Mathlib.AlgebraicTopology.DoldKan.Faces

Cited by

15 results in Mathlib

Foundations

Depth 33 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Preadditive