instance fin_zero_le_one (n : ℕ) : ZeroLEOneClass (Fin (n + 2))

Equations

• ⋯ = ⋯

theorem CategoryTheory.Functor.map_eqToHom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C D) (X Y : C) (h : X = Y) : F.map (CategoryTheory.eqToHom h) = CategoryTheory.eqToHom ⋯

theorem CategoryTheory.ComposableArrows.map'_def {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) (i j : ℕ) (hij : i ≤ j := by valid) (hjn : j ≤ n := by valid) : F.map' i j hij hjn = F.map (CategoryTheory.homOfLE ⋯)

Kan complexes and quasicategories

noncomputable def SSet.nerve.mk {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (n : ℕ) (obj : Fin (n + 1) → C) (mor : (i : Fin n) → obj i.castSucc ⟶ obj i.succ) : (CategoryTheory.nerve C).obj (Opposite.op (SimplexCategory.mk n))

A constructor for n-simplices of the nerve of a category, by specifying n+1 objects and a morphism between each of the n pairs of adjecent objects.

Equations

• SSet.nerve.mk n obj mor = CategoryTheory.ComposableArrows.mkOfObjOfMapSucc obj mor

def SSet.nerve.δ_mk_mor {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (n : ℕ) (obj : Fin (n + 2) → C) (mor : (i : Fin (n + 1)) → obj i.castSucc ⟶ obj i.succ) (j : Fin (n + 2)) (k : Fin n) : obj (j.succAbove k.castSucc) ⟶ obj (j.succAbove k.succ)

Equations

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

theorem SSet.nerve.δ_mk {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (n : ℕ) (obj : Fin (n + 2) → C) (mor : (i : Fin (n + 1)) → obj i.castSucc ⟶ obj i.succ) (j : Fin (n + 2)) : CategoryTheory.SimplicialObject.δ (CategoryTheory.nerve C) j (SSet.nerve.mk (n + 1) obj mor) = SSet.nerve.mk n (obj ∘ j.succAbove) (SSet.nerve.δ_mk_mor n obj mor j)

def SSet.nerve.arrow {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : (CategoryTheory.nerve C).obj (Opposite.op (SimplexCategory.mk 1))) : f.obj 0 ⟶ f.obj 1

Equations

• SSet.nerve.arrow f = CategoryTheory.ComposableArrows.map' f 0 1 SSet.nerve.arrow.proof_1 SSet.nerve.arrow.proof_2

theorem SSet.nerve.horn_app_obj {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (n : ℕ) (i : Fin (n + 3)) (σ : SSet.horn (n + 2) i ⟶ CategoryTheory.nerve C) (m : SimplexCategoryᵒᵖ) (f : (SSet.horn (n + 2) i).obj m) (k : Fin ((Opposite.unop m).len + 1)) : (σ.app m f).obj k = (σ.app (Opposite.op (SimplexCategory.mk 0)) (SSet.horn.const n i ((SSet.asOrderHom ↑f) k) (Opposite.op (SimplexCategory.mk 0)))).obj 0

def SSet.horn.edge'' {n m : ℕ} {i : Fin (n + 4)} (f : (SSet.horn (n + 3) i).obj (Opposite.op (SimplexCategory.mk m))) (a b : Fin (m + 1)) (h : a ≤ b) : (SSet.horn (n + 3) i).obj (Opposite.op (SimplexCategory.mk 1))

Equations

• SSet.horn.edge'' f a b h = SSet.horn.edge₃ (n + 3) i ((SSet.asOrderHom ↑f) a) ((SSet.asOrderHom ↑f) b) ⋯ ⋯

def SSet.horn.edge' {n m : ℕ} {i : Fin (n + 4)} (f : (SSet.horn (n + 3) i).obj (Opposite.op (SimplexCategory.mk m))) (k : ℕ) (hk : k + 1 ≤ m) : (SSet.horn (n + 3) i).obj (Opposite.op (SimplexCategory.mk 1))

Equations

• SSet.horn.edge' f k hk = SSet.horn.edge'' f ⟨k, ⋯⟩ ⟨k + 1, ⋯⟩ ⋯

theorem SSet.morphism_heq {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (hX : X₁ = X₂) (hY : Y₁ = Y₂) (H : f₁ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hX) (CategoryTheory.CategoryStruct.comp f₂ (CategoryTheory.eqToHom ⋯))) : HEq f₁ f₂

theorem SSet.nerve.arrow_app_congr {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (n : ℕ) (i : Fin (n + 3)) (σ : SSet.horn (n + 2) i ⟶ CategoryTheory.nerve C) (f g : (SSet.horn (n + 2) i).obj (Opposite.op (SimplexCategory.mk 1))) (h : f = g) : SSet.nerve.arrow (σ.app (Opposite.op (SimplexCategory.mk 1)) f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (SSet.nerve.arrow (σ.app (Opposite.op (SimplexCategory.mk 1)) g)) (CategoryTheory.eqToHom ⋯))

theorem SSet.nerve.horn_app_map {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (n : ℕ) (i : Fin (n + 4)) (σ : SSet.horn (n + 3) i ⟶ CategoryTheory.nerve C) (m : ℕ) (f : (SSet.horn (n + 3) i).obj (Opposite.op (SimplexCategory.mk m))) (a b : ℕ) (hab : a ≤ b) (hbm : b ≤ m) : CategoryTheory.ComposableArrows.map' (σ.app (Opposite.op (SimplexCategory.mk m)) f) a b hab hbm = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (SSet.nerve.arrow (σ.app (Opposite.op (SimplexCategory.mk 1)) (SSet.horn.edge'' f ⟨a, ⋯⟩ ⟨b, ⋯⟩ ⋯))) (CategoryTheory.eqToHom ⋯))

noncomputable def SSet.filler {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {i : Fin (n + 3)} (σ₀ : SSet.horn (n + 2) i ⟶ CategoryTheory.nerve C) (h₀ : 0 < i) (hₙ : i < Fin.last (n + 2)) : (CategoryTheory.nerve C).obj (Opposite.op (SimplexCategory.mk (n + 2)))

Equations

• SSet.filler σ₀ h₀ hₙ = SSet.nerve.mk (n + 2) (SSet.filler.obj σ₀) (SSet.filler.mor σ₀ h₀ hₙ)

theorem SSet.filler_spec_zero {C : Type u} [CategoryTheory.Category.{v, u} C] ⦃i : Fin 3⦄ (σ₀ : SSet.horn 2 i ⟶ CategoryTheory.nerve C) (h₀ : 0 < i) (hₙ : i < Fin.last 2) (j : Fin 3) (hj : j ≠ i) : CategoryTheory.SimplicialObject.δ (CategoryTheory.nerve C) j (SSet.filler σ₀ h₀ hₙ) = σ₀.app (Opposite.op (SimplexCategory.mk 1)) (SSet.horn.face i j hj)

theorem SSet.nerve.arrow_app_congr' {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {i : Fin (n + 4)} (σ : SSet.horn (n + 3) i ⟶ CategoryTheory.nerve C) {f₁ f₂ f₃ g₁ g₂ g₃ : (SSet.horn (n + 3) i).obj (Opposite.op (SimplexCategory.mk 1))} {h₁ : f₁ = g₁} {h₂ : f₂ = g₂} {h₃ : f₃ = g₃} {hf₁ : (σ.app (Opposite.op (SimplexCategory.mk 1)) f₁).obj 0 = (σ.app (Opposite.op (SimplexCategory.mk 1)) f₂).obj 0} {hf₂ : (σ.app (Opposite.op (SimplexCategory.mk 1)) f₂).obj 1 = (σ.app (Opposite.op (SimplexCategory.mk 1)) f₃).obj 0} {hf₃ : (σ.app (Opposite.op (SimplexCategory.mk 1)) f₃).obj 1 = (σ.app (Opposite.op (SimplexCategory.mk 1)) f₁).obj 1} {hg₁ : (σ.app (Opposite.op (SimplexCategory.mk 1)) g₁).obj 0 = (σ.app (Opposite.op (SimplexCategory.mk 1)) g₂).obj 0} {hg₂ : (σ.app (Opposite.op (SimplexCategory.mk 1)) g₂).obj 1 = (σ.app (Opposite.op (SimplexCategory.mk 1)) g₃).obj 0} {hg₃ : (σ.app (Opposite.op (SimplexCategory.mk 1)) g₃).obj 1 = (σ.app (Opposite.op (SimplexCategory.mk 1)) g₁).obj 1} (H : SSet.nerve.arrow (σ.app (Opposite.op (SimplexCategory.mk 1)) f₁) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hf₁) (CategoryTheory.CategoryStruct.comp (SSet.nerve.arrow (σ.app (Opposite.op (SimplexCategory.mk 1)) f₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hf₂) (CategoryTheory.CategoryStruct.comp (SSet.nerve.arrow (σ.app (Opposite.op (SimplexCategory.mk 1)) f₃)) (CategoryTheory.eqToHom hf₃))))) : SSet.nerve.arrow (σ.app (Opposite.op (SimplexCategory.mk 1)) g₁) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hg₁) (CategoryTheory.CategoryStruct.comp (SSet.nerve.arrow (σ.app (Opposite.op (SimplexCategory.mk 1)) g₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hg₂) (CategoryTheory.CategoryStruct.comp (SSet.nerve.arrow (σ.app (Opposite.op (SimplexCategory.mk 1)) g₃)) (CategoryTheory.eqToHom hg₃))))

theorem SSet.filler_spec_succ_aux {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} ⦃i : Fin (n + 4)⦄ (σ₀ : SSet.horn (n + 3) i ⟶ CategoryTheory.nerve C) (h₀ : 0 < i) (hₙ : i < Fin.last (n + 3)) (j : Fin (n + 4)) (hj : j ≠ i) (k : ℕ) (hk : k < n + 2) (hkj : ¬k + 1 < ↑j) (hkj' : k + 1 = ↑j) (h2 : k < n + 2) (h3 : (σ₀.app (Opposite.op (SimplexCategory.mk 1)) (SSet.horn.edge' (SSet.horn.face i j hj) k hk)).obj 0 = (σ₀.app (Opposite.op (SimplexCategory.mk 1)) (SSet.horn.primitiveEdge h₀ hₙ ⟨k, h2⟩.castSucc)).obj 0) (h4 : k.succ < (n + 2).succ) (h5 : (σ₀.app (Opposite.op (SimplexCategory.mk 1)) (SSet.horn.primitiveEdge h₀ hₙ ⟨k, h2⟩.castSucc)).obj 1 = (σ₀.app (Opposite.op (SimplexCategory.mk 1)) (SSet.horn.primitiveEdge h₀ hₙ ⟨k, h2⟩.succ)).obj 0) (h6 : (σ₀.app (Opposite.op (SimplexCategory.mk 1)) (SSet.horn.primitiveEdge h₀ hₙ ⟨k, h2⟩.succ)).obj 1 = (σ₀.app (Opposite.op (SimplexCategory.mk 1)) (SSet.horn.edge' (SSet.horn.face i j hj) k hk)).obj 1) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h3) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (SSet.nerve.arrow (σ₀.app (Opposite.op (SimplexCategory.mk 1)) (SSet.horn.primitiveEdge h₀ hₙ ⟨k, ⋯⟩))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h5) (SSet.nerve.arrow (σ₀.app (Opposite.op (SimplexCategory.mk 1)) (SSet.horn.primitiveEdge h₀ hₙ ⟨k + 1, h4⟩))))) (CategoryTheory.eqToHom h6)) = SSet.nerve.arrow (σ₀.app (Opposite.op (SimplexCategory.mk 1)) (SSet.horn.edge' (SSet.horn.face i j hj) k hk))

theorem SSet.filler_spec_succ {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} ⦃i : Fin (n + 4)⦄ (σ₀ : SSet.horn (n + 3) i ⟶ CategoryTheory.nerve C) (h₀ : 0 < i) (hₙ : i < Fin.last (n + 3)) (j : Fin (n + 4)) (hj : j ≠ i) : CategoryTheory.SimplicialObject.δ (CategoryTheory.nerve C) j (SSet.filler σ₀ h₀ hₙ) = σ₀.app (Opposite.op (SimplexCategory.mk (n + 2))) (SSet.horn.face i j hj)

instance SSet.instQuasicategoryNerve_infinityCosmos (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.nerve C).Quasicategory

The nerve of a category is a quasicategory.

[Kerodon, 0032]

Equations

• ⋯ = ⋯