A construction by Gabriel and Zisman

In this file, we construct a cosimplicial object SimplexCategory.II in SimplexCategoryᵒᵖ, i.e. a functor SimplexCategory ⥤ SimplexCategoryᵒᵖ. If we identify SimplexCategory with the category of finite nonempty linearly ordered types, this functor could be interpreted as the contravariant functor which sends a finite nonempty linearly ordered type T to T →o Fin 2 (with f ≤ g ↔ ∀ i, g i ≤ f i, which turns out to be a linear order); in particular, it sends Fin (n + 1) to a linearly ordered type which is isomorphic to Fin (n + 2). As a result, we define SimplexCategory.II as a functor which sends ⦋n⦌ to ⦋n + 1⦌: on morphisms, it sends faces to degeneracies and vice versa. This construction appeared in Calculus of fractions and homotopy theory, chapter III, paragraph 1.1, by Gabriel and Zisman.

References

• [P. Gabriel, M. Zisman, Calculus of fractions and homotopy theory][gabriel-zisman-1967]

def SimplexCategory.II.finset {n m : ℕ} (f : Fin (n + 1) →o Fin (m + 1)) (x : Fin (m + 2)) : Finset (Fin (n + 2))

Auxiliary definition for map'. Given f : Fin (n + 1) →o Fin (m + 1) and x : Fin (m + 2), map' f x shall be the smallest element in this finset f x : Finset (Fin (n + 2)).

Equations

• SimplexCategory.II.finset f x = {i : Fin (n + 2) | i = Fin.last (n + 1) ∨ ∃ (h : i ≠ Fin.last (n + 1)), x ≤ (f (i.castPred h)).castSucc}

theorem SimplexCategory.II.mem_finset_iff {n m : ℕ} (f : Fin (n + 1) →o Fin (m + 1)) (x : Fin (m + 2)) (i : Fin (n + 2)) : i ∈ finset f x ↔ i = Fin.last (n + 1) ∨ ∃ (h : i ≠ Fin.last (n + 1)), x ≤ (f (i.castPred h)).castSucc

@[simp]

theorem SimplexCategory.II.last_mem_finset {n m : ℕ} (f : Fin (n + 1) →o Fin (m + 1)) (x : Fin (m + 2)) : Fin.last (n + 1) ∈ finset f x

@[simp]

theorem SimplexCategory.II.castSucc_mem_finset_iff {n m : ℕ} (f : Fin (n + 1) →o Fin (m + 1)) (x : Fin (m + 2)) (i : Fin (n + 1)) : i.castSucc ∈ finset f x ↔ x ≤ (f i).castSucc

theorem SimplexCategory.II.nonempty_finset {n m : ℕ} (f : Fin (n + 1) →o Fin (m + 1)) (x : Fin (m + 2)) : (finset f x).Nonempty

def SimplexCategory.II.map' {n m : ℕ} (f : Fin (n + 1) →o Fin (m + 1)) (x : Fin (m + 2)) : Fin (n + 2)

Auxiliary definition for the definition of the action of the functor SimplexCategory.II on morphisms.

Equations

• SimplexCategory.II.map' f x = (SimplexCategory.II.finset f x).min' ⋯

theorem SimplexCategory.II.map'_eq_last_iff {n m : ℕ} (f : Fin (n + 1) →o Fin (m + 1)) (x : Fin (m + 2)) : map' f x = Fin.last (n + 1) ↔ ∀ (i : Fin (n + 1)), (f i).castSucc < x

theorem SimplexCategory.II.map'_eq_castSucc_iff {n m : ℕ} (f : Fin (n + 1) →o Fin (m + 1)) (x : Fin (m + 2)) (y : Fin (n + 1)) : map' f x = y.castSucc ↔ x ≤ (f y).castSucc ∧ ∀ i < y, (f i).castSucc < x

@[simp]

theorem SimplexCategory.II.map'_last {n m : ℕ} (f : Fin (n + 1) →o Fin (m + 1)) : map' f (Fin.last (m + 1)) = Fin.last (n + 1)

@[simp]

theorem SimplexCategory.II.map'_zero {n m : ℕ} (f : Fin (n + 1) →o Fin (m + 1)) : map' f 0 = 0

@[simp]

theorem SimplexCategory.II.map'_id {n : ℕ} (x : Fin (n + 2)) : map' OrderHom.id x = x

theorem SimplexCategory.II.map'_map' {n m p : ℕ} (f : Fin (n + 1) →o Fin (m + 1)) (g : Fin (m + 1) →o Fin (p + 1)) (x : Fin (p + 2)) : map' f (map' g x) = map' (g.comp f) x

@[simp]

theorem SimplexCategory.II.map'_succAboveOrderEmb {n : ℕ} (i : Fin (n + 2)) (x : Fin (n + 3)) : map' i.succAboveOrderEmb.toOrderHom x = i.predAbove x

@[simp]

theorem SimplexCategory.II.map'_predAbove {n : ℕ} (i : Fin (n + 1)) (x : Fin (n + 2)) : map' { toFun := i.predAbove, monotone' := ⋯ } x = i.succ.castSucc.succAbove x

theorem SimplexCategory.II.monotone_map' {n m : ℕ} (f : Fin (n + 1) →o Fin (m + 1)) : Monotone (map' f)

def SimplexCategory.II : CategoryTheory.CosimplicialObject SimplexCategoryᵒᵖ

The functor SimplexCategory ⥤ SimplexCategoryᵒᵖ (i.e. a cosimplicial object in SimplexCategoryᵒᵖ) which sends ⦋n⦌ to the object in SimplexCategoryᵒᵖ that is associated to the linearly ordered type ⦋n + 1⦌ (which could be identified to the ordered type ⦋n⦌ →o ⦋1⦌).

Equations

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

@[simp]

theorem SimplexCategory.II_obj (n : SimplexCategory) : II.obj n = Opposite.op (mk (n.len + 1))

@[simp]

theorem SimplexCategory.II_δ {n : ℕ} (i : Fin (n + 2)) : II.δ i = (σ i).op

@[simp]

theorem SimplexCategory.II_σ {n : ℕ} (i : Fin (n + 1)) : II.σ i = (δ i.succ.castSucc).op