# mathlib3documentation

algebraic_topology.simplicial_object

# Simplicial objects in a category. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_δ_assoc {C : Type u} {n : } {i j : fin (n + 2)} (H : i j) {X' : C} (f' : X.obj X') :
X.δ j.succ X.δ i f' = X.δ X.δ j f'
theorem category_theory.simplicial_object.δ_comp_δ'_assoc {C : Type u} {n : } {i : fin (n + 2)} {j : fin (n + 3)} (H : < j) {X' : C} (f' : X.obj X') :
X.δ j X.δ i f' = X.δ X.δ (j.pred _) f'
theorem category_theory.simplicial_object.δ_comp_δ' {C : Type u} {n : } {i : fin (n + 2)} {j : fin (n + 3)} (H : < j) :
X.δ j X.δ i = X.δ X.δ (j.pred _)
theorem category_theory.simplicial_object.δ_comp_δ''_assoc {C : Type u} {n : } {i : fin (n + 3)} {j : fin (n + 2)} (H : i ) {X' : C} (f' : X.obj X') :
X.δ j.succ X.δ (i.cast_lt _) f' = X.δ i X.δ j f'
theorem category_theory.simplicial_object.δ_comp_δ'' {C : Type u} {n : } {i : fin (n + 3)} {j : fin (n + 2)} (H : i ) :
X.δ j.succ X.δ (i.cast_lt _) = X.δ i X.δ j
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_δ_self_assoc {C : Type u} {n : } {i : fin (n + 2)} {X' : C} (f' : X.obj X') :
X.δ X.δ i f' = X.δ i.succ X.δ i f'
theorem category_theory.simplicial_object.δ_comp_δ_self'_assoc {C : Type u} {n : } {j : fin (n + 3)} {i : fin (n + 2)} (H : j = ) {X' : C} (f' : X.obj X') :
X.δ j X.δ i f' = X.δ i.succ X.δ i f'
theorem category_theory.simplicial_object.δ_comp_δ_self' {C : Type u} {n : } {j : fin (n + 3)} {i : fin (n + 2)} (H : j = ) :
X.δ j X.δ i = X.δ i.succ X.δ i
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_σ_of_le_assoc {C : Type u} {n : } {i : fin (n + 2)} {j : fin (n + 1)} (H : i ) {X' : C} (f' : X.obj (opposite.op (simplex_category.mk (n + 1))) X') :
X.σ j.succ X.δ f' = X.δ i X.σ j f'
theorem category_theory.simplicial_object.δ_comp_σ_self_assoc {C : Type u} {n : } {i : fin (n + 1)} {X' : C} (f' : X.obj X') :
X.σ i X.δ f' = f'
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_σ_self'_assoc {C : Type u} {n : } {j : fin (n + 2)} {i : fin (n + 1)} (H : j = ) {X' : C} (f' : X.obj X') :
X.σ i X.δ j f' = f'
theorem category_theory.simplicial_object.δ_comp_σ_self' {C : Type u} {n : } {j : fin (n + 2)} {i : fin (n + 1)} (H : j = ) :
X.σ i X.δ j = 𝟙 (X.obj
theorem category_theory.simplicial_object.δ_comp_σ_succ_assoc {C : Type u} {n : } {i : fin (n + 1)} {X' : C} (f' : X.obj X') :
X.σ i X.δ i.succ f' = f'
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_σ_succ' {C : Type u} {n : } {j : fin (n + 2)} {i : fin (n + 1)} (H : j = i.succ) :
X.σ i X.δ j = 𝟙 (X.obj
theorem category_theory.simplicial_object.δ_comp_σ_succ'_assoc {C : Type u} {n : } {j : fin (n + 2)} {i : fin (n + 1)} (H : j = i.succ) {X' : C} (f' : X.obj X') :
X.σ i X.δ j f' = f'
theorem category_theory.simplicial_object.δ_comp_σ_of_gt_assoc {C : Type u} {n : } {i : fin (n + 2)} {j : fin (n + 1)} (H : < i) {X' : C} (f' : X.obj (opposite.op (simplex_category.mk (n + 1))) X') :
X.σ X.δ i.succ f' = X.δ i X.σ j f'
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_σ_of_gt'_assoc {C : Type u} {n : } {i : fin (n + 3)} {j : fin (n + 2)} (H : j.succ < i) {X' : C} (f' : X.obj (opposite.op (simplex_category.mk (n + 1))) X') :
X.σ j X.δ i f' = X.δ (i.pred _) X.σ (j.cast_lt _) f'
theorem category_theory.simplicial_object.δ_comp_σ_of_gt' {C : Type u} {n : } {i : fin (n + 3)} {j : fin (n + 2)} (H : j.succ < i) :
X.σ j X.δ i = X.δ (i.pred _) X.σ (j.cast_lt _)
theorem category_theory.simplicial_object.σ_comp_σ_assoc {C : Type u} {n : } {i j : fin (n + 1)} (H : i j) {X' : C} (f' : X.obj (opposite.op (simplex_category.mk (n + 1 + 1))) X') :
X.σ j X.σ f' = X.σ i X.σ j.succ f'
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.δ_naturality_assoc {C : Type u} {X' X : category_theory.simplicial_object C} (f : X X') {n : } (i : fin (n + 2)) {X'_1 : C} (f' : X'.obj X'_1) :
X.δ i f.app f' = f.app (opposite.op (simplex_category.mk (n + 1))) X'.δ i f'
@[simp]
theorem category_theory.simplicial_object.δ_naturality {C : Type u} {X' X : category_theory.simplicial_object C} (f : X X') {n : } (i : fin (n + 2)) :
X.δ i f.app = f.app (opposite.op (simplex_category.mk (n + 1))) X'.δ i
@[simp]
theorem category_theory.simplicial_object.σ_naturality {C : Type u} {X' X : category_theory.simplicial_object C} (f : X X') {n : } (i : fin (n + 1)) :
X.σ i f.app (opposite.op (simplex_category.mk (n + 1))) = f.app X'.σ i
@[simp]
theorem category_theory.simplicial_object.σ_naturality_assoc {C : Type u} {X' X : category_theory.simplicial_object C} (f : X X') {n : } (i : fin (n + 1)) {X'_1 : C} (f' : X'.obj (opposite.op (simplex_category.mk (n + 1))) X'_1) :
X.σ i f.app (opposite.op (simplex_category.mk (n + 1))) f' = f.app X'.σ i f'
@[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]
@[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)

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)

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]

Drop the augmentation.

Equations
@[simp]
@[simp]

The point of the augmentation.

Equations
@[simp]

The functor from augmented objects to arrows.

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

The compatibility of a morphism with the augmentation, on 0-simplices

theorem category_theory.simplicial_object.augmented.w₀_assoc {C : Type u} (f : X Y) {X' : C} (f' : X') :
@[simp]

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]
@[simp]
theorem category_theory.simplicial_object.augmented.whiskering_map_app_left (C : Type u) (D : Type u') (X Y : C D) (η : X Y)  :

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_δ_assoc {C : Type u} {n : } {i j : fin (n + 2)} (H : i j) {X' : C} (f' : X.obj (simplex_category.mk (n + 1 + 1)) X') :
X.δ i X.δ j.succ f' = X.δ j X.δ f'
theorem category_theory.cosimplicial_object.δ_comp_δ' {C : Type u} {n : } {i : fin (n + 2)} {j : fin (n + 3)} (H : < j) :
X.δ i X.δ j = X.δ (j.pred _) X.δ
theorem category_theory.cosimplicial_object.δ_comp_δ'_assoc {C : Type u} {n : } {i : fin (n + 2)} {j : fin (n + 3)} (H : < j) {X' : C} (f' : X.obj (simplex_category.mk (n + 1 + 1)) X') :
X.δ i X.δ j f' = X.δ (j.pred _) X.δ f'
theorem category_theory.cosimplicial_object.δ_comp_δ''_assoc {C : Type u} {n : } {i : fin (n + 3)} {j : fin (n + 2)} (H : i ) {X' : C} (f' : X.obj (simplex_category.mk (n + 1 + 1)) X') :
X.δ (i.cast_lt _) X.δ j.succ f' = X.δ j X.δ i f'
theorem category_theory.cosimplicial_object.δ_comp_δ'' {C : Type u} {n : } {i : fin (n + 3)} {j : fin (n + 2)} (H : i ) :
X.δ (i.cast_lt _) X.δ j.succ = X.δ j X.δ i
theorem category_theory.cosimplicial_object.δ_comp_δ_self_assoc {C : Type u} {n : } {i : fin (n + 2)} {X' : C} (f' : X.obj (simplex_category.mk (n + 1 + 1)) X') :
X.δ i X.δ f' = X.δ i X.δ i.succ f'
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_δ_self'_assoc {C : Type u} {n : } {i : fin (n + 2)} {j : fin (n + 3)} (H : j = ) {X' : C} (f' : X.obj (simplex_category.mk (n + 1 + 1)) X') :
X.δ i X.δ j f' = X.δ i X.δ i.succ f'
theorem category_theory.cosimplicial_object.δ_comp_δ_self' {C : Type u} {n : } {i : fin (n + 2)} {j : fin (n + 3)} (H : j = ) :
X.δ i X.δ j = X.δ i X.δ i.succ
theorem category_theory.cosimplicial_object.δ_comp_σ_of_le_assoc {C : Type u} {n : } {i : fin (n + 2)} {j : fin (n + 1)} (H : i ) {X' : C} (f' : X.obj (simplex_category.mk (n + 1)) X') :
X.δ X.σ j.succ f' = X.σ j X.δ i f'
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_assoc {C : Type u} {n : } {i : fin (n + 1)} {X' : C} (f' : X.obj X') :
X.δ X.σ i f' = f'
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_σ_self' {C : Type u} {n : } {j : fin (n + 2)} {i : fin (n + 1)} (H : j = ) :
X.δ j X.σ i = 𝟙 (X.obj
theorem category_theory.cosimplicial_object.δ_comp_σ_self'_assoc {C : Type u} {n : } {j : fin (n + 2)} {i : fin (n + 1)} (H : j = ) {X' : C} (f' : X.obj X') :
X.δ j X.σ i f' = f'
theorem category_theory.cosimplicial_object.δ_comp_σ_succ_assoc {C : Type u} {n : } {i : fin (n + 1)} {X' : C} (f' : X.obj X') :
X.δ i.succ X.σ i f' = f'
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_σ_succ'_assoc {C : Type u} {n : } {j : fin (n + 2)} {i : fin (n + 1)} (H : j = i.succ) {X' : C} (f' : X.obj X') :
X.δ j X.σ i f' = f'
theorem category_theory.cosimplicial_object.δ_comp_σ_succ' {C : Type u} {n : } {j : fin (n + 2)} {i : fin (n + 1)} (H : j = i.succ) :
X.δ j X.σ i = 𝟙 (X.obj
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_σ_of_gt_assoc {C : Type u} {n : } {i : fin (n + 2)} {j : fin (n + 1)} (H : < i) {X' : C} (f' : X.obj (simplex_category.mk (n + 1)) X') :
X.δ i.succ X.σ f' = X.σ j X.δ i f'
theorem category_theory.cosimplicial_object.δ_comp_σ_of_gt'_assoc {C : Type u} {n : } {i : fin (n + 3)} {j : fin (n + 2)} (H : j.succ < i) {X' : C} (f' : X.obj (simplex_category.mk (n + 1)) X') :
X.δ i X.σ j f' = X.σ (j.cast_lt _) X.δ (i.pred _) f'
theorem category_theory.cosimplicial_object.δ_comp_σ_of_gt' {C : Type u} {n : } {i : fin (n + 3)} {j : fin (n + 2)} (H : j.succ < i) :
X.δ i X.σ j = X.σ (j.cast_lt _) X.δ (i.pred _)
theorem category_theory.cosimplicial_object.σ_comp_σ_assoc {C : Type u} {n : } {i j : fin (n + 1)} (H : i j) {X' : C} (f' : X.obj X') :
X.σ X.σ j f' = X.σ j.succ X.σ i f'
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.δ_naturality_assoc {C : Type u} {X' X : category_theory.cosimplicial_object C} (f : X X') {n : } (i : fin (n + 2)) {X'_1 : C} (f' : X'.obj (simplex_category.mk (n + 1)) X'_1) :
X.δ i f.app (simplex_category.mk (n + 1)) f' = f.app X'.δ i f'
@[simp]
theorem category_theory.cosimplicial_object.δ_naturality {C : Type u} {X' X : category_theory.cosimplicial_object C} (f : X X') {n : } (i : fin (n + 2)) :
X.δ i f.app (simplex_category.mk (n + 1)) = f.app X'.δ i
@[simp]
theorem category_theory.cosimplicial_object.σ_naturality_assoc {C : Type u} {X' X : category_theory.cosimplicial_object C} (f : X X') {n : } (i : fin (n + 1)) {X'_1 : C} (f' : X'.obj X'_1) :
X.σ i f.app f' = f.app (simplex_category.mk (n + 1)) X'.σ i f'
@[simp]
theorem category_theory.cosimplicial_object.σ_naturality {C : Type u} {X' X : category_theory.cosimplicial_object C} (f : X X') {n : } (i : fin (n + 1)) :
X.σ i f.app = f.app (simplex_category.mk (n + 1)) X'.σ i
@[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)

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]

Truncated cosimplicial objects.

Equations
Instances for `category_theory.cosimplicial_object.truncated`
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]

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]

Augmented cosimplicial objects.

Equations
Instances for `category_theory.cosimplicial_object.augmented`

Drop the augmentation.

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

The point of the augmentation.

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

The functor from augmented objects to arrows.

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

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

The anti-equivalence between simplicial objects and cosimplicial objects.

Equations
@[simp]

The anti-equivalence between cosimplicial objects and simplicial objects.

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

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

Equations