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.

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

@[reducible]

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
Instances for category_theory.simplicial_object.augmented
@[simp]
theorem category_theory.simplicial_object.augment_left {C : Type u} [category_theory.category C] (X : category_theory.simplicial_object C) (X₀ : C) (f : X.obj (opposite.op (simplex_category.mk 0)) X₀) (w : ∀ (i : simplex_category) (g₁ g₂ : simplex_category.mk 0 i), X.map g₁.op f = X.map g₂.op f) :
(X.augment X₀ f w).left = X

Augment a simplicial object with an object.

Equations
@[simp]
theorem category_theory.simplicial_object.augment_right {C : Type u} [category_theory.category C] (X : category_theory.simplicial_object C) (X₀ : C) (f : X.obj (opposite.op (simplex_category.mk 0)) X₀) (w : ∀ (i : simplex_category) (g₁ g₂ : simplex_category.mk 0 i), X.map g₁.op f = X.map g₂.op f) :
(X.augment X₀ f w).right = X₀
@[simp]
theorem category_theory.simplicial_object.augment_hom_app {C : Type u} [category_theory.category C] (X : category_theory.simplicial_object C) (X₀ : C) (f : X.obj (opposite.op (simplex_category.mk 0)) X₀) (w : ∀ (i : simplex_category) (g₁ g₂ : simplex_category.mk 0 i), X.map g₁.op f = X.map g₂.op f) (i : simplex_categoryᵒᵖ) :
(X.augment X₀ f w).hom.app i = X.map ((opposite.unop i).const 0).op f
@[simp]
theorem category_theory.simplicial_object.augment_hom_zero {C : Type u} [category_theory.category C] (X : category_theory.simplicial_object C) (X₀ : C) (f : X.obj (opposite.op (simplex_category.mk 0)) X₀) (w : ∀ (i : simplex_category) (g₁ g₂ : simplex_category.mk 0 i), X.map g₁.op f = X.map g₂.op f) :

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

@[reducible]

The constant cosimplicial object.

Augment a cosimplicial object with an object.

Equations
@[simp]
theorem category_theory.cosimplicial_object.augment_hom_app {C : Type u} [category_theory.category C] (X : category_theory.cosimplicial_object C) (X₀ : C) (f : X₀ X.obj (simplex_category.mk 0)) (w : ∀ (i : simplex_category) (g₁ g₂ : simplex_category.mk 0 i), f X.map g₁ = f X.map g₂) (i : simplex_category) :
(X.augment X₀ f w).hom.app i = f X.map (i.const 0)
@[simp]
theorem category_theory.cosimplicial_object.augment_right {C : Type u} [category_theory.category C] (X : category_theory.cosimplicial_object C) (X₀ : C) (f : X₀ X.obj (simplex_category.mk 0)) (w : ∀ (i : simplex_category) (g₁ g₂ : simplex_category.mk 0 i), f X.map g₁ = f X.map g₂) :
(X.augment X₀ f w).right = X
@[simp]
theorem category_theory.cosimplicial_object.augment_left {C : Type u} [category_theory.category C] (X : category_theory.cosimplicial_object C) (X₀ : C) (f : X₀ X.obj (simplex_category.mk 0)) (w : ∀ (i : simplex_category) (g₁ g₂ : simplex_category.mk 0 i), f X.map g₁ = f X.map g₂) :
(X.augment X₀ f w).left = X₀
@[simp]
theorem category_theory.cosimplicial_object.augment_hom_zero {C : Type u} [category_theory.category C] (X : category_theory.cosimplicial_object C) (X₀ : C) (f : X₀ X.obj (simplex_category.mk 0)) (w : ∀ (i : simplex_category) (g₁ g₂ : simplex_category.mk 0 i), f X.map g₁ = f X.map g₂) :
(X.augment X₀ f w).hom.app (simplex_category.mk 0) = f

Converting an augmented simplicial object to an augmented cosimplicial object and back is isomorphic to the given object.

Equations

Converting an augmented cosimplicial object to an augmented simplicial object and back is isomorphic to the given object.

Equations