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_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.obj X)

@[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)

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__[_]».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

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.

instance CategoryTheory.SimplicialObject.instHasLimitsOfShape (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

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance CategoryTheory.SimplicialObject.instHasColimitsOfShape (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

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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.obj { unop := SimplexCategory.mk (n + 1) } ⟶ X.obj { unop := SimplexCategory.mk n }

Face maps for a simplicial object.

Equations

• X.δ i = X.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.obj { unop := SimplexCategory.mk n } ⟶ X.obj { unop := SimplexCategory.mk (n + 1) }

Degeneracy maps for a simplicial object.

Equations

• X.σ i = X.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.obj { unop := SimplexCategory.mk n } ≅ X.obj { unop := SimplexCategory.mk m }

Isomorphisms from identities in ℕ.

Equations

• X.eqToIso h = CategoryTheory.Functor.mapIso X (CategoryTheory.eqToIso ⋯)

@[simp]

theorem CategoryTheory.SimplicialObject.eqToIso_refl {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} (h : n = n) : X.eqToIso h = CategoryTheory.Iso.refl (X.obj { unop := 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.obj { unop := SimplexCategory.mk n } ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.δ j.succ) (CategoryTheory.CategoryStruct.comp (X.δ i) h) = CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) (CategoryTheory.CategoryStruct.comp (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 (X.δ j.succ) (X.δ i) = CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) (X.δ j)

The generic case of the first simplicial identity

theorem CategoryTheory.SimplicialObject.δ_comp_δ'_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : i.castSucc < j) {Z : C} (h : X.obj { unop := SimplexCategory.mk n } ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.δ j) (CategoryTheory.CategoryStruct.comp (X.δ i) h) = CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) (CategoryTheory.CategoryStruct.comp (X.δ (j.pred ⋯)) 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 : i.castSucc < j) : CategoryTheory.CategoryStruct.comp (X.δ j) (X.δ i) = CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) (X.δ (j.pred ⋯))

theorem CategoryTheory.SimplicialObject.δ_comp_δ''_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : i ≤ j.castSucc) {Z : C} (h : X.obj { unop := SimplexCategory.mk n } ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.δ j.succ) (CategoryTheory.CategoryStruct.comp (X.δ (i.castLT ⋯)) h) = CategoryTheory.CategoryStruct.comp (X.δ i) (CategoryTheory.CategoryStruct.comp (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 ≤ j.castSucc) : CategoryTheory.CategoryStruct.comp (X.δ j.succ) (X.δ (i.castLT ⋯)) = CategoryTheory.CategoryStruct.comp (X.δ i) (X.δ j)

theorem CategoryTheory.SimplicialObject.δ_comp_δ_self_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {i : Fin (n + 2)} {Z : C} (h : X.obj { unop := SimplexCategory.mk n } ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) (CategoryTheory.CategoryStruct.comp (X.δ i) h) = CategoryTheory.CategoryStruct.comp (X.δ i.succ) (CategoryTheory.CategoryStruct.comp (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 (X.δ i.castSucc) (X.δ i) = CategoryTheory.CategoryStruct.comp (X.δ i.succ) (X.δ i)

The special case of the first simplicial identity

theorem CategoryTheory.SimplicialObject.δ_comp_δ_self'_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {j : Fin (n + 3)} {i : Fin (n + 2)} (H : j = i.castSucc) {Z : C} (h : X.obj { unop := SimplexCategory.mk n } ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.δ j) (CategoryTheory.CategoryStruct.comp (X.δ i) h) = CategoryTheory.CategoryStruct.comp (X.δ i.succ) (CategoryTheory.CategoryStruct.comp (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 = i.castSucc) : CategoryTheory.CategoryStruct.comp (X.δ j) (X.δ i) = CategoryTheory.CategoryStruct.comp (X.δ i.succ) (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 ≤ j.castSucc) {Z : C} (h : X.obj { unop := SimplexCategory.mk (n + 1) } ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.σ j.succ) (CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) h) = CategoryTheory.CategoryStruct.comp (X.δ i) (CategoryTheory.CategoryStruct.comp (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 ≤ j.castSucc) : CategoryTheory.CategoryStruct.comp (X.σ j.succ) (X.δ i.castSucc) = CategoryTheory.CategoryStruct.comp (X.δ i) (X.σ j)

The second simplicial identity

theorem CategoryTheory.SimplicialObject.δ_comp_σ_self_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {i : Fin (n + 1)} {Z : C} (h : X.obj { unop := SimplexCategory.mk n } ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.σ i) (CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) 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 (X.σ i) (X.δ i.castSucc) = CategoryTheory.CategoryStruct.id (X.obj { unop := 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 = i.castSucc) {Z : C} (h : X.obj { unop := SimplexCategory.mk n } ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.σ i) (CategoryTheory.CategoryStruct.comp (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 = i.castSucc) : CategoryTheory.CategoryStruct.comp (X.σ i) (X.δ j) = CategoryTheory.CategoryStruct.id (X.obj { unop := 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.obj { unop := SimplexCategory.mk n } ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.σ i) (CategoryTheory.CategoryStruct.comp (X.δ i.succ) 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 (X.σ i) (X.δ i.succ) = CategoryTheory.CategoryStruct.id (X.obj { unop := 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 = i.succ) {Z : C} (h : X.obj { unop := SimplexCategory.mk n } ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.σ i) (CategoryTheory.CategoryStruct.comp (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 = i.succ) : CategoryTheory.CategoryStruct.comp (X.σ i) (X.δ j) = CategoryTheory.CategoryStruct.id (X.obj { unop := 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 : j.castSucc < i) {Z : C} (h : X.obj { unop := SimplexCategory.mk (n + 1) } ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.σ j.castSucc) (CategoryTheory.CategoryStruct.comp (X.δ i.succ) h) = CategoryTheory.CategoryStruct.comp (X.δ i) (CategoryTheory.CategoryStruct.comp (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 : j.castSucc < i) : CategoryTheory.CategoryStruct.comp (X.σ j.castSucc) (X.δ i.succ) = CategoryTheory.CategoryStruct.comp (X.δ i) (X.σ j)

The fourth simplicial identity

theorem CategoryTheory.SimplicialObject.δ_comp_σ_of_gt'_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ < i) {Z : C} (h : X.obj { unop := SimplexCategory.mk (n + 1) } ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.σ j) (CategoryTheory.CategoryStruct.comp (X.δ i) h) = CategoryTheory.CategoryStruct.comp (X.δ (i.pred ⋯)) (CategoryTheory.CategoryStruct.comp (X.σ (j.castLT ⋯)) 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 : j.succ < i) : CategoryTheory.CategoryStruct.comp (X.σ j) (X.δ i) = CategoryTheory.CategoryStruct.comp (X.δ (i.pred ⋯)) (X.σ (j.castLT ⋯))

theorem CategoryTheory.SimplicialObject.σ_comp_σ_assoc {C : Type u} [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.obj { unop := SimplexCategory.mk (n + 1 + 1) } ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.σ j) (CategoryTheory.CategoryStruct.comp (X.σ i.castSucc) h) = CategoryTheory.CategoryStruct.comp (X.σ i) (CategoryTheory.CategoryStruct.comp (X.σ j.succ) 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 (X.σ j) (X.σ i.castSucc) = CategoryTheory.CategoryStruct.comp (X.σ i) (X.σ j.succ)

The fifth simplicial identity

@[simp]

theorem CategoryTheory.SimplicialObject.δ_naturality_assoc {C : Type u} [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'.obj { unop := SimplexCategory.mk n } ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.δ i) (CategoryTheory.CategoryStruct.comp (f.app { unop := SimplexCategory.mk n }) h) = CategoryTheory.CategoryStruct.comp (f.app { unop := SimplexCategory.mk (n + 1) }) (CategoryTheory.CategoryStruct.comp (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 (X.δ i) (f.app { unop := SimplexCategory.mk n }) = CategoryTheory.CategoryStruct.comp (f.app { unop := SimplexCategory.mk (n + 1) }) (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'.obj { unop := SimplexCategory.mk (n + 1) } ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.σ i) (CategoryTheory.CategoryStruct.comp (f.app { unop := SimplexCategory.mk (n + 1) }) h) = CategoryTheory.CategoryStruct.comp (f.app { unop := SimplexCategory.mk n }) (CategoryTheory.CategoryStruct.comp (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 (X.σ i) (f.app { unop := SimplexCategory.mk (n + 1) }) = CategoryTheory.CategoryStruct.comp (f.app { unop := SimplexCategory.mk n }) (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).map τ).app F).app c = τ.app (F.obj c)

@[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).obj H).obj F).map f = H.map (F.map f)

@[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).obj H).obj F).obj X = H.obj (F.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).obj H).map α).app X_1 = H.map (α.app X_1)

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.instHasLimitsOfShape {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

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance CategoryTheory.SimplicialObject.Truncated.instHasColimitsOfShape {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

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[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).map τ).app F).app c = τ.app (F.obj c)

@[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).obj H).obj F).obj X = H.obj (F.obj X)

@[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).obj H).obj F).map f = H.map (F.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).obj H).map α).app X_1 = H.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).obj SimplexCategory.Truncated.inclusion.op

@[reducible, inline]

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_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)

