Horns

This file introduces horns Λ[n, i].

def SSet.horn (n : ℕ) (i : Fin (n + 1)) : (stdSimplex.obj (SimplexCategory.mk n)).Subcomplex

horn n i (or Λ[n, i]) is the i-th horn of the n-th standard simplex, where i : n. It consists of all m-simplices α of Δ[n] for which the union of {i} and the range of α is not all of n (when viewing α as monotone function m → n).

theorem SSet.horn_obj (n : ℕ) (i : Fin (n + 1)) (x✝ : SimplexCategoryᵒᵖ) : (horn n i).obj x✝ = {s : (stdSimplex.obj (SimplexCategory.mk n)).obj x✝ | Set.range ⇑(stdSimplex.asOrderHom s) ∪ {i} ≠ Set.univ}

def Simplicial.«termΛ[_,_]» : Lean.ParserDescr

The i-th horn Λ[n, i] of the standard n-simplex

theorem SSet.horn_eq_iSup (n : ℕ) (i : Fin (n + 1)) : horn n i = ⨆ (j : ↑{i}ᶜ), stdSimplex.face {↑j}ᶜ

theorem SSet.face_le_horn {n : ℕ} (i j : Fin (n + 1)) (h : i ≠ j) : stdSimplex.face {i}ᶜ ≤ horn n j

@[simp]

theorem SSet.horn_obj_zero (n : ℕ) (i : Fin (n + 3)) : (horn (n + 2) i).obj (Opposite.op (SimplexCategory.mk 0)) = ⊤

def SSet.horn.const (n : ℕ) (i k : Fin (n + 3)) (m : SimplexCategoryᵒᵖ) : ↑((horn (n + 2) i).obj m)

The (degenerate) subsimplex of Λ[n+2, i] concentrated in vertex k.

@[simp]

theorem SSet.horn.const_val_apply (n : ℕ) (i k : Fin (n + 3)) {m : ℕ} (a : Fin (m + 1)) : ↑(const n i k (Opposite.op (SimplexCategory.mk m))) a = k

def SSet.horn.edge (n : ℕ) (i a b : Fin (n + 1)) (hab : a ≤ b) (H : {i, a, b}.card ≤ n) : (horn n i).toSSet.obj (Opposite.op (SimplexCategory.mk 1))

The edge of Λ[n, i] with endpoints a and b.

This edge only exists if {i, a, b} has cardinality less than n.

@[simp]

theorem SSet.horn.edge_coe (n : ℕ) (i a b : Fin (n + 1)) (hab : a ≤ b) (H : {i, a, b}.card ≤ n) : ↑(edge n i a b hab H) = stdSimplex.edge n a b hab

def SSet.horn.edge₃ (n : ℕ) (i a b : Fin (n + 1)) (hab : a ≤ b) (H : 3 ≤ n) : (horn n i).toSSet.obj (Opposite.op (SimplexCategory.mk 1))

Alternative constructor for the edge of Λ[n, i] with endpoints a and b, assuming 3 ≤ n.

@[simp]

