# Simplicial objects in a category. #

A simplicial object in a category C is a C-valued presheaf on SimplexCategory. (Similarly a cosimplicial object is functor SimplexCategory ⥤ 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.

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

Equations
Instances For
@[simp]
theorem CategoryTheory.instCategorySimplicialObject_comp_app (C : Type u) :
∀ {X Y Z : } (α : X Y) (β : Y Z) (X_1 : ), .app X_1 = CategoryTheory.CategoryStruct.comp (α.app X_1) (β.app X_1)
Equations
• = id inferInstance

Pretty printer defined by notation3 command.

Equations
• One or more equations did not get rendered due to their size.
Instances For

X _[n] denotes the nth-term of the simplicial object X

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• =
Equations
• =
Equations
• =
Equations
• =
theorem CategoryTheory.SimplicialObject.hom_ext {C : Type u} (f : X Y) (g : X Y) (h : ∀ (n : ), f.app n = g.app n) :
f = g
def CategoryTheory.SimplicialObject.δ {C : Type u} {n : } (i : Fin (n + 2)) :
X.obj { unop := SimplexCategory.mk (n + 1) } X.obj { unop := }

Face maps for a simplicial object.

Equations
• X i = X.map .op
Instances For
def CategoryTheory.SimplicialObject.σ {C : Type u} {n : } (i : Fin (n + 1)) :
X.obj { unop := } X.obj { unop := SimplexCategory.mk (n + 1) }

Degeneracy maps for a simplicial object.

Equations
• X i = X.map .op
Instances For
def CategoryTheory.SimplicialObject.eqToIso {C : Type u} {n : } {m : } (h : n = m) :
X.obj { unop := } X.obj { unop := }

Isomorphisms from identities in ℕ.

Equations
• X.eqToIso h =
Instances For
@[simp]
theorem CategoryTheory.SimplicialObject.eqToIso_refl {C : Type u} {n : } (h : n = n) :
X.eqToIso h = CategoryTheory.Iso.refl (X.obj { unop := })
theorem CategoryTheory.SimplicialObject.δ_comp_δ_assoc {C : Type u} {n : } {i : Fin (n + 2)} {j : Fin (n + 2)} (H : i j) {Z : C} (h : X.obj { unop := } Z) :
theorem CategoryTheory.SimplicialObject.δ_comp_δ {C : Type u} {n : } {i : Fin (n + 2)} {j : Fin (n + 2)} (H : i j) :
CategoryTheory.CategoryStruct.comp (X j.succ) (X i) = CategoryTheory.CategoryStruct.comp (X i.castSucc) (X j)

The generic case of the first simplicial identity

theorem CategoryTheory.SimplicialObject.δ_comp_δ'_assoc {C : Type u} {n : } {i : Fin (n + 2)} {j : Fin (n + 3)} (H : i.castSucc < j) {Z : C} (h : X.obj { unop := } Z) :
theorem CategoryTheory.SimplicialObject.δ_comp_δ' {C : Type u} {n : } {i : Fin (n + 2)} {j : Fin (n + 3)} (H : i.castSucc < j) :
CategoryTheory.CategoryStruct.comp (X j) (X i) = CategoryTheory.CategoryStruct.comp (X i.castSucc) (X (j.pred ))
theorem CategoryTheory.SimplicialObject.δ_comp_δ''_assoc {C : Type u} {n : } {i : Fin (n + 3)} {j : Fin (n + 2)} (H : i j.castSucc) {Z : C} (h : X.obj { unop := } Z) :
theorem CategoryTheory.SimplicialObject.δ_comp_δ'' {C : Type u} {n : } {i : Fin (n + 3)} {j : Fin (n + 2)} (H : i j.castSucc) :
CategoryTheory.CategoryStruct.comp (X j.succ) (X (i.castLT )) = CategoryTheory.CategoryStruct.comp (X i) (X j)
theorem CategoryTheory.SimplicialObject.δ_comp_δ_self_assoc {C : Type u} {n : } {i : Fin (n + 2)} {Z : C} (h : X.obj { unop := } Z) :
theorem CategoryTheory.SimplicialObject.δ_comp_δ_self {C : Type u} {n : } {i : Fin (n + 2)} :
CategoryTheory.CategoryStruct.comp (X i.castSucc) (X i) = CategoryTheory.CategoryStruct.comp (X i.succ) (X i)

The special case of the first simplicial identity

theorem CategoryTheory.SimplicialObject.δ_comp_δ_self'_assoc {C : Type u} {n : } {j : Fin (n + 3)} {i : Fin (n + 2)} (H : j = i.castSucc) {Z : C} (h : X.obj { unop := } Z) :
theorem CategoryTheory.SimplicialObject.δ_comp_δ_self' {C : Type u} {n : } {j : Fin (n + 3)} {i : Fin (n + 2)} (H : j = i.castSucc) :
theorem CategoryTheory.SimplicialObject.δ_comp_σ_of_le_assoc {C : Type u} {n : } {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i j.castSucc) {Z : C} (h : X.obj { unop := SimplexCategory.mk (n + 1) } Z) :
theorem CategoryTheory.SimplicialObject.δ_comp_σ_of_le {C : Type u} {n : } {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i j.castSucc) :
CategoryTheory.CategoryStruct.comp (X j.succ) (X i.castSucc) = CategoryTheory.CategoryStruct.comp (X i) (X j)

The second simplicial identity

theorem CategoryTheory.SimplicialObject.δ_comp_σ_self_assoc {C : Type u} {n : } {i : Fin (n + 1)} {Z : C} (h : X.obj { unop := } Z) :
theorem CategoryTheory.SimplicialObject.δ_comp_σ_self {C : Type u} {n : } {i : Fin (n + 1)} :
CategoryTheory.CategoryStruct.comp (X i) (X i.castSucc) = CategoryTheory.CategoryStruct.id (X.obj { unop := })

The first part of the third simplicial identity

theorem CategoryTheory.SimplicialObject.δ_comp_σ_self'_assoc {C : Type u} {n : } {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = i.castSucc) {Z : C} (h : X.obj { unop := } Z) :
theorem CategoryTheory.SimplicialObject.δ_comp_σ_self' {C : Type u} {n : } {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = i.castSucc) :
theorem CategoryTheory.SimplicialObject.δ_comp_σ_succ_assoc {C : Type u} {n : } {i : Fin (n + 1)} {Z : C} (h : X.obj { unop := } Z) :
theorem CategoryTheory.SimplicialObject.δ_comp_σ_succ {C : Type u} {n : } {i : Fin (n + 1)} :
CategoryTheory.CategoryStruct.comp (X i) (X i.succ) = CategoryTheory.CategoryStruct.id (X.obj { unop := })

The second part of the third simplicial identity

theorem CategoryTheory.SimplicialObject.δ_comp_σ_succ'_assoc {C : Type u} {n : } {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = i.succ) {Z : C} (h : X.obj { unop := } Z) :
theorem CategoryTheory.SimplicialObject.δ_comp_σ_succ' {C : Type u} {n : } {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = i.succ) :
theorem CategoryTheory.SimplicialObject.δ_comp_σ_of_gt_assoc {C : Type u} {n : } {i : Fin (n + 2)} {j : Fin (n + 1)} (H : j.castSucc < i) {Z : C} (h : X.obj { unop := SimplexCategory.mk (n + 1) } Z) :
theorem CategoryTheory.SimplicialObject.δ_comp_σ_of_gt {C : Type u} {n : } {i : Fin (n + 2)} {j : Fin (n + 1)} (H : j.castSucc < i) :
CategoryTheory.CategoryStruct.comp (X j.castSucc) (X i.succ) = CategoryTheory.CategoryStruct.comp (X i) (X j)

The fourth simplicial identity

theorem CategoryTheory.SimplicialObject.δ_comp_σ_of_gt'_assoc {C : Type u} {n : } {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ < i) {Z : C} (h : X.obj { unop := SimplexCategory.mk (n + 1) } Z) :
theorem CategoryTheory.SimplicialObject.δ_comp_σ_of_gt' {C : Type u} {n : } {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ < i) :
CategoryTheory.CategoryStruct.comp (X j) (X i) = CategoryTheory.CategoryStruct.comp (X (i.pred )) (X (j.castLT ))
theorem CategoryTheory.SimplicialObject.σ_comp_σ_assoc {C : Type u} {n : } {i : Fin (n + 1)} {j : Fin (n + 1)} (H : i j) {Z : C} (h : X.obj { unop := SimplexCategory.mk (n + 1 + 1) } Z) :
theorem CategoryTheory.SimplicialObject.σ_comp_σ {C : Type u} {n : } {i : Fin (n + 1)} {j : Fin (n + 1)} (H : i j) :
CategoryTheory.CategoryStruct.comp (X j) (X i.castSucc) = CategoryTheory.CategoryStruct.comp (X i) (X j.succ)

The fifth simplicial identity

@[simp]
theorem CategoryTheory.SimplicialObject.δ_naturality_assoc {C : Type u} {X' : } (f : X X') {n : } (i : Fin (n + 2)) {Z : C} (h : X'.obj { unop := } Z) :
@[simp]
theorem CategoryTheory.SimplicialObject.δ_naturality {C : Type u} {X' : } (f : X X') {n : } (i : Fin (n + 2)) :
CategoryTheory.CategoryStruct.comp (X i) (f.app { unop := }) = CategoryTheory.CategoryStruct.comp (f.app { unop := SimplexCategory.mk (n + 1) }) (X' i)
@[simp]
theorem CategoryTheory.SimplicialObject.σ_naturality_assoc {C : Type u} {X' : } (f : X X') {n : } (i : Fin (n + 1)) {Z : C} (h : X'.obj { unop := SimplexCategory.mk (n + 1) } Z) :
@[simp]
theorem CategoryTheory.SimplicialObject.σ_naturality {C : Type u} {X' : } (f : X X') {n : } (i : Fin (n + 1)) :
CategoryTheory.CategoryStruct.comp (X i) (f.app { unop := SimplexCategory.mk (n + 1) }) = CategoryTheory.CategoryStruct.comp (f.app { unop := }) (X' i)
@[simp]
theorem CategoryTheory.SimplicialObject.whiskering_map_app_app (C : Type u) (D : Type u_1) [] :
∀ {X Y : } (τ : X Y) (F : ) (c : ), (( τ).app F).app c = τ.app (F.obj c)
@[simp]
theorem CategoryTheory.SimplicialObject.whiskering_obj_obj_map (C : Type u) (D : Type u_1) [] (H : ) :
∀ {X Y : } (f : X Y), (( H).obj F).map f = H.map (F.map f)
@[simp]
theorem CategoryTheory.SimplicialObject.whiskering_obj_obj_obj (C : Type u) (D : Type u_1) [] (H : ) (X : ) :
(( H).obj F).obj X = H.obj (F.obj X)
@[simp]
theorem CategoryTheory.SimplicialObject.whiskering_obj_map_app (C : Type u) (D : Type u_1) [] (H : ) :
∀ {X Y : } (α : X Y) (X_1 : ), (( H).map α).app X_1 = H.map (α.app X_1)

Functor composition induces a functor on simplicial objects.

Equations
Instances For

Truncated simplicial objects.

Equations
Instances For
Equations
• = id inferInstance
Equations
• =
Equations
• =
Equations
• =
Equations
• =
@[simp]
theorem CategoryTheory.SimplicialObject.Truncated.whiskering_map_app_app (C : Type u) {n : } (D : Type u_1) [] :
∀ {X Y : } (τ : X Y) (F : ) (c : ), (().app F).app c = τ.app (F.obj c)
@[simp]
theorem CategoryTheory.SimplicialObject.Truncated.whiskering_obj_obj_obj (C : Type u) {n : } (D : Type u_1) [] (H : ) (X : ) :
(().obj F).obj X = H.obj (F.obj X)
@[simp]
theorem CategoryTheory.SimplicialObject.Truncated.whiskering_obj_obj_map (C : Type u) {n : } (D : Type u_1) [] (H : ) :
∀ {X Y : } (f : X Y), (().obj F).map f = H.map (F.map f)
@[simp]
theorem CategoryTheory.SimplicialObject.Truncated.whiskering_obj_map_app (C : Type u) {n : } (D : Type u_1) [] (H : ) :
∀ {X Y : } (α : X Y) (X_1 : ), (().map α).app X_1 = H.map (α.app X_1)

Functor composition induces a functor on truncated simplicial objects.

Equations
Instances For

The skeleton functor from simplicial objects to truncated simplicial objects.

Equations
• = SimplexCategory.Truncated.inclusion.op
Instances For
@[reducible, inline]

The constant simplicial object is the constant functor.

Equations
Instances For

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

Equations
Instances For
@[simp]
theorem CategoryTheory.SimplicialObject.instCategoryAugmented_comp_left_app (C : Type u) :
∀ {X Y Z : } (f : X Y) (g : Y Z) (X_1 : ), .left.app X_1 = CategoryTheory.CategoryStruct.comp (f.left.app X_1) (g.left.app X_1)
@[simp]
theorem CategoryTheory.SimplicialObject.instCategoryAugmented_comp_right (C : Type u) :
∀ {X Y Z : } (f : X Y) (g : Y Z), .right = CategoryTheory.CategoryStruct.comp f.right g.right
@[simp]
Equations
• = id inferInstance
theorem CategoryTheory.SimplicialObject.Augmented.hom_ext {C : Type u} (f : X Y) (g : X Y) (h₁ : f.left = g.left) (h₂ : f.right = g.right) :
f = g
@[simp]
theorem CategoryTheory.SimplicialObject.Augmented.drop_map {C : Type u} :
∀ {X Y : } (f : X Y), CategoryTheory.SimplicialObject.Augmented.drop.map f = f.left
@[simp]
theorem CategoryTheory.SimplicialObject.Augmented.drop_obj {C : Type u} :
CategoryTheory.SimplicialObject.Augmented.drop.obj X = X.left

Drop the augmentation.

Equations
• CategoryTheory.SimplicialObject.Augmented.drop =
Instances For
@[simp]
theorem CategoryTheory.SimplicialObject.Augmented.point_map {C : Type u} :
∀ {X Y : } (f : X Y), CategoryTheory.SimplicialObject.Augmented.point.map f = f.right
@[simp]
theorem CategoryTheory.SimplicialObject.Augmented.point_obj {C : Type u} :
CategoryTheory.SimplicialObject.Augmented.point.obj X = X.right

The point of the augmentation.

Equations
• CategoryTheory.SimplicialObject.Augmented.point =
Instances For
@[simp]
theorem CategoryTheory.SimplicialObject.Augmented.toArrow_map_right {C : Type u} :
∀ {X Y : } (η : X Y), (CategoryTheory.SimplicialObject.Augmented.toArrow.map η).right = CategoryTheory.SimplicialObject.Augmented.point.map η
@[simp]
theorem CategoryTheory.SimplicialObject.Augmented.toArrow_obj_right {C : Type u} :
(CategoryTheory.SimplicialObject.Augmented.toArrow.obj X).right = CategoryTheory.SimplicialObject.Augmented.point.obj X
@[simp]
theorem CategoryTheory.SimplicialObject.Augmented.toArrow_obj_hom {C : Type u} :
(CategoryTheory.SimplicialObject.Augmented.toArrow.obj X).hom = X.hom.app { unop := }
@[simp]
theorem CategoryTheory.SimplicialObject.Augmented.toArrow_map_left {C : Type u} :
∀ {X Y : } (η : X Y), (CategoryTheory.SimplicialObject.Augmented.toArrow.map η).left = (CategoryTheory.SimplicialObject.Augmented.drop.map η).app { unop := }
@[simp]
theorem CategoryTheory.SimplicialObject.Augmented.toArrow_obj_left {C : Type u} :
(CategoryTheory.SimplicialObject.Augmented.toArrow.obj X).left = (CategoryTheory.SimplicialObject.Augmented.drop.obj X).obj { unop := }

The functor from augmented objects to arrows.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.SimplicialObject.Augmented.w₀_assoc {C : Type u} (f : X Y) {Z : C} (h : ( Y.right).obj { unop := } Z) :
CategoryTheory.CategoryStruct.comp ((CategoryTheory.SimplicialObject.Augmented.drop.map f).app { unop := }) (CategoryTheory.CategoryStruct.comp (Y.hom.app { unop := }) h) = CategoryTheory.CategoryStruct.comp (X.hom.app { unop := }) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.Augmented.point.map f) h)
theorem CategoryTheory.SimplicialObject.Augmented.w₀ {C : Type u} (f : X Y) :
CategoryTheory.CategoryStruct.comp ((CategoryTheory.SimplicialObject.Augmented.drop.map f).app { unop := }) (Y.hom.app { unop := }) = CategoryTheory.CategoryStruct.comp (X.hom.app { unop := }) (CategoryTheory.SimplicialObject.Augmented.point.map f)

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

Functor composition induces a functor on augmented simplicial objects.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.SimplicialObject.Augmented.whiskering_map_app_left (C : Type u) (D : Type u') [] :
∀ {X Y : } (η : X Y) (A : ), (().app A).left = CategoryTheory.whiskerLeft (CategoryTheory.SimplicialObject.Augmented.drop.obj A) η
@[simp]
theorem CategoryTheory.SimplicialObject.Augmented.whiskering_map_app_right (C : Type u) (D : Type u') [] :
∀ {X Y : } (η : X Y) (A : ), (().app A).right = η.app (CategoryTheory.SimplicialObject.Augmented.point.obj A)
@[simp]

Functor composition induces a functor on augmented simplicial objects.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.SimplicialObject.augment_right {C : Type u} (X₀ : C) (f : X.obj { unop := } X₀) (w : ∀ (i : SimplexCategory) (g₁ g₂ : ), CategoryTheory.CategoryStruct.comp (X.map g₁.op) f = CategoryTheory.CategoryStruct.comp (X.map g₂.op) f) :
(X.augment X₀ f w).right = X₀
@[simp]
theorem CategoryTheory.SimplicialObject.augment_left {C : Type u} (X₀ : C) (f : X.obj { unop := } X₀) (w : ∀ (i : SimplexCategory) (g₁ g₂ : ), CategoryTheory.CategoryStruct.comp (X.map g₁.op) f = CategoryTheory.CategoryStruct.comp (X.map g₂.op) f) :
(X.augment X₀ f w).left = X
@[simp]
theorem CategoryTheory.SimplicialObject.augment_hom_app {C : Type u} (X₀ : C) (f : X.obj { unop := } X₀) (w : ∀ (i : SimplexCategory) (g₁ g₂ : ), CategoryTheory.CategoryStruct.comp (X.map g₁.op) f = CategoryTheory.CategoryStruct.comp (X.map g₂.op) f) (i : ) :
(X.augment X₀ f w).hom.app i = CategoryTheory.CategoryStruct.comp (X.map (.const i.unop 0).op) f
def CategoryTheory.SimplicialObject.augment {C : Type u} (X₀ : C) (f : X.obj { unop := } X₀) (w : ∀ (i : SimplexCategory) (g₁ g₂ : ), CategoryTheory.CategoryStruct.comp (X.map g₁.op) f = CategoryTheory.CategoryStruct.comp (X.map g₂.op) f) :

Augment a simplicial object with an object.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.SimplicialObject.augment_hom_zero {C : Type u} (X₀ : C) (f : X.obj { unop := } X₀) (w : ∀ (i : SimplexCategory) (g₁ g₂ : ), CategoryTheory.CategoryStruct.comp (X.map g₁.op) f = CategoryTheory.CategoryStruct.comp (X.map g₂.op) f) :
(X.augment X₀ f w).hom.app { unop := } = f

Cosimplicial objects.

Equations
Instances For
@[simp]
theorem CategoryTheory.instCategoryCosimplicialObject_comp_app (C : Type u) :
∀ {X Y Z : } (α : X Y) (β : Y Z) (X_1 : SimplexCategory), .app X_1 = CategoryTheory.CategoryStruct.comp (α.app X_1) (β.app X_1)
Equations
• = id inferInstance

X _[n] denotes the nth-term of the cosimplicial object X

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• =
Equations
• =
Equations
• =
Equations
• =
theorem CategoryTheory.CosimplicialObject.hom_ext {C : Type u} (f : X Y) (g : X Y) (h : ∀ (n : SimplexCategory), f.app n = g.app n) :
f = g
def CategoryTheory.CosimplicialObject.δ {C : Type u} {n : } (i : Fin (n + 2)) :
X.obj X.obj (SimplexCategory.mk (n + 1))

Coface maps for a cosimplicial object.

Equations
• X i = X.map
Instances For
def CategoryTheory.CosimplicialObject.σ {C : Type u} {n : } (i : Fin (n + 1)) :
X.obj (SimplexCategory.mk (n + 1)) X.obj

Codegeneracy maps for a cosimplicial object.

Equations
• X i = X.map
Instances For
def CategoryTheory.CosimplicialObject.eqToIso {C : Type u} {n : } {m : } (h : n = m) :
X.obj X.obj

Isomorphisms from identities in ℕ.

Equations
• X.eqToIso h =
Instances For
@[simp]
theorem CategoryTheory.CosimplicialObject.eqToIso_refl {C : Type u} {n : } (h : n = n) :
X.eqToIso h = CategoryTheory.Iso.refl (X.obj )
theorem CategoryTheory.CosimplicialObject.δ_comp_δ_assoc {C : Type u} {n : } {i : Fin (n + 2)} {j : Fin (n + 2)} (H : i j) {Z : C} (h : X.obj (SimplexCategory.mk (n + 1 + 1)) Z) :
theorem CategoryTheory.CosimplicialObject.δ_comp_δ {C : Type u} {n : } {i : Fin (n + 2)} {j : Fin (n + 2)} (H : i j) :
CategoryTheory.CategoryStruct.comp (X i) (X j.succ) = CategoryTheory.CategoryStruct.comp (X j) (X i.castSucc)

The generic case of the first cosimplicial identity

theorem CategoryTheory.CosimplicialObject.δ_comp_δ'_assoc {C : Type u} {n : } {i : Fin (n + 2)} {j : Fin (n + 3)} (H : i.castSucc < j) {Z : C} (h : X.obj (SimplexCategory.mk (n + 1 + 1)) Z) :
theorem CategoryTheory.CosimplicialObject.δ_comp_δ' {C : Type u} {n : } {i : Fin (n + 2)} {j : Fin (n + 3)} (H : i.castSucc < j) :
CategoryTheory.CategoryStruct.comp (X i) (X j) = CategoryTheory.CategoryStruct.comp (X (j.pred )) (X i.castSucc)
theorem CategoryTheory.CosimplicialObject.δ_comp_δ''_assoc {C : Type u} {n : } {i : Fin (n + 3)} {j : Fin (n + 2)} (H : i j.castSucc) {Z : C} (h : X.obj (SimplexCategory.mk (n + 1 + 1)) Z) :
theorem CategoryTheory.CosimplicialObject.δ_comp_δ'' {C : Type u} {n : } {i : Fin (n + 3)} {j : Fin (n + 2)} (H : i j.castSucc) :
CategoryTheory.CategoryStruct.comp (X (i.castLT )) (X j.succ) = CategoryTheory.CategoryStruct.comp (X j) (X i)
theorem CategoryTheory.CosimplicialObject.δ_comp_δ_self {C : Type u} {n : } {i : Fin (n + 2)} :
CategoryTheory.CategoryStruct.comp (X i) (X i.castSucc) = CategoryTheory.CategoryStruct.comp (X i) (X i.succ)

The special case of the first cosimplicial identity

theorem CategoryTheory.CosimplicialObject.δ_comp_δ_self'_assoc {C : Type u} {n : } {i : Fin (n + 2)} {j : Fin (n + 3)} (H : j = i.castSucc) {Z : C} (h : X.obj (SimplexCategory.mk (n + 1 + 1)) Z) :
theorem CategoryTheory.CosimplicialObject.δ_comp_δ_self' {C : Type u} {n : } {i : Fin (n + 2)} {j : Fin (n + 3)} (H : j = i.castSucc) :
theorem CategoryTheory.CosimplicialObject.δ_comp_σ_of_le_assoc {C : Type u} {n : } {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i j.castSucc) {Z : C} (h : X.obj (SimplexCategory.mk (n + 1)) Z) :
theorem CategoryTheory.CosimplicialObject.δ_comp_σ_of_le {C : Type u} {n : } {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i j.castSucc) :
CategoryTheory.CategoryStruct.comp (X i.castSucc) (X j.succ) = CategoryTheory.CategoryStruct.comp (X j) (X i)

The second cosimplicial identity

theorem CategoryTheory.CosimplicialObject.δ_comp_σ_self_assoc {C : Type u} {n : } {i : Fin (n + 1)} {Z : C} (h : X.obj Z) :
CategoryTheory.CategoryStruct.comp (X i.castSucc) () = h
theorem CategoryTheory.CosimplicialObject.δ_comp_σ_self {C : Type u} {n : } {i : Fin (n + 1)} :
CategoryTheory.CategoryStruct.comp (X i.castSucc) (X i) =

The first part of the third cosimplicial identity

theorem CategoryTheory.CosimplicialObject.δ_comp_σ_self'_assoc {C : Type u} {n : } {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = i.castSucc) {Z : C} (h : X.obj Z) :
theorem CategoryTheory.CosimplicialObject.δ_comp_σ_self' {C : Type u} {n : } {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = i.castSucc) :
theorem CategoryTheory.CosimplicialObject.δ_comp_σ_succ_assoc {C : Type u} {n : } {i : Fin (n + 1)} {Z : C} (h : X.obj Z) :
theorem CategoryTheory.CosimplicialObject.δ_comp_σ_succ {C : Type u} {n : } {i : Fin (n + 1)} :
CategoryTheory.CategoryStruct.comp (X i.succ) (X i) =

The second part of the third cosimplicial identity

theorem CategoryTheory.CosimplicialObject.δ_comp_σ_succ'_assoc {C : Type u} {n : } {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = i.succ) {Z : C} (h : X.obj Z) :
theorem CategoryTheory.CosimplicialObject.δ_comp_σ_succ' {C : Type u} {n : } {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = i.succ) :
theorem CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt_assoc {C : Type u} {n : } {i : Fin (n + 2)} {j : Fin (n + 1)} (H : j.castSucc < i) {Z : C} (h : X.obj (SimplexCategory.mk (n + 1)) Z) :
theorem CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt {C : Type u} {n : } {i : Fin (n + 2)} {j : Fin (n + 1)} (H : j.castSucc < i) :
CategoryTheory.CategoryStruct.comp (X i.succ) (X j.castSucc) = CategoryTheory.CategoryStruct.comp (X j) (X i)

The fourth cosimplicial identity

theorem CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt'_assoc {C : Type u} {n : } {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ < i) {Z : C} (h : X.obj (SimplexCategory.mk (n + 1)) Z) :
theorem CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt' {C : Type u} {n : } {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ < i) :
CategoryTheory.CategoryStruct.comp (X i) (X j) = CategoryTheory.CategoryStruct.comp (X (j.castLT )) (X (i.pred ))
theorem CategoryTheory.CosimplicialObject.σ_comp_σ_assoc {C : Type u} {n : } {i : Fin (n + 1)} {j : Fin (n + 1)} (H : i j) {Z : C} (h : X.obj Z) :
theorem CategoryTheory.CosimplicialObject.σ_comp_σ {C : Type u} {n : } {i : Fin (n + 1)} {j : Fin (n + 1)} (H : i j) :
CategoryTheory.CategoryStruct.comp (X i.castSucc) (X j) = CategoryTheory.CategoryStruct.comp (X j.succ) (X i)

The fifth cosimplicial identity

@[simp]
theorem CategoryTheory.CosimplicialObject.δ_naturality {C : Type u} (f : X X') {n : } (i : Fin (n + 2)) :
@[simp]
theorem CategoryTheory.CosimplicialObject.σ_naturality {C : Type u} (f : X X') {n : } (i : Fin (n + 1)) :
@[simp]
theorem CategoryTheory.CosimplicialObject.whiskering_obj_obj_map (C : Type u) (D : Type u_1) [] (H : ) :
∀ {X Y : SimplexCategory} (f : X Y), (( H).obj F).map f = H.map (F.map f)
@[simp]
theorem CategoryTheory.CosimplicialObject.whiskering_obj_map_app (C : Type u) (D : Type u_1) [] (H : ) :
∀ {X Y : } (α : X Y) (X_1 : SimplexCategory), (( H).map α).app X_1 = H.map (α.app X_1)
@[simp]
theorem CategoryTheory.CosimplicialObject.whiskering_map_app_app (C : Type u) (D : Type u_1) [] :
∀ {X Y : } (τ : X Y) (F : ) (c : SimplexCategory), (( τ).app F).app c = τ.app (F.obj c)
@[simp]
theorem CategoryTheory.CosimplicialObject.whiskering_obj_obj_obj (C : Type u) (D : Type u_1) [] (H : ) (X : SimplexCategory) :
(( H).obj F).obj X = H.obj (F.obj X)

Functor composition induces a functor on cosimplicial objects.

Equations
Instances For

Truncated cosimplicial objects.

Equations
Instances For
Equations
• = id inferInstance
Equations
• =
Equations
• =
Equations
• =
Equations
• =
@[simp]
theorem CategoryTheory.CosimplicialObject.Truncated.whiskering_obj_map_app (C : Type u) {n : } (D : Type u_1) [] (H : ) :
∀ {X Y : } (α : X Y) (X_1 : ), (().map α).app X_1 = H.map (α.app X_1)
@[simp]
theorem CategoryTheory.CosimplicialObject.Truncated.whiskering_map_app_app (C : Type u) {n : } (D : Type u_1) [] :
∀ {X Y : } (τ : X Y) (F : ) (c : ), (().app F).app c = τ.app (F.obj c)
@[simp]
theorem CategoryTheory.CosimplicialObject.Truncated.whiskering_obj_obj_obj (C : Type u) {n : } (D : Type u_1) [] (H : ) (F : ) (X : ) :
(().obj F).obj X = H.obj (F.obj X)
@[simp]
theorem CategoryTheory.CosimplicialObject.Truncated.whiskering_obj_obj_map (C : Type u) {n : } (D : Type u_1) [] (H : ) (F : ) :
∀ {X Y : } (f : X Y), (().obj F).map f = H.map (F.map f)

Functor composition induces a functor on truncated cosimplicial objects.

Equations
Instances For

The skeleton functor from cosimplicial objects to truncated cosimplicial objects.

Equations
• = SimplexCategory.Truncated.inclusion
Instances For
@[reducible, inline]

The constant cosimplicial object.

Equations
Instances For

Augmented cosimplicial objects.

Equations
Instances For
@[simp]
theorem CategoryTheory.CosimplicialObject.instCategoryAugmented_comp_right_app (C : Type u) :
∀ {X Y Z : } (f : X Y) (g : Y Z) (X_1 : SimplexCategory), .right.app X_1 = CategoryTheory.CategoryStruct.comp (f.right.app X_1) (g.right.app X_1)
@[simp]
@[simp]
theorem CategoryTheory.CosimplicialObject.instCategoryAugmented_comp_left (C : Type u) :
∀ {X Y Z : } (f : X Y) (g : Y Z), .left = CategoryTheory.CategoryStruct.comp f.left g.left
Equations
• = id inferInstance
theorem CategoryTheory.CosimplicialObject.Augmented.hom_ext {C : Type u} (f : X Y) (g : X Y) (h₁ : f.left = g.left) (h₂ : f.right = g.right) :
f = g
@[simp]
theorem CategoryTheory.CosimplicialObject.Augmented.drop_map {C : Type u} :
∀ {X Y : } (f : X Y), CategoryTheory.CosimplicialObject.Augmented.drop.map f = f.right
@[simp]
theorem CategoryTheory.CosimplicialObject.Augmented.drop_obj {C : Type u} :
CategoryTheory.CosimplicialObject.Augmented.drop.obj X = X.right

Drop the augmentation.

Equations
• CategoryTheory.CosimplicialObject.Augmented.drop =
Instances For
@[simp]
theorem CategoryTheory.CosimplicialObject.Augmented.point_obj {C : Type u} :
CategoryTheory.CosimplicialObject.Augmented.point.obj X = X.left
@[simp]
theorem CategoryTheory.CosimplicialObject.Augmented.point_map {C : Type u} :
∀ {X Y : } (f : X Y), CategoryTheory.CosimplicialObject.Augmented.point.map f = f.left

The point of the augmentation.

Equations
• CategoryTheory.CosimplicialObject.Augmented.point =
Instances For
@[simp]
theorem CategoryTheory.CosimplicialObject.Augmented.toArrow_obj_hom {C : Type u} :
(CategoryTheory.CosimplicialObject.Augmented.toArrow.obj X).hom = X.hom.app
@[simp]
theorem CategoryTheory.CosimplicialObject.Augmented.toArrow_obj_left {C : Type u} :
(CategoryTheory.CosimplicialObject.Augmented.toArrow.obj X).left = X.left
@[simp]
theorem CategoryTheory.CosimplicialObject.Augmented.toArrow_map_right {C : Type u} :
∀ {X Y : } (η : X Y), (CategoryTheory.CosimplicialObject.Augmented.toArrow.map η).right = η.right.app
@[simp]
theorem CategoryTheory.CosimplicialObject.Augmented.toArrow_map_left {C : Type u} :
∀ {X Y : } (η : X Y), (CategoryTheory.CosimplicialObject.Augmented.toArrow.map η).left = η.left
@[simp]
theorem CategoryTheory.CosimplicialObject.Augmented.toArrow_obj_right {C : Type u} :
(CategoryTheory.CosimplicialObject.Augmented.toArrow.obj X).right = X.right.obj

The functor from augmented objects to arrows.

Equations
• One or more equations did not get rendered due to their size.
Instances For

Functor composition induces a functor on augmented cosimplicial objects.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.CosimplicialObject.Augmented.whiskering_map_app_right (C : Type u) (D : Type u') [] :
∀ {X Y : } (η : X Y) (A : ), (().app A).right = CategoryTheory.whiskerLeft (CategoryTheory.CosimplicialObject.Augmented.drop.obj A) η
@[simp]
theorem CategoryTheory.CosimplicialObject.Augmented.whiskering_map_app_left (C : Type u) (D : Type u') [] :
∀ {X Y : } (η : X Y) (A : ), (().app A).left = η.app (CategoryTheory.CosimplicialObject.Augmented.point.obj A)

Functor composition induces a functor on augmented cosimplicial objects.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.CosimplicialObject.augment_right {C : Type u} (X₀ : C) (f : X₀ X.obj ) (w : ∀ (i : SimplexCategory) (g₁ g₂ : ), CategoryTheory.CategoryStruct.comp f (X.map g₁) = CategoryTheory.CategoryStruct.comp f (X.map g₂)) :
(X.augment X₀ f w).right = X
@[simp]
theorem CategoryTheory.CosimplicialObject.augment_hom_app {C : Type u} (X₀ : C) (f : X₀ X.obj ) (w : ∀ (i : SimplexCategory) (g₁ g₂ : ), CategoryTheory.CategoryStruct.comp f (X.map g₁) = CategoryTheory.CategoryStruct.comp f (X.map g₂)) (i : SimplexCategory) :
(X.augment X₀ f w).hom.app i = CategoryTheory.CategoryStruct.comp f (X.map (.const i 0))
@[simp]
theorem CategoryTheory.CosimplicialObject.augment_left {C : Type u} (X₀ : C) (f : X₀ X.obj ) (w : ∀ (i : SimplexCategory) (g₁ g₂ : ), CategoryTheory.CategoryStruct.comp f (X.map g₁) = CategoryTheory.CategoryStruct.comp f (X.map g₂)) :
(X.augment X₀ f w).left = X₀
def CategoryTheory.CosimplicialObject.augment {C : Type u} (X₀ : C) (f : X₀ X.obj ) (w : ∀ (i : SimplexCategory) (g₁ g₂ : ), CategoryTheory.CategoryStruct.comp f (X.map g₁) = CategoryTheory.CategoryStruct.comp f (X.map g₂)) :

Augment a cosimplicial object with an object.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.CosimplicialObject.augment_hom_zero {C : Type u} (X₀ : C) (f : X₀ X.obj ) (w : ∀ (i : SimplexCategory) (g₁ g₂ : ), CategoryTheory.CategoryStruct.comp f (X.map g₁) = CategoryTheory.CategoryStruct.comp f (X.map g₂)) :
(X.augment X₀ f w).hom.app = f
@[simp]
theorem CategoryTheory.simplicialCosimplicialEquiv_functor_map_app (C : Type u) :
∀ {X Y : } (η : X Y) (X_1 : SimplexCategory), (.functor.map η).app X_1 = (η.unop.app { unop := X_1 }).op
@[simp]
theorem CategoryTheory.simplicialCosimplicialEquiv_unitIso_inv_app (C : Type u) :
.unitIso.inv.app X = X.unop.rightOpLeftOpIso.inv.op
@[simp]
theorem CategoryTheory.simplicialCosimplicialEquiv_inverse_map (C : Type u) :
∀ {X Y : } (η : X Y), .inverse.map η =
@[simp]
theorem CategoryTheory.simplicialCosimplicialEquiv_inverse_obj (C : Type u) :
.inverse.obj F = { unop := F.leftOp }
@[simp]
theorem CategoryTheory.simplicialCosimplicialEquiv_unitIso_hom_app (C : Type u) :
.unitIso.hom.app X = X.unop.rightOpLeftOpIso.hom.op
@[simp]
theorem CategoryTheory.simplicialCosimplicialEquiv_functor_obj_obj (C : Type u) (X : SimplexCategory) :
(.functor.obj F).obj X = { unop := F.unop.obj { unop := X } }
@[simp]
theorem CategoryTheory.simplicialCosimplicialEquiv_functor_obj_map (C : Type u) :
∀ {X Y : SimplexCategory} (f : X Y), (.functor.obj F).map f = (F.unop.map f.op).op

The anti-equivalence between simplicial objects and cosimplicial objects.

Equations
Instances For
@[simp]
theorem CategoryTheory.cosimplicialSimplicialEquiv_counitIso_hom_app_app (C : Type u) (X : ) :
(.counitIso.hom.app X✝).app X = CategoryTheory.CategoryStruct.id (X✝.obj X)
@[simp]
theorem CategoryTheory.cosimplicialSimplicialEquiv_functor_obj_obj (C : Type u) (F : ) (X : ) :
(.functor.obj F).obj X = { unop := F.unop.obj X.unop }
@[simp]
theorem CategoryTheory.cosimplicialSimplicialEquiv_inverse_obj (C : Type u) :
.inverse.obj F = { unop := F.unop }
@[simp]
theorem CategoryTheory.cosimplicialSimplicialEquiv_unitIso_hom_app (C : Type u) (X : ) :
.unitIso.hom.app X = X.unop.opUnopIso.hom.op
@[simp]
theorem CategoryTheory.cosimplicialSimplicialEquiv_functor_obj_map (C : Type u) (F : ) :
∀ {X Y : } (f : X Y), (.functor.obj F).map f = (F.unop.map f.unop).op
@[simp]
theorem CategoryTheory.cosimplicialSimplicialEquiv_inverse_map (C : Type u) :
∀ {X Y : } (α : X Y), .inverse.map α = Quiver.Hom.op { app := fun (X_1 : SimplexCategory) => (α.app { unop := X_1 }).unop, naturality := }
@[simp]
theorem CategoryTheory.cosimplicialSimplicialEquiv_counitIso_inv_app_app (C : Type u) (X : ) :
(.counitIso.inv.app X✝).app X = CategoryTheory.CategoryStruct.id (X✝.obj X)
@[simp]
theorem CategoryTheory.cosimplicialSimplicialEquiv_unitIso_inv_app (C : Type u) (X : ) :
.unitIso.inv.app X = X.unop.opUnopIso.inv.op
@[simp]
theorem CategoryTheory.cosimplicialSimplicialEquiv_functor_map_app (C : Type u) :
∀ {X Y : } (α : X Y) (X_1 : ), (.functor.map α).app X_1 = (α.unop.app X_1.unop).op

The anti-equivalence between cosimplicial objects and simplicial objects.

Equations
Instances For
@[simp]
theorem CategoryTheory.SimplicialObject.Augmented.rightOp_hom_app {C : Type u} (X : SimplexCategory) :
X✝.rightOp.hom.app X = (X✝.hom.app { unop := X }).op
@[simp]
theorem CategoryTheory.SimplicialObject.Augmented.rightOp_right_obj {C : Type u} (X : SimplexCategory) :
X✝.rightOp.right.obj X = { unop := X✝.left.obj { unop := X } }
@[simp]
theorem CategoryTheory.SimplicialObject.Augmented.rightOp_left {C : Type u} :
X.rightOp.left = { unop := X.right }
@[simp]
theorem CategoryTheory.SimplicialObject.Augmented.rightOp_right_map {C : Type u} :
∀ {X_1 Y : SimplexCategory} (f : X_1 Y), X.rightOp.right.map f = (X.left.map f.op).op

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

Equations
• X.rightOp = { left := { unop := X.right }, right := , hom := }
Instances For
@[simp]
theorem CategoryTheory.CosimplicialObject.Augmented.leftOp_hom_app {C : Type u} (X : ) :
X✝.leftOp.hom.app X = (X✝.hom.app X.unop).unop
@[simp]
theorem CategoryTheory.CosimplicialObject.Augmented.leftOp_right {C : Type u} :
X.leftOp.right = X.left.unop
@[simp]
theorem CategoryTheory.CosimplicialObject.Augmented.leftOp_left_obj {C : Type u} (X : ) :
X✝.leftOp.left.obj X = (X✝.right.obj X.unop).unop
@[simp]
theorem CategoryTheory.CosimplicialObject.Augmented.leftOp_left_map {C : Type u} :
∀ {X_1 Y : } (f : X_1 Y), X.leftOp.left.map f = (X.right.map f.unop).unop

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

Equations
• X.leftOp = { left := , right := X.left.unop, hom := }
Instances For
@[simp]
theorem CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso_inv_right {C : Type u} :
X.rightOpLeftOpIso.inv.right =
@[simp]
theorem CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso_hom_left_app {C : Type u} (X : ) :
X✝.rightOpLeftOpIso.hom.left.app X = CategoryTheory.CategoryStruct.id (X✝.left.obj X)
@[simp]
theorem CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso_inv_left_app {C : Type u} (X : ) :
X✝.rightOpLeftOpIso.inv.left.app X = CategoryTheory.CategoryStruct.id (X✝.left.obj X)
@[simp]
theorem CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso_hom_right {C : Type u} :
X.rightOpLeftOpIso.hom.right =

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

Equations
• X.rightOpLeftOpIso =
Instances For
@[simp]
theorem CategoryTheory.CosimplicialObject.Augmented.leftOpRightOpIso_inv_right_app {C : Type u} (X : SimplexCategory) :
X✝.leftOpRightOpIso.inv.right.app X = CategoryTheory.CategoryStruct.id (X✝.right.obj X)
@[simp]
@[simp]
@[simp]
theorem CategoryTheory.CosimplicialObject.Augmented.leftOpRightOpIso_hom_right_app {C : Type u} (X : SimplexCategory) :
X✝.leftOpRightOpIso.hom.right.app X = CategoryTheory.CategoryStruct.id (X✝.right.obj X)

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

Equations
• X.leftOpRightOpIso =
Instances For
@[simp]
@[simp]
theorem CategoryTheory.simplicialToCosimplicialAugmented_map_right (C : Type u) :
∀ {X Y : } (f : X Y), ().right = CategoryTheory.NatTrans.rightOp f.unop.left
@[simp]
theorem CategoryTheory.simplicialToCosimplicialAugmented_map_left (C : Type u) :
∀ {X Y : } (f : X Y), ().left = f.unop.right.op

A functorial version of SimplicialObject.Augmented.rightOp.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.cosimplicialToSimplicialAugmented_obj (C : Type u) :
= { unop := X.leftOp }
@[simp]
theorem CategoryTheory.cosimplicialToSimplicialAugmented_map (C : Type u) :
∀ {X Y : } (f : X Y), = Quiver.Hom.op { left := , right := f.left.unop, w := }

A functorial version of Cosimplicial_object.Augmented.leftOp.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]

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

Equations
• One or more equations did not get rendered due to their size.
Instances For