@[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.obj X)

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

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_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.map f = f.left

@[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.obj X = X.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_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.map f = f.right

@[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.obj X = X.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_map_right {C : Type u} [CategoryTheory.Category.{v, u} C] : ∀ {X Y : CategoryTheory.SimplicialObject.Augmented C} (η : X ⟶ Y), (CategoryTheory.SimplicialObject.Augmented.toArrow.map η).right = CategoryTheory.SimplicialObject.Augmented.point.map η

@[simp]

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

@[simp]

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

@[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.map η).left = (CategoryTheory.SimplicialObject.Augmented.drop.map η).app { unop := SimplexCategory.mk 0 }

@[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.obj X).left = (CategoryTheory.SimplicialObject.Augmented.drop.obj X).obj { unop := 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).obj Y.right).obj { unop := SimplexCategory.mk 0 } ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.SimplicialObject.Augmented.drop.map f).app { unop := SimplexCategory.mk 0 }) (CategoryTheory.CategoryStruct.comp (Y.hom.app { unop := SimplexCategory.mk 0 }) h) = CategoryTheory.CategoryStruct.comp (X.hom.app { unop := SimplexCategory.mk 0 }) (CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.Augmented.point.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.map f).app { unop := SimplexCategory.mk 0 }) (Y.hom.app { unop := SimplexCategory.mk 0 }) = CategoryTheory.CategoryStruct.comp (X.hom.app { unop := SimplexCategory.mk 0 }) (CategoryTheory.SimplicialObject.Augmented.point.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).map η).app A).left = CategoryTheory.whiskerLeft (CategoryTheory.SimplicialObject.Augmented.drop.obj A) η

@[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).map η).app A).right = η.app (CategoryTheory.SimplicialObject.Augmented.point.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).obj F = CategoryTheory.SimplicialObject.Augmented.whiskeringObj C D F

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.obj { unop := SimplexCategory.mk 0 } ⟶ X₀) (w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 ⟶ i), CategoryTheory.CategoryStruct.comp (X.map g₁.op) f = CategoryTheory.CategoryStruct.comp (X.map g₂.op) f) : (X.augment X₀ f w).right = X₀

@[simp]

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

@[simp]

theorem CategoryTheory.SimplicialObject.augment_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) (X₀ : C) (f : X.obj { unop := SimplexCategory.mk 0 } ⟶ X₀) (w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 ⟶ i), CategoryTheory.CategoryStruct.comp (X.map g₁.op) f = CategoryTheory.CategoryStruct.comp (X.map g₂.op) f) (i : SimplexCategoryᵒᵖ) : (X.augment X₀ f w).hom.app i = CategoryTheory.CategoryStruct.comp (X.map ((SimplexCategory.mk 0).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.obj { unop := SimplexCategory.mk 0 } ⟶ X₀) (w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 ⟶ i), CategoryTheory.CategoryStruct.comp (X.map g₁.op) f = CategoryTheory.CategoryStruct.comp (X.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.obj { unop := SimplexCategory.mk 0 } ⟶ X₀) (w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 ⟶ i), CategoryTheory.CategoryStruct.comp (X.map g₁.op) f = CategoryTheory.CategoryStruct.comp (X.map g₂.op) f) : (X.augment X₀ f w).hom.app { unop := 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_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.obj X)

