Documentation

InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Wombat

instance fin_zero_le_one (n : ) :
Equations
  • =
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 : autoParam (i j) _auto✝) (hjn : autoParam (j n) _auto✝) :
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) :

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
Instances For
    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.
    Instances For
      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)) :
      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 : Fin (m + 1)) (b : Fin (m + 1)) (h : a b) :
      Equations
      Instances For
        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) :
        Equations
        Instances For
          theorem SSet.morphism_heq {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {Y₁ : C} {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₂
          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)) :
          Equations
          Instances For
            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) :
            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₁ : (SSet.horn (n + 3) i).obj (Opposite.op (SimplexCategory.mk 1))} {f₂ : (SSet.horn (n + 3) i).obj (Opposite.op (SimplexCategory.mk 1))} {f₃ : (SSet.horn (n + 3) i).obj (Opposite.op (SimplexCategory.mk 1))} {g₁ : (SSet.horn (n + 3) i).obj (Opposite.op (SimplexCategory.mk 1))} {g₂ : (SSet.horn (n + 3) i).obj (Opposite.op (SimplexCategory.mk 1))} {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₃))))) :
            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) :
            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) :

            The nerve of a category is a quasicategory.

            [Kerodon, 0032]

            Equations
            • =