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.

def CategoryTheory.SimplicialObject (C : Type u) [CategoryTheory.Category.{v, u} C] : Type (max v u)

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

Equations

• CategoryTheory.SimplicialObject C = CategoryTheory.Functor SimplexCategoryᵒᵖ C

@[simp]

theorem CategoryTheory.instCategorySimplicialObject_comp_app (C : Type u) [CategoryTheory.Category.{v, u} C] : ∀ {X Y Z : CategoryTheory.Functor SimplexCategoryᵒᵖ C} (α : X ⟶ Y) (β : Y ⟶ Z) (X_1 : SimplexCategoryᵒᵖ), (CategoryTheory.CategoryStruct.comp α β).app X_1 = CategoryTheory.CategoryStruct.comp (α.app X_1) (β.app X_1)

@[simp]

theorem CategoryTheory.instCategorySimplicialObject_id_app (C : Type u) [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor SimplexCategoryᵒᵖ C) (X : SimplexCategoryᵒᵖ) : (CategoryTheory.CategoryStruct.id F).app X = CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X)

instance CategoryTheory.instCategorySimplicialObject (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Category.{v, max u v} (CategoryTheory.SimplicialObject C)

Equations

• CategoryTheory.instCategorySimplicialObject C = id inferInstance

def Simplicial.«term__[_]» : Lean.TrailingParserDescr

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

Equations

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

def Simplicial.«term__[_]».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

instance CategoryTheory.SimplicialObject.instHasLimitsOfShapeSimplicialObjectInstCategorySimplicialObject (C : Type u) [CategoryTheory.Category.{v, u} C] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.SimplicialObject C)

Equations

• (_ : CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.SimplicialObject C)) = (_ : CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.SimplicialObject C))

instance CategoryTheory.SimplicialObject.instHasLimitsSimplicialObjectInstCategorySimplicialObject (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] : CategoryTheory.Limits.HasLimits (CategoryTheory.SimplicialObject C)

Equations

• (_ : CategoryTheory.Limits.HasLimits (CategoryTheory.SimplicialObject C)) = (_ : CategoryTheory.Limits.HasLimitsOfSize.{v, v, v, max u v} (CategoryTheory.SimplicialObject C))

instance CategoryTheory.SimplicialObject.instHasColimitsOfShapeSimplicialObjectInstCategorySimplicialObject (C : Type u) [CategoryTheory.Category.{v, u} C] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.Limits.HasColimitsOfShape J C] : CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.SimplicialObject C)

Equations

• (_ : CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.SimplicialObject C)) = (_ : CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.SimplicialObject C))

instance CategoryTheory.SimplicialObject.instHasColimitsSimplicialObjectInstCategorySimplicialObject (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] : CategoryTheory.Limits.HasColimits (CategoryTheory.SimplicialObject C)

Equations

• (_ : CategoryTheory.Limits.HasColimits (CategoryTheory.SimplicialObject C)) = (_ : CategoryTheory.Limits.HasColimitsOfSize.{v, v, v, max u v} (CategoryTheory.SimplicialObject C))

theorem CategoryTheory.SimplicialObject.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] {X : CategoryTheory.SimplicialObject C} {Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) (g : X ⟶ Y) (h : ∀ (n : SimplexCategoryᵒᵖ), f.app n = g.app n) : f = g

def CategoryTheory.SimplicialObject.δ {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} (i : Fin (n + 2)) : X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk (n + 1))) ⟶ X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n))

Face maps for a simplicial object.

Equations

• CategoryTheory.SimplicialObject.δ X i = X.toPrefunctor.map (SimplexCategory.δ i).op

def CategoryTheory.SimplicialObject.σ {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} (i : Fin (n + 1)) : X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n)) ⟶ X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk (n + 1)))

Degeneracy maps for a simplicial object.

Equations

• CategoryTheory.SimplicialObject.σ X i = X.toPrefunctor.map (SimplexCategory.σ i).op

def CategoryTheory.SimplicialObject.eqToIso {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {m : ℕ} (h : n = m) : X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n)) ≅ X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk m))

Isomorphisms from identities in ℕ.

Equations

• CategoryTheory.SimplicialObject.eqToIso X h = X.mapIso (CategoryTheory.eqToIso (_ : Opposite.op (SimplexCategory.mk n) = Opposite.op (SimplexCategory.mk m)))

@[simp]

theorem CategoryTheory.SimplicialObject.eqToIso_refl {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} (h : n = n) : CategoryTheory.SimplicialObject.eqToIso X h = CategoryTheory.Iso.refl (X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n)))

theorem CategoryTheory.SimplicialObject.δ_comp_δ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 2)} (H : i ≤ j) {Z : C} (h : X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X (Fin.succ j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X i) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X (Fin.castSucc i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X j) h)

theorem CategoryTheory.SimplicialObject.δ_comp_δ {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 2)} (H : i ≤ j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X (Fin.succ j)) (CategoryTheory.SimplicialObject.δ X i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X (Fin.castSucc i)) (CategoryTheory.SimplicialObject.δ X j)

The generic case of the first simplicial identity

theorem CategoryTheory.SimplicialObject.δ_comp_δ'_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : Fin.castSucc i < j) {Z : C} (h : X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X i) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X (Fin.castSucc i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X (Fin.pred j (_ : j = 0 → False))) h)

theorem CategoryTheory.SimplicialObject.δ_comp_δ' {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : Fin.castSucc i < j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X j) (CategoryTheory.SimplicialObject.δ X i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X (Fin.castSucc i)) (CategoryTheory.SimplicialObject.δ X (Fin.pred j (_ : j = 0 → False)))

theorem CategoryTheory.SimplicialObject.δ_comp_δ''_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : i ≤ Fin.castSucc j) {Z : C} (h : X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X (Fin.succ j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X (Fin.castLT i (_ : ↑i < n + 2))) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X j) h)

theorem CategoryTheory.SimplicialObject.δ_comp_δ'' {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : i ≤ Fin.castSucc j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X (Fin.succ j)) (CategoryTheory.SimplicialObject.δ X (Fin.castLT i (_ : ↑i < n + 2))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X i) (CategoryTheory.SimplicialObject.δ X j)

theorem CategoryTheory.SimplicialObject.δ_comp_δ_self_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {i : Fin (n + 2)} {Z : C} (h : X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X (Fin.castSucc i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X i) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X (Fin.succ i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X i) h)

theorem CategoryTheory.SimplicialObject.δ_comp_δ_self {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {i : Fin (n + 2)} : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X (Fin.castSucc i)) (CategoryTheory.SimplicialObject.δ X i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X (Fin.succ i)) (CategoryTheory.SimplicialObject.δ X i)

The special case of the first simplicial identity

theorem CategoryTheory.SimplicialObject.δ_comp_δ_self'_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {j : Fin (n + 3)} {i : Fin (n + 2)} (H : j = Fin.castSucc i) {Z : C} (h : X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X i) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X (Fin.succ i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X i) h)

theorem CategoryTheory.SimplicialObject.δ_comp_δ_self' {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {j : Fin (n + 3)} {i : Fin (n + 2)} (H : j = Fin.castSucc i) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X j) (CategoryTheory.SimplicialObject.δ X i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X (Fin.succ i)) (CategoryTheory.SimplicialObject.δ X i)

theorem CategoryTheory.SimplicialObject.δ_comp_σ_of_le_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i ≤ Fin.castSucc j) {Z : C} (h : X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk (n + 1))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X (Fin.succ j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X (Fin.castSucc i)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X j) h)

theorem CategoryTheory.SimplicialObject.δ_comp_σ_of_le {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i ≤ Fin.castSucc j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X (Fin.succ j)) (CategoryTheory.SimplicialObject.δ X (Fin.castSucc i)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X i) (CategoryTheory.SimplicialObject.σ X j)

The second simplicial identity

theorem CategoryTheory.SimplicialObject.δ_comp_σ_self_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {i : Fin (n + 1)} {Z : C} (h : X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X (Fin.castSucc i)) h) = h

theorem CategoryTheory.SimplicialObject.δ_comp_σ_self {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {i : Fin (n + 1)} : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X i) (CategoryTheory.SimplicialObject.δ X (Fin.castSucc i)) = CategoryTheory.CategoryStruct.id (X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n)))

The first part of the third simplicial identity

theorem CategoryTheory.SimplicialObject.δ_comp_σ_self'_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = Fin.castSucc i) {Z : C} (h : X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X j) h) = h

theorem CategoryTheory.SimplicialObject.δ_comp_σ_self' {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = Fin.castSucc i) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X i) (CategoryTheory.SimplicialObject.δ X j) = CategoryTheory.CategoryStruct.id (X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n)))

theorem CategoryTheory.SimplicialObject.δ_comp_σ_succ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {i : Fin (n + 1)} {Z : C} (h : X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X (Fin.succ i)) h) = h

theorem CategoryTheory.SimplicialObject.δ_comp_σ_succ {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {i : Fin (n + 1)} : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X i) (CategoryTheory.SimplicialObject.δ X (Fin.succ i)) = CategoryTheory.CategoryStruct.id (X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n)))

The second part of the third simplicial identity

theorem CategoryTheory.SimplicialObject.δ_comp_σ_succ'_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = Fin.succ i) {Z : C} (h : X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X j) h) = h

theorem CategoryTheory.SimplicialObject.δ_comp_σ_succ' {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = Fin.succ i) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X i) (CategoryTheory.SimplicialObject.δ X j) = CategoryTheory.CategoryStruct.id (X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n)))

theorem CategoryTheory.SimplicialObject.δ_comp_σ_of_gt_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : Fin.castSucc j < i) {Z : C} (h : X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk (n + 1))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X (Fin.castSucc j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X (Fin.succ i)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X j) h)

theorem CategoryTheory.SimplicialObject.δ_comp_σ_of_gt {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : Fin.castSucc j < i) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X (Fin.castSucc j)) (CategoryTheory.SimplicialObject.δ X (Fin.succ i)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X i) (CategoryTheory.SimplicialObject.σ X j)

The fourth simplicial identity

theorem CategoryTheory.SimplicialObject.δ_comp_σ_of_gt'_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : Fin.succ j < i) {Z : C} (h : X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk (n + 1))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X i) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X (Fin.pred i (_ : i = 0 → False))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X (Fin.castLT j (_ : ↑j < n + 1))) h)

theorem CategoryTheory.SimplicialObject.δ_comp_σ_of_gt' {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : Fin.succ j < i) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X j) (CategoryTheory.SimplicialObject.δ X i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X (Fin.pred i (_ : i = 0 → False))) (CategoryTheory.SimplicialObject.σ X (Fin.castLT j (_ : ↑j < n + 1)))

