Theorems · Definition · algebraic topology

CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (f : CategoryTheory.Arrow C) →
      [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] →
        CategoryTheory.SplitEpi f.hom →
          (n : ℕ) → f.cechNerve.obj (Opposite.op { len := n }) ⟶ f.cechNerve.obj (Opposite.op { len := n + 1 })

The extra degeneracy map on the Čech nerve of a split epi. It is given on the 0-projection by the given section of the split epi, and by shifting the indices on the other projections.

Defined in

Mathlib.AlgebraicTopology.ExtraDegeneracy

Cited by

6 results in Mathlib

Foundations

Depth 34 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasWidePullback