Arrows and faces of simplices of the nerve, and the images of its degeneracies

An n-simplex of the nerve CategoryTheory.nerve C of a category is a string F : ComposableArrows C n of composable arrows. For positions i ≤ j its arrow from the i-th to the j-th object, viewed as a total arrow of C, is F.totalArrow i j hij (defined in TauCeti.CategoryTheory.ComposableArrows.Basic), and the simplicial operators of the nerve reindex these arrows (CategoryTheory.ComposableArrows.totalArrow_whiskerLeft).

An n + 1-simplex of the nerve lies in the image of the i-th degeneracy exactly when its i-th arrow is an identity arrow (CategoryTheory.nerve.mem_range_σ_iff, in Set.range form CategoryTheory.nerve.range_σ_eq_preimage). This generalizes, and adapts the proof of, Mathlib's PartialOrder.mem_range_nerve_σ_iff from partial orders to arbitrary categories.

Prepending an arrow b to a string commutes with deleting any vertex but the first two, and deleting the second vertex composes b with the first arrow of the string (CategoryTheory.nerve.δ_succ_precomp).

A 3-simplex of the nerve is a sequence of three composable morphisms ComposableArrows.mk₃ f g h. Its faces are the 2-simplices obtained by dropping a vertex, whose arrows are composites of consecutive arrows among f, g and h. This extends Mathlib's description of the faces of 2-simplices (CategoryTheory.nerve.δ₀_mk₂_eq, …).

Main declarations

• CategoryTheory.nerve.σ_δ_castSucc_eq_self: a string whose i-th arrow is an identity is the i-th degeneracy of its i-th face.
• CategoryTheory.nerve.mem_range_σ_iff: the image of the i-th degeneracy consists of the strings whose i-th arrow is an identity.
• CategoryTheory.nerve.δ_succ_precomp: the faces of a string with a prepended arrow.
• CategoryTheory.nerve.δ₀_mk₃_eq, …, CategoryTheory.nerve.δ₃_mk₃_eq: the faces of the 3-simplex of the nerve given by three composable morphisms.

theorem CategoryTheory.nerve.σ_δ_castSucc_eq_self {C : Type u} [Category.{v, u} C] {n : ℕ} (s : ComposableArrows C (n + 1)) {i : Fin (n + 1)} {h : s.obj i.castSucc = s.obj i.succ} (hi : s.map (homOfLE ⋯) = eqToHom h) : (ConcreteCategory.hom (SimplicialObject.σ (nerve C) i)) ((ConcreteCategory.hom (SimplicialObject.δ (nerve C) i.castSucc)) s) = s

A string of composable arrows whose i-th arrow is an identity arrow is the i-th degeneracy of its face deleting the i-th object.

theorem CategoryTheory.nerve.mem_range_σ_iff {C : Type u} [Category.{v, u} C] {n : ℕ} (s : ComposableArrows C (n + 1)) (i : Fin (n + 1)) : s ∈ Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ (nerve C) i)) ↔ s.totalArrow i.castSucc i.succ ⋯ ∈ Set.range fun (x : C) => { left := x, right := x, hom := CategoryStruct.id x }

A simplex of the nerve lies in the image of the i-th degeneracy exactly when its i-th arrow is an identity arrow. This generalizes Mathlib's PartialOrder.mem_range_nerve_σ_iff (in Mathlib/AlgebraicTopology/SimplicialSet/NerveNondegenerate.lean) from partial orders to arbitrary categories.

theorem CategoryTheory.nerve.range_σ_eq_preimage {C : Type u} [Category.{v, u} C] {n : ℕ} (i : Fin (n + 1)) : Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ (nerve C) i)) = (fun (s : ComposableArrows C (n + 1)) => s.totalArrow i.castSucc i.succ ⋯) ⁻¹' Set.range fun (x : C) => { left := x, right := x, hom := CategoryStruct.id x }

The image of the i-th degeneracy is the set of strings whose i-th arrow is an identity arrow: the Set.range form of mem_range_σ_iff.

theorem CategoryTheory.nerve.δ_succ_precomp {C : Type u} [Category.{v, u} C] {n : ℕ} (j : Fin (n + 2)) (σ : ComposableArrows C (n + 1)) {y : C} (b : y ⟶ σ.left) : (ConcreteCategory.hom (SimplicialObject.δ (nerve C) j.succ)) (σ.precomp b) = ComposableArrows.precomp ((ConcreteCategory.hom (SimplicialObject.δ (nerve C) j)) σ) (CategoryStruct.comp b (σ.map (homOfLE ⋯)))

Deleting a vertex other than the first one from a string with a prepended arrow b deletes the corresponding vertex of the original string. If that vertex was the first one, the prepended arrow is composed with the deleted arrow, so in all cases b is followed by the arrow from the first vertex to the new second vertex.

The arrows of each face of mk₃ f g h are, by definition of mk₃, composites of consecutive arrows among f, g and h, so the faces are determined by ComposableArrows.ext₂_of_arrow.

@[simp]

theorem CategoryTheory.nerve.δ₀_mk₃_eq {C : Type u} [Category.{v, u} C] {X₀ X₁ X₂ X₃ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) (h : X₂ ⟶ X₃) : (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 0)) (ComposableArrows.mk₃ f g h) = ComposableArrows.mk₂ g h

The face of mk₃ f g h opposite to the vertex 0.

@[simp]

theorem CategoryTheory.nerve.δ₁_mk₃_eq {C : Type u} [Category.{v, u} C] {X₀ X₁ X₂ X₃ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) (h : X₂ ⟶ X₃) : (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) (ComposableArrows.mk₃ f g h) = ComposableArrows.mk₂ (CategoryStruct.comp f g) h

The face of mk₃ f g h opposite to the vertex 1.

@[simp]

theorem CategoryTheory.nerve.δ₂_mk₃_eq {C : Type u} [Category.{v, u} C] {X₀ X₁ X₂ X₃ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) (h : X₂ ⟶ X₃) : (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 2)) (ComposableArrows.mk₃ f g h) = ComposableArrows.mk₂ f (CategoryStruct.comp g h)

The face of mk₃ f g h opposite to the vertex 2.

@[simp]

theorem CategoryTheory.nerve.δ₃_mk₃_eq {C : Type u} [Category.{v, u} C] {X₀ X₁ X₂ X₃ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) (h : X₂ ⟶ X₃) : (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 3)) (ComposableArrows.mk₃ f g h) = ComposableArrows.mk₂ f g

The face of mk₃ f g h opposite to the vertex 3.