Simplicial objects in a category.

A simplicial object in a category C is a C-valued presheaf on SimplexCategory. (Similarly, a cosimplicial object is a functor SimplexCategory ⥤ C.)

Notation

The following notations can be enabled via open Simplicial.

• X _⦋n⦌ denotes the n-th term of a simplicial object X, where n : ℕ.
• X ^⦋n⦌ denotes the n-th term of a cosimplicial object X, where n : ℕ.

The following notations can be enabled via open CategoryTheory.SimplicialObject.Truncated.

• X _⦋m⦌ₙ denotes the m-th term of an n-truncated simplicial object X.
• X ^⦋m⦌ₙ denotes the m-th term of an n-truncated cosimplicial object X.

def CategoryTheory.SimplicialObject (C : Type u) [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

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

Equations

• CategoryTheory.instCategorySimplicialObject C = id inferInstance

@[simp]

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

@[simp]

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

def Simplicial.«term__⦋_⦌».«delab_app.Prefunctor.obj» : 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) [Category.{v, u} C] {J : Type v} [SmallCategory J] [Limits.HasLimitsOfShape J C] : Limits.HasLimitsOfShape J (SimplicialObject C)

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

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

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

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

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

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

Face maps for a simplicial object.

Equations

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

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

Degeneracy maps for a simplicial object.

Equations

• X.σ i = X.map (SimplexCategory.σ i).op

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

The diagonal of a simplex is the long edge of the simplex.

Equations

• X.diagonal = X.map (SimplexCategory.diag n).op