theorem CategoryTheory.SimplicialObject.σ_comp_σ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {i : Fin (n + 1)} {j : Fin (n + 1)} (H : i ≤ j) {Z : C} (h : X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk (n + 1 + 1))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X (Fin.castSucc i)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X (Fin.succ j)) h)

theorem CategoryTheory.SimplicialObject.σ_comp_σ {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {i : Fin (n + 1)} {j : Fin (n + 1)} (H : i ≤ j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X j) (CategoryTheory.SimplicialObject.σ X (Fin.castSucc i)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X i) (CategoryTheory.SimplicialObject.σ X (Fin.succ j))

The fifth simplicial identity

@[simp]

theorem CategoryTheory.SimplicialObject.δ_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X' : CategoryTheory.SimplicialObject C} {X : CategoryTheory.SimplicialObject C} (f : X ⟶ X') {n : ℕ} (i : Fin (n + 2)) {Z : C} (h : X'.toPrefunctor.obj (Opposite.op (SimplexCategory.mk n)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X i) (CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n))) h) = CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk (n + 1)))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X' i) h)

@[simp]

theorem CategoryTheory.SimplicialObject.δ_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] {X' : CategoryTheory.SimplicialObject C} {X : CategoryTheory.SimplicialObject C} (f : X ⟶ X') {n : ℕ} (i : Fin (n + 2)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.δ X i) (f.app (Opposite.op (SimplexCategory.mk n))) = CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk (n + 1)))) (CategoryTheory.SimplicialObject.δ X' i)

@[simp]

theorem CategoryTheory.SimplicialObject.σ_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X' : CategoryTheory.SimplicialObject C} {X : CategoryTheory.SimplicialObject C} (f : X ⟶ X') {n : ℕ} (i : Fin (n + 1)) {Z : C} (h : X'.toPrefunctor.obj (Opposite.op (SimplexCategory.mk (n + 1))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X i) (CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk (n + 1)))) h) = CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X' i) h)

@[simp]

theorem CategoryTheory.SimplicialObject.σ_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] {X' : CategoryTheory.SimplicialObject C} {X : CategoryTheory.SimplicialObject C} (f : X ⟶ X') {n : ℕ} (i : Fin (n + 1)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.σ X i) (f.app (Opposite.op (SimplexCategory.mk (n + 1)))) = CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n))) (CategoryTheory.SimplicialObject.σ X' i)

@[simp]

theorem CategoryTheory.SimplicialObject.whiskering_map_app_app (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] : ∀ {X Y : CategoryTheory.Functor C D} (τ : X ⟶ Y) (F : CategoryTheory.Functor SimplexCategoryᵒᵖ C) (c : SimplexCategoryᵒᵖ), (((CategoryTheory.SimplicialObject.whiskering C D).toPrefunctor.map τ).app F).app c = τ.app (F.toPrefunctor.obj c)

@[simp]

theorem CategoryTheory.SimplicialObject.whiskering_obj_obj_obj (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] (H : CategoryTheory.Functor C D) (F : CategoryTheory.Functor SimplexCategoryᵒᵖ C) (X : SimplexCategoryᵒᵖ) : (((CategoryTheory.SimplicialObject.whiskering C D).toPrefunctor.obj H).toPrefunctor.obj F).toPrefunctor.obj X = H.toPrefunctor.obj (F.toPrefunctor.obj X)

@[simp]

theorem CategoryTheory.SimplicialObject.whiskering_obj_map_app (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] (H : CategoryTheory.Functor C D) : ∀ {X Y : CategoryTheory.Functor SimplexCategoryᵒᵖ C} (α : X ⟶ Y) (X_1 : SimplexCategoryᵒᵖ), (((CategoryTheory.SimplicialObject.whiskering C D).toPrefunctor.obj H).toPrefunctor.map α).app X_1 = H.toPrefunctor.map (α.app X_1)

@[simp]

theorem CategoryTheory.SimplicialObject.whiskering_obj_obj_map (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] (H : CategoryTheory.Functor C D) (F : CategoryTheory.Functor SimplexCategoryᵒᵖ C) : ∀ {X Y : SimplexCategoryᵒᵖ} (f : X ⟶ Y), (((CategoryTheory.SimplicialObject.whiskering C D).toPrefunctor.obj H).toPrefunctor.obj F).toPrefunctor.map f = H.toPrefunctor.map (F.toPrefunctor.map f)

def CategoryTheory.SimplicialObject.whiskering (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] : CategoryTheory.Functor (CategoryTheory.Functor C D) (CategoryTheory.Functor (CategoryTheory.SimplicialObject C) (CategoryTheory.SimplicialObject D))

Functor composition induces a functor on simplicial objects.

Equations

• CategoryTheory.SimplicialObject.whiskering C D = CategoryTheory.whiskeringRight SimplexCategoryᵒᵖ C D

def CategoryTheory.SimplicialObject.Truncated (C : Type u) [CategoryTheory.Category.{v, u} C] (n : ℕ) : Type (max v u)

Truncated simplicial objects.

Equations

• CategoryTheory.SimplicialObject.Truncated C n = CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C

instance CategoryTheory.SimplicialObject.instCategoryTruncated (C : Type u) [CategoryTheory.Category.{v, u} C] {n : ℕ} : CategoryTheory.Category.{v, max u v} (CategoryTheory.SimplicialObject.Truncated C n)

Equations

• CategoryTheory.SimplicialObject.instCategoryTruncated C = id inferInstance

instance CategoryTheory.SimplicialObject.Truncated.instHasLimitsOfShapeTruncatedInstCategoryTruncated {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.SimplicialObject.Truncated C n)

Equations

• (_ : CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.SimplicialObject.Truncated C n)) = (_ : CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.SimplicialObject.Truncated C n))

instance CategoryTheory.SimplicialObject.Truncated.instHasLimitsTruncatedInstCategoryTruncated {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} [CategoryTheory.Limits.HasLimits C] : CategoryTheory.Limits.HasLimits (CategoryTheory.SimplicialObject.Truncated C n)

Equations

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

instance CategoryTheory.SimplicialObject.Truncated.instHasColimitsOfShapeTruncatedInstCategoryTruncated {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.Limits.HasColimitsOfShape J C] : CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.SimplicialObject.Truncated C n)

Equations

• (_ : CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.SimplicialObject.Truncated C n)) = (_ : CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.SimplicialObject.Truncated C n))

instance CategoryTheory.SimplicialObject.Truncated.instHasColimitsTruncatedInstCategoryTruncated {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} [CategoryTheory.Limits.HasColimits C] : CategoryTheory.Limits.HasColimits (CategoryTheory.SimplicialObject.Truncated C n)

Equations

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

@[simp]

theorem CategoryTheory.SimplicialObject.Truncated.whiskering_obj_obj_obj (C : Type u) [CategoryTheory.Category.{v, u} C] {n : ℕ} (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] (H : CategoryTheory.Functor C D) (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C) (X : (SimplexCategory.Truncated n)ᵒᵖ) : (((CategoryTheory.SimplicialObject.Truncated.whiskering C D).toPrefunctor.obj H).toPrefunctor.obj F).toPrefunctor.obj X = H.toPrefunctor.obj (F.toPrefunctor.obj X)

@[simp]

theorem CategoryTheory.SimplicialObject.Truncated.whiskering_map_app_app (C : Type u) [CategoryTheory.Category.{v, u} C] {n : ℕ} (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] : ∀ {X Y : CategoryTheory.Functor C D} (τ : X ⟶ Y) (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C) (c : (SimplexCategory.Truncated n)ᵒᵖ), (((CategoryTheory.SimplicialObject.Truncated.whiskering C D).toPrefunctor.map τ).app F).app c = τ.app (F.toPrefunctor.obj c)

@[simp]

theorem CategoryTheory.SimplicialObject.Truncated.whiskering_obj_obj_map (C : Type u) [CategoryTheory.Category.{v, u} C] {n : ℕ} (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] (H : CategoryTheory.Functor C D) (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C) : ∀ {X Y : (SimplexCategory.Truncated n)ᵒᵖ} (f : X ⟶ Y), (((CategoryTheory.SimplicialObject.Truncated.whiskering C D).toPrefunctor.obj H).toPrefunctor.obj F).toPrefunctor.map f = H.toPrefunctor.map (F.toPrefunctor.map f)

@[simp]

theorem CategoryTheory.SimplicialObject.Truncated.whiskering_obj_map_app (C : Type u) [CategoryTheory.Category.{v, u} C] {n : ℕ} (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] (H : CategoryTheory.Functor C D) : ∀ {X Y : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C} (α : X ⟶ Y) (X_1 : (SimplexCategory.Truncated n)ᵒᵖ), (((CategoryTheory.SimplicialObject.Truncated.whiskering C D).toPrefunctor.obj H).toPrefunctor.map α).app X_1 = H.toPrefunctor.map (α.app X_1)

def CategoryTheory.SimplicialObject.Truncated.whiskering (C : Type u) [CategoryTheory.Category.{v, u} C] {n : ℕ} (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] : CategoryTheory.Functor (CategoryTheory.Functor C D) (CategoryTheory.Functor (CategoryTheory.SimplicialObject.Truncated C n) (CategoryTheory.SimplicialObject.Truncated D n))

Functor composition induces a functor on truncated simplicial objects.

Equations

• CategoryTheory.SimplicialObject.Truncated.whiskering C D = CategoryTheory.whiskeringRight (SimplexCategory.Truncated n)ᵒᵖ C D

def CategoryTheory.SimplicialObject.sk {C : Type u} [CategoryTheory.Category.{v, u} C] (n : ℕ) : CategoryTheory.Functor (CategoryTheory.SimplicialObject C) (CategoryTheory.SimplicialObject.Truncated C n)

The skeleton functor from simplicial objects to truncated simplicial objects.

Equations

• CategoryTheory.SimplicialObject.sk n = (CategoryTheory.whiskeringLeft (SimplexCategory.Truncated n)ᵒᵖ SimplexCategoryᵒᵖ C).toPrefunctor.obj SimplexCategory.Truncated.inclusion.op

@[inline, reducible]

abbrev CategoryTheory.SimplicialObject.const (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor C (CategoryTheory.SimplicialObject C)

The constant simplicial object is the constant functor.

Equations

• CategoryTheory.SimplicialObject.const C = CategoryTheory.Functor.const SimplexCategoryᵒᵖ

def CategoryTheory.SimplicialObject.Augmented (C : Type u) [CategoryTheory.Category.{v, u} C] : Type (max u v)

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

Equations

• CategoryTheory.SimplicialObject.Augmented C = CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.SimplicialObject C)) (CategoryTheory.SimplicialObject.const C)

