mathlib documentation

algebraic_topology.simplicial_object

Simplicial objects in a category. #

A simplicial object in a category C is a C-valued presheaf on simplex_category. (Similarly a cosimplicial object is functor simplex_category ⥤ C.)

Use the notation X _[n] in the simplicial locale to obtain the n-th term of a (co)simplicial object X, where n is a natural number.

@[nolint]
def category_theory.simplicial_object (C : Type u) [category_theory.category C] :
Type (max v u)

The category of simplicial objects valued in a category C. This is the category of contravariant functors from simplex_category to C.

Equations

Face maps for a simplicial object.

Equations

Degeneracy maps for a simplicial object.

Equations
theorem category_theory.simplicial_object.δ_comp_δ {C : Type u} [category_theory.category C] (X : category_theory.simplicial_object C) {n : } {i j : fin (n + 2)} (H : i j) :
X.δ j.succ X.δ i = X.δ (fin.cast_succ i) X.δ j

The generic case of the first simplicial identity

The special case of the first simplicial identity

The second simplicial identity

The first part of the third simplicial identity

The second part of the third simplicial identity

theorem category_theory.simplicial_object.δ_comp_σ_of_gt {C : Type u} [category_theory.category C] (X : category_theory.simplicial_object C) {n : } {i : fin (n + 2)} {j : fin (n + 1)} (H : fin.cast_succ j < i) :
X.σ (fin.cast_succ j) X.δ i.succ = X.δ i X.σ j

The fourth simplicial identity

theorem category_theory.simplicial_object.σ_comp_σ {C : Type u} [category_theory.category C] (X : category_theory.simplicial_object C) {n : } {i j : fin (n + 1)} (H : i j) :
X.σ j X.σ (fin.cast_succ i) = X.σ i X.σ j.succ

The fifth simplicial identity

@[nolint]
def category_theory.simplicial_object.truncated (C : Type u) [category_theory.category C] (n : ) :
Type (max v u)

Truncated simplicial objects.

Equations

The constant simplicial object is the constant functor.

@[nolint]
def category_theory.simplicial_object.augmented (C : Type u) [category_theory.category C] :
Type (max (max v u) u v)

The category of augmented simplicial objects, defined as a comma category.

Equations
@[nolint]
def category_theory.cosimplicial_object (C : Type u) [category_theory.category C] :
Type (max v u)

Cosimplicial objects.

Equations

Coface maps for a cosimplicial object.

Equations

Codegeneracy maps for a cosimplicial object.

Equations
theorem category_theory.cosimplicial_object.δ_comp_δ {C : Type u} [category_theory.category C] (X : category_theory.cosimplicial_object C) {n : } {i j : fin (n + 2)} (H : i j) :
X.δ i X.δ j.succ = X.δ j X.δ (fin.cast_succ i)

The generic case of the first cosimplicial identity

The special case of the first cosimplicial identity

The second cosimplicial identity

The first part of the third cosimplicial identity

The second part of the third cosimplicial identity

The fourth cosimplicial identity

theorem category_theory.cosimplicial_object.σ_comp_σ {C : Type u} [category_theory.category C] (X : category_theory.cosimplicial_object C) {n : } {i j : fin (n + 1)} (H : i j) :
X.σ (fin.cast_succ i) X.σ j = X.σ j.succ X.σ i

The fifth cosimplicial identity

@[nolint]
def category_theory.cosimplicial_object.truncated (C : Type u) [category_theory.category C] (n : ) :
Type (max v u)

Truncated cosimplicial objects.

Equations