Theorems · Inductive type · algebraic topology

CategoryTheory.SimplicialObject.Splitting

{C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.SimplicialObject C → Type (max u_1 v_1)

A splitting of a simplicial object X consists of the datum of a sequence of objects N, a sequence of morphisms ι : N n ⟶ X _⦋n⦌ such that for all Δ : SimplexCategoryᵒᵖ, the canonical map Splitting.map X ι Δ is an isomorphism.

Defined in

Mathlib.AlgebraicTopology.SimplicialObject.Split

Cited by

59 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category