@[simp]

theorem CategoryTheory.SimplicialObject.instCategoryAugmented_id_left_app (C : Type u) [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.SimplicialObject C)) (CategoryTheory.SimplicialObject.const C)) (X : SimplexCategoryᵒᵖ) : (CategoryTheory.CategoryStruct.id X✝).left.app X = CategoryTheory.CategoryStruct.id (X✝.left.toPrefunctor.obj X)

@[simp]

theorem CategoryTheory.SimplicialObject.instCategoryAugmented_id_right (C : Type u) [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.SimplicialObject C)) (CategoryTheory.SimplicialObject.const C)) : (CategoryTheory.CategoryStruct.id X).right = CategoryTheory.CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.SimplicialObject.instCategoryAugmented_comp_right (C : Type u) [CategoryTheory.Category.{v, u} C] : ∀ {X Y Z : CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.SimplicialObject C)) (CategoryTheory.SimplicialObject.const C)} (f : X ⟶ Y) (g : Y ⟶ Z), (CategoryTheory.CategoryStruct.comp f g).right = CategoryTheory.CategoryStruct.comp f.right g.right

@[simp]

theorem CategoryTheory.SimplicialObject.instCategoryAugmented_comp_left_app (C : Type u) [CategoryTheory.Category.{v, u} C] : ∀ {X Y Z : CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.SimplicialObject C)) (CategoryTheory.SimplicialObject.const C)} (f : X ⟶ Y) (g : Y ⟶ Z) (X_1 : SimplexCategoryᵒᵖ), (CategoryTheory.CategoryStruct.comp f g).left.app X_1 = CategoryTheory.CategoryStruct.comp (f.left.app X_1) (g.left.app X_1)

instance CategoryTheory.SimplicialObject.instCategoryAugmented (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Category.{v, max u v} (CategoryTheory.SimplicialObject.Augmented C)

Equations

• CategoryTheory.SimplicialObject.instCategoryAugmented C = id inferInstance

theorem CategoryTheory.SimplicialObject.Augmented.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] {X : CategoryTheory.SimplicialObject.Augmented C} {Y : CategoryTheory.SimplicialObject.Augmented C} (f : X ⟶ Y) (g : X ⟶ Y) (h₁ : f.left = g.left) (h₂ : f.right = g.right) : f = g

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.drop_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.SimplicialObject C)) (CategoryTheory.SimplicialObject.const C)) : CategoryTheory.SimplicialObject.Augmented.drop.toPrefunctor.obj X = X.left

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.drop_map {C : Type u} [CategoryTheory.Category.{v, u} C] : ∀ {X Y : CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.SimplicialObject C)) (CategoryTheory.SimplicialObject.const C)} (f : X ⟶ Y), CategoryTheory.SimplicialObject.Augmented.drop.toPrefunctor.map f = f.left

def CategoryTheory.SimplicialObject.Augmented.drop {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (CategoryTheory.SimplicialObject.Augmented C) (CategoryTheory.SimplicialObject C)

Drop the augmentation.

Equations

• CategoryTheory.SimplicialObject.Augmented.drop = CategoryTheory.Comma.fst (CategoryTheory.Functor.id (CategoryTheory.SimplicialObject C)) (CategoryTheory.SimplicialObject.const C)

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.point_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.SimplicialObject C)) (CategoryTheory.SimplicialObject.const C)) : CategoryTheory.SimplicialObject.Augmented.point.toPrefunctor.obj X = X.right

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.point_map {C : Type u} [CategoryTheory.Category.{v, u} C] : ∀ {X Y : CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.SimplicialObject C)) (CategoryTheory.SimplicialObject.const C)} (f : X ⟶ Y), CategoryTheory.SimplicialObject.Augmented.point.toPrefunctor.map f = f.right

def CategoryTheory.SimplicialObject.Augmented.point {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (CategoryTheory.SimplicialObject.Augmented C) C

The point of the augmentation.

Equations

• CategoryTheory.SimplicialObject.Augmented.point = CategoryTheory.Comma.snd (CategoryTheory.Functor.id (CategoryTheory.SimplicialObject C)) (CategoryTheory.SimplicialObject.const C)

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.toArrow_obj_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C) : (CategoryTheory.SimplicialObject.Augmented.toArrow.toPrefunctor.obj X).hom = X.hom.app (Opposite.op (SimplexCategory.mk 0))

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.toArrow_map_right {C : Type u} [CategoryTheory.Category.{v, u} C] : ∀ {X Y : CategoryTheory.SimplicialObject.Augmented C} (η : X ⟶ Y), (CategoryTheory.SimplicialObject.Augmented.toArrow.toPrefunctor.map η).right = CategoryTheory.SimplicialObject.Augmented.point.toPrefunctor.map η

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.toArrow_obj_left {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C) : (CategoryTheory.SimplicialObject.Augmented.toArrow.toPrefunctor.obj X).left = (CategoryTheory.SimplicialObject.Augmented.drop.toPrefunctor.obj X).toPrefunctor.obj (Opposite.op (SimplexCategory.mk 0))

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.toArrow_obj_right {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C) : (CategoryTheory.SimplicialObject.Augmented.toArrow.toPrefunctor.obj X).right = CategoryTheory.SimplicialObject.Augmented.point.toPrefunctor.obj X

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.toArrow_map_left {C : Type u} [CategoryTheory.Category.{v, u} C] : ∀ {X Y : CategoryTheory.SimplicialObject.Augmented C} (η : X ⟶ Y), (CategoryTheory.SimplicialObject.Augmented.toArrow.toPrefunctor.map η).left = (CategoryTheory.SimplicialObject.Augmented.drop.toPrefunctor.map η).app (Opposite.op (SimplexCategory.mk 0))

def CategoryTheory.SimplicialObject.Augmented.toArrow {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (CategoryTheory.SimplicialObject.Augmented C) (CategoryTheory.Arrow C)

The functor from augmented objects to arrows.

Equations

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

theorem CategoryTheory.SimplicialObject.Augmented.w₀_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X : CategoryTheory.SimplicialObject.Augmented C} {Y : CategoryTheory.SimplicialObject.Augmented C} (f : X ⟶ Y) {Z : C} (h : ((CategoryTheory.SimplicialObject.const C).toPrefunctor.obj Y.right).toPrefunctor.obj (Opposite.op (SimplexCategory.mk 0)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.SimplicialObject.Augmented.drop.toPrefunctor.map f).app (Opposite.op (SimplexCategory.mk 0))) (CategoryTheory.CategoryStruct.comp (Y.hom.app (Opposite.op (SimplexCategory.mk 0))) h) = CategoryTheory.CategoryStruct.comp (X.hom.app (Opposite.op (SimplexCategory.mk 0))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.Augmented.point.toPrefunctor.map f) h)

theorem CategoryTheory.SimplicialObject.Augmented.w₀ {C : Type u} [CategoryTheory.Category.{v, u} C] {X : CategoryTheory.SimplicialObject.Augmented C} {Y : CategoryTheory.SimplicialObject.Augmented C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.SimplicialObject.Augmented.drop.toPrefunctor.map f).app (Opposite.op (SimplexCategory.mk 0))) (Y.hom.app (Opposite.op (SimplexCategory.mk 0))) = CategoryTheory.CategoryStruct.comp (X.hom.app (Opposite.op (SimplexCategory.mk 0))) (CategoryTheory.SimplicialObject.Augmented.point.toPrefunctor.map f)

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

def CategoryTheory.SimplicialObject.Augmented.whiskeringObj (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] (F : CategoryTheory.Functor C D) : CategoryTheory.Functor (CategoryTheory.SimplicialObject.Augmented C) (CategoryTheory.SimplicialObject.Augmented D)

Functor composition induces a functor on augmented simplicial objects.

Equations

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

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.whiskering_map_app_left (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u') [CategoryTheory.Category.{v', u'} D] : ∀ {X Y : CategoryTheory.Functor C D} (η : X ⟶ Y) (A : CategoryTheory.SimplicialObject.Augmented C), (((CategoryTheory.SimplicialObject.Augmented.whiskering C D).toPrefunctor.map η).app A).left = CategoryTheory.whiskerLeft (CategoryTheory.SimplicialObject.Augmented.drop.toPrefunctor.obj A) η

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.whiskering_obj (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u') [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) : (CategoryTheory.SimplicialObject.Augmented.whiskering C D).toPrefunctor.obj F = CategoryTheory.SimplicialObject.Augmented.whiskeringObj C D F

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.whiskering_map_app_right (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u') [CategoryTheory.Category.{v', u'} D] : ∀ {X Y : CategoryTheory.Functor C D} (η : X ⟶ Y) (A : CategoryTheory.SimplicialObject.Augmented C), (((CategoryTheory.SimplicialObject.Augmented.whiskering C D).toPrefunctor.map η).app A).right = η.app (CategoryTheory.SimplicialObject.Augmented.point.toPrefunctor.obj A)

def CategoryTheory.SimplicialObject.Augmented.whiskering (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u') [CategoryTheory.Category.{v', u'} D] : CategoryTheory.Functor (CategoryTheory.Functor C D) (CategoryTheory.Functor (CategoryTheory.SimplicialObject.Augmented C) (CategoryTheory.SimplicialObject.Augmented D))

Functor composition induces a functor on augmented simplicial objects.

Equations

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

@[simp]

theorem CategoryTheory.SimplicialObject.augment_right {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) (X₀ : C) (f : X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk 0)) ⟶ X₀) (w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 ⟶ i), CategoryTheory.CategoryStruct.comp (X.toPrefunctor.map g₁.op) f = CategoryTheory.CategoryStruct.comp (X.toPrefunctor.map g₂.op) f) : (CategoryTheory.SimplicialObject.augment X X₀ f w).right = X₀

@[simp]

theorem CategoryTheory.SimplicialObject.augment_left {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) (X₀ : C) (f : X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk 0)) ⟶ X₀) (w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 ⟶ i), CategoryTheory.CategoryStruct.comp (X.toPrefunctor.map g₁.op) f = CategoryTheory.CategoryStruct.comp (X.toPrefunctor.map g₂.op) f) : (CategoryTheory.SimplicialObject.augment X X₀ f w).left = X

@[simp]

theorem CategoryTheory.SimplicialObject.augment_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) (X₀ : C) (f : X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk 0)) ⟶ X₀) (w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 ⟶ i), CategoryTheory.CategoryStruct.comp (X.toPrefunctor.map g₁.op) f = CategoryTheory.CategoryStruct.comp (X.toPrefunctor.map g₂.op) f) (i : SimplexCategoryᵒᵖ) : (CategoryTheory.SimplicialObject.augment X X₀ f w).hom.app i = CategoryTheory.CategoryStruct.comp (X.toPrefunctor.map (SimplexCategory.const i.unop 0).op) f