def CategoryTheory.SimplicialObject.eqToIso {C : Type u} [Category.{v, u} C] (X : SimplicialObject C) {n m : ℕ} (h : n = m) : X.obj (Opposite.op (SimplexCategory.mk n)) ≅ X.obj (Opposite.op (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} [Category.{v, u} C] (X : SimplicialObject C) {n : ℕ} (h : n = n) : X.eqToIso h = Iso.refl (X.obj (Opposite.op (SimplexCategory.mk n)))

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

The generic case of the first simplicial identity

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

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

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

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

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

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

The special case of the first simplicial identity

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

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

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

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

The second simplicial identity

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

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

The first part of the third simplicial identity

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

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

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

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

The second part of the third simplicial identity

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

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

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

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

The fourth simplicial identity

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

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

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

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

The fifth simplicial identity

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Functor composition induces a functor on simplicial objects.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.SimplicialObject.Truncated (C : Type u) [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) [Category.{v, u} C] {n : ℕ} : Category.{v, max u v} (Truncated C n)

Equations

• CategoryTheory.SimplicialObject.instCategoryTruncated C = id inferInstance

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

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

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

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

def CategoryTheory.SimplicialObject.Truncated.whiskering (C : Type u) [Category.{v, u} C] {n : ℕ} (D : Type u_1) [Category.{u_2, u_1} D] : Functor (Functor C D) (Functor (Truncated C n) (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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.SimplicialObject.Truncated.mkNotation : Lean.TrailingParserDescr

For X : Truncated C n and m ≤ n, X _⦋m⦌ₙ is the m-th term of X. The proof p : m ≤ n can also be provided using the syntax X _⦋m, p⦌ₙ.

Equations

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

def CategoryTheory.SimplicialObject.Truncated.trunc (C : Type u) [Category.{v, u} C] (n m : ℕ) (h : m ≤ n := by omega) : Functor (Truncated C n) (Truncated C m)

Further truncation of truncated simplicial objects.

Equations

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

@[simp]

theorem CategoryTheory.SimplicialObject.Truncated.trunc_obj_obj (C : Type u) [Category.{v, u} C] (n m : ℕ) (h : m ≤ n := by omega) (G : Functor (SimplexCategory.Truncated n)ᵒᵖ C) (X : (SimplexCategory.Truncated m)ᵒᵖ) : ((trunc C n m h).obj G).obj X = G.obj (Opposite.op ((SimplexCategory.Truncated.incl m n h).obj (Opposite.unop X)))

@[simp]

theorem CategoryTheory.SimplicialObject.Truncated.trunc_obj_map (C : Type u) [Category.{v, u} C] (n m : ℕ) (h : m ≤ n := by omega) (G : Functor (SimplexCategory.Truncated n)ᵒᵖ C) {X✝ Y✝ : (SimplexCategory.Truncated m)ᵒᵖ} (f : X✝ ⟶ Y✝) : ((trunc C n m h).obj G).map f = G.map ((SimplexCategory.Truncated.incl m n h).map f.unop).op

@[simp]

theorem CategoryTheory.SimplicialObject.Truncated.trunc_map_app (C : Type u) [Category.{v, u} C] (n m : ℕ) (h : m ≤ n := by omega) {X✝ Y✝ : Functor (SimplexCategory.Truncated n)ᵒᵖ C} (α : X✝ ⟶ Y✝) (X : (SimplexCategory.Truncated m)ᵒᵖ) : ((trunc C n m h).map α).app X = α.app (Opposite.op ((SimplexCategory.Truncated.incl m n h).obj (Opposite.unop X)))

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

The truncation functor from simplicial objects to truncated simplicial objects.

Equations

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

def CategoryTheory.SimplicialObject.truncationCompTrunc {C : Type u} [Category.{v, u} C] {n m : ℕ} (h : m ≤ n) : (truncation n).comp (Truncated.trunc C n m h) ≅ truncation m

For all m ≤ n, truncation m factors through Truncated n.

Equations

• CategoryTheory.SimplicialObject.truncationCompTrunc h = CategoryTheory.Iso.refl ((CategoryTheory.SimplicialObject.truncation n).comp (CategoryTheory.SimplicialObject.Truncated.trunc C n m h))

@[reducible, inline]

abbrev CategoryTheory.SimplicialObject.Truncated.sk {C : Type u} [Category.{v, u} C] (n : ℕ) [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F] : Functor (Truncated C n) (SimplicialObject C)

The n-skeleton as a functor SimplicialObject.Truncated C n ⥤ SimplicialObject C.

Equations

• CategoryTheory.SimplicialObject.Truncated.sk n = (SimplexCategory.Truncated.inclusion n).op.lan

@[reducible, inline]

abbrev CategoryTheory.SimplicialObject.Truncated.cosk {C : Type u} [Category.{v, u} C] (n : ℕ) [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F] : Functor (Truncated C n) (SimplicialObject C)

The n-coskeleton as a functor SimplicialObject.Truncated C n ⥤ SimplicialObject C.

Equations

• CategoryTheory.SimplicialObject.Truncated.cosk n = (SimplexCategory.Truncated.inclusion n).op.ran

@[reducible, inline]

abbrev CategoryTheory.SimplicialObject.sk {C : Type u} [Category.{v, u} C] (n : ℕ) [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F] : Functor (SimplicialObject C) (SimplicialObject C)

The n-skeleton as an endofunctor on SimplicialObject C.

Equations

• CategoryTheory.SimplicialObject.sk n = (CategoryTheory.SimplicialObject.truncation n).comp (CategoryTheory.SimplicialObject.Truncated.sk n)

@[reducible, inline]

abbrev CategoryTheory.SimplicialObject.cosk {C : Type u} [Category.{v, u} C] (n : ℕ) [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F] : Functor (SimplicialObject C) (SimplicialObject C)

The n-coskeleton as an endofunctor on SimplicialObject C.

Equations

• CategoryTheory.SimplicialObject.cosk n = (CategoryTheory.SimplicialObject.truncation n).comp (CategoryTheory.SimplicialObject.Truncated.cosk n)

noncomputable def CategoryTheory.SimplicialObject.skAdj {C : Type u} [Category.{v, u} C] (n : ℕ) [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F] : Truncated.sk n ⊣ truncation n

The adjunction between the n-skeleton and n-truncation.

Equations

• CategoryTheory.SimplicialObject.skAdj n = (SimplexCategory.Truncated.inclusion n).op.lanAdjunction C

noncomputable def CategoryTheory.SimplicialObject.coskAdj {C : Type u} [Category.{v, u} C] (n : ℕ) [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F] : truncation n ⊣ Truncated.cosk n

The adjunction between n-truncation and the n-coskeleton.

Equations

• CategoryTheory.SimplicialObject.coskAdj n = (SimplexCategory.Truncated.inclusion n).op.ranAdjunction C

instance CategoryTheory.SimplicialObject.instIsLeftKanExtensionOppositeTruncatedSimplexCategoryObjSkAppTruncatedUnitSkAdjTruncation {C : Type u} [Category.{v, u} C] (X : SimplicialObject C) (n : ℕ) [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F] : Functor.IsLeftKanExtension ((sk n).obj X) ((skAdj n).unit.app ((truncation n).obj X))

instance CategoryTheory.SimplicialObject.instIsRightKanExtensionOppositeTruncatedSimplexCategoryObjCoskAppTruncatedCounitCoskAdjTruncation {C : Type u} [Category.{v, u} C] (X : SimplicialObject C) (n : ℕ) [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F] : Functor.IsRightKanExtension ((cosk n).obj X) ((coskAdj n).counit.app ((truncation n).obj X))

instance CategoryTheory.SimplicialObject.Truncated.cosk_reflective {C : Type u} [Category.{v, u} C] (n : ℕ) [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F] [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasPointwiseRightKanExtension F] : IsIso (coskAdj n).counit

instance CategoryTheory.SimplicialObject.Truncated.sk_coreflective {C : Type u} [Category.{v, u} C] (n : ℕ) [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F] [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasPointwiseLeftKanExtension F] : IsIso (skAdj n).unit

noncomputable def CategoryTheory.SimplicialObject.Truncated.cosk.fullyFaithful {C : Type u} [Category.{v, u} C] (n : ℕ) [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F] [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasPointwiseRightKanExtension F] : (Truncated.cosk n).FullyFaithful

Since Truncated.inclusion is fully faithful, so is right Kan extension along it.

Equations

• CategoryTheory.SimplicialObject.Truncated.cosk.fullyFaithful n = (CategoryTheory.SimplicialObject.coskAdj n).fullyFaithfulROfIsIsoCounit

instance CategoryTheory.SimplicialObject.Truncated.cosk.full {C : Type u} [Category.{v, u} C] (n : ℕ) [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F] [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasPointwiseRightKanExtension F] : (Truncated.cosk n).Full

instance CategoryTheory.SimplicialObject.Truncated.cosk.faithful {C : Type u} [Category.{v, u} C] (n : ℕ) [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F] [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasPointwiseRightKanExtension F] : (Truncated.cosk n).Faithful

noncomputable instance CategoryTheory.SimplicialObject.Truncated.coskAdj.reflective {C : Type u} [Category.{v, u} C] (n : ℕ) [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F] [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasPointwiseRightKanExtension F] : Reflective (Truncated.cosk n)

Equations

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

noncomputable def CategoryTheory.SimplicialObject.Truncated.sk.fullyFaithful {C : Type u} [Category.{v, u} C] (n : ℕ) [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F] [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasPointwiseLeftKanExtension F] : (Truncated.sk n).FullyFaithful

Since Truncated.inclusion is fully faithful, so is left Kan extension along it.

Equations

• CategoryTheory.SimplicialObject.Truncated.sk.fullyFaithful n = (CategoryTheory.SimplicialObject.skAdj n).fullyFaithfulLOfIsIsoUnit

instance CategoryTheory.SimplicialObject.Truncated.sk.full {C : Type u} [Category.{v, u} C] (n : ℕ) [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F] [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasPointwiseLeftKanExtension F] : (Truncated.sk n).Full

instance CategoryTheory.SimplicialObject.Truncated.sk.faithful {C : Type u} [Category.{v, u} C] (n : ℕ) [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F] [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasPointwiseLeftKanExtension F] : (Truncated.sk n).Faithful

noncomputable instance CategoryTheory.SimplicialObject.Truncated.skAdj.coreflective {C : Type u} [Category.{v, u} C] (n : ℕ) [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F] [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasPointwiseLeftKanExtension F] : Coreflective (Truncated.sk n)

Equations

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

@[reducible, inline]

abbrev CategoryTheory.SimplicialObject.const (C : Type u) [Category.{v, u} C] : Functor C (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) [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)

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

Equations

• CategoryTheory.SimplicialObject.instCategoryAugmented C = id inferInstance

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem CategoryTheory.SimplicialObject.Augmented.hom_ext_iff {C : Type u} [Category.{v, u} C] {X Y : Augmented C} {f g : X ⟶ Y} : f = g ↔ f.left = g.left ∧ f.right = g.right

def CategoryTheory.SimplicialObject.Augmented.drop {C : Type u} [Category.{v, u} C] : Functor (Augmented C) (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.drop_obj {C : Type u} [Category.{v, u} C] (X : Comma (Functor.id (SimplicialObject C)) (SimplicialObject.const C)) : drop.obj X = X.left

@[simp]

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

def CategoryTheory.SimplicialObject.Augmented.point {C : Type u} [Category.{v, u} C] : Functor (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.point_map {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Comma (Functor.id (SimplicialObject C)) (SimplicialObject.const C)} (f : X✝ ⟶ Y✝) : point.map f = f.right

@[simp]

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

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

The functor from augmented objects to arrows.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

Functor composition induces a functor on augmented simplicial objects.

Equations

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

def CategoryTheory.SimplicialObject.Augmented.whiskering (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] : Functor (Functor C D) (Functor (Augmented C) (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_obj (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] (F : Functor C D) : (whiskering C D).obj F = whiskeringObj C D F

@[simp]

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

@[simp]

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

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

The constant augmented simplicial object functor.

Equations

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

@[simp]

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

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.const_obj_hom {C : Type u} [Category.{v, u} C] (X : C) : (const.obj X).hom = CategoryStruct.id ((Functor.id (SimplicialObject C)).obj ((SimplicialObject.const C).obj X))

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.const_map_right {C : Type u} [Category.{v, u} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (const.map f).right = f

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.const_map_left {C : Type u} [Category.{v, u} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (const.map f).left = (SimplicialObject.const C).map f

@[simp]

theorem CategoryTheory.SimplicialObject.Augmented.const_obj_left {C : Type u} [Category.{v, u} C] (X : C) : (const.obj X).left = (SimplicialObject.const C).obj X

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

Augment a simplicial object with an object.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Cosimplicial objects.

Equations

• CategoryTheory.CosimplicialObject C = CategoryTheory.Functor SimplexCategory C

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

Equations

• CategoryTheory.CosimplicialObject.instCategory C = id inferInstance

@[simp]

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

@[simp]

theorem CategoryTheory.CosimplicialObject.comp_app (C : Type u) [Category.{v, u} C] {X✝ Y✝ Z✝ : Functor SimplexCategory C} (α : NatTrans X✝ Y✝) (β : NatTrans Y✝ Z✝) (X : SimplexCategory) : (CategoryStruct.comp α β).app X = CategoryStruct.comp (α.app X) (β.app X)

def Simplicial.«term_^⦋_⦌» : 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.

def Simplicial.«term_^⦋_⦌».«delab_app.Prefunctor.obj» : 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.CosimplicialObject.instHasLimitsOfShape (C : Type u) [Category.{v, u} C] {J : Type v} [SmallCategory J] [Limits.HasLimitsOfShape J C] : Limits.HasLimitsOfShape J (CosimplicialObject C)

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

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

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

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

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

def CategoryTheory.CosimplicialObject.δ {C : Type u} [Category.{v, u} C] (X : 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} [Category.{v, u} C] (X : 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} [Category.{v, u} C] (X : 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} [Category.{v, u} C] (X : CosimplicialObject C) {n : ℕ} (h : n = n) : X.eqToIso h = Iso.refl (X.obj (SimplexCategory.mk n))

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

The generic case of the first cosimplicial identity

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

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

theorem CategoryTheory.CosimplicialObject.δ_comp_δ'_assoc {C : Type u} [Category.{v, u} C] (X : 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) : CategoryStruct.comp (X.δ i) (CategoryStruct.comp (X.δ j) h) = CategoryStruct.comp (X.δ (j.pred ⋯)) (CategoryStruct.comp (X.δ i.castSucc) h)

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

theorem CategoryTheory.CosimplicialObject.δ_comp_δ''_assoc {C : Type u} [Category.{v, u} C] (X : 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) : CategoryStruct.comp (X.δ (i.castLT ⋯)) (CategoryStruct.comp (X.δ j.succ) h) = CategoryStruct.comp (X.δ j) (CategoryStruct.comp (X.δ i) h)

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

The special case of the first cosimplicial identity

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

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

theorem CategoryTheory.CosimplicialObject.δ_comp_δ_self'_assoc {C : Type u} [Category.{v, u} C] (X : 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) : CategoryStruct.comp (X.δ i) (CategoryStruct.comp (X.δ j) h) = CategoryStruct.comp (X.δ i) (CategoryStruct.comp (X.δ i.succ) h)

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

The second cosimplicial identity

theorem CategoryTheory.CosimplicialObject.δ_comp_σ_of_le_assoc {C : Type u} [Category.{v, u} C] (X : 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) : CategoryStruct.comp (X.δ i.castSucc) (CategoryStruct.comp (X.σ j.succ) h) = CategoryStruct.comp (X.σ j) (CategoryStruct.comp (X.δ i) h)

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

The first part of the third cosimplicial identity

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

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

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

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

The second part of the third cosimplicial identity

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

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

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

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

The fourth cosimplicial identity

theorem CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt_assoc {C : Type u} [Category.{v, u} C] (X : 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) : CategoryStruct.comp (X.δ i.succ) (CategoryStruct.comp (X.σ j.castSucc) h) = CategoryStruct.comp (X.σ j) (CategoryStruct.comp (X.δ i) h)

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

theorem CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt'_assoc {C : Type u} [Category.{v, u} C] (X : 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) : CategoryStruct.comp (X.δ i) (CategoryStruct.comp (X.σ j) h) = CategoryStruct.comp (X.σ (j.castLT ⋯)) (CategoryStruct.comp (X.δ (i.pred ⋯)) h)

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

The fifth cosimplicial identity

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Functor composition induces a functor on cosimplicial objects.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.CosimplicialObject.Truncated (C : Type u) [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) [Category.{v, u} C] {n : ℕ} : Category.{v, max u v} (Truncated C n)

Equations

• CategoryTheory.CosimplicialObject.instCategoryTruncated C = id inferInstance

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

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

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

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

def CategoryTheory.CosimplicialObject.Truncated.whiskering (C : Type u) [Category.{v, u} C] {n : ℕ} (D : Type u_1) [Category.{u_2, u_1} D] : Functor (Functor C D) (Functor (Truncated C n) (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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.CosimplicialObject.Truncated.mkNotation : Lean.TrailingParserDescr

For X : Truncated C n and m ≤ n, X ^⦋m⦌ₙ is the m-th term of X. The proof p : m ≤ n can also be provided using the syntax X ^⦋m, p⦌ₙ.

Equations

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

def CategoryTheory.CosimplicialObject.Truncated.trunc (C : Type u) [Category.{v, u} C] (n m : ℕ) (h : m ≤ n := by omega) : Functor (Truncated C n) (Truncated C m)

Further truncation of truncated cosimplicial objects.

Equations

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

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

The truncation functor from cosimplicial objects to truncated cosimplicial objects.

Equations

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

def CategoryTheory.CosimplicialObject.truncationCompTrunc {C : Type u} [Category.{v, u} C] {n m : ℕ} (h : m ≤ n) : (truncation n).comp (Truncated.trunc C n m h) ≅ truncation m

For all m ≤ n, truncation m factors through Truncated n.

Equations

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

@[reducible, inline]

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

The constant cosimplicial object.

Equations

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

def CategoryTheory.CosimplicialObject.Augmented (C : Type u) [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))

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

Equations

• CategoryTheory.CosimplicialObject.instCategoryAugmented C = id inferInstance

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem CategoryTheory.CosimplicialObject.Augmented.hom_ext_iff {C : Type u} [Category.{v, u} C] {X Y : Augmented C} {f g : X ⟶ Y} : f = g ↔ f.left = g.left ∧ f.right = g.right

def CategoryTheory.CosimplicialObject.Augmented.drop {C : Type u} [Category.{v, u} C] : Functor (Augmented C) (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.drop_obj {C : Type u} [Category.{v, u} C] (X : Comma (CosimplicialObject.const C) (Functor.id (CosimplicialObject C))) : drop.obj X = X.right

@[simp]

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

def CategoryTheory.CosimplicialObject.Augmented.point {C : Type u} [Category.{v, u} C] : Functor (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.point_map {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Comma (CosimplicialObject.const C) (Functor.id (CosimplicialObject C))} (f : X✝ ⟶ Y✝) : point.map f = f.left

@[simp]

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

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

The functor from augmented objects to arrows.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Functor composition induces a functor on augmented cosimplicial objects.

Equations

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

def CategoryTheory.CosimplicialObject.Augmented.whiskering (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] : Functor (Functor C D) (Functor (Augmented C) (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) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] {X✝ Y✝ : Functor C D} (η : X✝ ⟶ Y✝) (A : Augmented C) : (((whiskering C D).map η).app A).left = η.app (point.obj A)

@[simp]

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

@[simp]

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

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

The constant augmented cosimplicial object functor.

Equations

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

@[simp]

theorem CategoryTheory.CosimplicialObject.Augmented.const_map_left {C : Type u} [Category.{v, u} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (const.map f).left = f

@[simp]

theorem CategoryTheory.CosimplicialObject.Augmented.const_obj_hom {C : Type u} [Category.{v, u} C] (X : C) : (const.obj X).hom = CategoryStruct.id ((CosimplicialObject.const C).obj X)

@[simp]

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

@[simp]

theorem CategoryTheory.CosimplicialObject.Augmented.const_obj_right {C : Type u} [Category.{v, u} C] (X : C) : (const.obj X).right = (CosimplicialObject.const C).obj X

@[simp]

theorem CategoryTheory.CosimplicialObject.Augmented.const_map_right {C : Type u} [Category.{v, u} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (const.map f).right = (CosimplicialObject.const C).map f

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

Augment a cosimplicial object with an object.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

The anti-equivalence between simplicial objects and cosimplicial objects.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The anti-equivalence between cosimplicial objects and simplicial objects.

Equations

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

@[simp]

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

@[simp]

theorem CategoryTheory.cosimplicialSimplicialEquiv_inverse_map (C : Type u) [Category.{v, u} C] {X✝ Y✝ : Functor SimplexCategoryᵒᵖ Cᵒᵖ} (α : X✝ ⟶ Y✝) : (cosimplicialSimplicialEquiv C).inverse.map α = Quiver.Hom.op { app := fun (X : SimplexCategory) => (α.app (Opposite.op X)).unop, naturality := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.CosimplicialObject.Augmented.leftOp {C : Type u} [Category.{v, u} C] (X : Augmented Cᵒᵖ) : 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 := Opposite.unop X.left, hom := CategoryTheory.NatTrans.leftOp X.hom }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso {C : Type u} [Category.{v, u} C] (X : 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.SimplicialObject.Augmented.rightOpLeftOpIso_inv_left_app {C : Type u} [Category.{v, u} C] (X : Augmented C) (X✝ : SimplexCategoryᵒᵖ) : X.rightOpLeftOpIso.inv.left.app X✝ = CategoryStruct.id (X.left.obj X✝)

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.simplicialToCosimplicialAugmented (C : Type u) [Category.{v, u} C] : Functor (SimplicialObject.Augmented C)ᵒᵖ (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.simplicialToCosimplicialAugmented_map_right (C : Type u) [Category.{v, u} C] {X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ} (f : X✝ ⟶ Y✝) : ((simplicialToCosimplicialAugmented C).map f).right = NatTrans.rightOp f.unop.left

@[simp]

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

@[simp]

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

def CategoryTheory.cosimplicialToSimplicialAugmented (C : Type u) [Category.{v, u} C] : Functor (CosimplicialObject.Augmented Cᵒᵖ) (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.cosimplicialToSimplicialAugmented_map (C : Type u) [Category.{v, u} C] {X✝ Y✝ : CosimplicialObject.Augmented Cᵒᵖ} (f : X✝ ⟶ Y✝) : (cosimplicialToSimplicialAugmented C).map f = Quiver.Hom.op { left := NatTrans.leftOp f.right, right := f.left.unop, w := ⋯ }

@[simp]

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

def CategoryTheory.simplicialCosimplicialAugmentedEquiv (C : Type u) [Category.{v, u} C] : (SimplicialObject.Augmented C)ᵒᵖ ≌ 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.

@[simp]

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

@[simp]

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