# mathlibdocumentation

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)  :
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
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
def category_theory.simplicial_object.δ {C : Type u} {n : } (i : fin (n + 2)) :

Face maps for a simplicial object.

Equations
def category_theory.simplicial_object.σ {C : Type u} {n : } (i : fin (n + 1)) :

Degeneracy maps for a simplicial object.

Equations
def category_theory.simplicial_object.eq_to_iso {C : Type u} {n m : } (h : n = m) :
X.obj X.obj

Isomorphisms from identities in ℕ.

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

The generic case of the first simplicial identity

theorem category_theory.simplicial_object.δ_comp_δ_self {C : Type u} {n : } {i : fin (n + 2)} :
X.δ X.δ i = X.δ i.succ X.δ i

The special case of the first simplicial identity

theorem category_theory.simplicial_object.δ_comp_σ_of_le {C : Type u} {n : } {i : fin (n + 2)} {j : fin (n + 1)} (H : i ) :
X.σ j.succ X.δ = X.δ i X.σ j

The second simplicial identity

theorem category_theory.simplicial_object.δ_comp_σ_self {C : Type u} {n : } {i : fin (n + 1)} :
X.σ i X.δ = 𝟙 (X.obj

The first part of the third simplicial identity

theorem category_theory.simplicial_object.δ_comp_σ_succ {C : Type u} {n : } {i : fin (n + 1)} :
X.σ i X.δ i.succ = 𝟙 (X.obj

The second part of the third simplicial identity

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

The fourth simplicial identity

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

The fifth simplicial identity

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

Truncated simplicial objects.

Equations
@[instance]
@[instance]
@[instance]
@[instance]

The skeleton functor from simplicial objects to truncated simplicial objects.

Equations

The constant simplicial object is the constant functor.

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

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

Equations
@[simp]
theorem category_theory.simplicial_object.augmented.drop_map {C : Type u} (f : _x _x_1) :

Drop the augmentation.

Equations
@[simp]
@[simp]
theorem category_theory.simplicial_object.augmented.point_map {C : Type u} (f : _x _x_1) :

The point of the augmentation.

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

Cosimplicial objects.

Equations
@[instance]
@[instance]
@[instance]
@[instance]
def category_theory.cosimplicial_object.δ {C : Type u} {n : } (i : fin (n + 2)) :

Coface maps for a cosimplicial object.

Equations
def category_theory.cosimplicial_object.σ {C : Type u} {n : } (i : fin (n + 1)) :

Codegeneracy maps for a cosimplicial object.

Equations
def category_theory.cosimplicial_object.eq_to_iso {C : Type u} {n m : } (h : n = m) :
X.obj X.obj

Isomorphisms from identities in ℕ.

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

The generic case of the first cosimplicial identity

theorem category_theory.cosimplicial_object.δ_comp_δ_self {C : Type u} {n : } {i : fin (n + 2)} :
X.δ i X.δ = X.δ i X.δ i.succ

The special case of the first cosimplicial identity

theorem category_theory.cosimplicial_object.δ_comp_σ_of_le {C : Type u} {n : } {i : fin (n + 2)} {j : fin (n + 1)} (H : i ) :
X.δ X.σ j.succ = X.σ j X.δ i

The second cosimplicial identity

theorem category_theory.cosimplicial_object.δ_comp_σ_self {C : Type u} {n : } {i : fin (n + 1)} :
X.δ X.σ i = 𝟙 (X.obj

The first part of the third cosimplicial identity

theorem category_theory.cosimplicial_object.δ_comp_σ_succ {C : Type u} {n : } {i : fin (n + 1)} :
X.δ i.succ X.σ i = 𝟙 (X.obj

The second part of the third cosimplicial identity

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

The fourth cosimplicial identity

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

The fifth cosimplicial identity

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

Truncated cosimplicial objects.

Equations
@[instance]
@[instance]
@[instance]
@[instance]

The skeleton functor from cosimplicial objects to truncated cosimplicial objects.

Equations

The constant cosimplicial object.

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

Augmented cosimplicial objects.

Equations

Drop the augmentation.

Equations
@[simp]
theorem category_theory.cosimplicial_object.augmented.drop_map {C : Type u} (f : _x _x_1) :
@[simp]
@[simp]

The point of the augmentation.

Equations
@[simp]
theorem category_theory.cosimplicial_object.augmented.point_map {C : Type u} (f : _x _x_1) :