def CategoryTheory.SimplicialObject.augment {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) (X₀ : C) (f : X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk 0)) ⟶ X₀) (w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 ⟶ i), CategoryTheory.CategoryStruct.comp (X.toPrefunctor.map g₁.op) f = CategoryTheory.CategoryStruct.comp (X.toPrefunctor.map g₂.op) f) : CategoryTheory.SimplicialObject.Augmented C

Augment a simplicial object with an object.

Equations

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

theorem CategoryTheory.SimplicialObject.augment_hom_zero {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) (X₀ : C) (f : X.toPrefunctor.obj (Opposite.op (SimplexCategory.mk 0)) ⟶ X₀) (w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 ⟶ i), CategoryTheory.CategoryStruct.comp (X.toPrefunctor.map g₁.op) f = CategoryTheory.CategoryStruct.comp (X.toPrefunctor.map g₂.op) f) : (CategoryTheory.SimplicialObject.augment X X₀ f w).hom.app (Opposite.op (SimplexCategory.mk 0)) = f

def CategoryTheory.CosimplicialObject (C : Type u) [CategoryTheory.Category.{v, u} C] : Type (max v u)

Cosimplicial objects.

Equations

• CategoryTheory.CosimplicialObject C = CategoryTheory.Functor SimplexCategory C

@[simp]

theorem CategoryTheory.instCategoryCosimplicialObject_comp_app (C : Type u) [CategoryTheory.Category.{v, u} C] : ∀ {X Y Z : CategoryTheory.Functor SimplexCategory C} (α : X ⟶ Y) (β : Y ⟶ Z) (X_1 : SimplexCategory), (CategoryTheory.CategoryStruct.comp α β).app X_1 = CategoryTheory.CategoryStruct.comp (α.app X_1) (β.app X_1)

@[simp]

theorem CategoryTheory.instCategoryCosimplicialObject_id_app (C : Type u) [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor SimplexCategory C) (X : SimplexCategory) : (CategoryTheory.CategoryStruct.id F).app X = CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X)

instance CategoryTheory.instCategoryCosimplicialObject (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Category.{v, max u v} (CategoryTheory.CosimplicialObject C)

Equations

• CategoryTheory.instCategoryCosimplicialObject C = id inferInstance

def Simplicial.«term__[_]_1» : Lean.TrailingParserDescr

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

Equations

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

instance CategoryTheory.CosimplicialObject.instHasLimitsOfShapeCosimplicialObjectInstCategoryCosimplicialObject (C : Type u) [CategoryTheory.Category.{v, u} C] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.CosimplicialObject C)

Equations

• (_ : CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.CosimplicialObject C)) = (_ : CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.CosimplicialObject C))

instance CategoryTheory.CosimplicialObject.instHasLimitsCosimplicialObjectInstCategoryCosimplicialObject (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] : CategoryTheory.Limits.HasLimits (CategoryTheory.CosimplicialObject C)

Equations

• (_ : CategoryTheory.Limits.HasLimits (CategoryTheory.CosimplicialObject C)) = (_ : CategoryTheory.Limits.HasLimitsOfSize.{v, v, v, max u v} (CategoryTheory.CosimplicialObject C))

instance CategoryTheory.CosimplicialObject.instHasColimitsOfShapeCosimplicialObjectInstCategoryCosimplicialObject (C : Type u) [CategoryTheory.Category.{v, u} C] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.Limits.HasColimitsOfShape J C] : CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.CosimplicialObject C)

Equations

• (_ : CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.CosimplicialObject C)) = (_ : CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.CosimplicialObject C))

instance CategoryTheory.CosimplicialObject.instHasColimitsCosimplicialObjectInstCategoryCosimplicialObject (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] : CategoryTheory.Limits.HasColimits (CategoryTheory.CosimplicialObject C)

Equations

• (_ : CategoryTheory.Limits.HasColimits (CategoryTheory.CosimplicialObject C)) = (_ : CategoryTheory.Limits.HasColimitsOfSize.{v, v, v, max u v} (CategoryTheory.CosimplicialObject C))

theorem CategoryTheory.CosimplicialObject.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] {X : CategoryTheory.CosimplicialObject C} {Y : CategoryTheory.CosimplicialObject C} (f : X ⟶ Y) (g : X ⟶ Y) (h : ∀ (n : SimplexCategory), f.app n = g.app n) : f = g

def CategoryTheory.CosimplicialObject.δ {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} (i : Fin (n + 2)) : X.toPrefunctor.obj (SimplexCategory.mk n) ⟶ X.toPrefunctor.obj (SimplexCategory.mk (n + 1))

Coface maps for a cosimplicial object.

Equations

• CategoryTheory.CosimplicialObject.δ X i = X.toPrefunctor.map (SimplexCategory.δ i)

def CategoryTheory.CosimplicialObject.σ {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} (i : Fin (n + 1)) : X.toPrefunctor.obj (SimplexCategory.mk (n + 1)) ⟶ X.toPrefunctor.obj (SimplexCategory.mk n)

Codegeneracy maps for a cosimplicial object.

Equations

• CategoryTheory.CosimplicialObject.σ X i = X.toPrefunctor.map (SimplexCategory.σ i)

def CategoryTheory.CosimplicialObject.eqToIso {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {m : ℕ} (h : n = m) : X.toPrefunctor.obj (SimplexCategory.mk n) ≅ X.toPrefunctor.obj (SimplexCategory.mk m)

Isomorphisms from identities in ℕ.

Equations

• CategoryTheory.CosimplicialObject.eqToIso X h = X.mapIso (CategoryTheory.eqToIso (_ : SimplexCategory.mk n = SimplexCategory.mk m))

@[simp]

theorem CategoryTheory.CosimplicialObject.eqToIso_refl {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} (h : n = n) : CategoryTheory.CosimplicialObject.eqToIso X h = CategoryTheory.Iso.refl (X.toPrefunctor.obj (SimplexCategory.mk n))

theorem CategoryTheory.CosimplicialObject.δ_comp_δ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 2)} (H : i ≤ j) {Z : C} (h : X.toPrefunctor.obj (SimplexCategory.mk (n + 1 + 1)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X (Fin.succ j)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X (Fin.castSucc i)) h)

theorem CategoryTheory.CosimplicialObject.δ_comp_δ {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 2)} (H : i ≤ j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X i) (CategoryTheory.CosimplicialObject.δ X (Fin.succ j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X j) (CategoryTheory.CosimplicialObject.δ X (Fin.castSucc i))

The generic case of the first cosimplicial identity

theorem CategoryTheory.CosimplicialObject.δ_comp_δ'_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : Fin.castSucc i < j) {Z : C} (h : X.toPrefunctor.obj (SimplexCategory.mk (n + 1 + 1)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X (Fin.pred j (_ : j = 0 → False))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X (Fin.castSucc i)) h)

theorem CategoryTheory.CosimplicialObject.δ_comp_δ' {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : Fin.castSucc i < j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X i) (CategoryTheory.CosimplicialObject.δ X j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X (Fin.pred j (_ : j = 0 → False))) (CategoryTheory.CosimplicialObject.δ X (Fin.castSucc i))

theorem CategoryTheory.CosimplicialObject.δ_comp_δ''_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : i ≤ Fin.castSucc j) {Z : C} (h : X.toPrefunctor.obj (SimplexCategory.mk (n + 1 + 1)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X (Fin.castLT i (_ : ↑i < n + 2))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X (Fin.succ j)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X i) h)

theorem CategoryTheory.CosimplicialObject.δ_comp_δ'' {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : i ≤ Fin.castSucc j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X (Fin.castLT i (_ : ↑i < n + 2))) (CategoryTheory.CosimplicialObject.δ X (Fin.succ j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X j) (CategoryTheory.CosimplicialObject.δ X i)

theorem CategoryTheory.CosimplicialObject.δ_comp_δ_self_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {i : Fin (n + 2)} {Z : C} (h : X.toPrefunctor.obj (SimplexCategory.mk (n + 1 + 1)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X (Fin.castSucc i)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X (Fin.succ i)) h)

theorem CategoryTheory.CosimplicialObject.δ_comp_δ_self {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {i : Fin (n + 2)} : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X i) (CategoryTheory.CosimplicialObject.δ X (Fin.castSucc i)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X i) (CategoryTheory.CosimplicialObject.δ X (Fin.succ i))

The special case of the first cosimplicial identity

theorem CategoryTheory.CosimplicialObject.δ_comp_δ_self'_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : j = Fin.castSucc i) {Z : C} (h : X.toPrefunctor.obj (SimplexCategory.mk (n + 1 + 1)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X (Fin.succ i)) h)

theorem CategoryTheory.CosimplicialObject.δ_comp_δ_self' {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : j = Fin.castSucc i) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X i) (CategoryTheory.CosimplicialObject.δ X j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X i) (CategoryTheory.CosimplicialObject.δ X (Fin.succ i))

theorem CategoryTheory.CosimplicialObject.δ_comp_σ_of_le_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i ≤ Fin.castSucc j) {Z : C} (h : X.toPrefunctor.obj (SimplexCategory.mk (n + 1)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X (Fin.castSucc i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.σ X (Fin.succ j)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.σ X j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X i) h)

theorem CategoryTheory.CosimplicialObject.δ_comp_σ_of_le {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i ≤ Fin.castSucc j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X (Fin.castSucc i)) (CategoryTheory.CosimplicialObject.σ X (Fin.succ j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.σ X j) (CategoryTheory.CosimplicialObject.δ X i)

The second cosimplicial identity

theorem CategoryTheory.CosimplicialObject.δ_comp_σ_self_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {i : Fin (n + 1)} {Z : C} (h : X.toPrefunctor.obj (SimplexCategory.mk n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X (Fin.castSucc i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.σ X i) h) = h

theorem CategoryTheory.CosimplicialObject.δ_comp_σ_self {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {i : Fin (n + 1)} : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X (Fin.castSucc i)) (CategoryTheory.CosimplicialObject.σ X i) = CategoryTheory.CategoryStruct.id (X.toPrefunctor.obj (SimplexCategory.mk n))

The first part of the third cosimplicial identity

theorem CategoryTheory.CosimplicialObject.δ_comp_σ_self'_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = Fin.castSucc i) {Z : C} (h : X.toPrefunctor.obj (SimplexCategory.mk n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.σ X i) h) = h

theorem CategoryTheory.CosimplicialObject.δ_comp_σ_self' {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = Fin.castSucc i) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X j) (CategoryTheory.CosimplicialObject.σ X i) = CategoryTheory.CategoryStruct.id (X.toPrefunctor.obj (SimplexCategory.mk n))

theorem CategoryTheory.CosimplicialObject.δ_comp_σ_succ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {i : Fin (n + 1)} {Z : C} (h : X.toPrefunctor.obj (SimplexCategory.mk n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X (Fin.succ i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.σ X i) h) = h

theorem CategoryTheory.CosimplicialObject.δ_comp_σ_succ {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {i : Fin (n + 1)} : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X (Fin.succ i)) (CategoryTheory.CosimplicialObject.σ X i) = CategoryTheory.CategoryStruct.id (X.toPrefunctor.obj (SimplexCategory.mk n))

The second part of the third cosimplicial identity

theorem CategoryTheory.CosimplicialObject.δ_comp_σ_succ'_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = Fin.succ i) {Z : C} (h : X.toPrefunctor.obj (SimplexCategory.mk n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.σ X i) h) = h

theorem CategoryTheory.CosimplicialObject.δ_comp_σ_succ' {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = Fin.succ i) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X j) (CategoryTheory.CosimplicialObject.σ X i) = CategoryTheory.CategoryStruct.id (X.toPrefunctor.obj (SimplexCategory.mk n))

theorem CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : Fin.castSucc j < i) {Z : C} (h : X.toPrefunctor.obj (SimplexCategory.mk (n + 1)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X (Fin.succ i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.σ X (Fin.castSucc j)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.σ X j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X i) h)

theorem CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : Fin.castSucc j < i) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X (Fin.succ i)) (CategoryTheory.CosimplicialObject.σ X (Fin.castSucc j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.σ X j) (CategoryTheory.CosimplicialObject.δ X i)

The fourth cosimplicial identity

theorem CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt'_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : Fin.succ j < i) {Z : C} (h : X.toPrefunctor.obj (SimplexCategory.mk (n + 1)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.σ X j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.σ X (Fin.castLT j (_ : ↑j < n + 1))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X (Fin.pred i (_ : i = 0 → False))) h)

theorem CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt' {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : Fin.succ j < i) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X i) (CategoryTheory.CosimplicialObject.σ X j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.σ X (Fin.castLT j (_ : ↑j < n + 1))) (CategoryTheory.CosimplicialObject.δ X (Fin.pred i (_ : i = 0 → False)))

theorem CategoryTheory.CosimplicialObject.σ_comp_σ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {i : Fin (n + 1)} {j : Fin (n + 1)} (H : i ≤ j) {Z : C} (h : X.toPrefunctor.obj (SimplexCategory.mk n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.σ X (Fin.castSucc i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.σ X j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.σ X (Fin.succ j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.σ X i) h)

theorem CategoryTheory.CosimplicialObject.σ_comp_σ {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {i : Fin (n + 1)} {j : Fin (n + 1)} (H : i ≤ j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.σ X (Fin.castSucc i)) (CategoryTheory.CosimplicialObject.σ X j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.σ X (Fin.succ j)) (CategoryTheory.CosimplicialObject.σ X i)

The fifth cosimplicial identity

@[simp]

theorem CategoryTheory.CosimplicialObject.δ_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X' : CategoryTheory.CosimplicialObject C} {X : CategoryTheory.CosimplicialObject C} (f : X ⟶ X') {n : ℕ} (i : Fin (n + 2)) {Z : C} (h : X'.toPrefunctor.obj (SimplexCategory.mk (n + 1)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X i) (CategoryTheory.CategoryStruct.comp (f.app (SimplexCategory.mk (n + 1))) h) = CategoryTheory.CategoryStruct.comp (f.app (SimplexCategory.mk n)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X' i) h)

@[simp]

theorem CategoryTheory.CosimplicialObject.δ_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] {X' : CategoryTheory.CosimplicialObject C} {X : CategoryTheory.CosimplicialObject C} (f : X ⟶ X') {n : ℕ} (i : Fin (n + 2)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.δ X i) (f.app (SimplexCategory.mk (n + 1))) = CategoryTheory.CategoryStruct.comp (f.app (SimplexCategory.mk n)) (CategoryTheory.CosimplicialObject.δ X' i)

@[simp]

theorem CategoryTheory.CosimplicialObject.σ_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X' : CategoryTheory.CosimplicialObject C} {X : CategoryTheory.CosimplicialObject C} (f : X ⟶ X') {n : ℕ} (i : Fin (n + 1)) {Z : C} (h : X'.toPrefunctor.obj (SimplexCategory.mk n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.σ X i) (CategoryTheory.CategoryStruct.comp (f.app (SimplexCategory.mk n)) h) = CategoryTheory.CategoryStruct.comp (f.app (SimplexCategory.mk (n + 1))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.σ X' i) h)

@[simp]

theorem CategoryTheory.CosimplicialObject.σ_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] {X' : CategoryTheory.CosimplicialObject C} {X : CategoryTheory.CosimplicialObject C} (f : X ⟶ X') {n : ℕ} (i : Fin (n + 1)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CosimplicialObject.σ X i) (f.app (SimplexCategory.mk n)) = CategoryTheory.CategoryStruct.comp (f.app (SimplexCategory.mk (n + 1))) (CategoryTheory.CosimplicialObject.σ X' i)

@[simp]

theorem CategoryTheory.CosimplicialObject.whiskering_map_app_app (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] : ∀ {X Y : CategoryTheory.Functor C D} (τ : X ⟶ Y) (F : CategoryTheory.Functor SimplexCategory C) (c : SimplexCategory), (((CategoryTheory.CosimplicialObject.whiskering C D).toPrefunctor.map τ).app F).app c = τ.app (F.toPrefunctor.obj c)

@[simp]

theorem CategoryTheory.CosimplicialObject.whiskering_obj_obj_map (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] (H : CategoryTheory.Functor C D) (F : CategoryTheory.Functor SimplexCategory C) : ∀ {X Y : SimplexCategory} (f : X ⟶ Y), (((CategoryTheory.CosimplicialObject.whiskering C D).toPrefunctor.obj H).toPrefunctor.obj F).toPrefunctor.map f = H.toPrefunctor.map (F.toPrefunctor.map f)

@[simp]

theorem CategoryTheory.CosimplicialObject.whiskering_obj_map_app (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] (H : CategoryTheory.Functor C D) : ∀ {X Y : CategoryTheory.Functor SimplexCategory C} (α : X ⟶ Y) (X_1 : SimplexCategory), (((CategoryTheory.CosimplicialObject.whiskering C D).toPrefunctor.obj H).toPrefunctor.map α).app X_1 = H.toPrefunctor.map (α.app X_1)

@[simp]

theorem CategoryTheory.CosimplicialObject.whiskering_obj_obj_obj (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] (H : CategoryTheory.Functor C D) (F : CategoryTheory.Functor SimplexCategory C) (X : SimplexCategory) : (((CategoryTheory.CosimplicialObject.whiskering C D).toPrefunctor.obj H).toPrefunctor.obj F).toPrefunctor.obj X = H.toPrefunctor.obj (F.toPrefunctor.obj X)

def CategoryTheory.CosimplicialObject.whiskering (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] : CategoryTheory.Functor (CategoryTheory.Functor C D) (CategoryTheory.Functor (CategoryTheory.CosimplicialObject C) (CategoryTheory.CosimplicialObject D))

Functor composition induces a functor on cosimplicial objects.

Equations

• CategoryTheory.CosimplicialObject.whiskering C D = CategoryTheory.whiskeringRight SimplexCategory C D

def CategoryTheory.CosimplicialObject.Truncated (C : Type u) [CategoryTheory.Category.{v, u} C] (n : ℕ) : Type (max v u)

Truncated cosimplicial objects.

Equations

• CategoryTheory.CosimplicialObject.Truncated C n = CategoryTheory.Functor (SimplexCategory.Truncated n) C

instance CategoryTheory.CosimplicialObject.instCategoryTruncated (C : Type u) [CategoryTheory.Category.{v, u} C] {n : ℕ} : CategoryTheory.Category.{v, max u v} (CategoryTheory.CosimplicialObject.Truncated C n)

Equations

• CategoryTheory.CosimplicialObject.instCategoryTruncated C = id inferInstance

instance CategoryTheory.CosimplicialObject.Truncated.instHasLimitsOfShapeTruncatedInstCategoryTruncated {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.CosimplicialObject.Truncated C n)

Equations

• (_ : CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.CosimplicialObject.Truncated C n)) = (_ : CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.CosimplicialObject.Truncated C n))

instance CategoryTheory.CosimplicialObject.Truncated.instHasLimitsTruncatedInstCategoryTruncated {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} [CategoryTheory.Limits.HasLimits C] : CategoryTheory.Limits.HasLimits (CategoryTheory.CosimplicialObject.Truncated C n)

Equations

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

instance CategoryTheory.CosimplicialObject.Truncated.instHasColimitsOfShapeTruncatedInstCategoryTruncated {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.Limits.HasColimitsOfShape J C] : CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.CosimplicialObject.Truncated C n)

Equations

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

instance CategoryTheory.CosimplicialObject.Truncated.instHasColimitsTruncatedInstCategoryTruncated {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} [CategoryTheory.Limits.HasColimits C] : CategoryTheory.Limits.HasColimits (CategoryTheory.CosimplicialObject.Truncated C n)

Equations

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

@[simp]

theorem CategoryTheory.CosimplicialObject.Truncated.whiskering_obj_obj_map (C : Type u) [CategoryTheory.Category.{v, u} C] {n : ℕ} (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] (H : CategoryTheory.Functor C D) (F : CategoryTheory.Functor (SimplexCategory.Truncated n) C) : ∀ {X Y : SimplexCategory.Truncated n} (f : X ⟶ Y), (((CategoryTheory.CosimplicialObject.Truncated.whiskering C D).toPrefunctor.obj H).toPrefunctor.obj F).toPrefunctor.map f = H.toPrefunctor.map (F.toPrefunctor.map f)

@[simp]

theorem CategoryTheory.CosimplicialObject.Truncated.whiskering_obj_obj_obj (C : Type u) [CategoryTheory.Category.{v, u} C] {n : ℕ} (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] (H : CategoryTheory.Functor C D) (F : CategoryTheory.Functor (SimplexCategory.Truncated n) C) (X : SimplexCategory.Truncated n) : (((CategoryTheory.CosimplicialObject.Truncated.whiskering C D).toPrefunctor.obj H).toPrefunctor.obj F).toPrefunctor.obj X = H.toPrefunctor.obj (F.toPrefunctor.obj X)

