Horns

This file introduce horns Λ[n, i].

def SSet.horn (n : ℕ) (i : Fin (n + 1)) : SSet

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

Equations

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

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

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

Equations

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

def Simplicial.«termΛ[_,_]».«delab_app.SSet.horn» : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

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

The inclusion of the i-th horn of the n-th standard simplex into that standard simplex.

Equations

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

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.

Equations

• SSet.horn.const n i k m = ⟨SSet.stdSimplex.const (n + 2) k m, ⋯⟩

@[simp]

theorem SSet.horn.const_coe (n : ℕ) (i k : Fin (n + 3)) (m : SimplexCategoryᵒᵖ) : ↑(const n i k m) = stdSimplex.const (n + 2) k m

def SSet.horn.edge (n : ℕ) (i a b : Fin (n + 1)) (hab : a ≤ b) (H : {i, a, b}.card ≤ n) : (horn n i).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.

Equations

• SSet.horn.edge n i a b hab H = ⟨SSet.stdSimplex.edge n a b hab, ⋯⟩

@[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).obj (Opposite.op (SimplexCategory.mk 1))

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

Equations

• SSet.horn.edge₃ n i a b hab H = SSet.horn.edge n i a b hab ⋯

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

Equations

• SSet.horn.primitiveEdge h₀ hₙ j = SSet.horn.edge n i j.castSucc j.succ ⋯ ⋯

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

Equations

• SSet.horn.primitiveTriangle i h₀ hₙ k h = ⟨SSet.stdSimplex.triangle ⟨k, ⋯⟩ ⟨k + 1, ⋯⟩ ⟨k + 2, ⋯⟩ ⋯ ⋯, ⋯⟩

@[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).obj (Opposite.op (SimplexCategory.mk n))

The jth subface of the i-th horn.

Equations

• SSet.horn.face i j h = ⟨(SSet.stdSimplex.objEquiv (SimplexCategory.mk (n + 1)) (Opposite.op (SimplexCategory.mk n))).symm (SimplexCategory.δ j), ⋯⟩

@[simp]

theorem SSet.horn.face_coe {n : ℕ} (i j : Fin (n + 2)) (h : j ≠ i) : ↑(face i j h) = (stdSimplex.objEquiv (SimplexCategory.mk (n + 1)) (Opposite.op (SimplexCategory.mk n))).symm (SimplexCategory.δ j)

theorem SSet.horn.hom_ext {n : ℕ} {i : Fin (n + 2)} {S : SSet} (σ₁ σ₂ : horn (n + 1) i ⟶ 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.