Horns

This file introduces horns Λ[n, i].

def SSet.horn (n : ℕ) (i : Fin (n + 1)) : (stdSimplex.obj { len := 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).

Equations

• SSet.horn n i = { obj := fun (x : SimplexCategoryᵒᵖ) => {s : (SSet.stdSimplex.obj { len := n }).obj x | Set.range ⇑(SSet.stdSimplex.asOrderHom s) ∪ {i} ≠ Set.univ}, map := ⋯ }

theorem SSet.horn_obj (n : ℕ) (i : Fin (n + 1)) (x✝ : SimplexCategoryᵒᵖ) : (horn n i).obj x✝ = {s : (stdSimplex.obj { len := 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

Equations

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

theorem SSet.mem_horn_iff {n : ℕ} (i : Fin (n + 1)) {m : SimplexCategoryᵒᵖ} (x : (stdSimplex.obj { len := n }).obj m) : x ∈ (horn n i).obj m ↔ Set.range ⇑(stdSimplex.asOrderHom x) ∪ {i} ≠ Set.univ

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

instance SSet.instHasDimensionLTToSSetHorn {n : ℕ} (i : Fin (n + 1)) : (horn n i).toSSet.HasDimensionLT n

theorem SSet.mem_horn_iff_notMem_range {n d : ℕ} (s : (stdSimplex.obj { len := n }).obj (Opposite.op { len := d })) (i : Fin (n + 1)) : s ∈ (horn n i).obj (Opposite.op { len := d }) ↔ ∃ (j : Fin (n + 1)) (_ : j ≠ i), j ∉ Set.range ⇑s

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 { len := 0 }) = ⊤

theorem SSet.horn_obj_eq_univ {n : ℕ} (i : Fin (n + 1)) (m : ℕ) (h : m + 1 < n := by lia) : (horn n i).obj (Opposite.op { len := m }) = Set.univ

theorem SSet.subcomplex_le_horn_iff {n : ℕ} (A : (stdSimplex.obj { len := n + 1 }).Subcomplex) (i : Fin (n + 2)) : A ≤ horn (n + 1) i ↔ ¬stdSimplex.face {i}ᶜ ≤ A

theorem SSet.face_le_horn_iff {n : ℕ} (S : Finset (Fin (n + 2))) (j : Fin (n + 2)) : stdSimplex.face S ≤ horn (n + 1) j ↔ S ≠ Finset.univ ∧ S ≠ {j}ᶜ

theorem SSet.objEquiv_symm_notMem_horn_of_isIso {n : ℕ} (i : Fin (n + 1)) {d : SimplexCategory} (f : d ⟶ { len := n }) [CategoryTheory.IsIso f] : stdSimplex.objEquiv.symm f ∉ (horn n i).obj (Opposite.op d)

theorem SSet.objEquiv_symm_δ_mem_horn_iff {n : ℕ} (i j : Fin (n + 2)) : stdSimplex.objEquiv.symm (SimplexCategory.δ i) ∈ (horn (n + 1) j).obj (Opposite.op { len := n }) ↔ i ≠ j

theorem SSet.objEquiv_symm_δ_notMem_horn_iff {n : ℕ} (i j : Fin (n + 2)) : stdSimplex.objEquiv.symm (SimplexCategory.δ i) ∉ (horn (n + 1) j).obj (Opposite.op { len := n }) ↔ i = j

theorem SSet.op_horn {n : ℕ} (i : Fin (n + 1)) : (horn n i).op.preimage (stdSimplex.opIso { len := n }).inv = horn n i.rev

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.yonedaEquiv (SSet.const ⟨SSet.stdSimplex.obj₀Equiv.symm 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 { len := 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 { len := 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).toSSet.obj (Opposite.op { len := 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).toSSet.obj (Opposite.op { len := 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).toSSet.obj (Opposite.op { len := 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).toSSet.obj (Opposite.op { len := n })

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

Equations

• SSet.horn.face i j h = SSet.yonedaEquiv (CategoryTheory.Subfunctor.lift (SSet.stdSimplex.δ j) ⋯)

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), (CategoryTheory.ConcreteCategory.hom (σ₁.app (Opposite.op { len := n }))) (face i j h) = (CategoryTheory.ConcreteCategory.hom (σ₂.app (Opposite.op { len := 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.

Equations

• SSet.horn.faceι i j hij = SSet.Subcomplex.homOfLE ⋯

@[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 { len := 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 { len := 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.

Equations

• SSet.horn.ι i j hij = SSet.yonedaEquiv.symm (SSet.horn.face i j hij)

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 { len := 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