@[simp]

theorem CategoryTheory.CosimplicialObject.Truncated.whiskering_obj_map_app (C : Type u) [CategoryTheory.Category.{v, u} C] {n : ℕ} (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] (H : CategoryTheory.Functor C D) : ∀ {X Y : CategoryTheory.Functor (SimplexCategory.Truncated n) C} (α : X ⟶ Y) (X_1 : SimplexCategory.Truncated n), (((CategoryTheory.CosimplicialObject.Truncated.whiskering C D).toPrefunctor.obj H).toPrefunctor.map α).app X_1 = H.toPrefunctor.map (α.app X_1)

@[simp]

theorem CategoryTheory.CosimplicialObject.Truncated.whiskering_map_app_app (C : Type u) [CategoryTheory.Category.{v, u} C] {n : ℕ} (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] : ∀ {X Y : CategoryTheory.Functor C D} (τ : X ⟶ Y) (F : CategoryTheory.Functor (SimplexCategory.Truncated n) C) (c : SimplexCategory.Truncated n), (((CategoryTheory.CosimplicialObject.Truncated.whiskering C D).toPrefunctor.map τ).app F).app c = τ.app (F.toPrefunctor.obj c)

def CategoryTheory.CosimplicialObject.Truncated.whiskering (C : Type u) [CategoryTheory.Category.{v, u} C] {n : ℕ} (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] : CategoryTheory.Functor (CategoryTheory.Functor C D) (CategoryTheory.Functor (CategoryTheory.CosimplicialObject.Truncated C n) (CategoryTheory.CosimplicialObject.Truncated D n))

Functor composition induces a functor on truncated cosimplicial objects.

Equations

• CategoryTheory.CosimplicialObject.Truncated.whiskering C D = CategoryTheory.whiskeringRight (SimplexCategory.Truncated n) C D

def CategoryTheory.CosimplicialObject.sk {C : Type u} [CategoryTheory.Category.{v, u} C] (n : ℕ) : CategoryTheory.Functor (CategoryTheory.CosimplicialObject C) (CategoryTheory.CosimplicialObject.Truncated C n)

The skeleton functor from cosimplicial objects to truncated cosimplicial objects.

Equations

• CategoryTheory.CosimplicialObject.sk n = (CategoryTheory.whiskeringLeft (SimplexCategory.Truncated n) SimplexCategory C).toPrefunctor.obj SimplexCategory.Truncated.inclusion

@[inline, reducible]

abbrev CategoryTheory.CosimplicialObject.const (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor C (CategoryTheory.CosimplicialObject C)

The constant cosimplicial object.

Equations

• CategoryTheory.CosimplicialObject.const C = CategoryTheory.Functor.const SimplexCategory

def CategoryTheory.CosimplicialObject.Augmented (C : Type u) [CategoryTheory.Category.{v, u} C] : Type (max u v)

Augmented cosimplicial objects.

Equations

• CategoryTheory.CosimplicialObject.Augmented C = CategoryTheory.Comma (CategoryTheory.CosimplicialObject.const C) (CategoryTheory.Functor.id (CategoryTheory.CosimplicialObject C))

@[simp]

theorem CategoryTheory.CosimplicialObject.instCategoryAugmented_id_left (C : Type u) [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Comma (CategoryTheory.CosimplicialObject.const C) (CategoryTheory.Functor.id (CategoryTheory.CosimplicialObject C))) : (CategoryTheory.CategoryStruct.id X).left = CategoryTheory.CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.CosimplicialObject.instCategoryAugmented_comp_right_app (C : Type u) [CategoryTheory.Category.{v, u} C] : ∀ {X Y Z : CategoryTheory.Comma (CategoryTheory.CosimplicialObject.const C) (CategoryTheory.Functor.id (CategoryTheory.CosimplicialObject C))} (f : X ⟶ Y) (g : Y ⟶ Z) (X_1 : SimplexCategory), (CategoryTheory.CategoryStruct.comp f g).right.app X_1 = CategoryTheory.CategoryStruct.comp (f.right.app X_1) (g.right.app X_1)

@[simp]

theorem CategoryTheory.CosimplicialObject.instCategoryAugmented_comp_left (C : Type u) [CategoryTheory.Category.{v, u} C] : ∀ {X Y Z : CategoryTheory.Comma (CategoryTheory.CosimplicialObject.const C) (CategoryTheory.Functor.id (CategoryTheory.CosimplicialObject C))} (f : X ⟶ Y) (g : Y ⟶ Z), (CategoryTheory.CategoryStruct.comp f g).left = CategoryTheory.CategoryStruct.comp f.left g.left

@[simp]

theorem CategoryTheory.CosimplicialObject.instCategoryAugmented_id_right_app (C : Type u) [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Comma (CategoryTheory.CosimplicialObject.const C) (CategoryTheory.Functor.id (CategoryTheory.CosimplicialObject C))) (X : SimplexCategory) : (CategoryTheory.CategoryStruct.id X✝).right.app X = CategoryTheory.CategoryStruct.id (X✝.right.toPrefunctor.obj X)

instance CategoryTheory.CosimplicialObject.instCategoryAugmented (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Category.{v, max u v} (CategoryTheory.CosimplicialObject.Augmented C)

Equations

• CategoryTheory.CosimplicialObject.instCategoryAugmented C = id inferInstance

theorem CategoryTheory.CosimplicialObject.Augmented.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] {X : CategoryTheory.CosimplicialObject.Augmented C} {Y : CategoryTheory.CosimplicialObject.Augmented C} (f : X ⟶ Y) (g : X ⟶ Y) (h₁ : f.left = g.left) (h₂ : f.right = g.right) : f = g

@[simp]

theorem CategoryTheory.CosimplicialObject.Augmented.drop_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Comma (CategoryTheory.CosimplicialObject.const C) (CategoryTheory.Functor.id (CategoryTheory.CosimplicialObject C))) : CategoryTheory.CosimplicialObject.Augmented.drop.toPrefunctor.obj X = X.right

@[simp]

theorem CategoryTheory.CosimplicialObject.Augmented.drop_map {C : Type u} [CategoryTheory.Category.{v, u} C] : ∀ {X Y : CategoryTheory.Comma (CategoryTheory.CosimplicialObject.const C) (CategoryTheory.Functor.id (CategoryTheory.CosimplicialObject C))} (f : X ⟶ Y), CategoryTheory.CosimplicialObject.Augmented.drop.toPrefunctor.map f = f.right

def CategoryTheory.CosimplicialObject.Augmented.drop {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (CategoryTheory.CosimplicialObject.Augmented C) (CategoryTheory.CosimplicialObject C)

Drop the augmentation.

Equations

• CategoryTheory.CosimplicialObject.Augmented.drop = CategoryTheory.Comma.snd (CategoryTheory.CosimplicialObject.const C) (CategoryTheory.Functor.id (CategoryTheory.CosimplicialObject C))

@[simp]

theorem CategoryTheory.CosimplicialObject.Augmented.point_map {C : Type u} [CategoryTheory.Category.{v, u} C] : ∀ {X Y : CategoryTheory.Comma (CategoryTheory.CosimplicialObject.const C) (CategoryTheory.Functor.id (CategoryTheory.CosimplicialObject C))} (f : X ⟶ Y), CategoryTheory.CosimplicialObject.Augmented.point.toPrefunctor.map f = f.left

@[simp]

theorem CategoryTheory.CosimplicialObject.Augmented.point_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Comma (CategoryTheory.CosimplicialObject.const C) (CategoryTheory.Functor.id (CategoryTheory.CosimplicialObject C))) : CategoryTheory.CosimplicialObject.Augmented.point.toPrefunctor.obj X = X.left

def CategoryTheory.CosimplicialObject.Augmented.point {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (CategoryTheory.CosimplicialObject.Augmented C) C

The point of the augmentation.

Equations

• CategoryTheory.CosimplicialObject.Augmented.point = CategoryTheory.Comma.fst (CategoryTheory.CosimplicialObject.const C) (CategoryTheory.Functor.id (CategoryTheory.CosimplicialObject C))

@[simp]

theorem CategoryTheory.CosimplicialObject.Augmented.toArrow_obj_left {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented C) : (CategoryTheory.CosimplicialObject.Augmented.toArrow.toPrefunctor.obj X).left = X.left

@[simp]

theorem CategoryTheory.CosimplicialObject.Augmented.toArrow_map_left {C : Type u} [CategoryTheory.Category.{v, u} C] : ∀ {X Y : CategoryTheory.CosimplicialObject.Augmented C} (η : X ⟶ Y), (CategoryTheory.CosimplicialObject.Augmented.toArrow.toPrefunctor.map η).left = η.left

@[simp]

theorem CategoryTheory.CosimplicialObject.Augmented.toArrow_obj_right {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented C) : (CategoryTheory.CosimplicialObject.Augmented.toArrow.toPrefunctor.obj X).right = X.right.toPrefunctor.obj (SimplexCategory.mk 0)

@[simp]

theorem CategoryTheory.CosimplicialObject.Augmented.toArrow_obj_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented C) : (CategoryTheory.CosimplicialObject.Augmented.toArrow.toPrefunctor.obj X).hom = X.hom.app (SimplexCategory.mk 0)

@[simp]

theorem CategoryTheory.CosimplicialObject.Augmented.toArrow_map_right {C : Type u} [CategoryTheory.Category.{v, u} C] : ∀ {X Y : CategoryTheory.CosimplicialObject.Augmented C} (η : X ⟶ Y), (CategoryTheory.CosimplicialObject.Augmented.toArrow.toPrefunctor.map η).right = η.right.app (SimplexCategory.mk 0)

