# 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
Instances for category_theory.simplicial_object
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, 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

@[simp]
theorem category_theory.simplicial_object.whiskering_obj_obj_map (C : Type u) (D : Type u_1) (H : C D) (F : simplex_categoryᵒᵖ C) (_x _x_1 : simplex_categoryᵒᵖ) (f : _x _x_1) :
.obj F).map f = H.map (F.map f)
@[simp]
theorem category_theory.simplicial_object.whiskering_map_app_app (C : Type u) (D : Type u_1) (G H : C D) (τ : G H) (F : simplex_categoryᵒᵖ C) (c : simplex_categoryᵒᵖ) :
.app F).app c = τ.app (F.obj c)
@[simp]
theorem category_theory.simplicial_object.whiskering_obj_obj_obj (C : Type u) (D : Type u_1) (H : C D) (F : simplex_categoryᵒᵖ C) (X : simplex_categoryᵒᵖ) :
.obj F).obj X = H.obj (F.obj X)
@[simp]
theorem category_theory.simplicial_object.whiskering_obj_map_app (C : Type u) (D : Type u_1) (H : C D) (_x _x_1 : simplex_categoryᵒᵖ C) (α : _x _x_1) (X : simplex_categoryᵒᵖ) :
.map α).app X = H.map (α.app X)
def category_theory.simplicial_object.whiskering (C : Type u) (D : Type u_1)  :

Functor composition induces a functor on simplicial objects.

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

Truncated simplicial objects.

Equations
Instances for category_theory.simplicial_object.truncated
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[simp]
theorem category_theory.simplicial_object.truncated.whiskering_obj_obj_obj (C : Type u) {n : } (D : Type u_1) (H : C D) (F : C) (X : ᵒᵖ) :
F).obj X = H.obj (F.obj X)
def category_theory.simplicial_object.truncated.whiskering (C : Type u) {n : } (D : Type u_1)  :

Functor composition induces a functor on truncated simplicial objects.

Equations
@[simp]
theorem category_theory.simplicial_object.truncated.whiskering_obj_map_app (C : Type u) {n : } (D : Type u_1) (H : C D) (_x _x_1 : C) (α : _x _x_1) (X : ᵒᵖ) :
α).app X = H.map (α.app X)
@[simp]
theorem category_theory.simplicial_object.truncated.whiskering_map_app_app (C : Type u) {n : } (D : Type u_1) (G H : C D) (τ : G H) (F : C) (c : ᵒᵖ) :
F).app c = τ.app (F.obj c)
@[simp]
theorem category_theory.simplicial_object.truncated.whiskering_obj_obj_map (C : Type u) {n : } (D : Type u_1) (H : C D) (F : C) (_x _x_1 : ᵒᵖ) (f : _x _x_1) :
F).map f = H.map (F.map f)

The skeleton functor from simplicial objects to truncated simplicial objects.

Equations
@[reducible]

The constant simplicial object is the constant functor.