theorem SSet.horn.edge₃_coe_down (n : ℕ) (i a b : Fin (n + 1)) (hab : a ≤ b) (H : 3 ≤ n) : (↑(edge₃ n i a b hab H)).down = SimplexCategory.Hom.mk { toFun := ![a, b], monotone' := ⋯ }

def SSet.horn.primitiveEdge {n : ℕ} {i : Fin (n + 1)} (h₀ : 0 < i) (hₙ : i < Fin.last n) (j : Fin n) : (horn n i).toSSet.obj (Opposite.op (SimplexCategory.mk 1))

The edge of Λ[n, i] with endpoints j and j+1.

This constructor assumes 0 < i < n, which is the type of horn that occurs in the horn-filling condition of quasicategories.

@[simp]

theorem SSet.horn.primitiveEdge_coe_down {n : ℕ} {i : Fin (n + 1)} (h₀ : 0 < i) (hₙ : i < Fin.last n) (j : Fin n) : (↑(primitiveEdge h₀ hₙ j)).down = SimplexCategory.Hom.mk { toFun := ![j.castSucc, j.succ], monotone' := ⋯ }

def SSet.horn.primitiveTriangle {n : ℕ} (i : Fin (n + 4)) (h₀ : 0 < i) (hₙ : i < Fin.last (n + 3)) (k : ℕ) (h : k < n + 2) : (horn (n + 3) i).toSSet.obj (Opposite.op (SimplexCategory.mk 2))

The triangle in the standard simplex with vertices k, k+1, and k+2.

This constructor assumes 0 < i < n, which is the type of horn that occurs in the horn-filling condition of quasicategories.

@[simp]

theorem SSet.horn.primitiveTriangle_coe {n : ℕ} (i : Fin (n + 4)) (h₀ : 0 < i) (hₙ : i < Fin.last (n + 3)) (k : ℕ) (h : k < n + 2) : ↑(primitiveTriangle i h₀ hₙ k h) = stdSimplex.triangle ⟨k, ⋯⟩ ⟨k + 1, ⋯⟩ ⟨k + 2, ⋯⟩ ⋯ ⋯

def SSet.horn.face {n : ℕ} (i j : Fin (n + 2)) (h : j ≠ i) : (horn (n + 1) i).toSSet.obj (Opposite.op (SimplexCategory.mk n))

The jth face of codimension 1 of the i-th horn.

theorem SSet.horn.hom_ext {n : ℕ} {i : Fin (n + 2)} {S : SSet} (σ₁ σ₂ : (horn (n + 1) i).toSSet ⟶ S) (h : ∀ (j : Fin (n + 2)) (h : j ≠ i), σ₁.app (Opposite.op (SimplexCategory.mk n)) (face i j h) = σ₂.app (Opposite.op (SimplexCategory.mk n)) (face i j h)) : σ₁ = σ₂

Two morphisms from a horn are equal if they are equal on all suitable faces.

def SSet.horn.faceι {n : ℕ} (i j : Fin (n + 1)) (hij : j ≠ i) : (stdSimplex.face {j}ᶜ).toSSet ⟶ (horn n i).toSSet

Given i and j in Fin (n + 1) such that j ≠ i, this is the inclusion of stdSimplex.face {j}ᶜ in the horn horn n i.

@[simp]

theorem SSet.horn.faceι_ι {n : ℕ} (i j : Fin (n + 1)) (hij : j ≠ i) : CategoryTheory.CategoryStruct.comp (faceι i j hij) (horn n i).ι = (stdSimplex.face {j}ᶜ).ι

@[simp]

theorem SSet.horn.faceι_ι_assoc {n : ℕ} (i j : Fin (n + 1)) (hij : j ≠ i) {Z : SSet} (h : stdSimplex.obj (SimplexCategory.mk n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (faceι i j hij) (CategoryTheory.CategoryStruct.comp (horn n i).ι h) = CategoryTheory.CategoryStruct.comp (stdSimplex.face {j}ᶜ).ι h

def SSet.horn.ι {n : ℕ} (i j : Fin (n + 2)) (hij : j ≠ i) : stdSimplex.obj (SimplexCategory.mk n) ⟶ (horn (n + 1) i).toSSet

Given i and j in Fin (n + 2) such that j ≠ i, this is the inclusion of Δ[n] in horn (n + 1) i given by stdSimplex.δ j.

theorem SSet.horn.yonedaEquiv_ι {n : ℕ} (i j : Fin (n + 2)) (hij : j ≠ i) : yonedaEquiv (ι i j hij) = face i j hij

@[simp]

theorem SSet.horn.ι_ι {n : ℕ} (i j : Fin (n + 2)) (hij : j ≠ i) : CategoryTheory.CategoryStruct.comp (ι i j hij) (horn (n + 1) i).ι = stdSimplex.δ j

@[simp]

theorem SSet.horn.ι_ι_assoc {n : ℕ} (i j : Fin (n + 2)) (hij : j ≠ i) {Z : SSet} (h : stdSimplex.obj (SimplexCategory.mk (n + 1)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (ι i j hij) (CategoryTheory.CategoryStruct.comp (horn (n + 1) i).ι h) = CategoryTheory.CategoryStruct.comp (stdSimplex.δ j) h

@[simp]

theorem SSet.horn.faceSingletonComplIso_inv_ι {n : ℕ} (i j : Fin (n + 2)) (hij : j ≠ i) : CategoryTheory.CategoryStruct.comp (stdSimplex.faceSingletonComplIso j).inv (ι i j hij) = faceι i j hij

@[simp]

theorem SSet.horn.faceSingletonComplIso_inv_ι_assoc {n : ℕ} (i j : Fin (n + 2)) (hij : j ≠ i) {Z : SSet} (h : (horn (n + 1) i).toSSet ⟶ Z) : CategoryTheory.CategoryStruct.comp (stdSimplex.faceSingletonComplIso j).inv (CategoryTheory.CategoryStruct.comp (ι i j hij) h) = CategoryTheory.CategoryStruct.comp (faceι i j hij) h