def CategoryTheory.CosimplicialObject.Augmented.toArrow {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (CategoryTheory.CosimplicialObject.Augmented C) (CategoryTheory.Arrow C)

The functor from augmented objects to arrows.

Equations

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

def CategoryTheory.CosimplicialObject.Augmented.whiskeringObj (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] (F : CategoryTheory.Functor C D) : CategoryTheory.Functor (CategoryTheory.CosimplicialObject.Augmented C) (CategoryTheory.CosimplicialObject.Augmented D)

Functor composition induces a functor on augmented cosimplicial objects.

Equations

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

@[simp]

theorem CategoryTheory.CosimplicialObject.Augmented.whiskering_map_app_left (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u') [CategoryTheory.Category.{v', u'} D] : ∀ {X Y : CategoryTheory.Functor C D} (η : X ⟶ Y) (A : CategoryTheory.CosimplicialObject.Augmented C), (((CategoryTheory.CosimplicialObject.Augmented.whiskering C D).toPrefunctor.map η).app A).left = η.app (CategoryTheory.CosimplicialObject.Augmented.point.toPrefunctor.obj A)

@[simp]

theorem CategoryTheory.CosimplicialObject.Augmented.whiskering_obj (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u') [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) : (CategoryTheory.CosimplicialObject.Augmented.whiskering C D).toPrefunctor.obj F = CategoryTheory.CosimplicialObject.Augmented.whiskeringObj C D F

@[simp]

theorem CategoryTheory.CosimplicialObject.Augmented.whiskering_map_app_right (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u') [CategoryTheory.Category.{v', u'} D] : ∀ {X Y : CategoryTheory.Functor C D} (η : X ⟶ Y) (A : CategoryTheory.CosimplicialObject.Augmented C), (((CategoryTheory.CosimplicialObject.Augmented.whiskering C D).toPrefunctor.map η).app A).right = CategoryTheory.whiskerLeft (CategoryTheory.CosimplicialObject.Augmented.drop.toPrefunctor.obj A) η

def CategoryTheory.CosimplicialObject.Augmented.whiskering (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u') [CategoryTheory.Category.{v', u'} D] : CategoryTheory.Functor (CategoryTheory.Functor C D) (CategoryTheory.Functor (CategoryTheory.CosimplicialObject.Augmented C) (CategoryTheory.CosimplicialObject.Augmented D))

Functor composition induces a functor on augmented cosimplicial objects.

Equations

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

@[simp]

theorem CategoryTheory.CosimplicialObject.augment_left {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) (X₀ : C) (f : X₀ ⟶ X.toPrefunctor.obj (SimplexCategory.mk 0)) (w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 ⟶ i), CategoryTheory.CategoryStruct.comp f (X.toPrefunctor.map g₁) = CategoryTheory.CategoryStruct.comp f (X.toPrefunctor.map g₂)) : (CategoryTheory.CosimplicialObject.augment X X₀ f w).left = X₀

@[simp]

theorem CategoryTheory.CosimplicialObject.augment_right {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) (X₀ : C) (f : X₀ ⟶ X.toPrefunctor.obj (SimplexCategory.mk 0)) (w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 ⟶ i), CategoryTheory.CategoryStruct.comp f (X.toPrefunctor.map g₁) = CategoryTheory.CategoryStruct.comp f (X.toPrefunctor.map g₂)) : (CategoryTheory.CosimplicialObject.augment X X₀ f w).right = X

@[simp]

theorem CategoryTheory.CosimplicialObject.augment_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) (X₀ : C) (f : X₀ ⟶ X.toPrefunctor.obj (SimplexCategory.mk 0)) (w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 ⟶ i), CategoryTheory.CategoryStruct.comp f (X.toPrefunctor.map g₁) = CategoryTheory.CategoryStruct.comp f (X.toPrefunctor.map g₂)) (i : SimplexCategory) : (CategoryTheory.CosimplicialObject.augment X X₀ f w).hom.app i = CategoryTheory.CategoryStruct.comp f (X.toPrefunctor.map (SimplexCategory.const i 0))

def CategoryTheory.CosimplicialObject.augment {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) (X₀ : C) (f : X₀ ⟶ X.toPrefunctor.obj (SimplexCategory.mk 0)) (w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 ⟶ i), CategoryTheory.CategoryStruct.comp f (X.toPrefunctor.map g₁) = CategoryTheory.CategoryStruct.comp f (X.toPrefunctor.map g₂)) : CategoryTheory.CosimplicialObject.Augmented C

Augment a cosimplicial object with an object.

Equations

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

theorem CategoryTheory.CosimplicialObject.augment_hom_zero {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) (X₀ : C) (f : X₀ ⟶ X.toPrefunctor.obj (SimplexCategory.mk 0)) (w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 ⟶ i), CategoryTheory.CategoryStruct.comp f (X.toPrefunctor.map g₁) = CategoryTheory.CategoryStruct.comp f (X.toPrefunctor.map g₂)) : (CategoryTheory.CosimplicialObject.augment X X₀ f w).hom.app (SimplexCategory.mk 0) = f

@[simp]

theorem CategoryTheory.simplicialCosimplicialEquiv_unitIso_hom_app (C : Type u) [CategoryTheory.Category.{v, u} C] (X : (CategoryTheory.Functor SimplexCategoryᵒᵖ C)ᵒᵖ) : (CategoryTheory.simplicialCosimplicialEquiv C).unitIso.hom.app X = (CategoryTheory.Functor.rightOpLeftOpIso X.unop).hom.op

@[simp]

theorem CategoryTheory.simplicialCosimplicialEquiv_inverse_obj (C : Type u) [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor SimplexCategory Cᵒᵖ) : (CategoryTheory.simplicialCosimplicialEquiv C).inverse.toPrefunctor.obj F = Opposite.op F.leftOp

@[simp]

theorem CategoryTheory.simplicialCosimplicialEquiv_counitIso_inv_app_app (C : Type u) [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor SimplexCategory Cᵒᵖ) (X : SimplexCategory) : ((CategoryTheory.simplicialCosimplicialEquiv C).counitIso.inv.app X✝).app X = CategoryTheory.CategoryStruct.id (X✝.toPrefunctor.obj X)

@[simp]

theorem CategoryTheory.simplicialCosimplicialEquiv_inverse_map (C : Type u) [CategoryTheory.Category.{v, u} C] : ∀ {X Y : CategoryTheory.Functor SimplexCategory Cᵒᵖ} (η : X ⟶ Y), (CategoryTheory.simplicialCosimplicialEquiv C).inverse.toPrefunctor.map η = (CategoryTheory.NatTrans.leftOp η).op

@[simp]

theorem CategoryTheory.simplicialCosimplicialEquiv_functor_obj_map (C : Type u) [CategoryTheory.Category.{v, u} C] (F : (CategoryTheory.Functor SimplexCategoryᵒᵖ C)ᵒᵖ) : ∀ {X Y : SimplexCategory} (f : X ⟶ Y), ((CategoryTheory.simplicialCosimplicialEquiv C).functor.toPrefunctor.obj F).toPrefunctor.map f = (F.unop.toPrefunctor.map f.op).op

@[simp]

theorem CategoryTheory.simplicialCosimplicialEquiv_functor_map_app (C : Type u) [CategoryTheory.Category.{v, u} C] : ∀ {X Y : (CategoryTheory.Functor SimplexCategoryᵒᵖ C)ᵒᵖ} (η : X ⟶ Y) (X_1 : SimplexCategory), ((CategoryTheory.simplicialCosimplicialEquiv C).functor.toPrefunctor.map η).app X_1 = (η.unop.app (Opposite.op X_1)).op

@[simp]

theorem CategoryTheory.simplicialCosimplicialEquiv_functor_obj_obj (C : Type u) [CategoryTheory.Category.{v, u} C] (F : (CategoryTheory.Functor SimplexCategoryᵒᵖ C)ᵒᵖ) (X : SimplexCategory) : ((CategoryTheory.simplicialCosimplicialEquiv C).functor.toPrefunctor.obj F).toPrefunctor.obj X = Opposite.op (F.unop.toPrefunctor.obj (Opposite.op X))

@[simp]

theorem CategoryTheory.simplicialCosimplicialEquiv_counitIso_hom_app_app (C : Type u) [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor SimplexCategory Cᵒᵖ) (X : SimplexCategory) : ((CategoryTheory.simplicialCosimplicialEquiv C).counitIso.hom.app X✝).app X = CategoryTheory.CategoryStruct.id (X✝.toPrefunctor.obj X)

@[simp]

theorem CategoryTheory.simplicialCosimplicialEquiv_unitIso_inv_app (C : Type u) [CategoryTheory.Category.{v, u} C] (X : (CategoryTheory.Functor SimplexCategoryᵒᵖ C)ᵒᵖ) : (CategoryTheory.simplicialCosimplicialEquiv C).unitIso.inv.app X = (CategoryTheory.Functor.rightOpLeftOpIso X.unop).inv.op

def CategoryTheory.simplicialCosimplicialEquiv (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.SimplicialObject C)ᵒᵖ ≌ CategoryTheory.CosimplicialObject Cᵒᵖ

The anti-equivalence between simplicial objects and cosimplicial objects.

Equations

• CategoryTheory.simplicialCosimplicialEquiv C = CategoryTheory.Functor.leftOpRightOpEquiv SimplexCategory C

@[simp]

theorem CategoryTheory.cosimplicialSimplicialEquiv_counitIso_hom_app_app (C : Type u) [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor SimplexCategoryᵒᵖ Cᵒᵖ) (X : SimplexCategoryᵒᵖ) : ((CategoryTheory.cosimplicialSimplicialEquiv C).counitIso.hom.app X✝).app X = CategoryTheory.CategoryStruct.id (X✝.toPrefunctor.obj X)

@[simp]

theorem CategoryTheory.cosimplicialSimplicialEquiv_counitIso_inv_app_app (C : Type u) [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor SimplexCategoryᵒᵖ Cᵒᵖ) (X : SimplexCategoryᵒᵖ) : ((CategoryTheory.cosimplicialSimplicialEquiv C).counitIso.inv.app X✝).app X = CategoryTheory.CategoryStruct.id (X✝.toPrefunctor.obj X)

@[simp]

theorem CategoryTheory.cosimplicialSimplicialEquiv_functor_obj_obj (C : Type u) [CategoryTheory.Category.{v, u} C] (F : (CategoryTheory.Functor SimplexCategory C)ᵒᵖ) (X : SimplexCategoryᵒᵖ) : ((CategoryTheory.cosimplicialSimplicialEquiv C).functor.toPrefunctor.obj F).toPrefunctor.obj X = Opposite.op (F.unop.toPrefunctor.obj X.unop)

@[simp]

theorem CategoryTheory.cosimplicialSimplicialEquiv_unitIso_hom_app (C : Type u) [CategoryTheory.Category.{v, u} C] (X : (CategoryTheory.Functor SimplexCategory C)ᵒᵖ) : (CategoryTheory.cosimplicialSimplicialEquiv C).unitIso.hom.app X = (CategoryTheory.Functor.opUnopIso X.unop).hom.op

@[simp]

theorem CategoryTheory.cosimplicialSimplicialEquiv_functor_obj_map (C : Type u) [CategoryTheory.Category.{v, u} C] (F : (CategoryTheory.Functor SimplexCategory C)ᵒᵖ) : ∀ {X Y : SimplexCategoryᵒᵖ} (f : X ⟶ Y), ((CategoryTheory.cosimplicialSimplicialEquiv C).functor.toPrefunctor.obj F).toPrefunctor.map f = (F.unop.toPrefunctor.map f.unop).op