@[protected, 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
Instances for category_theory.simplicial_object.augmented
@[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]

The functor from augmented objects to arrows.

Equations
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
def category_theory.simplicial_object.augmented.whiskering_obj (C : Type u) (D : Type u_1) (F : C D) :

Functor composition induces a functor on augmented simplicial objects.

Equations
@[simp]
theorem category_theory.simplicial_object.augmented.whiskering_map_app_right (C : Type u) (D : Type u') (X Y : C D) (η : X Y)  :
@[simp]
theorem category_theory.simplicial_object.augmented.whiskering_obj_2 (C : Type u) (D : Type u') (F : C D) :
@[simp]
theorem category_theory.simplicial_object.augmented.whiskering_map_app_left (C : Type u) (D : Type u') (X Y : C D) (η : X Y)  :
def category_theory.simplicial_object.augmented.whiskering (C : Type u) (D : Type u')  :

Functor composition induces a functor on augmented simplicial objects.

Equations
@[simp]
theorem category_theory.simplicial_object.augment_left {C : Type u} (X₀ : C) (f : X.obj X₀) (w : ∀ (i : simplex_category) (g₁ g₂ : , X.map g₁.op f = X.map g₂.op f) :
(X.augment X₀ f w).left = X
def category_theory.simplicial_object.augment {C : Type u} (X₀ : C) (f : X.obj X₀) (w : ∀ (i : simplex_category) (g₁ g₂ : , X.map g₁.op f = X.map g₂.op f) :

Augment a simplicial object with an object.

Equations
@[simp]
theorem category_theory.simplicial_object.augment_right {C : Type u} (X₀ : C) (f : X.obj X₀) (w : ∀ (i : simplex_category) (g₁ g₂ : , 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} (X₀ : C) (f : X.obj X₀) (w : ∀ (i : simplex_category) (g₁ g₂ : , 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} (X₀ : C) (f : X.obj X₀) (w : ∀ (i : simplex_category) (g₁ g₂ : , X.map g₁.op f = X.map g₂.op f) :
(X.augment X₀ f w).hom.app = f
@[protected, instance]
@[nolint]
def category_theory.cosimplicial_object (C : Type u)  :
Type (max v u)

Cosimplicial objects.

Equations
Instances for category_theory.cosimplicial_object
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, 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

@[simp]
theorem category_theory.cosimplicial_object.whiskering_obj_obj_obj (C : Type u) (D : Type u_1) (H : C D) (F : simplex_category C) (X : simplex_category) :
.obj F).obj X = H.obj (F.obj X)
@[simp]
theorem category_theory.cosimplicial_object.whiskering_obj_map_app (C : Type u) (D : Type u_1) (H : C D) (_x _x_1 : simplex_category C) (α : _x _x_1) (X : simplex_category) :
.map α).app X = H.map (α.app X)
@[simp]
theorem category_theory.cosimplicial_object.whiskering_map_app_app (C : Type u) (D : Type u_1) (G H : C D) (τ : G H) (F : simplex_category C) (c : simplex_category) :
.app F).app c = τ.app (F.obj c)
def category_theory.cosimplicial_object.whiskering (C : Type u) (D : Type u_1)  :

Functor composition induces a functor on cosimplicial objects.

Equations
@[simp]
theorem category_theory.cosimplicial_object.whiskering_obj_obj_map (C : Type u) (D : Type u_1) (H : C D) (F : simplex_category C) (_x _x_1 : simplex_category) (f : _x _x_1) :
.obj F).map f = H.map (F.map f)
@[protected, instance]
@[nolint]
def category_theory.cosimplicial_object.truncated (C : Type u) (n : ) :
Type (max v u)

Truncated cosimplicial objects.

Equations
Instances for category_theory.cosimplicial_object.truncated
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def category_theory.cosimplicial_object.truncated.whiskering (C : Type u) {n : } (D : Type u_1)  :

Functor composition induces a functor on truncated cosimplicial objects.

Equations
@[simp]
theorem category_theory.cosimplicial_object.truncated.whiskering_obj_map_app (C : Type u) {n : } (D : Type u_1) (H : C D) (_x _x_1 : C) (α : _x _x_1)  :
.app X = H.map (α.app X)
@[simp]
theorem category_theory.cosimplicial_object.truncated.whiskering_map_app_app (C : Type u) {n : } (D : Type u_1) (G H : C D) (τ : G H) (F : C)  :
.app c = τ.app (F.obj c)
@[simp]
theorem category_theory.cosimplicial_object.truncated.whiskering_obj_obj_map (C : Type u) {n : } (D : Type u_1) (H : C D) (F : C) (_x _x_1 : simplex_category.truncated n) (f : _x _x_1) :
.map f = H.map (F.map f)
@[simp]
theorem category_theory.cosimplicial_object.truncated.whiskering_obj_obj_obj (C : Type u) {n : } (D : Type u_1) (H : C D) (F : C)  :
.obj X = H.obj (F.obj X)

The skeleton functor from cosimplicial objects to truncated cosimplicial objects.

Equations
@[reducible]

The constant cosimplicial object.

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

Augmented cosimplicial objects.

Equations
Instances for category_theory.cosimplicial_object.augmented

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) :
@[simp]
@[simp]
@[simp]

The functor from augmented objects to arrows.

Equations
@[simp]
@[simp]
@[simp]
def category_theory.cosimplicial_object.augmented.whiskering_obj (C : Type u) (D : Type u_1) (F : C D) :

Functor composition induces a functor on augmented cosimplicial objects.

Equations

Functor composition induces a functor on augmented cosimplicial objects.

Equations
@[simp]
theorem category_theory.cosimplicial_object.augmented.whiskering_map_app_left (C : Type u) (D : Type u') (X Y : C D) (η : X Y)  :
@[simp]
theorem category_theory.cosimplicial_object.augmented.whiskering_obj_2 (C : Type u) (D : Type u') (F : C D) :
@[simp]
theorem category_theory.cosimplicial_object.augmented.whiskering_map_app_right (C : Type u) (D : Type u') (X Y : C D) (η : X Y)  :
def category_theory.cosimplicial_object.augment {C : Type u} (X₀ : C) (f : X₀ X.obj ) (w : ∀ (i : simplex_category) (g₁ g₂ : , f X.map g₁ = f X.map g₂) :

Augment a cosimplicial object with an object.

Equations
@[simp]
theorem category_theory.cosimplicial_object.augment_hom_app {C : Type u} (X₀ : C) (f : X₀ X.obj ) (w : ∀ (i : simplex_category) (g₁ g₂ : , 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} (X₀ : C) (f : X₀ X.obj ) (w : ∀ (i : simplex_category) (g₁ g₂ : , 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} (X₀ : C) (f : X₀ X.obj ) (w : ∀ (i : simplex_category) (g₁ g₂ : , 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} (X₀ : C) (f : X₀ X.obj ) (w : ∀ (i : simplex_category) (g₁ g₂ : , f X.map g₁ = f X.map g₂) :
(X.augment X₀ f w).hom.app = f

The anti-equivalence between simplicial objects and cosimplicial objects.

Equations
@[simp]

The anti-equivalence between cosimplicial objects and simplicial objects.

Equations
@[simp]

Construct an augmented cosimplicial object in the opposite category from an augmented simplicial object.

Equations
@[simp]

Construct an augmented simplicial object from an augmented cosimplicial object in the opposite category.

Equations
@[simp]
@[simp]
@[simp]
@[simp]

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

Equations
@[simp]
@[simp]

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

Equations

A functorial version of simplicial_object.augmented.right_op.

Equations
@[simp]
@[simp]
@[simp]

A functorial version of cosimplicial_object.augmented.left_op.

Equations
@[simp]
@[simp]
@[simp]

The contravariant categorical equivalence between augmented simplicial objects and augmented cosimplicial objects in the opposite category.

Equations
@[simp]