@[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)

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.instHasLimitsOfShape (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

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance CategoryTheory.CosimplicialObject.instHasColimitsOfShape (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

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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.obj (SimplexCategory.mk n) ⟶ X.obj (SimplexCategory.mk (n + 1))

Coface maps for a cosimplicial object.

Equations

• X.δ i = X.map (SimplexCategory.δ i)

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

Codegeneracy maps for a cosimplicial object.

Equations

• X.σ i = X.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.obj (SimplexCategory.mk n) ≅ X.obj (SimplexCategory.mk m)

Isomorphisms from identities in ℕ.

Equations

• X.eqToIso h = CategoryTheory.Functor.mapIso X (CategoryTheory.eqToIso ⋯)

@[simp]

theorem CategoryTheory.CosimplicialObject.eqToIso_refl {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} (h : n = n) : X.eqToIso h = CategoryTheory.Iso.refl (X.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.obj (SimplexCategory.mk (n + 1 + 1)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.δ i) (CategoryTheory.CategoryStruct.comp (X.δ j.succ) h) = CategoryTheory.CategoryStruct.comp (X.δ j) (CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) 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 (X.δ i) (X.δ j.succ) = CategoryTheory.CategoryStruct.comp (X.δ j) (X.δ i.castSucc)

The generic case of the first cosimplicial identity

theorem CategoryTheory.CosimplicialObject.δ_comp_δ'_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : i.castSucc < j) {Z : C} (h : X.obj (SimplexCategory.mk (n + 1 + 1)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.δ i) (CategoryTheory.CategoryStruct.comp (X.δ j) h) = CategoryTheory.CategoryStruct.comp (X.δ (j.pred ⋯)) (CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) 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 : i.castSucc < j) : CategoryTheory.CategoryStruct.comp (X.δ i) (X.δ j) = CategoryTheory.CategoryStruct.comp (X.δ (j.pred ⋯)) (X.δ i.castSucc)

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

The special case of the first cosimplicial identity

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

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 ≤ j.castSucc) {Z : C} (h : X.obj (SimplexCategory.mk (n + 1)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) (CategoryTheory.CategoryStruct.comp (X.σ j.succ) h) = CategoryTheory.CategoryStruct.comp (X.σ j) (CategoryTheory.CategoryStruct.comp (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 ≤ j.castSucc) : CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) (X.σ j.succ) = CategoryTheory.CategoryStruct.comp (X.σ j) (X.δ i)

The second cosimplicial identity

theorem CategoryTheory.CosimplicialObject.δ_comp_σ_self_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {i : Fin (n + 1)} {Z : C} (h : X.obj (SimplexCategory.mk n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) (CategoryTheory.CategoryStruct.comp (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 (X.δ i.castSucc) (X.σ i) = CategoryTheory.CategoryStruct.id (X.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 = i.castSucc) {Z : C} (h : X.obj (SimplexCategory.mk n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.δ j) (CategoryTheory.CategoryStruct.comp (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 = i.castSucc) : CategoryTheory.CategoryStruct.comp (X.δ j) (X.σ i) = CategoryTheory.CategoryStruct.id (X.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.obj (SimplexCategory.mk n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.δ i.succ) (CategoryTheory.CategoryStruct.comp (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 (X.δ i.succ) (X.σ i) = CategoryTheory.CategoryStruct.id (X.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 = i.succ) {Z : C} (h : X.obj (SimplexCategory.mk n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.δ j) (CategoryTheory.CategoryStruct.comp (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 = i.succ) : CategoryTheory.CategoryStruct.comp (X.δ j) (X.σ i) = CategoryTheory.CategoryStruct.id (X.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 : j.castSucc < i) {Z : C} (h : X.obj (SimplexCategory.mk (n + 1)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.δ i.succ) (CategoryTheory.CategoryStruct.comp (X.σ j.castSucc) h) = CategoryTheory.CategoryStruct.comp (X.σ j) (CategoryTheory.CategoryStruct.comp (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 : j.castSucc < i) : CategoryTheory.CategoryStruct.comp (X.δ i.succ) (X.σ j.castSucc) = CategoryTheory.CategoryStruct.comp (X.σ j) (X.δ i)

The fourth cosimplicial identity

theorem CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt'_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ < i) {Z : C} (h : X.obj (SimplexCategory.mk (n + 1)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.δ i) (CategoryTheory.CategoryStruct.comp (X.σ j) h) = CategoryTheory.CategoryStruct.comp (X.σ (j.castLT ⋯)) (CategoryTheory.CategoryStruct.comp (X.δ (i.pred ⋯)) 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 : j.succ < i) : CategoryTheory.CategoryStruct.comp (X.δ i) (X.σ j) = CategoryTheory.CategoryStruct.comp (X.σ (j.castLT ⋯)) (X.δ (i.pred ⋯))

theorem CategoryTheory.CosimplicialObject.σ_comp_σ_assoc {C : Type u} [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.obj (SimplexCategory.mk n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.σ i.castSucc) (CategoryTheory.CategoryStruct.comp (X.σ j) h) = CategoryTheory.CategoryStruct.comp (X.σ j.succ) (CategoryTheory.CategoryStruct.comp (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 (X.σ i.castSucc) (X.σ j) = CategoryTheory.CategoryStruct.comp (X.σ j.succ) (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'.obj (SimplexCategory.mk (n + 1)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.δ i) (CategoryTheory.CategoryStruct.comp (f.app (SimplexCategory.mk (n + 1))) h) = CategoryTheory.CategoryStruct.comp (f.app (SimplexCategory.mk n)) (CategoryTheory.CategoryStruct.comp (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 (X.δ i) (f.app (SimplexCategory.mk (n + 1))) = CategoryTheory.CategoryStruct.comp (f.app (SimplexCategory.mk n)) (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'.obj (SimplexCategory.mk n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.σ i) (CategoryTheory.CategoryStruct.comp (f.app (SimplexCategory.mk n)) h) = CategoryTheory.CategoryStruct.comp (f.app (SimplexCategory.mk (n + 1))) (CategoryTheory.CategoryStruct.comp (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 (X.σ i) (f.app (SimplexCategory.mk n)) = CategoryTheory.CategoryStruct.comp (f.app (SimplexCategory.mk (n + 1))) (X'.σ i)

@[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).obj H).obj F).map f = H.map (F.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).obj H).map α).app X_1 = H.map (α.app X_1)

@[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).map τ).app F).app c = τ.app (F.obj c)

@[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).obj H).obj F).obj X = H.obj (F.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.instHasLimitsOfShape {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

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance CategoryTheory.CosimplicialObject.Truncated.instHasColimitsOfShape {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

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[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).obj H).map α).app X_1 = H.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).map τ).app F).app c = τ.app (F.obj c)

@[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).obj H).obj F).obj X = H.obj (F.obj X)

@[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).obj H).obj F).map f = H.map (F.map f)

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).obj SimplexCategory.Truncated.inclusion

@[reducible, inline]

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_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_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_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.obj X)

@[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

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_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.map f = f.right

@[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.obj X = X.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_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.obj X = X.left

@[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.map f = f.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_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented C) : (CategoryTheory.CosimplicialObject.Augmented.toArrow.obj X).hom = X.hom.app (SimplexCategory.mk 0)

@[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.obj X).left = X.left

@[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.map η).right = η.right.app (SimplexCategory.mk 0)

@[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.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.obj X).right = X.right.obj (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_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).map η).app A).right = CategoryTheory.whiskerLeft (CategoryTheory.CosimplicialObject.Augmented.drop.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).obj F = CategoryTheory.CosimplicialObject.Augmented.whiskeringObj C D F

@[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).map η).app A).left = η.app (CategoryTheory.CosimplicialObject.Augmented.point.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_right {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) (X₀ : C) (f : X₀ ⟶ X.obj (SimplexCategory.mk 0)) (w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 ⟶ i), CategoryTheory.CategoryStruct.comp f (X.map g₁) = CategoryTheory.CategoryStruct.comp f (X.map g₂)) : (X.augment X₀ f w).right = X

@[simp]

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

@[simp]

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

def CategoryTheory.CosimplicialObject.augment {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) (X₀ : C) (f : X₀ ⟶ X.obj (SimplexCategory.mk 0)) (w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 ⟶ i), CategoryTheory.CategoryStruct.comp f (X.map g₁) = CategoryTheory.CategoryStruct.comp f (X.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.obj (SimplexCategory.mk 0)) (w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 ⟶ i), CategoryTheory.CategoryStruct.comp f (X.map g₁) = CategoryTheory.CategoryStruct.comp f (X.map g₂)) : (X.augment X₀ f w).hom.app (SimplexCategory.mk 0) = f

@[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.map η).app X_1 = (η.unop.app { unop := X_1 }).op

@[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 = X.unop.rightOpLeftOpIso.inv.op

@[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✝.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.map η = (CategoryTheory.NatTrans.leftOp η).op

@[simp]

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

@[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✝.obj X)

@[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 = X.unop.rightOpLeftOpIso.hom.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.obj F).obj X = { unop := F.unop.obj { unop := X } }

@[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.obj F).map f = (F.unop.map f.op).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✝.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.obj F).obj X = { unop := F.unop.obj X.unop }

@[simp]

theorem CategoryTheory.cosimplicialSimplicialEquiv_inverse_obj (C : Type u) [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor SimplexCategoryᵒᵖ Cᵒᵖ) : (CategoryTheory.cosimplicialSimplicialEquiv C).inverse.obj F = { unop := F.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 = X.unop.opUnopIso.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.obj F).map f = (F.unop.map f.unop).op

@[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.map α = Quiver.Hom.op { app := fun (X_1 : SimplexCategory) => (α.app { unop := X_1 }).unop, naturality := ⋯ }

@[simp]

theorem CategoryTheory.cosimplicialSimplicialEquiv_counitIso_inv_app_app (C : Type u) [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✝.obj X)

@[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 = X.unop.opUnopIso.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.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_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C) (X : SimplexCategory) : X✝.rightOp.hom.app X = (X✝.hom.app { unop := X }).op

@[simp]

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

@[simp]

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

@[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), X.rightOp.right.map f = (X.left.map f.op).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

• X.rightOp = { left := { unop := X.right }, right := CategoryTheory.Functor.rightOp X.left, hom := CategoryTheory.NatTrans.rightOp X.hom }

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.CosimplicialObject.Augmented.leftOp_left_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ) (X : SimplexCategoryᵒᵖ) : X✝.leftOp.left.obj X = (X✝.right.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), X.leftOp.left.map f = (X.right.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

• X.leftOp = { left := CategoryTheory.Functor.leftOp X.right, 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) : X.rightOpLeftOpIso.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ᵒᵖ) : X✝.rightOpLeftOpIso.hom.left.app X = CategoryTheory.CategoryStruct.id (X✝.left.obj X)

@[simp]

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

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso_hom_right {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C) : X.rightOpLeftOpIso.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) : X.rightOp.leftOp ≅ X

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

Equations

• X.rightOpLeftOpIso = CategoryTheory.Comma.isoMk (CategoryTheory.Functor.rightOpLeftOpIso X.left) (CategoryTheory.eqToIso ⋯) ⋯

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.CosimplicialObject.Augmented.leftOpRightOpIso_inv_left {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ) : X.leftOpRightOpIso.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) : X✝.leftOpRightOpIso.hom.right.app X = CategoryTheory.CategoryStruct.id (X✝.right.obj X)

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

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

Equations

• X.leftOpRightOpIso = CategoryTheory.Comma.isoMk (CategoryTheory.eqToIso ⋯) (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).obj X = X.unop.rightOp

@[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).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).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_obj (C : Type u) [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ) : (CategoryTheory.cosimplicialToSimplicialAugmented C).obj X = { unop := X.leftOp }

@[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).map f = Quiver.Hom.op { left := CategoryTheory.NatTrans.leftOp f.right, right := f.left.unop, w := ⋯ }

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_inverse (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.simplicialCosimplicialAugmentedEquiv C).inverse = CategoryTheory.cosimplicialToSimplicialAugmented C

@[simp]

theorem CategoryTheory.simplicialCosimplicialAugmentedEquiv_functor (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.simplicialCosimplicialAugmentedEquiv C).functor = CategoryTheory.simplicialToCosimplicialAugmented 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.