@[simp]

theorem CategoryTheory.cosimplicialSimplicialEquiv_inverse_obj (C : Type u) [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor SimplexCategoryᵒᵖ Cᵒᵖ) : (CategoryTheory.cosimplicialSimplicialEquiv C).inverse.toPrefunctor.obj F = Opposite.op (CategoryTheory.Functor.unop F)

@[simp]

theorem CategoryTheory.cosimplicialSimplicialEquiv_inverse_map (C : Type u) [CategoryTheory.Category.{v, u} C] : ∀ {X Y : CategoryTheory.Functor SimplexCategoryᵒᵖ Cᵒᵖ} (α : X ⟶ Y), (CategoryTheory.cosimplicialSimplicialEquiv C).inverse.toPrefunctor.map α = (CategoryTheory.NatTrans.mk fun (X_1 : SimplexCategory) => (α.app (Opposite.op X_1)).unop).op

@[simp]

theorem CategoryTheory.cosimplicialSimplicialEquiv_unitIso_inv_app (C : Type u) [CategoryTheory.Category.{v, u} C] (X : (CategoryTheory.Functor SimplexCategory C)ᵒᵖ) : (CategoryTheory.cosimplicialSimplicialEquiv C).unitIso.inv.app X = (CategoryTheory.Functor.opUnopIso X.unop).inv.op

@[simp]

theorem CategoryTheory.cosimplicialSimplicialEquiv_functor_map_app (C : Type u) [CategoryTheory.Category.{v, u} C] : ∀ {X Y : (CategoryTheory.Functor SimplexCategory C)ᵒᵖ} (α : X ⟶ Y) (X_1 : SimplexCategoryᵒᵖ), ((CategoryTheory.cosimplicialSimplicialEquiv C).functor.toPrefunctor.map α).app X_1 = (α.unop.app X_1.unop).op

def CategoryTheory.cosimplicialSimplicialEquiv (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.CosimplicialObject C)ᵒᵖ ≌ CategoryTheory.SimplicialObject Cᵒᵖ

The anti-equivalence between cosimplicial objects and simplicial objects.

Equations

• CategoryTheory.cosimplicialSimplicialEquiv C = CategoryTheory.Functor.opUnopEquiv SimplexCategory C

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.rightOp_right_map {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C) : ∀ {X_1 Y : SimplexCategory} (f : X_1 ⟶ Y), (CategoryTheory.SimplicialObject.Augmented.rightOp X).right.toPrefunctor.map f = (X.left.toPrefunctor.map f.op).op

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.rightOp_left {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C) : (CategoryTheory.SimplicialObject.Augmented.rightOp X).left = Opposite.op X.right

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.rightOp_right_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C) (X : SimplexCategory) : (CategoryTheory.SimplicialObject.Augmented.rightOp X✝).right.toPrefunctor.obj X = Opposite.op (X✝.left.toPrefunctor.obj (Opposite.op X))

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.rightOp_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C) (X : SimplexCategory) : (CategoryTheory.SimplicialObject.Augmented.rightOp X✝).hom.app X = (X✝.hom.app (Opposite.op X)).op

def CategoryTheory.SimplicialObject.Augmented.rightOp {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C) : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ

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

Equations

• CategoryTheory.SimplicialObject.Augmented.rightOp X = { left := Opposite.op X.right, right := X.left.rightOp, hom := CategoryTheory.NatTrans.rightOp X.hom }

@[simp]

theorem CategoryTheory.CosimplicialObject.Augmented.leftOp_right {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ) : (CategoryTheory.CosimplicialObject.Augmented.leftOp X).right = X.left.unop

@[simp]

theorem CategoryTheory.CosimplicialObject.Augmented.leftOp_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ) (X : SimplexCategoryᵒᵖ) : (CategoryTheory.CosimplicialObject.Augmented.leftOp X✝).hom.app X = (X✝.hom.app X.unop).unop

@[simp]

theorem CategoryTheory.CosimplicialObject.Augmented.leftOp_left_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ) (X : SimplexCategoryᵒᵖ) : (CategoryTheory.CosimplicialObject.Augmented.leftOp X✝).left.toPrefunctor.obj X = (X✝.right.toPrefunctor.obj X.unop).unop

@[simp]

theorem CategoryTheory.CosimplicialObject.Augmented.leftOp_left_map {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ) : ∀ {X_1 Y : SimplexCategoryᵒᵖ} (f : X_1 ⟶ Y), (CategoryTheory.CosimplicialObject.Augmented.leftOp X).left.toPrefunctor.map f = (X.right.toPrefunctor.map f.unop).unop

def CategoryTheory.CosimplicialObject.Augmented.leftOp {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ) : CategoryTheory.SimplicialObject.Augmented C

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

Equations

• CategoryTheory.CosimplicialObject.Augmented.leftOp X = { left := X.right.leftOp, right := X.left.unop, hom := CategoryTheory.NatTrans.leftOp X.hom }

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso_inv_right {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C) : (CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso X).inv.right = CategoryTheory.CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso_hom_left_app {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C) (X : SimplexCategoryᵒᵖ) : (CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso X✝).hom.left.app X = CategoryTheory.CategoryStruct.id (X✝.left.toPrefunctor.obj X)

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso_inv_left_app {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C) (X : SimplexCategoryᵒᵖ) : (CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso X✝).inv.left.app X = CategoryTheory.CategoryStruct.id (X✝.left.toPrefunctor.obj X)

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso_hom_right {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C) : (CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso X).hom.right = CategoryTheory.CategoryStruct.id X.right

def CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C) : CategoryTheory.CosimplicialObject.Augmented.leftOp (CategoryTheory.SimplicialObject.Augmented.rightOp X) ≅ X

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

Equations

• CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso X = CategoryTheory.Comma.isoMk (CategoryTheory.Functor.rightOpLeftOpIso X.left) (CategoryTheory.eqToIso (_ : X.right = X.right))

@[simp]

theorem CategoryTheory.CosimplicialObject.Augmented.leftOpRightOpIso_inv_left {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ) : (CategoryTheory.CosimplicialObject.Augmented.leftOpRightOpIso X).inv.left = CategoryTheory.CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.CosimplicialObject.Augmented.leftOpRightOpIso_hom_right_app {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ) (X : SimplexCategory) : (CategoryTheory.CosimplicialObject.Augmented.leftOpRightOpIso X✝).hom.right.app X = CategoryTheory.CategoryStruct.id (X✝.right.toPrefunctor.obj X)

@[simp]

theorem CategoryTheory.CosimplicialObject.Augmented.leftOpRightOpIso_hom_left {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ) : (CategoryTheory.CosimplicialObject.Augmented.leftOpRightOpIso X).hom.left = CategoryTheory.CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.CosimplicialObject.Augmented.leftOpRightOpIso_inv_right_app {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ) (X : SimplexCategory) : (CategoryTheory.CosimplicialObject.Augmented.leftOpRightOpIso X✝).inv.right.app X = CategoryTheory.CategoryStruct.id (X✝.right.toPrefunctor.obj X)

def CategoryTheory.CosimplicialObject.Augmented.leftOpRightOpIso {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ) : CategoryTheory.SimplicialObject.Augmented.rightOp (CategoryTheory.CosimplicialObject.Augmented.leftOp X) ≅ X

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

Equations

• CategoryTheory.CosimplicialObject.Augmented.leftOpRightOpIso X = CategoryTheory.Comma.isoMk (CategoryTheory.eqToIso (_ : X.left = X.left)) (CategoryTheory.Functor.leftOpRightOpIso X.right)

@[simp]

theorem CategoryTheory.simplicialToCosimplicialAugmented_obj (C : Type u) [CategoryTheory.Category.{v, u} C] (X : (CategoryTheory.SimplicialObject.Augmented C)ᵒᵖ) : (CategoryTheory.simplicialToCosimplicialAugmented C).toPrefunctor.obj X = CategoryTheory.SimplicialObject.Augmented.rightOp X.unop

@[simp]

theorem CategoryTheory.simplicialToCosimplicialAugmented_map_right (C : Type u) [CategoryTheory.Category.{v, u} C] : ∀ {X Y : (CategoryTheory.SimplicialObject.Augmented C)ᵒᵖ} (f : X ⟶ Y), ((CategoryTheory.simplicialToCosimplicialAugmented C).toPrefunctor.map f).right = CategoryTheory.NatTrans.rightOp f.unop.left

@[simp]

theorem CategoryTheory.simplicialToCosimplicialAugmented_map_left (C : Type u) [CategoryTheory.Category.{v, u} C] : ∀ {X Y : (CategoryTheory.SimplicialObject.Augmented C)ᵒᵖ} (f : X ⟶ Y), ((CategoryTheory.simplicialToCosimplicialAugmented C).toPrefunctor.map f).left = f.unop.right.op

def CategoryTheory.simplicialToCosimplicialAugmented (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (CategoryTheory.SimplicialObject.Augmented C)ᵒᵖ (CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ)

A functorial version of SimplicialObject.Augmented.rightOp.

Equations

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

@[simp]

theorem CategoryTheory.cosimplicialToSimplicialAugmented_map (C : Type u) [CategoryTheory.Category.{v, u} C] : ∀ {X Y : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ} (f : X ⟶ Y), (CategoryTheory.cosimplicialToSimplicialAugmented C).toPrefunctor.map f = (CategoryTheory.CommaMorphism.mk (CategoryTheory.NatTrans.leftOp f.right) f.left.unop).op

@[simp]

theorem CategoryTheory.cosimplicialToSimplicialAugmented_obj (C : Type u) [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ) : (CategoryTheory.cosimplicialToSimplicialAugmented C).toPrefunctor.obj X = Opposite.op (CategoryTheory.CosimplicialObject.Augmented.leftOp X)

def CategoryTheory.cosimplicialToSimplicialAugmented (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ) (CategoryTheory.SimplicialObject.Augmented C)ᵒᵖ

A functorial version of Cosimplicial_object.Augmented.leftOp.

Equations

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

@[simp]

theorem CategoryTheory.simplicialCosimplicialAugmentedEquiv_functor (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.simplicialCosimplicialAugmentedEquiv C).functor = CategoryTheory.simplicialToCosimplicialAugmented C

@[simp]

theorem CategoryTheory.simplicialCosimplicialAugmentedEquiv_inverse (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.simplicialCosimplicialAugmentedEquiv C).inverse = CategoryTheory.cosimplicialToSimplicialAugmented C

def CategoryTheory.simplicialCosimplicialAugmentedEquiv (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.SimplicialObject.Augmented C)ᵒᵖ ≌ CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ

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.