Documentation

InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

theorem CategoryTheory.Fin.le_succ {n : } (i : Fin n) :
i.castSucc i.succ
def CategoryTheory.Fin.hom_succ {n : } (i : Fin n) :
i.castSucc i.succ
Equations
Instances For
    Equations
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def CategoryTheory.SimplexCategory.mkOfLeComp {n : } (i j k : Fin (n + 1)) (h₁ : i j) (h₂ : j k) :
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[reducible, inline]

          The fully faithful inclusion of the truncated simplex category into the usual simplex category.

          Equations
          Instances For

            The ulift functor SSet.Truncated.{u} ⥤ SSet.Truncated.{max u v} on truncated simplicial sets.

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

              This is called "sk" in SimplicialSet and SimplicialObject, but this is a better name.

              Equations
              Instances For

                The identity natural transformation exhibits nerve C as a right extension of its restriction to (Δ 2).op along (Δ.ι 2).op.

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

                  The natural transformation in nerveRightExtension C defines a cone with summit nerve C _[n] over the diagram (StructuredArrow.proj (op ([n] : SimplexCategory)) (Δ.ι 2).op ⋙ nerveFunctor₂.obj C) indexed by the category StructuredArrow (op [n]) (Δ.ι 2).op.

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

                        It follows that we have a natural isomorphism between nerveFunctor and nerveFunctor ⋙ cosk₂ whose components are the isomorphisms just established.

                        Equations
                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            theorem CategoryTheory.opstuff {C : Type u} [CategoryTheory.Category.{v, u} C] (V : CategoryTheory.Functor Cᵒᵖ (Type w)) {X Y Z : C} {α : X Y} {β : Y Z} {γ : X Z} {φ : V.obj (Opposite.op Z)} :
                            CategoryTheory.CategoryStruct.comp α β = γV.map α.op (V.map β.op φ) = V.map γ.op φ
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                Equations
                                Instances For
                                  @[simp]
                                  Instances For
                                    theorem CategoryTheory.SSet.HoRel.ext_triangle {V : SSet} (X X' Y Y' Z Z' : CategoryTheory.SSet.OneTruncation V) (hX : X = X') (hY : Y = Y') (hZ : Z = Z') (f : X Z) (f' : X' Z') (hf : f = f') (g : X Y) (g' : X' Y') (hg : g = g') (h : Y Z) (h' : Y' Z') (hh : h = h') :
                                    CategoryTheory.SSet.HoRel ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).obj X) ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).obj Z) ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).map (Quiver.Path.nil.cons f)) ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).map ((Quiver.Path.nil.cons g).cons h)) CategoryTheory.SSet.HoRel ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).obj X') ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).obj Z') ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).map (Quiver.Path.nil.cons f')) ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).map ((Quiver.Path.nil.cons g').cons h'))
                                    Equations
                                    Instances For
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          @[reducible, inline]
                                          abbrev CategoryTheory.SSet.δ₂ {n : } (i : Fin (n + 2)) (hn : (SimplexCategory.mk n).len 2 := by decide) (hn' : (SimplexCategory.mk (n + 1)).len 2 := by decide) :
                                          { obj := SimplexCategory.mk n, property := hn } { obj := SimplexCategory.mk (n + 1), property := hn' }
                                          Equations
                                          Instances For
                                            @[reducible, inline]
                                            abbrev CategoryTheory.SSet.σ₂ {n : } (i : Fin (n + 1)) (hn : (SimplexCategory.mk (n + 1)).len 2 := by decide) (hn' : (SimplexCategory.mk n).len 2 := by decide) :
                                            { obj := SimplexCategory.mk (n + 1), property := hn } { obj := SimplexCategory.mk n, property := hn' }
                                            Equations
                                            Instances For
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  Instances For
                                                    theorem CategoryTheory.SSet.HoRel₂.ext_triangle {V : SSet.Truncated 2} (X X' Y Y' Z Z' : CategoryTheory.SSet.OneTruncation₂ V) (hX : X = X') (hY : Y = Y') (hZ : Z = Z') (f : X Z) (f' : X' Z') (hf : f = f') (g : X Y) (g' : X' Y') (hg : g = g') (h : Y Z) (h' : Y' Z') (hh : h = h') :
                                                    CategoryTheory.SSet.HoRel₂ ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).obj X) ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).obj Z) ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).map (Quiver.Path.nil.cons f)) ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).map ((Quiver.Path.nil.cons g).cons h)) CategoryTheory.SSet.HoRel₂ ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).obj X') ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).obj Z') ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).map (Quiver.Path.nil.cons f')) ((CategoryTheory.Quotient.functor CategoryTheory.Cat.FreeReflRel).map ((Quiver.Path.nil.cons g').cons h'))
                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        @[simp]
                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          @[simp]
                                                          theorem CategoryTheory.nerve₂Adj.counit.component_map (C : CategoryTheory.Cat) (a b : CategoryTheory.Quotient CategoryTheory.SSet.HoRel₂) (hf : a b) :
                                                          (CategoryTheory.nerve₂Adj.counit.component C).map hf = Quot.liftOn hf (fun (f : a.as b.as) => (CategoryTheory.ReflQuiv.adj.counit.app C).map (Quot.liftOn f (fun (f : a.as.as b.as.as) => (CategoryTheory.Cat.FreeRefl.quotientFunctor C).map ((CategoryTheory.forgetToReflQuiv.natIso.hom.app C).mapPath f)) ))
                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            def CategoryTheory.nerve₂.seagull (C : CategoryTheory.Cat) :
                                                            (CategoryTheory.nerveFunctor₂.obj C).obj (Opposite.op { obj := SimplexCategory.mk 2, property := }) (CategoryTheory.nerveFunctor₂.obj C).obj (Opposite.op { obj := SimplexCategory.mk 1, property := }) (CategoryTheory.nerveFunctor₂.obj C).obj (Opposite.op { obj := SimplexCategory.mk 1, property := })

                                                            This is similiar to one of the famous Segal maps, except valued in a product rather than a pullback.

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

                                                              Now do a case split. For n = 0 and n = 1 this is covered by the hypothesis. For n = 2 this is covered by the new lemma above.

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

                                                                The adjunction between forming the free category on a quiver, and forgetting a category to a quiver.

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

                                                                  Repleteness exists for full and faithful functors but not fully faithful functors, which is why we do this inefficiently.

                                                                  Equations